1module Runtime.NativePhysicalProgram
2
3import Model.Parameter
4import Model.Word32
5import Runtime.NativeTelemetry
6import Runtime.NativePhysicalMemory
7import Std.Natural
8import Model.Word64
9
10family NativePhysicalErrorCode : Type 0
11constructor NativePhysicalIdentityInvalid
12constructor NativePhysicalFallbackObserved
13constructor NativePhysicalCommandCountMismatch
14constructor NativePhysicalStateExtentZero
15constructor NativePhysicalCopyPayloadEmpty
16constructor NativePhysicalCopyExtentZero
17constructor NativePhysicalMachineCodeEmpty
18constructor NativePhysicalFencePollCountZero
19constructor NativePhysicalTelemetryPathEmpty
20constructor NativePhysicalTelemetryRecordEmpty
21constructor NativePhysicalResultSlotUnavailable
22constructor NativePhysicalExecutionAssertionFailed
23constructor NativePhysicalRepeatCountZero
24constructor NativePhysicalRepeatUnbalanced
25constructor NativePhysicalFenceWaitCountZero
26constructor NativePhysicalFenceWaitIntervalInvalid
27constructor NativePhysicalBranchTargetInvalid
28constructor NativePhysicalMemoryExtentInvalid
29
30end-family
31
32family NativePhysicalSlot : Type 0
33constructor NativePhysicalSlotValue
34field unrestricted nativePhysicalSlotIndex : (family ModelWord64)
35
36end-family
37
38family NativePhysicalOperand : Type 0
39constructor NativePhysicalImmediate
40field unrestricted nativePhysicalImmediateValue : (family ModelWord64)
41constructor NativePhysicalResultValue
42field unrestricted nativePhysicalResultValueSlot : (family NativePhysicalSlot)
43constructor NativePhysicalResultAddress
44field unrestricted nativePhysicalResultAddressSlot : (family NativePhysicalSlot)
45field unrestricted nativePhysicalResultAddressOffset : (family ModelWord64)
46constructor NativePhysicalStateAddress
47field unrestricted nativePhysicalStateAddressOffset : (family ModelWord64)
48constructor NativePhysicalStateLoad64
49field unrestricted nativePhysicalStateLoadOffset : (family ModelWord64)
50constructor NativePhysicalPayloadAddress
51field unrestricted nativePhysicalPayloadAddressOffset : (family ModelWord64)
52constructor NativePhysicalPayloadLoad64
53field unrestricted nativePhysicalPayloadLoadOffset : (family ModelWord64)
54constructor NativePhysicalProcessArgument
55field unrestricted nativePhysicalProcessArgumentIndex : (family ModelWord64)
56-- base + iteration * stride, where iteration counts the enclosing repeat's
57-- completed passes from zero. Outside a repeat the iteration is zero.
58constructor NativePhysicalLoopAffine
59field unrestricted nativePhysicalLoopAffineBase : (family ModelWord64)
60field unrestricted nativePhysicalLoopAffineStride : (family ModelWord64)
61
62end-family
63
64family NativePhysicalArguments : Type 0
65constructor NativePhysicalArgumentsValue
66field unrestricted nativePhysicalArgument0 : (family NativePhysicalOperand)
67field unrestricted nativePhysicalArgument1 : (family NativePhysicalOperand)
68field unrestricted nativePhysicalArgument2 : (family NativePhysicalOperand)
69field unrestricted nativePhysicalArgument3 : (family NativePhysicalOperand)
70field unrestricted nativePhysicalArgument4 : (family NativePhysicalOperand)
71field unrestricted nativePhysicalArgument5 : (family NativePhysicalOperand)
72
73end-family
74
75family NativePhysicalResultBinding : Type 0
76constructor NativePhysicalDiscardResult
77constructor NativePhysicalStoreResult
78field unrestricted nativePhysicalStoredResultSlot : (family NativePhysicalSlot)
79
80end-family
81
82-- The binary64 operations the host computes with (IEEE 754, round to
83-- nearest even; x86 SSE2): the sum, difference, product and quotient of
84-- the left and right operands' words read as binary64; the square root of
85-- the right one; the left word, a natural below 2^63, as the nearest
86-- binary64; the left binary64 rounded to the nearest binary32 (its word
87-- zero-extended); the left word's low half, a binary32, as the binary64 of
88-- the same value. (Binary32 +, -, *, / and square root are these binary64
89-- operations rounded to binary32: 53 bits hold 2 x 24 + 2, so the double
90-- rounding is exact.)
91family NativePhysicalFloat64Operation : Type 0
92constructor NativePhysicalFloat64Add
93constructor NativePhysicalFloat64Subtract
94constructor NativePhysicalFloat64Multiply
95constructor NativePhysicalFloat64Divide
96constructor NativePhysicalFloat64SquareRoot
97constructor NativePhysicalFloat64FromNatural
98constructor NativePhysicalFloat64ToBinary32
99constructor NativePhysicalFloat64FromBinary32
100
101end-family
102
103family NativePhysicalOperation : Type 0
104constructor NativePhysicalSystemCall
105field unrestricted nativePhysicalSystemCallNumber : (family NativePhysicalOperand)
106field unrestricted nativePhysicalSystemCallArguments : (family NativePhysicalArguments)
107field unrestricted nativePhysicalSystemCallPayload : Bytes
108field unrestricted nativePhysicalSystemCallResult : (family NativePhysicalResultBinding)
109constructor NativePhysicalCopyPayloadToState
110field unrestricted nativePhysicalCopyDestinationOffset : (family ModelWord64)
111field unrestricted nativePhysicalCopyExtent : (family ModelWord64)
112field unrestricted nativePhysicalCopyPayload : Bytes
113constructor NativePhysicalMachineRoutine
114field unrestricted nativePhysicalMachineCode : Bytes
115field unrestricted nativePhysicalMachineArguments : (family NativePhysicalArguments)
116field unrestricted nativePhysicalMachineResult : (family NativePhysicalResultBinding)
117constructor NativePhysicalFencePoll
118field unrestricted nativePhysicalFenceAddress : (family NativePhysicalOperand)
119field unrestricted nativePhysicalFenceExpected : (family NativePhysicalOperand)
120field unrestricted nativePhysicalFenceMaximumPolls : (family ModelWord64)
121constructor NativePhysicalTelemetryAppend
122field unrestricted nativePhysicalTelemetryPath : Bytes
123field unrestricted nativePhysicalTelemetryRecord : Bytes
124constructor NativePhysicalAssertEqual
125field unrestricted nativePhysicalAssertLeft : (family NativePhysicalOperand)
126field unrestricted nativePhysicalAssertRight : (family NativePhysicalOperand)
127field unrestricted nativePhysicalAssertError : (family NativePhysicalErrorCode)
128constructor NativePhysicalAssertOneOf
129field unrestricted nativePhysicalAssertOneOfObserved : (family NativePhysicalOperand)
130field unrestricted nativePhysicalAssertOneOfFirst : (family NativePhysicalOperand)
131field unrestricted nativePhysicalAssertOneOfSecond : (family NativePhysicalOperand)
132field unrestricted nativePhysicalAssertOneOfError : (family NativePhysicalErrorCode)
133constructor NativePhysicalHaltSuccess
134-- Execute the commands up to the matching RepeatEnd count times. Repeats do
135-- not nest; the runtime keeps one iteration counter and the loop-affine
136-- operands read it.
137constructor NativePhysicalRepeatBegin
138field unrestricted nativePhysicalRepeatCount : (family ModelWord64)
139-- Skip a derived count of following command records when two runtime words
140-- differ. The target must stay inside the same repeat frame. Unlike using a
141-- zero/one counted loop as a guard, this leaves loop-affine state untouched.
142constructor NativePhysicalSkipUnlessEqual
143field unrestricted nativePhysicalBranchLeft : (family NativePhysicalOperand)
144field unrestricted nativePhysicalBranchRight : (family NativePhysicalOperand)
145field unrestricted nativePhysicalBranchSkip : (family ModelWord64)
146constructor NativePhysicalRepeatEnd
147-- Finish this iteration and leave the bounded loop when the operands agree.
148-- This closes the same loop as RepeatEnd; it is not a nested conditional.
149constructor NativePhysicalRepeatEndWhen
150field unrestricted nativePhysicalRepeatObserved : (family NativePhysicalOperand)
151field unrestricted nativePhysicalRepeatExpected : (family NativePhysicalOperand)
152-- Store the 64-bit value of an operand at the address another operand
153-- resolves to (a state or result address): how a repeat body places a
154-- loop-affine value where a system call can read it.
155constructor NativePhysicalStoreWord64
156field unrestricted nativePhysicalStoreDestination : (family NativePhysicalOperand)
157field unrestricted nativePhysicalStoreValue : (family NativePhysicalOperand)
158-- Wait until the 64-bit word at an address equals the expected value,
159-- sleeping intervalNanoseconds between polls (a nanosleep, so the host does
160-- not spin), at most maximumPolls times: how a host waits on device state
161-- (a completion semaphore) instead of on the clock. A timeout is a command
162-- failure -- it never yields a ready value. The interval must be below one
163-- second so the timespec is a single nanosecond field.
164constructor NativePhysicalFenceWait
165field unrestricted nativePhysicalFenceWaitAddress : (family NativePhysicalOperand)
166field unrestricted nativePhysicalFenceWaitExpected : (family NativePhysicalOperand)
167field unrestricted nativePhysicalFenceWaitMaximumPolls : (family ModelWord64)
168field unrestricted nativePhysicalFenceWaitIntervalNanoseconds : (family ModelWord64)
169-- A repeat whose count an operand gives at run time (a state word): a
170-- count of zero skips the body, so it is how a block is made conditional
171-- on what the host has read.
172constructor NativePhysicalRepeatBeginCounted
173field unrestricted nativePhysicalRepeatCountOperand : (family NativePhysicalOperand)
174-- The 64-bit sum (modulo 2^64) of two operands, stored at the address a
175-- third resolves to.
176constructor NativePhysicalAddWord64
177field unrestricted nativePhysicalAddDestination : (family NativePhysicalOperand)
178field unrestricted nativePhysicalAddLeft : (family NativePhysicalOperand)
179field unrestricted nativePhysicalAddRight : (family NativePhysicalOperand)
180-- A binary64 operation on two operands' words, the result's word stored at
181-- the address a third resolves to.
182constructor NativePhysicalFloat64
183field unrestricted nativePhysicalFloat64Operation : (family NativePhysicalFloat64Operation)
184field unrestricted nativePhysicalFloat64Destination : (family NativePhysicalOperand)
185field unrestricted nativePhysicalFloat64Left : (family NativePhysicalOperand)
186field unrestricted nativePhysicalFloat64Right : (family NativePhysicalOperand)
187
188end-family
189
190family NativePhysicalCommand : Type 0
191constructor NativePhysicalCommandValue
192field unrestricted nativePhysicalCommandOperation : (family NativePhysicalOperation)
193field unrestricted nativePhysicalCommandErrorIdentity : Bytes
194
195end-family
196
197family NativePhysicalCommands : Type 0
198constructor NativePhysicalCommandsEnd
199constructor NativePhysicalCommandsNext
200field unrestricted nativePhysicalCommandHead : (family NativePhysicalCommand)
201recursive unrestricted nativePhysicalCommandTail
202
203end-family
204
205family NativePhysicalProgram : Type 0
206constructor NativePhysicalProgramValue
207field unrestricted nativePhysicalProgramStateExtent : (family ModelWord64)
208field unrestricted nativePhysicalProgramResultSlots : (family ModelWord64)
209field unrestricted nativePhysicalProgramCommands : (family NativePhysicalCommands)
210field unrestricted nativePhysicalProgramExpectedCommands : Nat
211field unrestricted nativePhysicalProgramIdentity : Bytes
212field unrestricted nativePhysicalProgramFallbacks : Nat
213
214end-family
215
216family NativePhysicalCounts : Type 0
217constructor NativePhysicalCountsValue
218field unrestricted nativePhysicalCountCommands : Nat
219field unrestricted nativePhysicalCountSystemCalls : Nat
220field unrestricted nativePhysicalCountCopies : Nat
221field unrestricted nativePhysicalCountMachineRoutines : Nat
222field unrestricted nativePhysicalCountFencePolls : Nat
223field unrestricted nativePhysicalCountTelemetryAppends : Nat
224field unrestricted nativePhysicalCountAssertions : Nat
225field unrestricted nativePhysicalCountHalts : Nat
226field unrestricted nativePhysicalCountPayloadBytes : Nat
227
228end-family
229
230family NativePhysicalOperationValidation : Type 0
231constructor NativePhysicalOperationValid
232constructor NativePhysicalOperationInvalid
233field unrestricted nativePhysicalOperationError : (family NativePhysicalErrorCode)
234
235end-family
236
237family NativePhysicalCommandsValidation : Type 0
238constructor NativePhysicalCommandsValid
239field unrestricted nativePhysicalValidatedCommands : Nat
240constructor NativePhysicalCommandsInvalid
241field unrestricted nativePhysicalCommandsError : (family NativePhysicalErrorCode)
242field unrestricted nativePhysicalCommandsErrorOrdinal : Nat
243
244end-family
245
246family NativePhysicalValidationTelemetry : Type 0
247constructor NativePhysicalValidationTelemetryValue
248field unrestricted nativePhysicalValidationCounts : (family NativePhysicalCounts)
249field unrestricted nativePhysicalValidationExpectedCommands : Nat
250field unrestricted nativePhysicalValidationStateExtent : (family ModelWord64)
251field unrestricted nativePhysicalValidationResultSlots : (family ModelWord64)
252field unrestricted nativePhysicalValidationFallbacks : Nat
253field unrestricted nativePhysicalValidationIdentity : Bytes
254field unrestricted nativePhysicalValidationFailures : Nat
255field unrestricted nativePhysicalValidationFailureOrdinal : Nat
256field unrestricted nativePhysicalValidationFailureCode : Bytes
257
258end-family
259
260family NativePhysicalProgramValidation : Type 0
261constructor NativePhysicalProgramValidated
262field unrestricted nativePhysicalValidatedProgram : (family NativePhysicalProgram)
263field unrestricted nativePhysicalValidatedTelemetry : (family NativePhysicalValidationTelemetry)
264constructor NativePhysicalProgramRejected
265field unrestricted nativePhysicalRejectedError : (family NativePhysicalErrorCode)
266field unrestricted nativePhysicalRejectedTelemetry : (family NativePhysicalValidationTelemetry)
267
268end-family
269
270def nativePhysicalErrorCodeBytes =
271 (lambda unrestricted code : (family NativePhysicalErrorCode) .
272 (eliminate
273 NativePhysicalErrorCode
274 (lambda unrestricted current : (family NativePhysicalErrorCode) . Bytes)
275 code
276 (branch NativePhysicalIdentityInvalid . b"ALPHA-PHYS-001")
277 (branch NativePhysicalFallbackObserved . b"ALPHA-PHYS-002")
278 (branch NativePhysicalCommandCountMismatch . b"ALPHA-PHYS-003")
279 (branch NativePhysicalStateExtentZero . b"ALPHA-PHYS-004")
280 (branch NativePhysicalCopyPayloadEmpty . b"ALPHA-PHYS-005")
281 (branch NativePhysicalCopyExtentZero . b"ALPHA-PHYS-006")
282 (branch NativePhysicalMachineCodeEmpty . b"ALPHA-PHYS-007")
283 (branch NativePhysicalFencePollCountZero . b"ALPHA-PHYS-008")
284 (branch NativePhysicalTelemetryPathEmpty . b"ALPHA-PHYS-009")
285 (branch NativePhysicalTelemetryRecordEmpty . b"ALPHA-PHYS-010")
286 (branch NativePhysicalResultSlotUnavailable . b"ALPHA-PHYS-011")
287 (branch NativePhysicalExecutionAssertionFailed . b"ALPHA-PHYS-012")
288 (branch NativePhysicalRepeatCountZero . b"ALPHA-PHYS-013")
289 (branch NativePhysicalRepeatUnbalanced . b"ALPHA-PHYS-014")
290 (branch NativePhysicalFenceWaitCountZero . b"ALPHA-PHYS-015")
291 (branch NativePhysicalFenceWaitIntervalInvalid . b"ALPHA-PHYS-016")
292 (branch NativePhysicalBranchTargetInvalid . b"ALPHA-PHYS-017")
293 (branch NativePhysicalMemoryExtentInvalid . b"ALPHA-PHYS-018")))
294
295def nativePhysicalZeroCounts : (family NativePhysicalCounts) =
296 (constructor
297 NativePhysicalCounts
298 NativePhysicalCountsValue
299 zero
300 zero
301 zero
302 zero
303 zero
304 zero
305 zero
306 zero
307 zero)
308
309def nativePhysicalAddCounts =
310 (lambda unrestricted left : (family NativePhysicalCounts) .
311 (lambda unrestricted right : (family NativePhysicalCounts) .
312 (eliminate
313 NativePhysicalCounts
314 (lambda unrestricted current : (family NativePhysicalCounts) .
315 (family NativePhysicalCounts))
316 left
317 (branch
318 NativePhysicalCountsValue
319 leftCommands
320 leftSystemCalls
321 leftCopies
322 leftRoutines
323 leftFences
324 leftTelemetry
325 leftAssertions
326 leftHalts
327 leftPayload
328 .
329 (eliminate
330 NativePhysicalCounts
331 (lambda unrestricted current : (family NativePhysicalCounts) .
332 (family NativePhysicalCounts))
333 right
334 (branch
335 NativePhysicalCountsValue
336 rightCommands
337 rightSystemCalls
338 rightCopies
339 rightRoutines
340 rightFences
341 rightTelemetry
342 rightAssertions
343 rightHalts
344 rightPayload
345 .
346 (constructor
347 NativePhysicalCounts
348 NativePhysicalCountsValue
349 (naturalAdd leftCommands rightCommands)
350 (naturalAdd leftSystemCalls rightSystemCalls)
351 (naturalAdd leftCopies rightCopies)
352 (naturalAdd leftRoutines rightRoutines)
353 (naturalAdd leftFences rightFences)
354 (naturalAdd leftTelemetry rightTelemetry)
355 (naturalAdd leftAssertions rightAssertions)
356 (naturalAdd leftHalts rightHalts)
357 (naturalAdd leftPayload rightPayload))))))))
358
359def nativePhysicalOperationCounts =
360 (lambda unrestricted operation : (family NativePhysicalOperation) .
361 (eliminate
362 NativePhysicalOperation
363 (lambda unrestricted current : (family NativePhysicalOperation) .
364 (family NativePhysicalCounts))
365 operation
366 (branch
367 NativePhysicalSystemCall
368 number
369 arguments
370 payload
371 result
372 .
373 (constructor
374 NativePhysicalCounts
375 NativePhysicalCountsValue
376 (succ zero)
377 (succ zero)
378 zero
379 zero
380 zero
381 zero
382 zero
383 zero
384 (bytes-length payload)))
385 (branch
386 NativePhysicalCopyPayloadToState
387 destination
388 extent
389 payload
390 .
391 (constructor
392 NativePhysicalCounts
393 NativePhysicalCountsValue
394 (succ zero)
395 zero
396 (succ zero)
397 zero
398 zero
399 zero
400 zero
401 zero
402 (bytes-length payload)))
403 (branch
404 NativePhysicalMachineRoutine
405 code
406 arguments
407 result
408 .
409 (constructor
410 NativePhysicalCounts
411 NativePhysicalCountsValue
412 (succ zero)
413 zero
414 zero
415 (succ zero)
416 zero
417 zero
418 zero
419 zero
420 (bytes-length code)))
421 (branch
422 NativePhysicalFencePoll
423 address
424 expected
425 maximumPolls
426 .
427 (constructor
428 NativePhysicalCounts
429 NativePhysicalCountsValue
430 (succ zero)
431 zero
432 zero
433 zero
434 (succ zero)
435 zero
436 zero
437 zero
438 zero))
439 (branch
440 NativePhysicalTelemetryAppend
441 path
442 record
443 .
444 (constructor
445 NativePhysicalCounts
446 NativePhysicalCountsValue
447 (succ zero)
448 zero
449 zero
450 zero
451 zero
452 (succ zero)
453 zero
454 zero
455 (naturalAdd (bytes-length path) (bytes-length record))))
456 (branch
457 NativePhysicalAssertEqual
458 left
459 right
460 error
461 .
462 (constructor
463 NativePhysicalCounts
464 NativePhysicalCountsValue
465 (succ zero)
466 zero
467 zero
468 zero
469 zero
470 zero
471 (succ zero)
472 zero
473 zero))
474 (branch
475 NativePhysicalAssertOneOf
476 observed
477 first
478 second
479 error
480 .
481 (constructor
482 NativePhysicalCounts
483 NativePhysicalCountsValue
484 (succ zero)
485 zero
486 zero
487 zero
488 zero
489 zero
490 (succ zero)
491 zero
492 zero))
493 (branch
494 NativePhysicalHaltSuccess
495 .
496 (constructor
497 NativePhysicalCounts
498 NativePhysicalCountsValue
499 (succ zero)
500 zero
501 zero
502 zero
503 zero
504 zero
505 zero
506 (succ zero)
507 zero))
508 (branch
509 NativePhysicalRepeatBegin
510 count
511 .
512 (constructor
513 NativePhysicalCounts
514 NativePhysicalCountsValue
515 (succ zero)
516 zero
517 zero
518 zero
519 zero
520 zero
521 zero
522 zero
523 zero))
524 (branch
525 NativePhysicalSkipUnlessEqual
526 left
527 right
528 count
529 .
530 (constructor NativePhysicalCounts NativePhysicalCountsValue 1 0 0 0 0 0 0 0 0))
531 (branch
532 NativePhysicalRepeatEnd
533 .
534 (constructor
535 NativePhysicalCounts
536 NativePhysicalCountsValue
537 (succ zero)
538 zero
539 zero
540 zero
541 zero
542 zero
543 zero
544 zero
545 zero))
546 (branch
547 NativePhysicalRepeatEndWhen
548 observed
549 expected
550 .
551 (constructor
552 NativePhysicalCounts
553 NativePhysicalCountsValue
554 (succ zero)
555 zero
556 zero
557 zero
558 zero
559 zero
560 zero
561 zero
562 zero))
563 (branch
564 NativePhysicalStoreWord64
565 destination
566 value
567 .
568 (constructor
569 NativePhysicalCounts
570 NativePhysicalCountsValue
571 (succ zero)
572 zero
573 zero
574 zero
575 zero
576 zero
577 zero
578 zero
579 zero))
580 (branch
581 NativePhysicalFenceWait
582 address
583 expected
584 maximumPolls
585 interval
586 .
587 (constructor
588 NativePhysicalCounts
589 NativePhysicalCountsValue
590 (succ zero)
591 zero
592 zero
593 zero
594 zero
595 zero
596 zero
597 zero
598 zero))
599 (branch
600 NativePhysicalRepeatBeginCounted
601 count
602 .
603 (constructor
604 NativePhysicalCounts
605 NativePhysicalCountsValue
606 (succ zero)
607 zero
608 zero
609 zero
610 zero
611 zero
612 zero
613 zero
614 zero))
615 (branch
616 NativePhysicalAddWord64
617 destination
618 left
619 right
620 .
621 (constructor
622 NativePhysicalCounts
623 NativePhysicalCountsValue
624 (succ zero)
625 zero
626 zero
627 zero
628 zero
629 zero
630 zero
631 zero
632 zero))
633 (branch
634 NativePhysicalFloat64
635 operation
636 destination
637 left
638 right
639 .
640 (constructor
641 NativePhysicalCounts
642 NativePhysicalCountsValue
643 (succ zero)
644 zero
645 zero
646 zero
647 zero
648 zero
649 zero
650 zero
651 zero))))
652
653def nativePhysicalCommandCounts =
654 (lambda unrestricted command : (family NativePhysicalCommand) .
655 (eliminate
656 NativePhysicalCommand
657 (lambda unrestricted current : (family NativePhysicalCommand) . (family NativePhysicalCounts))
658 command
659 (branch
660 NativePhysicalCommandValue
661 operation
662 errorIdentity
663 .
664 (nativePhysicalOperationCounts operation))))
665
666def nativePhysicalCommandsCounts =
667 (lambda unrestricted commands : (family NativePhysicalCommands) .
668 (eliminate
669 NativePhysicalCommands
670 (lambda unrestricted current : (family NativePhysicalCommands) .
671 (family NativePhysicalCounts))
672 commands
673 (branch NativePhysicalCommandsEnd . nativePhysicalZeroCounts)
674 (branch
675 NativePhysicalCommandsNext
676 head
677 tail
678 induction
679 .
680 (nativePhysicalAddCounts (nativePhysicalCommandCounts head) induction))))
681
682def nativePhysicalRequireBytes =
683 (lambda unrestricted payload : Bytes .
684 (lambda unrestricted error : (family NativePhysicalErrorCode) .
685 (nat-eliminate
686 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
687 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error)
688 (lambda unrestricted predecessor : Nat .
689 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
690 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
691 (bytes-length payload))))
692
693-- A wait interval is valid when it is at least one nanosecond and below one
694-- second (999,999,999 nanoseconds), so a timespec with a zero seconds field
695-- carries it.
696def nativePhysicalFenceWaitIntervalValid =
697 (lambda unrestricted interval : (family ModelWord64) .
698 (naturalAnd
699 (naturalIsZero (modelWord64IsZero interval))
700 (modelWord64LessThan interval (modelWord64FromNaturalTruncated 1000000000))))
701
702-- Repeats must pair and never nest: 0 means balanced, 1 means a repeat is
703-- still open, 2 means an end without a begin or a begin inside a repeat.
704def nativePhysicalRepeatBalance =
705 (lambda unrestricted commands : (family NativePhysicalCommands) .
706 (app
707 (eliminate
708 NativePhysicalCommands
709 (lambda unrestricted current : (family NativePhysicalCommands) .
710 (pi unrestricted open : Nat . Nat))
711 commands
712 (branch NativePhysicalCommandsEnd . (lambda unrestricted open : Nat . open))
713 (branch
714 NativePhysicalCommandsNext
715 head
716 tail
717 induction
718 .
719 (lambda unrestricted open : Nat .
720 (eliminate
721 NativePhysicalCommand
722 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
723 head
724 (branch
725 NativePhysicalCommandValue
726 operation
727 errorIdentity
728 .
729 (eliminate
730 NativePhysicalOperation
731 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
732 operation
733 (branch
734 NativePhysicalSystemCall
735 number
736 arguments
737 payload
738 result
739 .
740 (induction open))
741 (branch
742 NativePhysicalCopyPayloadToState
743 destination
744 extent
745 payload
746 .
747 (induction open))
748 (branch NativePhysicalMachineRoutine code arguments result . (induction open))
749 (branch NativePhysicalFencePoll address expected polls . (induction open))
750 (branch NativePhysicalTelemetryAppend path record . (induction open))
751 (branch NativePhysicalAssertEqual left right error . (induction open))
752 (branch NativePhysicalAssertOneOf observed first second error . (induction open))
753 (branch NativePhysicalHaltSuccess . (induction open))
754 (branch
755 NativePhysicalRepeatBegin
756 count
757 .
758 (nat-eliminate
759 (lambda unrestricted current : Nat . Nat)
760 (induction (succ zero))
761 (lambda unrestricted predecessor : Nat .
762 (lambda unrestricted ignored : Nat . 2))
763 open))
764 (branch NativePhysicalSkipUnlessEqual left right count . (induction open))
765 (branch
766 NativePhysicalRepeatEnd
767 .
768 (nat-eliminate
769 (lambda unrestricted current : Nat . Nat)
770 2
771 (lambda unrestricted predecessor : Nat .
772 (lambda unrestricted ignored : Nat .
773 (nat-eliminate
774 (lambda unrestricted current : Nat . Nat)
775 (induction zero)
776 (lambda unrestricted deeper : Nat .
777 (lambda unrestricted ignoredDeeper : Nat . 2))
778 predecessor)))
779 open))
780 (branch
781 NativePhysicalRepeatEndWhen
782 observed
783 expected
784 .
785 (nat-eliminate
786 (lambda unrestricted current : Nat . Nat)
787 2
788 (lambda unrestricted predecessor : Nat .
789 (lambda unrestricted ignored : Nat .
790 (nat-eliminate
791 (lambda unrestricted current : Nat . Nat)
792 (induction zero)
793 (lambda unrestricted deeper : Nat .
794 (lambda unrestricted ignoredDeeper : Nat . 2))
795 predecessor)))
796 open))
797 (branch NativePhysicalStoreWord64 destination value . (induction open))
798 (branch
799 NativePhysicalFenceWait
800 address
801 expected
802 polls
803 interval
804 .
805 (induction open))
806 (branch
807 NativePhysicalRepeatBeginCounted
808 count
809 .
810 (nat-eliminate
811 (lambda unrestricted current : Nat . Nat)
812 (induction (succ zero))
813 (lambda unrestricted predecessor : Nat .
814 (lambda unrestricted ignored : Nat . 2))
815 open))
816 (branch NativePhysicalAddWord64 destination left right . (induction open))
817 (branch NativePhysicalFloat64 operation destination left right . (induction open))))))))
818 zero))
819
820def nativePhysicalCommandsLength =
821 (lambda unrestricted commands : (family NativePhysicalCommands) .
822 (eliminate
823 NativePhysicalCommands
824 (lambda unrestricted current : (family NativePhysicalCommands) . Nat)
825 commands
826 (branch NativePhysicalCommandsEnd . 0)
827 (branch NativePhysicalCommandsNext command rest induction . (succ induction))))
828
829-- Arena/slot admission belongs to the caller's checked plan. The program owns
830-- its command count and declares no fallback; native encoding still validates
831-- the exact identity width, nonempty program and reachable command contracts.
832def nativePhysicalCommandsTake =
833 (lambda unrestricted commands : (family NativePhysicalCommands) .
834 (eliminate
835 NativePhysicalCommands
836 (lambda unrestricted current : (family NativePhysicalCommands) .
837 (pi unrestricted count : Nat . (family NativePhysicalCommands)))
838 commands
839 (branch
840 NativePhysicalCommandsEnd
841 .
842 (lambda unrestricted count : Nat .
843 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))
844 (branch
845 NativePhysicalCommandsNext
846 head
847 tail
848 induction
849 .
850 (lambda unrestricted count : Nat .
851 (nat-eliminate
852 (lambda unrestricted remaining : Nat . (family NativePhysicalCommands))
853 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
854 (lambda unrestricted previous : Nat .
855 (lambda unrestricted ignored : (family NativePhysicalCommands) .
856 (constructor
857 NativePhysicalCommands
858 NativePhysicalCommandsNext
859 head
860 (induction previous))))
861 count)))))
862
863-- A jump may skip a complete loop, but may neither enter nor leave one.
864-- Checking the isolated prefix also refuses skipping an end and a different
865-- begin, which comparing only the source and target nesting depth would miss.
866def nativePhysicalBranchWindowValid =
867 (lambda unrestricted count : (family ModelWord64) .
868 (lambda unrestricted rest : (family NativePhysicalCommands) .
869 (let unrestricted prefix =
870 (nativePhysicalCommandsTake rest (modelWord64Natural count))
871 in
872 (naturalAnd
873 (naturalEqual (nativePhysicalCommandsLength prefix) (modelWord64Natural count))
874 (naturalEqual (nativePhysicalRepeatBalance prefix) 0)))))
875
876def nativePhysicalValidateOperation =
877 (lambda unrestricted rest : (family NativePhysicalCommands) .
878 (lambda unrestricted operation : (family NativePhysicalOperation) .
879 (eliminate
880 NativePhysicalOperation
881 (lambda unrestricted current : (family NativePhysicalOperation) .
882 (family NativePhysicalOperationValidation))
883 operation
884 (branch
885 NativePhysicalSystemCall
886 number
887 arguments
888 payload
889 result
890 .
891 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
892 (branch
893 NativePhysicalCopyPayloadToState
894 destination
895 extent
896 payload
897 .
898 (eliminate
899 NativePhysicalOperationValidation
900 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
901 (family NativePhysicalOperationValidation))
902 (nativePhysicalRequireBytes
903 payload
904 (constructor NativePhysicalErrorCode NativePhysicalCopyPayloadEmpty))
905 (branch
906 NativePhysicalOperationValid
907 .
908 (nat-eliminate
909 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
910 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
911 (lambda unrestricted predecessor : Nat .
912 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
913 (constructor
914 NativePhysicalOperationValidation
915 NativePhysicalOperationInvalid
916 (constructor NativePhysicalErrorCode NativePhysicalCopyExtentZero))))
917 (modelWord64IsZero extent)))
918 (branch
919 NativePhysicalOperationInvalid
920 error
921 .
922 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
923 (branch
924 NativePhysicalMachineRoutine
925 code
926 arguments
927 result
928 .
929 (nativePhysicalRequireBytes
930 code
931 (constructor NativePhysicalErrorCode NativePhysicalMachineCodeEmpty)))
932 (branch
933 NativePhysicalFencePoll
934 address
935 expected
936 maximumPolls
937 .
938 (nat-eliminate
939 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
940 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
941 (lambda unrestricted predecessor : Nat .
942 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
943 (constructor
944 NativePhysicalOperationValidation
945 NativePhysicalOperationInvalid
946 (constructor NativePhysicalErrorCode NativePhysicalFencePollCountZero))))
947 (modelWord64IsZero maximumPolls)))
948 (branch
949 NativePhysicalTelemetryAppend
950 path
951 record
952 .
953 (eliminate
954 NativePhysicalOperationValidation
955 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
956 (family NativePhysicalOperationValidation))
957 (nativePhysicalRequireBytes
958 path
959 (constructor NativePhysicalErrorCode NativePhysicalTelemetryPathEmpty))
960 (branch
961 NativePhysicalOperationValid
962 .
963 (nativePhysicalRequireBytes
964 record
965 (constructor NativePhysicalErrorCode NativePhysicalTelemetryRecordEmpty)))
966 (branch
967 NativePhysicalOperationInvalid
968 error
969 .
970 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
971 (branch
972 NativePhysicalAssertEqual
973 left
974 right
975 error
976 .
977 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
978 (branch
979 NativePhysicalAssertOneOf
980 observed
981 first
982 second
983 error
984 .
985 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
986 (branch
987 NativePhysicalHaltSuccess
988 .
989 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
990 (branch
991 NativePhysicalRepeatBegin
992 count
993 .
994 (nat-eliminate
995 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
996 (constructor
997 NativePhysicalOperationValidation
998 NativePhysicalOperationInvalid
999 (constructor NativePhysicalErrorCode NativePhysicalRepeatCountZero))
1000 (lambda unrestricted predecessor : Nat .
1001 (lambda unrestricted induction : (family NativePhysicalOperationValidation) .
1002 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1003 (naturalIsZero (modelWord64IsZero count))))
1004 (branch
1005 NativePhysicalSkipUnlessEqual
1006 left
1007 right
1008 count
1009 .
1010 (nat-eliminate
1011 (lambda unrestricted valid : Nat . (family NativePhysicalOperationValidation))
1012 (constructor
1013 NativePhysicalOperationValidation
1014 NativePhysicalOperationInvalid
1015 (constructor NativePhysicalErrorCode NativePhysicalBranchTargetInvalid))
1016 (lambda unrestricted previous : Nat .
1017 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1018 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1019 (nativePhysicalBranchWindowValid count rest)))
1020 (branch
1021 NativePhysicalRepeatEnd
1022 .
1023 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1024 (branch
1025 NativePhysicalRepeatEndWhen
1026 observed
1027 expected
1028 .
1029 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1030 (branch
1031 NativePhysicalStoreWord64
1032 destination
1033 value
1034 .
1035 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1036 (branch
1037 NativePhysicalFenceWait
1038 address
1039 expected
1040 maximumPolls
1041 interval
1042 .
1043 (nat-eliminate
1044 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1045 (nat-eliminate
1046 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1047 (constructor
1048 NativePhysicalOperationValidation
1049 NativePhysicalOperationInvalid
1050 (constructor NativePhysicalErrorCode NativePhysicalFenceWaitIntervalInvalid))
1051 (lambda unrestricted predecessor : Nat .
1052 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1053 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1054 (nativePhysicalFenceWaitIntervalValid interval))
1055 (lambda unrestricted predecessor : Nat .
1056 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1057 (constructor
1058 NativePhysicalOperationValidation
1059 NativePhysicalOperationInvalid
1060 (constructor NativePhysicalErrorCode NativePhysicalFenceWaitCountZero))))
1061 (modelWord64IsZero maximumPolls)))
1062 (branch
1063 NativePhysicalRepeatBeginCounted
1064 count
1065 .
1066 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1067 (branch
1068 NativePhysicalAddWord64
1069 destination
1070 left
1071 right
1072 .
1073 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1074 (branch
1075 NativePhysicalFloat64
1076 operation
1077 destination
1078 left
1079 right
1080 .
1081 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))))
1082
1083def nativePhysicalValidateCommands =
1084 (lambda unrestricted commands : (family NativePhysicalCommands) .
1085 (eliminate
1086 NativePhysicalCommands
1087 (lambda unrestricted current : (family NativePhysicalCommands) .
1088 (family NativePhysicalCommandsValidation))
1089 commands
1090 (branch
1091 NativePhysicalCommandsEnd
1092 .
1093 (constructor NativePhysicalCommandsValidation NativePhysicalCommandsValid zero))
1094 (branch
1095 NativePhysicalCommandsNext
1096 head
1097 tail
1098 induction
1099 .
1100 (eliminate
1101 NativePhysicalCommand
1102 (lambda unrestricted current : (family NativePhysicalCommand) .
1103 (family NativePhysicalCommandsValidation))
1104 head
1105 (branch
1106 NativePhysicalCommandValue
1107 operation
1108 errorIdentity
1109 .
1110 (eliminate
1111 NativePhysicalOperationValidation
1112 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
1113 (family NativePhysicalCommandsValidation))
1114 (nativePhysicalValidateOperation tail operation)
1115 (branch
1116 NativePhysicalOperationValid
1117 .
1118 (eliminate
1119 NativePhysicalCommandsValidation
1120 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
1121 (family NativePhysicalCommandsValidation))
1122 induction
1123 (branch
1124 NativePhysicalCommandsValid
1125 completed
1126 .
1127 (constructor
1128 NativePhysicalCommandsValidation
1129 NativePhysicalCommandsValid
1130 (succ completed)))
1131 (branch
1132 NativePhysicalCommandsInvalid
1133 error
1134 ordinal
1135 .
1136 (constructor
1137 NativePhysicalCommandsValidation
1138 NativePhysicalCommandsInvalid
1139 error
1140 (succ ordinal)))))
1141 (branch
1142 NativePhysicalOperationInvalid
1143 error
1144 .
1145 (constructor
1146 NativePhysicalCommandsValidation
1147 NativePhysicalCommandsInvalid
1148 error
1149 zero))))))))
1150
1151def nativePhysicalValidationTelemetryFor =
1152 (lambda unrestricted program : (family NativePhysicalProgram) .
1153 (lambda unrestricted failures : Nat .
1154 (lambda unrestricted ordinal : Nat .
1155 (lambda unrestricted code : Bytes .
1156 (eliminate
1157 NativePhysicalProgram
1158 (lambda unrestricted current : (family NativePhysicalProgram) .
1159 (family NativePhysicalValidationTelemetry))
1160 program
1161 (branch
1162 NativePhysicalProgramValue
1163 stateExtent
1164 resultSlots
1165 commands
1166 expected
1167 identity
1168 fallbacks
1169 .
1170 (constructor
1171 NativePhysicalValidationTelemetry
1172 NativePhysicalValidationTelemetryValue
1173 (nativePhysicalCommandsCounts commands)
1174 expected
1175 stateExtent
1176 resultSlots
1177 fallbacks
1178 identity
1179 failures
1180 ordinal
1181 code)))))))
1182
1183def nativePhysicalReject =
1184 (lambda unrestricted program : (family NativePhysicalProgram) .
1185 (lambda unrestricted error : (family NativePhysicalErrorCode) .
1186 (lambda unrestricted ordinal : Nat .
1187 (constructor
1188 NativePhysicalProgramValidation
1189 NativePhysicalProgramRejected
1190 error
1191 (nativePhysicalValidationTelemetryFor
1192 program
1193 (succ zero)
1194 ordinal
1195 (nativePhysicalErrorCodeBytes error))))))
1196
1197def nativePhysicalValidateProgram =
1198 (lambda unrestricted program : (family NativePhysicalProgram) .
1199 (eliminate
1200 NativePhysicalProgram
1201 (lambda unrestricted current : (family NativePhysicalProgram) .
1202 (family NativePhysicalProgramValidation))
1203 program
1204 (branch
1205 NativePhysicalProgramValue
1206 stateExtent
1207 resultSlots
1208 commands
1209 expected
1210 identity
1211 fallbacks
1212 .
1213 (nat-eliminate
1214 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1215 (nativePhysicalReject
1216 program
1217 (constructor NativePhysicalErrorCode NativePhysicalIdentityInvalid)
1218 zero)
1219 (lambda unrestricted identityPredecessor : Nat .
1220 (lambda unrestricted ignoredIdentity : (family NativePhysicalProgramValidation) .
1221 (nat-eliminate
1222 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1223 (nativePhysicalReject
1224 program
1225 (constructor NativePhysicalErrorCode NativePhysicalFallbackObserved)
1226 zero)
1227 (lambda unrestricted fallbackPredecessor : Nat .
1228 (lambda unrestricted ignoredFallback : (family NativePhysicalProgramValidation) .
1229 (nat-eliminate
1230 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1231 (eliminate
1232 NativePhysicalCommandsValidation
1233 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
1234 (family NativePhysicalProgramValidation))
1235 (nat-eliminate
1236 (lambda unrestricted current : Nat .
1237 (family NativePhysicalCommandsValidation))
1238 (nativePhysicalValidateCommands commands)
1239 (lambda unrestricted predecessor : Nat .
1240 (lambda unrestricted ignoredBalance : (family NativePhysicalCommandsValidation) .
1241 (constructor
1242 NativePhysicalCommandsValidation
1243 NativePhysicalCommandsInvalid
1244 (constructor NativePhysicalErrorCode NativePhysicalRepeatUnbalanced)
1245 zero)))
1246 (nativePhysicalRepeatBalance commands))
1247 (branch
1248 NativePhysicalCommandsValid
1249 completed
1250 .
1251 (nat-eliminate
1252 (lambda unrestricted current : Nat .
1253 (family NativePhysicalProgramValidation))
1254 (nativePhysicalReject
1255 program
1256 (constructor
1257 NativePhysicalErrorCode
1258 NativePhysicalCommandCountMismatch)
1259 zero)
1260 (lambda unrestricted countPredecessor : Nat .
1261 (lambda unrestricted ignoredCount : (family NativePhysicalProgramValidation) .
1262 (nat-eliminate
1263 (lambda unrestricted valid : Nat .
1264 (family NativePhysicalProgramValidation))
1265 (nativePhysicalReject
1266 program
1267 (constructor
1268 NativePhysicalErrorCode
1269 NativePhysicalMemoryExtentInvalid)
1270 zero)
1271 (lambda unrestricted previous : Nat .
1272 (lambda unrestricted ignored : (family NativePhysicalProgramValidation) .
1273 (constructor
1274 NativePhysicalProgramValidation
1275 NativePhysicalProgramValidated
1276 program
1277 (nativePhysicalValidationTelemetryFor program zero zero b""))))
1278 (nativePhysicalMemoryAdmitted
1279 (modelWord64Natural stateExtent)
1280 (modelWord64Natural resultSlots)))))
1281 (naturalEqual completed expected)))
1282 (branch
1283 NativePhysicalCommandsInvalid
1284 error
1285 ordinal
1286 .
1287 (nativePhysicalReject program error ordinal)))
1288 (lambda unrestricted statePredecessor : Nat .
1289 (lambda unrestricted ignoredState : (family NativePhysicalProgramValidation) .
1290 (nativePhysicalReject
1291 program
1292 (constructor NativePhysicalErrorCode NativePhysicalStateExtentZero)
1293 zero)))
1294 (modelWord64IsZero stateExtent))))
1295 (naturalEqual fallbacks zero))))
1296 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))))
1297
1298-- Derive the record count from the command spine without evaluating payloads
1299-- or machine routines. Inspection of other counts remains a separate operation.
1300def nativePhysicalProgramFromCommands =
1301 (lambda unrestricted identity : Bytes .
1302 (lambda unrestricted extent : Nat .
1303 (lambda unrestricted slots : Nat .
1304 (lambda unrestricted commands : (family NativePhysicalCommands) .
1305 (constructor
1306 NativePhysicalProgram
1307 NativePhysicalProgramValue
1308 (modelWord64FromNaturalTruncated extent)
1309 (modelWord64FromNaturalTruncated slots)
1310 commands
1311 (nativePhysicalCommandsLength commands)
1312 identity
1313 0)))))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.