1module Runtime.NativePhysicalProgram
2
3import Model.Parameter
4import Model.Word32
5import Runtime.NativeTelemetry
6import Std.Natural
7import Model.Word64
8
9family NativePhysicalErrorCode : Type 0
10constructor NativePhysicalIdentityInvalid
11constructor NativePhysicalFallbackObserved
12constructor NativePhysicalCommandCountMismatch
13constructor NativePhysicalStateExtentZero
14constructor NativePhysicalCopyPayloadEmpty
15constructor NativePhysicalCopyExtentZero
16constructor NativePhysicalMachineCodeEmpty
17constructor NativePhysicalFencePollCountZero
18constructor NativePhysicalTelemetryPathEmpty
19constructor NativePhysicalTelemetryRecordEmpty
20constructor NativePhysicalResultSlotUnavailable
21constructor NativePhysicalExecutionAssertionFailed
22constructor NativePhysicalRepeatCountZero
23constructor NativePhysicalRepeatUnbalanced
24constructor NativePhysicalFenceWaitCountZero
25constructor NativePhysicalFenceWaitIntervalInvalid
26
27end-family
28
29family NativePhysicalSlot : Type 0
30constructor NativePhysicalSlotValue
31field unrestricted nativePhysicalSlotIndex : (family ModelWord64)
32
33end-family
34
35family NativePhysicalOperand : Type 0
36constructor NativePhysicalImmediate
37field unrestricted nativePhysicalImmediateValue : (family ModelWord64)
38constructor NativePhysicalResultValue
39field unrestricted nativePhysicalResultValueSlot : (family NativePhysicalSlot)
40constructor NativePhysicalResultAddress
41field unrestricted nativePhysicalResultAddressSlot : (family NativePhysicalSlot)
42field unrestricted nativePhysicalResultAddressOffset : (family ModelWord64)
43constructor NativePhysicalStateAddress
44field unrestricted nativePhysicalStateAddressOffset : (family ModelWord64)
45constructor NativePhysicalStateLoad64
46field unrestricted nativePhysicalStateLoadOffset : (family ModelWord64)
47constructor NativePhysicalPayloadAddress
48field unrestricted nativePhysicalPayloadAddressOffset : (family ModelWord64)
49constructor NativePhysicalPayloadLoad64
50field unrestricted nativePhysicalPayloadLoadOffset : (family ModelWord64)
51constructor NativePhysicalProcessArgument
52field unrestricted nativePhysicalProcessArgumentIndex : (family ModelWord64)
53-- base + iteration * stride, where iteration counts the enclosing repeat's
54-- completed passes from zero. Outside a repeat the iteration is zero.
55constructor NativePhysicalLoopAffine
56field unrestricted nativePhysicalLoopAffineBase : (family ModelWord64)
57field unrestricted nativePhysicalLoopAffineStride : (family ModelWord64)
58
59end-family
60
61family NativePhysicalArguments : Type 0
62constructor NativePhysicalArgumentsValue
63field unrestricted nativePhysicalArgument0 : (family NativePhysicalOperand)
64field unrestricted nativePhysicalArgument1 : (family NativePhysicalOperand)
65field unrestricted nativePhysicalArgument2 : (family NativePhysicalOperand)
66field unrestricted nativePhysicalArgument3 : (family NativePhysicalOperand)
67field unrestricted nativePhysicalArgument4 : (family NativePhysicalOperand)
68field unrestricted nativePhysicalArgument5 : (family NativePhysicalOperand)
69
70end-family
71
72family NativePhysicalResultBinding : Type 0
73constructor NativePhysicalDiscardResult
74constructor NativePhysicalStoreResult
75field unrestricted nativePhysicalStoredResultSlot : (family NativePhysicalSlot)
76
77end-family
78
79-- The binary64 operations the host computes with (IEEE 754, round to
80-- nearest even; x86 SSE2): the sum, difference, product and quotient of
81-- the left and right operands' words read as binary64; the square root of
82-- the right one; the left word, a natural below 2^63, as the nearest
83-- binary64; the left binary64 rounded to the nearest binary32 (its word
84-- zero-extended); the left word's low half, a binary32, as the binary64 of
85-- the same value. (Binary32 +, -, *, / and square root are these binary64
86-- operations rounded to binary32: 53 bits hold 2 x 24 + 2, so the double
87-- rounding is exact.)
88family NativePhysicalFloat64Operation : Type 0
89constructor NativePhysicalFloat64Add
90constructor NativePhysicalFloat64Subtract
91constructor NativePhysicalFloat64Multiply
92constructor NativePhysicalFloat64Divide
93constructor NativePhysicalFloat64SquareRoot
94constructor NativePhysicalFloat64FromNatural
95constructor NativePhysicalFloat64ToBinary32
96constructor NativePhysicalFloat64FromBinary32
97
98end-family
99
100family NativePhysicalOperation : Type 0
101constructor NativePhysicalSystemCall
102field unrestricted nativePhysicalSystemCallNumber : (family NativePhysicalOperand)
103field unrestricted nativePhysicalSystemCallArguments : (family NativePhysicalArguments)
104field unrestricted nativePhysicalSystemCallPayload : Bytes
105field unrestricted nativePhysicalSystemCallResult : (family NativePhysicalResultBinding)
106constructor NativePhysicalCopyPayloadToState
107field unrestricted nativePhysicalCopyDestinationOffset : (family ModelWord64)
108field unrestricted nativePhysicalCopyExtent : (family ModelWord64)
109field unrestricted nativePhysicalCopyPayload : Bytes
110constructor NativePhysicalMachineRoutine
111field unrestricted nativePhysicalMachineCode : Bytes
112field unrestricted nativePhysicalMachineArguments : (family NativePhysicalArguments)
113field unrestricted nativePhysicalMachineResult : (family NativePhysicalResultBinding)
114constructor NativePhysicalFencePoll
115field unrestricted nativePhysicalFenceAddress : (family NativePhysicalOperand)
116field unrestricted nativePhysicalFenceExpected : (family NativePhysicalOperand)
117field unrestricted nativePhysicalFenceMaximumPolls : (family ModelWord64)
118constructor NativePhysicalTelemetryAppend
119field unrestricted nativePhysicalTelemetryPath : Bytes
120field unrestricted nativePhysicalTelemetryRecord : Bytes
121constructor NativePhysicalAssertEqual
122field unrestricted nativePhysicalAssertLeft : (family NativePhysicalOperand)
123field unrestricted nativePhysicalAssertRight : (family NativePhysicalOperand)
124field unrestricted nativePhysicalAssertError : (family NativePhysicalErrorCode)
125constructor NativePhysicalAssertOneOf
126field unrestricted nativePhysicalAssertOneOfObserved : (family NativePhysicalOperand)
127field unrestricted nativePhysicalAssertOneOfFirst : (family NativePhysicalOperand)
128field unrestricted nativePhysicalAssertOneOfSecond : (family NativePhysicalOperand)
129field unrestricted nativePhysicalAssertOneOfError : (family NativePhysicalErrorCode)
130constructor NativePhysicalHaltSuccess
131-- Execute the commands up to the matching RepeatEnd count times. Repeats do
132-- not nest; the runtime keeps one iteration counter and the loop-affine
133-- operands read it.
134constructor NativePhysicalRepeatBegin
135field unrestricted nativePhysicalRepeatCount : (family ModelWord64)
136constructor NativePhysicalRepeatEnd
137-- Store the 64-bit value of an operand at the address another operand
138-- resolves to (a state or result address): how a repeat body places a
139-- loop-affine value where a system call can read it.
140constructor NativePhysicalStoreWord64
141field unrestricted nativePhysicalStoreDestination : (family NativePhysicalOperand)
142field unrestricted nativePhysicalStoreValue : (family NativePhysicalOperand)
143-- Wait until the 64-bit word at an address equals the expected value,
144-- sleeping intervalNanoseconds between polls (a nanosleep, so the host does
145-- not spin), at most maximumPolls times: how a host waits on device state
146-- (a completion semaphore) instead of on the clock. A timeout is a command
147-- failure -- it never yields a ready value. The interval must be below one
148-- second so the timespec is a single nanosecond field.
149constructor NativePhysicalFenceWait
150field unrestricted nativePhysicalFenceWaitAddress : (family NativePhysicalOperand)
151field unrestricted nativePhysicalFenceWaitExpected : (family NativePhysicalOperand)
152field unrestricted nativePhysicalFenceWaitMaximumPolls : (family ModelWord64)
153field unrestricted nativePhysicalFenceWaitIntervalNanoseconds : (family ModelWord64)
154
155-- A repeat whose count an operand gives at run time (a state word): a
156-- count of zero skips the body, so it is how a block is made conditional
157-- on what the host has read.
158constructor NativePhysicalRepeatBeginCounted
159field unrestricted nativePhysicalRepeatCountOperand : (family NativePhysicalOperand)
160-- The 64-bit sum (modulo 2^64) of two operands, stored at the address a
161-- third resolves to.
162constructor NativePhysicalAddWord64
163field unrestricted nativePhysicalAddDestination : (family NativePhysicalOperand)
164field unrestricted nativePhysicalAddLeft : (family NativePhysicalOperand)
165field unrestricted nativePhysicalAddRight : (family NativePhysicalOperand)
166-- A binary64 operation on two operands' words, the result's word stored at
167-- the address a third resolves to.
168constructor NativePhysicalFloat64
169field unrestricted nativePhysicalFloat64Operation : (family NativePhysicalFloat64Operation)
170field unrestricted nativePhysicalFloat64Destination : (family NativePhysicalOperand)
171field unrestricted nativePhysicalFloat64Left : (family NativePhysicalOperand)
172field unrestricted nativePhysicalFloat64Right : (family NativePhysicalOperand)
173end-family
174
175family NativePhysicalCommand : Type 0
176constructor NativePhysicalCommandValue
177field unrestricted nativePhysicalCommandOperation : (family NativePhysicalOperation)
178field unrestricted nativePhysicalCommandErrorIdentity : Bytes
179
180end-family
181
182family NativePhysicalCommands : Type 0
183constructor NativePhysicalCommandsEnd
184constructor NativePhysicalCommandsNext
185field unrestricted nativePhysicalCommandHead : (family NativePhysicalCommand)
186recursive unrestricted nativePhysicalCommandTail
187
188end-family
189
190family NativePhysicalProgram : Type 0
191constructor NativePhysicalProgramValue
192field unrestricted nativePhysicalProgramStateExtent : (family ModelWord64)
193field unrestricted nativePhysicalProgramResultSlots : (family ModelWord64)
194field unrestricted nativePhysicalProgramCommands : (family NativePhysicalCommands)
195field unrestricted nativePhysicalProgramExpectedCommands : Nat
196field unrestricted nativePhysicalProgramIdentity : Bytes
197field unrestricted nativePhysicalProgramFallbacks : Nat
198
199end-family
200
201family NativePhysicalCounts : Type 0
202constructor NativePhysicalCountsValue
203field unrestricted nativePhysicalCountCommands : Nat
204field unrestricted nativePhysicalCountSystemCalls : Nat
205field unrestricted nativePhysicalCountCopies : Nat
206field unrestricted nativePhysicalCountMachineRoutines : Nat
207field unrestricted nativePhysicalCountFencePolls : Nat
208field unrestricted nativePhysicalCountTelemetryAppends : Nat
209field unrestricted nativePhysicalCountAssertions : Nat
210field unrestricted nativePhysicalCountHalts : Nat
211field unrestricted nativePhysicalCountPayloadBytes : Nat
212
213end-family
214
215family NativePhysicalOperationValidation : Type 0
216constructor NativePhysicalOperationValid
217constructor NativePhysicalOperationInvalid
218field unrestricted nativePhysicalOperationError : (family NativePhysicalErrorCode)
219
220end-family
221
222family NativePhysicalCommandsValidation : Type 0
223constructor NativePhysicalCommandsValid
224field unrestricted nativePhysicalValidatedCommands : Nat
225constructor NativePhysicalCommandsInvalid
226field unrestricted nativePhysicalCommandsError : (family NativePhysicalErrorCode)
227field unrestricted nativePhysicalCommandsErrorOrdinal : Nat
228
229end-family
230
231family NativePhysicalValidationTelemetry : Type 0
232constructor NativePhysicalValidationTelemetryValue
233field unrestricted nativePhysicalValidationCounts : (family NativePhysicalCounts)
234field unrestricted nativePhysicalValidationExpectedCommands : Nat
235field unrestricted nativePhysicalValidationStateExtent : (family ModelWord64)
236field unrestricted nativePhysicalValidationResultSlots : (family ModelWord64)
237field unrestricted nativePhysicalValidationFallbacks : Nat
238field unrestricted nativePhysicalValidationIdentity : Bytes
239field unrestricted nativePhysicalValidationFailures : Nat
240field unrestricted nativePhysicalValidationFailureOrdinal : Nat
241field unrestricted nativePhysicalValidationFailureCode : Bytes
242
243end-family
244
245family NativePhysicalProgramValidation : Type 0
246constructor NativePhysicalProgramValidated
247field unrestricted nativePhysicalValidatedProgram : (family NativePhysicalProgram)
248field unrestricted nativePhysicalValidatedTelemetry : (family NativePhysicalValidationTelemetry)
249constructor NativePhysicalProgramRejected
250field unrestricted nativePhysicalRejectedError : (family NativePhysicalErrorCode)
251field unrestricted nativePhysicalRejectedTelemetry : (family NativePhysicalValidationTelemetry)
252
253end-family
254
255def nativePhysicalErrorCodeBytes =
256 (lambda unrestricted code : (family NativePhysicalErrorCode) .
257 (eliminate
258 NativePhysicalErrorCode
259 (lambda unrestricted current : (family NativePhysicalErrorCode) . Bytes)
260 code
261 (branch NativePhysicalIdentityInvalid . b"ALPHA-PHYS-001")
262 (branch NativePhysicalFallbackObserved . b"ALPHA-PHYS-002")
263 (branch
264 NativePhysicalCommandCountMismatch
265 .
266 b"ALPHA-PHYS-003")
267 (branch NativePhysicalStateExtentZero . b"ALPHA-PHYS-004")
268 (branch NativePhysicalCopyPayloadEmpty . b"ALPHA-PHYS-005")
269 (branch NativePhysicalCopyExtentZero . b"ALPHA-PHYS-006")
270 (branch NativePhysicalMachineCodeEmpty . b"ALPHA-PHYS-007")
271 (branch NativePhysicalFencePollCountZero . b"ALPHA-PHYS-008")
272 (branch NativePhysicalTelemetryPathEmpty . b"ALPHA-PHYS-009")
273 (branch
274 NativePhysicalTelemetryRecordEmpty
275 .
276 b"ALPHA-PHYS-010")
277 (branch
278 NativePhysicalResultSlotUnavailable
279 .
280 b"ALPHA-PHYS-011")
281 (branch
282 NativePhysicalExecutionAssertionFailed
283 .
284 b"ALPHA-PHYS-012")
285 (branch NativePhysicalRepeatCountZero . b"ALPHA-PHYS-013")
286 (branch NativePhysicalRepeatUnbalanced . b"ALPHA-PHYS-014")
287 (branch NativePhysicalFenceWaitCountZero . b"ALPHA-PHYS-015")
288 (branch NativePhysicalFenceWaitIntervalInvalid . b"ALPHA-PHYS-016")))
289
290def nativePhysicalZeroCounts : (family NativePhysicalCounts) =
291 (constructor
292 NativePhysicalCounts
293 NativePhysicalCountsValue
294 zero
295 zero
296 zero
297 zero
298 zero
299 zero
300 zero
301 zero
302 zero)
303
304def nativePhysicalAddCounts =
305 (lambda unrestricted left : (family NativePhysicalCounts) .
306 (lambda unrestricted right : (family NativePhysicalCounts) .
307 (eliminate
308 NativePhysicalCounts
309 (lambda unrestricted current : (family NativePhysicalCounts) .
310 (family NativePhysicalCounts))
311 left
312 (branch
313 NativePhysicalCountsValue
314 leftCommands
315 leftSystemCalls
316 leftCopies
317 leftRoutines
318 leftFences
319 leftTelemetry
320 leftAssertions
321 leftHalts
322 leftPayload
323 .
324 (eliminate
325 NativePhysicalCounts
326 (lambda unrestricted current : (family NativePhysicalCounts) .
327 (family NativePhysicalCounts))
328 right
329 (branch
330 NativePhysicalCountsValue
331 rightCommands
332 rightSystemCalls
333 rightCopies
334 rightRoutines
335 rightFences
336 rightTelemetry
337 rightAssertions
338 rightHalts
339 rightPayload
340 .
341 (constructor
342 NativePhysicalCounts
343 NativePhysicalCountsValue
344 (naturalAdd leftCommands rightCommands)
345 (naturalAdd leftSystemCalls rightSystemCalls)
346 (naturalAdd leftCopies rightCopies)
347 (naturalAdd leftRoutines rightRoutines)
348 (naturalAdd leftFences rightFences)
349 (naturalAdd leftTelemetry rightTelemetry)
350 (naturalAdd leftAssertions rightAssertions)
351 (naturalAdd leftHalts rightHalts)
352 (naturalAdd leftPayload rightPayload))))))))
353
354def nativePhysicalOperationCounts =
355 (lambda unrestricted operation : (family NativePhysicalOperation) .
356 (eliminate
357 NativePhysicalOperation
358 (lambda unrestricted current : (family NativePhysicalOperation) .
359 (family NativePhysicalCounts))
360 operation
361 (branch
362 NativePhysicalSystemCall
363 number
364 arguments
365 payload
366 result
367 .
368 (constructor
369 NativePhysicalCounts
370 NativePhysicalCountsValue
371 (succ zero)
372 (succ zero)
373 zero
374 zero
375 zero
376 zero
377 zero
378 zero
379 (bytes-length payload)))
380 (branch
381 NativePhysicalCopyPayloadToState
382 destination
383 extent
384 payload
385 .
386 (constructor
387 NativePhysicalCounts
388 NativePhysicalCountsValue
389 (succ zero)
390 zero
391 (succ zero)
392 zero
393 zero
394 zero
395 zero
396 zero
397 (bytes-length payload)))
398 (branch
399 NativePhysicalMachineRoutine
400 code
401 arguments
402 result
403 .
404 (constructor
405 NativePhysicalCounts
406 NativePhysicalCountsValue
407 (succ zero)
408 zero
409 zero
410 (succ zero)
411 zero
412 zero
413 zero
414 zero
415 (bytes-length code)))
416 (branch
417 NativePhysicalFencePoll
418 address
419 expected
420 maximumPolls
421 .
422 (constructor
423 NativePhysicalCounts
424 NativePhysicalCountsValue
425 (succ zero)
426 zero
427 zero
428 zero
429 (succ zero)
430 zero
431 zero
432 zero
433 zero))
434 (branch
435 NativePhysicalTelemetryAppend
436 path
437 record
438 .
439 (constructor
440 NativePhysicalCounts
441 NativePhysicalCountsValue
442 (succ zero)
443 zero
444 zero
445 zero
446 zero
447 (succ zero)
448 zero
449 zero
450 (naturalAdd (bytes-length path) (bytes-length record))))
451 (branch
452 NativePhysicalAssertEqual
453 left
454 right
455 error
456 .
457 (constructor
458 NativePhysicalCounts
459 NativePhysicalCountsValue
460 (succ zero)
461 zero
462 zero
463 zero
464 zero
465 zero
466 (succ zero)
467 zero
468 zero))
469 (branch
470 NativePhysicalAssertOneOf
471 observed
472 first
473 second
474 error
475 .
476 (constructor
477 NativePhysicalCounts
478 NativePhysicalCountsValue
479 (succ zero)
480 zero
481 zero
482 zero
483 zero
484 zero
485 (succ zero)
486 zero
487 zero))
488 (branch
489 NativePhysicalHaltSuccess
490 .
491 (constructor
492 NativePhysicalCounts
493 NativePhysicalCountsValue
494 (succ zero)
495 zero
496 zero
497 zero
498 zero
499 zero
500 zero
501 (succ zero)
502 zero))
503 (branch
504 NativePhysicalRepeatBegin
505 count
506 .
507 (constructor NativePhysicalCounts NativePhysicalCountsValue
508 (succ zero) zero zero zero zero zero zero zero zero))
509 (branch
510 NativePhysicalRepeatEnd
511 .
512 (constructor NativePhysicalCounts NativePhysicalCountsValue
513 (succ zero) zero zero zero zero zero zero zero zero))
514 (branch
515 NativePhysicalStoreWord64
516 destination
517 value
518 .
519 (constructor NativePhysicalCounts NativePhysicalCountsValue
520 (succ zero) zero zero zero zero zero zero zero zero))
521 (branch
522 NativePhysicalFenceWait
523 address
524 expected
525 maximumPolls
526 interval
527 .
528 (constructor NativePhysicalCounts NativePhysicalCountsValue
529 (succ zero) zero zero zero zero zero zero zero zero))
530 (branch NativePhysicalRepeatBeginCounted count .
531 (constructor NativePhysicalCounts NativePhysicalCountsValue
532 (succ zero) zero zero zero zero zero zero zero zero))
533 (branch NativePhysicalAddWord64 destination left right .
534 (constructor NativePhysicalCounts NativePhysicalCountsValue
535 (succ zero) zero zero zero zero zero zero zero zero))
536 (branch NativePhysicalFloat64 operation destination left right .
537 (constructor NativePhysicalCounts NativePhysicalCountsValue
538 (succ zero) zero zero zero zero zero zero zero zero))))
539
540def nativePhysicalCommandCounts =
541 (lambda unrestricted command : (family NativePhysicalCommand) .
542 (eliminate
543 NativePhysicalCommand
544 (lambda unrestricted current : (family NativePhysicalCommand) . (family NativePhysicalCounts))
545 command
546 (branch
547 NativePhysicalCommandValue
548 operation
549 errorIdentity
550 .
551 (nativePhysicalOperationCounts operation))))
552
553def nativePhysicalCommandsCounts =
554 (lambda unrestricted commands : (family NativePhysicalCommands) .
555 (eliminate
556 NativePhysicalCommands
557 (lambda unrestricted current : (family NativePhysicalCommands) .
558 (family NativePhysicalCounts))
559 commands
560 (branch NativePhysicalCommandsEnd . nativePhysicalZeroCounts)
561 (branch
562 NativePhysicalCommandsNext
563 head
564 tail
565 induction
566 .
567 (nativePhysicalAddCounts (nativePhysicalCommandCounts head) induction))))
568
569def nativePhysicalRequireBytes =
570 (lambda unrestricted payload : Bytes .
571 (lambda unrestricted error : (family NativePhysicalErrorCode) .
572 (nat-eliminate
573 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
574 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error)
575 (lambda unrestricted predecessor : Nat .
576 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
577 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
578 (bytes-length payload))))
579
580-- A wait interval is valid when it is at least one nanosecond and below one
581-- second (999,999,999 nanoseconds), so a timespec with a zero seconds field
582-- carries it.
583def nativePhysicalFenceWaitIntervalValid =
584 (lambda unrestricted interval : (family ModelWord64) .
585 (naturalAnd
586 (naturalIsZero (modelWord64IsZero interval))
587 (modelWord64LessThan interval (modelWord64FromNaturalTruncated 1000000000))))
588
589def nativePhysicalValidateOperation =
590 (lambda unrestricted operation : (family NativePhysicalOperation) .
591 (eliminate
592 NativePhysicalOperation
593 (lambda unrestricted current : (family NativePhysicalOperation) .
594 (family NativePhysicalOperationValidation))
595 operation
596 (branch
597 NativePhysicalSystemCall
598 number
599 arguments
600 payload
601 result
602 .
603 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
604 (branch
605 NativePhysicalCopyPayloadToState
606 destination
607 extent
608 payload
609 .
610 (eliminate
611 NativePhysicalOperationValidation
612 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
613 (family NativePhysicalOperationValidation))
614 (nativePhysicalRequireBytes
615 payload
616 (constructor NativePhysicalErrorCode NativePhysicalCopyPayloadEmpty))
617 (branch
618 NativePhysicalOperationValid
619 .
620 (nat-eliminate
621 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
622 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
623 (lambda unrestricted predecessor : Nat .
624 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
625 (constructor
626 NativePhysicalOperationValidation
627 NativePhysicalOperationInvalid
628 (constructor NativePhysicalErrorCode NativePhysicalCopyExtentZero))))
629 (modelWord64IsZero extent)))
630 (branch
631 NativePhysicalOperationInvalid
632 error
633 .
634 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
635 (branch
636 NativePhysicalMachineRoutine
637 code
638 arguments
639 result
640 .
641 (nativePhysicalRequireBytes
642 code
643 (constructor NativePhysicalErrorCode NativePhysicalMachineCodeEmpty)))
644 (branch
645 NativePhysicalFencePoll
646 address
647 expected
648 maximumPolls
649 .
650 (nat-eliminate
651 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
652 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
653 (lambda unrestricted predecessor : Nat .
654 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
655 (constructor
656 NativePhysicalOperationValidation
657 NativePhysicalOperationInvalid
658 (constructor NativePhysicalErrorCode NativePhysicalFencePollCountZero))))
659 (modelWord64IsZero maximumPolls)))
660 (branch
661 NativePhysicalTelemetryAppend
662 path
663 record
664 .
665 (eliminate
666 NativePhysicalOperationValidation
667 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
668 (family NativePhysicalOperationValidation))
669 (nativePhysicalRequireBytes
670 path
671 (constructor NativePhysicalErrorCode NativePhysicalTelemetryPathEmpty))
672 (branch
673 NativePhysicalOperationValid
674 .
675 (nativePhysicalRequireBytes
676 record
677 (constructor NativePhysicalErrorCode NativePhysicalTelemetryRecordEmpty)))
678 (branch
679 NativePhysicalOperationInvalid
680 error
681 .
682 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
683 (branch
684 NativePhysicalAssertEqual
685 left
686 right
687 error
688 .
689 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
690 (branch
691 NativePhysicalAssertOneOf
692 observed
693 first
694 second
695 error
696 .
697 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
698 (branch
699 NativePhysicalHaltSuccess
700 .
701 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
702 (branch
703 NativePhysicalRepeatBegin
704 count
705 .
706 (nat-eliminate
707 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
708 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid
709 (constructor NativePhysicalErrorCode NativePhysicalRepeatCountZero))
710 (lambda unrestricted predecessor : Nat .
711 (lambda unrestricted induction : (family NativePhysicalOperationValidation) .
712 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
713 (naturalIsZero (modelWord64IsZero count))))
714 (branch
715 NativePhysicalRepeatEnd
716 .
717 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
718 (branch
719 NativePhysicalStoreWord64
720 destination
721 value
722 .
723 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
724 (branch
725 NativePhysicalFenceWait
726 address
727 expected
728 maximumPolls
729 interval
730 .
731 (nat-eliminate
732 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
733 (nat-eliminate
734 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
735 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid
736 (constructor NativePhysicalErrorCode NativePhysicalFenceWaitIntervalInvalid))
737 (lambda unrestricted predecessor : Nat .
738 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
739 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
740 (nativePhysicalFenceWaitIntervalValid interval))
741 (lambda unrestricted predecessor : Nat .
742 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
743 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid
744 (constructor NativePhysicalErrorCode NativePhysicalFenceWaitCountZero))))
745 (modelWord64IsZero maximumPolls)))
746 (branch NativePhysicalRepeatBeginCounted count .
747 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
748 (branch NativePhysicalAddWord64 destination left right .
749 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
750 (branch NativePhysicalFloat64 operation destination left right .
751 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))))
752
753-- Repeats must pair and never nest: 0 means balanced, 1 means a repeat is
754-- still open, 2 means an end without a begin or a begin inside a repeat.
755def nativePhysicalRepeatBalance =
756 (lambda unrestricted commands : (family NativePhysicalCommands) .
757 (app
758 (eliminate
759 NativePhysicalCommands
760 (lambda unrestricted current : (family NativePhysicalCommands) . (pi unrestricted open : Nat . Nat))
761 commands
762 (branch NativePhysicalCommandsEnd . (lambda unrestricted open : Nat . open))
763 (branch NativePhysicalCommandsNext head tail induction .
764 (lambda unrestricted open : Nat .
765 (eliminate
766 NativePhysicalCommand
767 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
768 head
769 (branch NativePhysicalCommandValue operation errorIdentity .
770 (eliminate
771 NativePhysicalOperation
772 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
773 operation
774 (branch NativePhysicalSystemCall number arguments payload result . (induction open))
775 (branch NativePhysicalCopyPayloadToState destination extent payload . (induction open))
776 (branch NativePhysicalMachineRoutine code arguments result . (induction open))
777 (branch NativePhysicalFencePoll address expected polls . (induction open))
778 (branch NativePhysicalTelemetryAppend path record . (induction open))
779 (branch NativePhysicalAssertEqual left right error . (induction open))
780 (branch NativePhysicalAssertOneOf observed first second error . (induction open))
781 (branch NativePhysicalHaltSuccess . (induction open))
782 (branch NativePhysicalRepeatBegin count .
783 (nat-eliminate
784 (lambda unrestricted current : Nat . Nat)
785 (induction (succ zero))
786 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . 2))
787 open))
788 (branch NativePhysicalRepeatEnd .
789 (nat-eliminate
790 (lambda unrestricted current : Nat . Nat)
791 2
792 (lambda unrestricted predecessor : Nat .
793 (lambda unrestricted ignored : Nat .
794 (nat-eliminate
795 (lambda unrestricted current : Nat . Nat)
796 (induction zero)
797 (lambda unrestricted deeper : Nat . (lambda unrestricted ignoredDeeper : Nat . 2))
798 predecessor)))
799 open))
800 (branch NativePhysicalStoreWord64 destination value . (induction open))
801 (branch NativePhysicalFenceWait address expected polls interval . (induction open))
802 (branch NativePhysicalRepeatBeginCounted count .
803 (nat-eliminate
804 (lambda unrestricted current : Nat . Nat)
805 (induction (succ zero))
806 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . 2))
807 open))
808 (branch NativePhysicalAddWord64 destination left right . (induction open))
809 (branch NativePhysicalFloat64 operation destination left right . (induction open))))))))
810 zero))
811
812def nativePhysicalValidateCommands =
813 (lambda unrestricted commands : (family NativePhysicalCommands) .
814 (eliminate
815 NativePhysicalCommands
816 (lambda unrestricted current : (family NativePhysicalCommands) .
817 (family NativePhysicalCommandsValidation))
818 commands
819 (branch
820 NativePhysicalCommandsEnd
821 .
822 (constructor NativePhysicalCommandsValidation NativePhysicalCommandsValid zero))
823 (branch
824 NativePhysicalCommandsNext
825 head
826 tail
827 induction
828 .
829 (eliminate
830 NativePhysicalCommand
831 (lambda unrestricted current : (family NativePhysicalCommand) .
832 (family NativePhysicalCommandsValidation))
833 head
834 (branch
835 NativePhysicalCommandValue
836 operation
837 errorIdentity
838 .
839 (eliminate
840 NativePhysicalOperationValidation
841 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
842 (family NativePhysicalCommandsValidation))
843 (nativePhysicalValidateOperation operation)
844 (branch
845 NativePhysicalOperationValid
846 .
847 (eliminate
848 NativePhysicalCommandsValidation
849 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
850 (family NativePhysicalCommandsValidation))
851 induction
852 (branch
853 NativePhysicalCommandsValid
854 completed
855 .
856 (constructor
857 NativePhysicalCommandsValidation
858 NativePhysicalCommandsValid
859 (succ completed)))
860 (branch
861 NativePhysicalCommandsInvalid
862 error
863 ordinal
864 .
865 (constructor
866 NativePhysicalCommandsValidation
867 NativePhysicalCommandsInvalid
868 error
869 (succ ordinal)))))
870 (branch
871 NativePhysicalOperationInvalid
872 error
873 .
874 (constructor
875 NativePhysicalCommandsValidation
876 NativePhysicalCommandsInvalid
877 error
878 zero))))))))
879
880def nativePhysicalValidationTelemetryFor =
881 (lambda unrestricted program : (family NativePhysicalProgram) .
882 (lambda unrestricted failures : Nat .
883 (lambda unrestricted ordinal : Nat .
884 (lambda unrestricted code : Bytes .
885 (eliminate
886 NativePhysicalProgram
887 (lambda unrestricted current : (family NativePhysicalProgram) .
888 (family NativePhysicalValidationTelemetry))
889 program
890 (branch
891 NativePhysicalProgramValue
892 stateExtent
893 resultSlots
894 commands
895 expected
896 identity
897 fallbacks
898 .
899 (constructor
900 NativePhysicalValidationTelemetry
901 NativePhysicalValidationTelemetryValue
902 (nativePhysicalCommandsCounts commands)
903 expected
904 stateExtent
905 resultSlots
906 fallbacks
907 identity
908 failures
909 ordinal
910 code)))))))
911
912def nativePhysicalReject =
913 (lambda unrestricted program : (family NativePhysicalProgram) .
914 (lambda unrestricted error : (family NativePhysicalErrorCode) .
915 (lambda unrestricted ordinal : Nat .
916 (constructor
917 NativePhysicalProgramValidation
918 NativePhysicalProgramRejected
919 error
920 (nativePhysicalValidationTelemetryFor
921 program
922 (succ zero)
923 ordinal
924 (nativePhysicalErrorCodeBytes error))))))
925
926def nativePhysicalValidateProgram =
927 (lambda unrestricted program : (family NativePhysicalProgram) .
928 (eliminate
929 NativePhysicalProgram
930 (lambda unrestricted current : (family NativePhysicalProgram) .
931 (family NativePhysicalProgramValidation))
932 program
933 (branch
934 NativePhysicalProgramValue
935 stateExtent
936 resultSlots
937 commands
938 expected
939 identity
940 fallbacks
941 .
942 (nat-eliminate
943 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
944 (nativePhysicalReject
945 program
946 (constructor NativePhysicalErrorCode NativePhysicalIdentityInvalid)
947 zero)
948 (lambda unrestricted identityPredecessor : Nat .
949 (lambda unrestricted ignoredIdentity : (family NativePhysicalProgramValidation) .
950 (nat-eliminate
951 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
952 (nativePhysicalReject
953 program
954 (constructor NativePhysicalErrorCode NativePhysicalFallbackObserved)
955 zero)
956 (lambda unrestricted fallbackPredecessor : Nat .
957 (lambda unrestricted ignoredFallback : (family NativePhysicalProgramValidation) .
958 (nat-eliminate
959 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
960 (eliminate
961 NativePhysicalCommandsValidation
962 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
963 (family NativePhysicalProgramValidation))
964 (nat-eliminate
965 (lambda unrestricted current : Nat . (family NativePhysicalCommandsValidation))
966 (nativePhysicalValidateCommands commands)
967 (lambda unrestricted predecessor : Nat .
968 (lambda unrestricted ignoredBalance : (family NativePhysicalCommandsValidation) .
969 (constructor NativePhysicalCommandsValidation NativePhysicalCommandsInvalid
970 (constructor NativePhysicalErrorCode NativePhysicalRepeatUnbalanced)
971 zero)))
972 (nativePhysicalRepeatBalance commands))
973 (branch
974 NativePhysicalCommandsValid
975 completed
976 .
977 (nat-eliminate
978 (lambda unrestricted current : Nat .
979 (family NativePhysicalProgramValidation))
980 (nativePhysicalReject
981 program
982 (constructor
983 NativePhysicalErrorCode
984 NativePhysicalCommandCountMismatch)
985 zero)
986 (lambda unrestricted countPredecessor : Nat .
987 (lambda unrestricted ignoredCount : (family NativePhysicalProgramValidation) .
988 (constructor
989 NativePhysicalProgramValidation
990 NativePhysicalProgramValidated
991 program
992 (nativePhysicalValidationTelemetryFor program zero zero b""))))
993 (naturalEqual completed expected)))
994 (branch
995 NativePhysicalCommandsInvalid
996 error
997 ordinal
998 .
999 (nativePhysicalReject program error ordinal)))
1000 (lambda unrestricted statePredecessor : Nat .
1001 (lambda unrestricted ignoredState : (family NativePhysicalProgramValidation) .
1002 (nativePhysicalReject
1003 program
1004 (constructor NativePhysicalErrorCode NativePhysicalStateExtentZero)
1005 zero)))
1006 (modelWord64IsZero stateExtent))))
1007 (naturalEqual fallbacks zero))))
1008 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))))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.