1module Hardware.Nvidia.SM86.Command.LaunchBatch
2
3import Hardware.Nvidia.SM86.Command.Pushbuffer
4import Model.Word32
5import Model.Word64
6import Std.Natural
7import Model.Config
8import Model.Parameter
9
10family LaunchOrdering : Type 0
11constructor LaunchWithIdleBarrier
12constructor LaunchWithSemaphore
13field unrestricted launchSemaphoreAddress : (family ModelWord64)
14field unrestricted launchFirstSemaphorePayload : (family ModelWord32)
15constructor LaunchInChannelOrder
16
17end-family
18
19family LaunchAddressList : Type 0
20constructor LaunchAddressEnd
21constructor LaunchAddressNext
22field unrestricted launchAddressHead : (family ModelWord64)
23recursive unrestricted launchAddressTail
24
25end-family
26
27family LaunchBatchErrorCode : Type 0
28constructor LaunchBatchLimitZero
29constructor LaunchAddressSetEmpty
30constructor LaunchPayloadRangeWraps
31constructor LaunchExceedsBatchLimit
32constructor LaunchPushbufferRejected
33field unrestricted launchPushbufferError : (family PushbufferErrorCode)
34
35end-family
36
37family LaunchCommandUnit : Type 0
38constructor LaunchCommandUnitValue
39field unrestricted launchCommandBytes : Bytes
40field unrestricted launchCommandDwords : Nat
41
42end-family
43
44family LaunchCommandUnits : Type 0
45constructor LaunchCommandUnitsEnd
46constructor LaunchCommandUnitsNext
47field unrestricted launchCommandUnitHead : (family LaunchCommandUnit)
48recursive unrestricted launchCommandUnitTail
49
50end-family
51
52family LaunchCommandUnitsResult : Type 0
53constructor LaunchCommandUnitsReady
54field unrestricted launchReadyCommandUnits : (family LaunchCommandUnits)
55constructor LaunchCommandUnitsRejected
56field unrestricted launchCommandUnitsError : (family LaunchBatchErrorCode)
57
58end-family
59
60family LaunchBatch : Type 0
61constructor LaunchBatchValue
62field unrestricted launchBatchBytes : Bytes
63field unrestricted launchBatchDwords : Nat
64
65end-family
66
67family LaunchBatches : Type 0
68constructor LaunchBatchesEnd
69constructor LaunchBatchesNext
70field unrestricted launchBatchHead : (family LaunchBatch)
71recursive unrestricted launchBatchTail
72
73end-family
74
75family LaunchPackResult : Type 0
76constructor LaunchPackReady
77field unrestricted launchPackedBatches : (family LaunchBatches)
78constructor LaunchPackRejected
79field unrestricted launchPackError : (family LaunchBatchErrorCode)
80
81end-family
82
83family LaunchBatchTelemetry : Type 0
84constructor LaunchBatchTelemetryValue
85field unrestricted launchBatchTelemetryLaunches : Nat
86field unrestricted launchBatchTelemetryBatches : Nat
87field unrestricted launchBatchTelemetryHostFallbacks : Nat
88
89end-family
90
91family LaunchBatchResult : Type 0
92constructor LaunchBatchesReady
93field unrestricted launchReadyBatches : (family LaunchBatches)
94field unrestricted launchBatchSuccessTelemetry : (family LaunchBatchTelemetry)
95constructor LaunchBatchesRejected
96field unrestricted launchBatchFailure : (family LaunchBatchErrorCode)
97
98end-family
99
100family LaunchPhysicalIdentityBinding : Type 0
101constructor LaunchPhysicalIdentityBindingValue
102field unrestricted launchPhysicalProgramIdentity : Bytes
103field unrestricted launchPhysicalResourceIdentity : Bytes
104field unrestricted launchPhysicalConstantIdentity : Bytes
105
106end-family
107
108family LaunchPhysicalReceipt : Type 0
109constructor LaunchPhysicalReceiptValue
110field unrestricted launchPhysicalReceiptIdentity : Bytes
111field unrestricted launchPhysicalReceiptBinding : (family LaunchPhysicalIdentityBinding)
112field unrestricted launchPhysicalExpectedLaunches : Nat
113field unrestricted launchPhysicalSubmittedLaunches : Nat
114field unrestricted launchPhysicalRetiredLaunches : Nat
115field unrestricted launchPhysicalFinalTimestampLE64 : Bytes
116field unrestricted launchPhysicalHostFallbacks : Nat
117
118end-family
119
120family LaunchPhysicalReceiptResult : Type 0
121constructor LaunchPhysicalReceiptAccepted
122field unrestricted launchAcceptedPhysicalReceipt : (family LaunchPhysicalReceipt)
123constructor LaunchPhysicalReceiptRejected
124field unrestricted launchPhysicalReceiptFailure : (family LaunchBatchErrorCode)
125
126end-family
127
128def launchBatchErrorCodeBytes =
129 (lambda unrestricted code : (family LaunchBatchErrorCode) .
130 (eliminate
131 LaunchBatchErrorCode
132 (lambda unrestricted current : (family LaunchBatchErrorCode) . Bytes)
133 code
134 (branch LaunchBatchLimitZero . b"ALPHA-HLBT-801")
135 (branch LaunchAddressSetEmpty . b"ALPHA-HLBT-802")
136 (branch LaunchPayloadRangeWraps . b"ALPHA-HLBT-803")
137 (branch LaunchExceedsBatchLimit . b"ALPHA-HLBT-804")
138 (branch LaunchPushbufferRejected error . (pushbufferErrorCodeBytes error))))
139
140def launchFlagAnd =
141 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalAnd left right)))
142
143def launchByteLess =
144 (lambda unrestricted left : Byte .
145 (lambda unrestricted right : Byte . (nat-less-than (byte-to-nat left) (byte-to-nat right))))
146
147def launchIf =
148 (lambda unrestricted condition : Nat .
149 (lambda unrestricted whenTrue : Nat .
150 (lambda unrestricted whenFalse : Nat .
151 (nat-eliminate
152 (lambda unrestricted current : Nat . Nat)
153 whenFalse
154 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . whenTrue))
155 condition))))
156
157def launchLexStep =
158 (lambda unrestricted left : Byte .
159 (lambda unrestricted right : Byte .
160 (lambda unrestricted lowerLess : Nat .
161 (launchIf
162 (launchByteLess left right)
163 (succ zero)
164 (launchIf (byte-equal left right) lowerLess zero)))))
165
166def launchWord32Less =
167 (lambda unrestricted left : (family ModelWord32) .
168 (lambda unrestricted right : (family ModelWord32) .
169 (eliminate
170 ModelWord32
171 (lambda unrestricted current : (family ModelWord32) . Nat)
172 left
173 (branch
174 ModelWord32Value
175 l0
176 l1
177 l2
178 l3
179 .
180 (eliminate
181 ModelWord32
182 (lambda unrestricted current : (family ModelWord32) . Nat)
183 right
184 (branch
185 ModelWord32Value
186 r0
187 r1
188 r2
189 r3
190 .
191 (launchLexStep
192 l3
193 r3
194 (launchLexStep l2 r2 (launchLexStep l1 r1 (launchByteLess l0 r0))))))))))
195
196def launchNaturalWord32 =
197 (lambda unrestricted value : Nat .
198 (constructor ModelWord32 ModelWord32Value (nat-to-byte value) (byte 0) (byte 0) (byte 0)))
199
200def launchAppendPushbuffer =
201 (lambda unrestricted left : (family PushbufferBytesResult) .
202 (lambda unrestricted right : (family PushbufferBytesResult) .
203 (eliminate
204 PushbufferBytesResult
205 (lambda unrestricted current : (family PushbufferBytesResult) .
206 (family PushbufferBytesResult))
207 left
208 (branch
209 PushbufferBytesReady
210 leftBytes
211 .
212 (eliminate
213 PushbufferBytesResult
214 (lambda unrestricted current : (family PushbufferBytesResult) .
215 (family PushbufferBytesResult))
216 right
217 (branch
218 PushbufferBytesReady
219 rightBytes
220 .
221 (constructor
222 PushbufferBytesResult
223 PushbufferBytesReady
224 (bytes-append leftBytes rightBytes)))
225 (branch
226 PushbufferBytesRejected
227 error
228 .
229 (constructor PushbufferBytesResult PushbufferBytesRejected error))))
230 (branch
231 PushbufferBytesRejected
232 error
233 .
234 (constructor PushbufferBytesResult PushbufferBytesRejected error)))))
235
236def launchSynchronization =
237 (lambda unrestricted ordering : (family LaunchOrdering) .
238 (lambda unrestricted ordinal : Nat .
239 (eliminate
240 LaunchOrdering
241 (lambda unrestricted current : (family LaunchOrdering) . (family PushbufferBytesResult))
242 ordering
243 (branch LaunchWithIdleBarrier . pushbufferBarrier)
244 (branch
245 LaunchWithSemaphore
246 address
247 firstPayload
248 .
249 (app
250 (lambda unrestricted payload : (family ModelWord32) .
251 (nat-eliminate
252 (lambda unrestricted wrapped : Nat . (family PushbufferBytesResult))
253 (launchAppendPushbuffer
254 (pushbufferSemaphoreRelease address payload)
255 (pushbufferSemaphoreAcquire address payload))
256 (lambda unrestricted predecessor : Nat .
257 (lambda unrestricted induction : (family PushbufferBytesResult) .
258 (constructor
259 PushbufferBytesResult
260 PushbufferBytesRejected
261 (constructor PushbufferErrorCode PushbufferLengthOutOfRange))))
262 (launchWord32Less payload firstPayload)))
263 (modelWord32Add firstPayload (launchNaturalWord32 ordinal))))
264 (branch LaunchInChannelOrder . (constructor PushbufferBytesResult PushbufferBytesReady b"")))))
265
266def launchEncodeOne =
267 (lambda unrestricted ordering : (family LaunchOrdering) .
268 (lambda unrestricted ordinal : Nat .
269 (lambda unrestricted address : (family ModelWord64) .
270 (eliminate
271 PushbufferBytesResult
272 (lambda unrestricted current : (family PushbufferBytesResult) .
273 (family LaunchCommandUnitsResult))
274 (launchAppendPushbuffer
275 (pushbufferPCASLaunch address)
276 (launchSynchronization ordering ordinal))
277 (branch
278 PushbufferBytesReady
279 commandBytes
280 .
281 (constructor
282 LaunchCommandUnitsResult
283 LaunchCommandUnitsReady
284 (constructor
285 LaunchCommandUnits
286 LaunchCommandUnitsNext
287 (constructor
288 LaunchCommandUnit
289 LaunchCommandUnitValue
290 commandBytes
291 (naturalDivideUnchecked (bytes-length commandBytes) (byte-to-nat (byte 4))))
292 (constructor LaunchCommandUnits LaunchCommandUnitsEnd))))
293 (branch
294 PushbufferBytesRejected
295 error
296 .
297 (constructor
298 LaunchCommandUnitsResult
299 LaunchCommandUnitsRejected
300 (constructor LaunchBatchErrorCode LaunchPushbufferRejected error)))))))
301
302def launchEncodeAddressesWithFuel =
303 (lambda unrestricted fuel : Nat .
304 (nat-eliminate
305 (lambda unrestricted remainingFuel : Nat .
306 (pi unrestricted ordering : (family LaunchOrdering) .
307 (pi unrestricted ordinal : Nat .
308 (pi unrestricted addresses : (family LaunchAddressList) .
309 (family LaunchCommandUnitsResult)))))
310 (lambda unrestricted ordering : (family LaunchOrdering) .
311 (lambda unrestricted ordinal : Nat .
312 (lambda unrestricted addresses : (family LaunchAddressList) .
313 (constructor
314 LaunchCommandUnitsResult
315 LaunchCommandUnitsReady
316 (constructor LaunchCommandUnits LaunchCommandUnitsEnd)))))
317 (lambda unrestricted predecessor : Nat .
318 (lambda unrestricted induction : (pi unrestricted ordering : (family LaunchOrdering) . (pi unrestricted ordinal : Nat . (pi unrestricted addresses : (family LaunchAddressList) . (family LaunchCommandUnitsResult)))) .
319 (lambda unrestricted ordering : (family LaunchOrdering) .
320 (lambda unrestricted ordinal : Nat .
321 (lambda unrestricted addresses : (family LaunchAddressList) .
322 (eliminate
323 LaunchAddressList
324 (lambda unrestricted current : (family LaunchAddressList) .
325 (family LaunchCommandUnitsResult))
326 addresses
327 (branch
328 LaunchAddressEnd
329 .
330 (constructor
331 LaunchCommandUnitsResult
332 LaunchCommandUnitsReady
333 (constructor LaunchCommandUnits LaunchCommandUnitsEnd)))
334 (branch
335 LaunchAddressNext
336 address
337 tail
338 ih_tail
339 .
340 (eliminate
341 LaunchCommandUnitsResult
342 (lambda unrestricted current : (family LaunchCommandUnitsResult) .
343 (family LaunchCommandUnitsResult))
344 (launchEncodeOne ordering ordinal address)
345 (branch
346 LaunchCommandUnitsReady
347 oneUnits
348 .
349 (eliminate
350 LaunchCommandUnitsResult
351 (lambda unrestricted current : (family LaunchCommandUnitsResult) .
352 (family LaunchCommandUnitsResult))
353 (induction ordering (succ ordinal) tail)
354 (branch
355 LaunchCommandUnitsReady
356 tailUnits
357 .
358 (eliminate
359 LaunchCommandUnits
360 (lambda unrestricted current : (family LaunchCommandUnits) .
361 (family LaunchCommandUnitsResult))
362 oneUnits
363 (branch
364 LaunchCommandUnitsEnd
365 .
366 (constructor
367 LaunchCommandUnitsResult
368 LaunchCommandUnitsReady
369 tailUnits))
370 (branch
371 LaunchCommandUnitsNext
372 unit
373 ignoredTail
374 ih_ignoredTail
375 .
376 (constructor
377 LaunchCommandUnitsResult
378 LaunchCommandUnitsReady
379 (constructor
380 LaunchCommandUnits
381 LaunchCommandUnitsNext
382 unit
383 tailUnits)))))
384 (branch
385 LaunchCommandUnitsRejected
386 error
387 .
388 (constructor LaunchCommandUnitsResult LaunchCommandUnitsRejected error))))
389 (branch
390 LaunchCommandUnitsRejected
391 error
392 .
393 (constructor LaunchCommandUnitsResult LaunchCommandUnitsRejected error))))))))))
394 fuel))
395
396def launchAddressCount =
397 (lambda unrestricted addresses : (family LaunchAddressList) .
398 (eliminate
399 LaunchAddressList
400 (lambda unrestricted current : (family LaunchAddressList) . Nat)
401 addresses
402 (branch LaunchAddressEnd . zero)
403 (branch LaunchAddressNext head tail ih_tail . (succ ih_tail))))
404
405def launchPrependUnit =
406 (lambda unrestricted maximumDwords : Nat .
407 (lambda unrestricted unit : (family LaunchCommandUnit) .
408 (lambda unrestricted batches : (family LaunchBatches) .
409 (eliminate
410 LaunchCommandUnit
411 (lambda unrestricted current : (family LaunchCommandUnit) . (family LaunchBatches))
412 unit
413 (branch
414 LaunchCommandUnitValue
415 unitBytes
416 unitDwords
417 .
418 (eliminate
419 LaunchBatches
420 (lambda unrestricted current : (family LaunchBatches) . (family LaunchBatches))
421 batches
422 (branch
423 LaunchBatchesEnd
424 .
425 (constructor
426 LaunchBatches
427 LaunchBatchesNext
428 (constructor LaunchBatch LaunchBatchValue unitBytes unitDwords)
429 (constructor LaunchBatches LaunchBatchesEnd)))
430 (branch
431 LaunchBatchesNext
432 first
433 rest
434 ih_rest
435 .
436 (eliminate
437 LaunchBatch
438 (lambda unrestricted current : (family LaunchBatch) . (family LaunchBatches))
439 first
440 (branch
441 LaunchBatchValue
442 firstBytes
443 firstDwords
444 .
445 (nat-eliminate
446 (lambda unrestricted fits : Nat . (family LaunchBatches))
447 (constructor
448 LaunchBatches
449 LaunchBatchesNext
450 (constructor LaunchBatch LaunchBatchValue unitBytes unitDwords)
451 batches)
452 (lambda unrestricted fitsPredecessor : Nat .
453 (lambda unrestricted fitsInduction : (family LaunchBatches) .
454 (constructor
455 LaunchBatches
456 LaunchBatchesNext
457 (constructor
458 LaunchBatch
459 LaunchBatchValue
460 (bytes-append unitBytes firstBytes)
461 (naturalAdd unitDwords firstDwords))
462 rest)))
463 (naturalLessOrEqual (naturalAdd unitDwords firstDwords) maximumDwords)))))))))))
464
465def launchPackUnits =
466 (lambda unrestricted maximumDwords : Nat .
467 (lambda unrestricted units : (family LaunchCommandUnits) .
468 (eliminate
469 LaunchCommandUnits
470 (lambda unrestricted current : (family LaunchCommandUnits) . (family LaunchPackResult))
471 units
472 (branch
473 LaunchCommandUnitsEnd
474 .
475 (constructor
476 LaunchPackResult
477 LaunchPackReady
478 (constructor LaunchBatches LaunchBatchesEnd)))
479 (branch
480 LaunchCommandUnitsNext
481 unit
482 tail
483 ih_tail
484 .
485 (eliminate
486 LaunchCommandUnit
487 (lambda unrestricted current : (family LaunchCommandUnit) . (family LaunchPackResult))
488 unit
489 (branch
490 LaunchCommandUnitValue
491 unitBytes
492 unitDwords
493 .
494 (nat-eliminate
495 (lambda unrestricted unitFits : Nat . (family LaunchPackResult))
496 (constructor
497 LaunchPackResult
498 LaunchPackRejected
499 (constructor LaunchBatchErrorCode LaunchExceedsBatchLimit))
500 (lambda unrestricted fitsPredecessor : Nat .
501 (lambda unrestricted fitsInduction : (family LaunchPackResult) .
502 (eliminate
503 LaunchPackResult
504 (lambda unrestricted current : (family LaunchPackResult) .
505 (family LaunchPackResult))
506 ih_tail
507 (branch
508 LaunchPackReady
509 batches
510 .
511 (constructor
512 LaunchPackResult
513 LaunchPackReady
514 (launchPrependUnit maximumDwords unit batches)))
515 (branch
516 LaunchPackRejected
517 error
518 .
519 (constructor LaunchPackResult LaunchPackRejected error)))))
520 (naturalLessOrEqual unitDwords maximumDwords))))))))
521
522def launchBatchCount =
523 (lambda unrestricted batches : (family LaunchBatches) .
524 (eliminate
525 LaunchBatches
526 (lambda unrestricted current : (family LaunchBatches) . Nat)
527 batches
528 (branch LaunchBatchesEnd . zero)
529 (branch LaunchBatchesNext head tail ih_tail . (succ ih_tail))))
530
531def launchBuildBatchesUnchecked =
532 (lambda unrestricted maximumDwords : Nat .
533 (lambda unrestricted ordering : (family LaunchOrdering) .
534 (lambda unrestricted addresses : (family LaunchAddressList) .
535 (nat-eliminate
536 (lambda unrestricted maximumPresent : Nat . (family LaunchBatchResult))
537 (constructor
538 LaunchBatchResult
539 LaunchBatchesRejected
540 (constructor LaunchBatchErrorCode LaunchBatchLimitZero))
541 (lambda unrestricted maximumPredecessor : Nat .
542 (lambda unrestricted maximumInduction : (family LaunchBatchResult) .
543 (app
544 (lambda unrestricted launchCount : Nat .
545 (nat-eliminate
546 (lambda unrestricted launchesPresent : Nat . (family LaunchBatchResult))
547 (constructor
548 LaunchBatchResult
549 LaunchBatchesRejected
550 (constructor LaunchBatchErrorCode LaunchAddressSetEmpty))
551 (lambda unrestricted launchesPredecessor : Nat .
552 (lambda unrestricted launchesInduction : (family LaunchBatchResult) .
553 (eliminate
554 LaunchCommandUnitsResult
555 (lambda unrestricted current : (family LaunchCommandUnitsResult) .
556 (family LaunchBatchResult))
557 (launchEncodeAddressesWithFuel launchCount ordering zero addresses)
558 (branch
559 LaunchCommandUnitsReady
560 units
561 .
562 (eliminate
563 LaunchPackResult
564 (lambda unrestricted current : (family LaunchPackResult) .
565 (family LaunchBatchResult))
566 (launchPackUnits maximumDwords units)
567 (branch
568 LaunchPackReady
569 batches
570 .
571 (constructor
572 LaunchBatchResult
573 LaunchBatchesReady
574 batches
575 (constructor
576 LaunchBatchTelemetry
577 LaunchBatchTelemetryValue
578 launchCount
579 (launchBatchCount batches)
580 zero)))
581 (branch
582 LaunchPackRejected
583 error
584 .
585 (constructor LaunchBatchResult LaunchBatchesRejected error))))
586 (branch
587 LaunchCommandUnitsRejected
588 error
589 .
590 (constructor LaunchBatchResult LaunchBatchesRejected error)))))
591 launchCount))
592 (launchAddressCount addresses))))
593 maximumDwords))))
594
595def launchOrderingRangeValid =
596 (lambda unrestricted ordering : (family LaunchOrdering) .
597 (lambda unrestricted launchCount : Nat .
598 (eliminate
599 LaunchOrdering
600 (lambda unrestricted current : (family LaunchOrdering) . Nat)
601 ordering
602 (branch LaunchWithIdleBarrier . (succ zero))
603 (branch
604 LaunchWithSemaphore
605 address
606 firstPayload
607 .
608 (nat-eliminate
609 (lambda unrestricted current : Nat . Nat)
610 zero
611 (lambda unrestricted predecessor : Nat .
612 (lambda unrestricted induction : Nat .
613 (naturalIsZero
614 (launchWord32Less
615 (modelWord32Add firstPayload (launchNaturalWord32 predecessor))
616 firstPayload))))
617 launchCount))
618 (branch LaunchInChannelOrder . (succ zero)))))
619
620def launchBuildBatches =
621 (lambda unrestricted maximumDwords : Nat .
622 (lambda unrestricted ordering : (family LaunchOrdering) .
623 (lambda unrestricted addresses : (family LaunchAddressList) .
624 (nat-eliminate
625 (lambda unrestricted rangeValid : Nat . (family LaunchBatchResult))
626 (constructor
627 LaunchBatchResult
628 LaunchBatchesRejected
629 (constructor LaunchBatchErrorCode LaunchPayloadRangeWraps))
630 (lambda unrestricted validPredecessor : Nat .
631 (lambda unrestricted validInduction : (family LaunchBatchResult) .
632 (launchBuildBatchesUnchecked maximumDwords ordering addresses)))
633 (launchOrderingRangeValid ordering (launchAddressCount addresses))))))
634
635def launchPhysicalIdentityBindingValid =
636 (lambda unrestricted binding : (family LaunchPhysicalIdentityBinding) .
637 (eliminate
638 LaunchPhysicalIdentityBinding
639 (lambda unrestricted current : (family LaunchPhysicalIdentityBinding) . Nat)
640 binding
641 (branch
642 LaunchPhysicalIdentityBindingValue
643 program
644 resource
645 constant
646 .
647 (naturalAnd
648 (naturalEqual (bytes-length program) (byte-to-nat (byte 64)))
649 (naturalAnd
650 (naturalEqual (bytes-length resource) (byte-to-nat (byte 64)))
651 (naturalEqual (bytes-length constant) (byte-to-nat (byte 64))))))))
652
653def launchValidatePhysicalReceipt =
654 (lambda unrestricted expectedIdentity : Bytes .
655 (lambda unrestricted expectedLaunches : Nat .
656 (lambda unrestricted receipt : (family LaunchPhysicalReceipt) .
657 (eliminate
658 LaunchPhysicalReceipt
659 (lambda unrestricted current : (family LaunchPhysicalReceipt) .
660 (family LaunchPhysicalReceiptResult))
661 receipt
662 (branch
663 LaunchPhysicalReceiptValue
664 identity
665 binding
666 expected
667 submitted
668 retired
669 timestamp
670 fallbacks
671 .
672 (nat-eliminate
673 (lambda unrestricted complete : Nat . (family LaunchPhysicalReceiptResult))
674 (constructor
675 LaunchPhysicalReceiptResult
676 LaunchPhysicalReceiptRejected
677 (constructor LaunchBatchErrorCode LaunchAddressSetEmpty))
678 (lambda unrestricted completePredecessor : Nat .
679 (lambda unrestricted completeInduction : (family LaunchPhysicalReceiptResult) .
680 (constructor LaunchPhysicalReceiptResult LaunchPhysicalReceiptAccepted receipt)))
681 (naturalAnd
682 (naturalEqual (bytes-length expectedIdentity) (byte-to-nat (byte 64)))
683 (naturalAnd
684 (bytes-equal expectedIdentity identity)
685 (naturalAnd
686 (launchPhysicalIdentityBindingValid binding)
687 (naturalAnd
688 (naturalEqual expectedLaunches expected)
689 (naturalAnd
690 (naturalEqual expected submitted)
691 (naturalAnd
692 (naturalEqual submitted retired)
693 (naturalAnd
694 (naturalEqual (bytes-length timestamp) (byte-to-nat (byte 8)))
695 (naturalIsZero fallbacks))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.