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 through the matching RepeatEnd count times. Nested repeats have
135-- private frames; loop-affine operands read the innermost active iteration.
136-- A target without that realization must refuse nested programs at lowering.
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-- Repeat classification is shared by balance and exact frame-depth derivation.
703def nativePhysicalRepeatAction =
704 (lambda unrestricted operation : (family NativePhysicalOperation) .
705 (eliminate
706 NativePhysicalOperation
707 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
708 operation
709 (branch NativePhysicalSystemCall number arguments payload result . 0)
710 (branch NativePhysicalCopyPayloadToState destination extent payload . 0)
711 (branch NativePhysicalMachineRoutine code arguments result . 0)
712 (branch NativePhysicalFencePoll address expected polls . 0)
713 (branch NativePhysicalTelemetryAppend path record . 0)
714 (branch NativePhysicalAssertEqual left right error . 0)
715 (branch NativePhysicalAssertOneOf observed first second error . 0)
716 (branch NativePhysicalHaltSuccess . 0)
717 (branch NativePhysicalRepeatBegin count . 1)
718 (branch NativePhysicalSkipUnlessEqual left right count . 0)
719 (branch NativePhysicalRepeatEnd . 2)
720 (branch NativePhysicalRepeatEndWhen observed expected . 2)
721 (branch NativePhysicalStoreWord64 destination value . 0)
722 (branch NativePhysicalFenceWait address expected polls interval . 0)
723 (branch NativePhysicalRepeatBeginCounted count . 1)
724 (branch NativePhysicalAddWord64 destination left right . 0)
725 (branch NativePhysicalFloat64 operation destination left right . 0)))
726
727-- Zero is balanced; nonzero means an unmatched end or an open frame.
728def nativePhysicalRepeatBalance =
729 (lambda unrestricted commands : (family NativePhysicalCommands) .
730 (app
731 (eliminate
732 NativePhysicalCommands
733 (lambda unrestricted current : (family NativePhysicalCommands) .
734 (pi unrestricted open : Nat . Nat))
735 commands
736 (branch NativePhysicalCommandsEnd . (lambda unrestricted open : Nat . open))
737 (branch
738 NativePhysicalCommandsNext
739 head
740 tail
741 induction
742 .
743 (lambda unrestricted open : Nat .
744 (eliminate
745 NativePhysicalCommand
746 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
747 head
748 (branch
749 NativePhysicalCommandValue
750 operation
751 errorIdentity
752 .
753 (eliminate
754 NativePhysicalOperation
755 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
756 operation
757 (branch
758 NativePhysicalSystemCall
759 number
760 arguments
761 payload
762 result
763 .
764 (induction open))
765 (branch
766 NativePhysicalCopyPayloadToState
767 destination
768 extent
769 payload
770 .
771 (induction open))
772 (branch NativePhysicalMachineRoutine code arguments result . (induction open))
773 (branch NativePhysicalFencePoll address expected polls . (induction open))
774 (branch NativePhysicalTelemetryAppend path record . (induction open))
775 (branch NativePhysicalAssertEqual left right error . (induction open))
776 (branch NativePhysicalAssertOneOf observed first second error . (induction open))
777 (branch NativePhysicalHaltSuccess . (induction open))
778 (branch NativePhysicalRepeatBegin count . (induction (succ open)))
779 (branch NativePhysicalSkipUnlessEqual left right count . (induction open))
780 (branch
781 NativePhysicalRepeatEnd
782 .
783 (nat-eliminate
784 (lambda unrestricted count : Nat . Nat)
785 2
786 (lambda unrestricted predecessor : Nat .
787 (lambda unrestricted ignored : Nat . (induction predecessor)))
788 open))
789 (branch
790 NativePhysicalRepeatEndWhen
791 observed
792 expected
793 .
794 (nat-eliminate
795 (lambda unrestricted count : Nat . Nat)
796 2
797 (lambda unrestricted predecessor : Nat .
798 (lambda unrestricted ignored : Nat . (induction predecessor)))
799 open))
800 (branch NativePhysicalStoreWord64 destination value . (induction open))
801 (branch
802 NativePhysicalFenceWait
803 address
804 expected
805 polls
806 interval
807 .
808 (induction open))
809 (branch NativePhysicalRepeatBeginCounted count . (induction (succ open)))
810 (branch NativePhysicalAddWord64 destination left right . (induction open))
811 (branch NativePhysicalFloat64 operation destination left right . (induction open))))))))
812 0))
813
814def nativePhysicalRepeatMaximumDepth =
815 (lambda unrestricted commands : (family NativePhysicalCommands) .
816 (app
817 (eliminate
818 NativePhysicalCommands
819 (lambda unrestricted current : (family NativePhysicalCommands) .
820 (pi unrestricted open : Nat . (pi unrestricted highest : Nat . Nat)))
821 commands
822 (branch
823 NativePhysicalCommandsEnd
824 .
825 (lambda unrestricted open : Nat . (lambda unrestricted highest : Nat . highest)))
826 (branch
827 NativePhysicalCommandsNext
828 head
829 tail
830 induction
831 .
832 (lambda unrestricted open : Nat .
833 (lambda unrestricted highest : Nat .
834 (eliminate
835 NativePhysicalCommand
836 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
837 head
838 (branch
839 NativePhysicalCommandValue
840 operation
841 identity
842 .
843 (let unrestricted action =
844 (nativePhysicalRepeatAction operation)
845 in
846 (let unrestricted next =
847 (naturalSelect
848 (naturalEqual action 1)
849 (succ open)
850 (naturalSaturatingSubtract open (naturalSelect (naturalEqual action 2) 1 0)))
851 in
852 (induction
853 next
854 (naturalSelect (naturalLessOrEqual highest next) next highest))))))))))
855 0
856 0))
857
858-- Only consulted after maximum-depth admission has failed. Report the first
859-- begin that would exceed the target's frame bound, in original command order.
860def nativePhysicalRepeatFirstExcess =
861 (lambda unrestricted commands : (family NativePhysicalCommands) .
862 (lambda unrestricted bound : Nat .
863 (app
864 (eliminate
865 NativePhysicalCommands
866 (lambda unrestricted current : (family NativePhysicalCommands) .
867 (pi unrestricted open : Nat . (pi unrestricted ordinal : Nat . Nat)))
868 commands
869 (branch
870 NativePhysicalCommandsEnd
871 .
872 (lambda unrestricted open : Nat . (lambda unrestricted ordinal : Nat . ordinal)))
873 (branch
874 NativePhysicalCommandsNext
875 head
876 tail
877 induction
878 .
879 (lambda unrestricted open : Nat .
880 (lambda unrestricted ordinal : Nat .
881 (eliminate
882 NativePhysicalCommand
883 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
884 head
885 (branch
886 NativePhysicalCommandValue
887 operation
888 identity
889 .
890 (let unrestricted action =
891 (nativePhysicalRepeatAction operation)
892 in
893 (naturalSelect
894 (naturalAnd (naturalEqual action 1) (naturalLessOrEqual bound open))
895 ordinal
896 (induction
897 (naturalSelect
898 (naturalEqual action 1)
899 (succ open)
900 (naturalSaturatingSubtract
901 open
902 (naturalSelect (naturalEqual action 2) 1 0)))
903 (succ ordinal))))))))))
904 0
905 0)))
906
907def nativePhysicalProgramRepeatDepth =
908 (lambda unrestricted program : (family NativePhysicalProgram) .
909 (eliminate
910 NativePhysicalProgram
911 (lambda unrestricted current : (family NativePhysicalProgram) . Nat)
912 program
913 (branch
914 NativePhysicalProgramValue
915 extent
916 slots
917 commands
918 count
919 identity
920 fallbacks
921 .
922 (nativePhysicalRepeatMaximumDepth commands))))
923
924def nativePhysicalProgramRepeatBalance =
925 (lambda unrestricted program : (family NativePhysicalProgram) .
926 (eliminate
927 NativePhysicalProgram
928 (lambda unrestricted current : (family NativePhysicalProgram) . Nat)
929 program
930 (branch
931 NativePhysicalProgramValue
932 extent
933 slots
934 commands
935 count
936 identity
937 fallbacks
938 .
939 (nativePhysicalRepeatBalance commands))))
940
941-- The repeat-frame scratch layout (nativePhysicalRepeatScratchBytes and its
942-- offsets) is part of the interpreter memory ABI in Runtime.NativePhysicalMemory,
943-- so admission, reservations and both interpreters share one calculation.
944
945-- The x86 realization adds this extent with a signed 32-bit immediate.
946-- Reject before truncating that encoding; the bound is an ISA field limit,
947-- not a guessed stack capacity or a resource promise about a particular host.
948def nativePhysicalRepeatExtentAdmission =
949 (lambda unrestricted depth : Nat .
950 (naturalLessOrEqual (nativePhysicalRepeatScratchBytes depth) 2147483647))
951
952def nativePhysicalCommandsLength =
953 (lambda unrestricted commands : (family NativePhysicalCommands) .
954 (eliminate
955 NativePhysicalCommands
956 (lambda unrestricted current : (family NativePhysicalCommands) . Nat)
957 commands
958 (branch NativePhysicalCommandsEnd . 0)
959 (branch NativePhysicalCommandsNext command rest induction . (succ induction))))
960
961-- Arena/slot admission belongs to the caller's checked plan. The program owns
962-- its command count and declares no fallback; native encoding still validates
963-- the exact identity width, nonempty program and reachable command contracts.
964def nativePhysicalCommandsTake =
965 (lambda unrestricted commands : (family NativePhysicalCommands) .
966 (eliminate
967 NativePhysicalCommands
968 (lambda unrestricted current : (family NativePhysicalCommands) .
969 (pi unrestricted count : Nat . (family NativePhysicalCommands)))
970 commands
971 (branch
972 NativePhysicalCommandsEnd
973 .
974 (lambda unrestricted count : Nat .
975 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))
976 (branch
977 NativePhysicalCommandsNext
978 head
979 tail
980 induction
981 .
982 (lambda unrestricted count : Nat .
983 (nat-eliminate
984 (lambda unrestricted remaining : Nat . (family NativePhysicalCommands))
985 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
986 (lambda unrestricted previous : Nat .
987 (lambda unrestricted ignored : (family NativePhysicalCommands) .
988 (constructor
989 NativePhysicalCommands
990 NativePhysicalCommandsNext
991 head
992 (induction previous))))
993 count)))))
994
995-- A jump may skip a complete loop, but may neither enter nor leave one.
996-- Checking the isolated prefix also refuses skipping an end and a different
997-- begin, which comparing only the source and target nesting depth would miss.
998def nativePhysicalBranchWindowValid =
999 (lambda unrestricted count : (family ModelWord64) .
1000 (lambda unrestricted rest : (family NativePhysicalCommands) .
1001 (let unrestricted prefix =
1002 (nativePhysicalCommandsTake rest (modelWord64Natural count))
1003 in
1004 (naturalAnd
1005 (naturalEqual (nativePhysicalCommandsLength prefix) (modelWord64Natural count))
1006 (naturalEqual (nativePhysicalRepeatBalance prefix) 0)))))
1007
1008def nativePhysicalValidateOperation =
1009 (lambda unrestricted rest : (family NativePhysicalCommands) .
1010 (lambda unrestricted operation : (family NativePhysicalOperation) .
1011 (eliminate
1012 NativePhysicalOperation
1013 (lambda unrestricted current : (family NativePhysicalOperation) .
1014 (family NativePhysicalOperationValidation))
1015 operation
1016 (branch
1017 NativePhysicalSystemCall
1018 number
1019 arguments
1020 payload
1021 result
1022 .
1023 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1024 (branch
1025 NativePhysicalCopyPayloadToState
1026 destination
1027 extent
1028 payload
1029 .
1030 (eliminate
1031 NativePhysicalOperationValidation
1032 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
1033 (family NativePhysicalOperationValidation))
1034 (nativePhysicalRequireBytes
1035 payload
1036 (constructor NativePhysicalErrorCode NativePhysicalCopyPayloadEmpty))
1037 (branch
1038 NativePhysicalOperationValid
1039 .
1040 (nat-eliminate
1041 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1042 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
1043 (lambda unrestricted predecessor : Nat .
1044 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1045 (constructor
1046 NativePhysicalOperationValidation
1047 NativePhysicalOperationInvalid
1048 (constructor NativePhysicalErrorCode NativePhysicalCopyExtentZero))))
1049 (modelWord64IsZero extent)))
1050 (branch
1051 NativePhysicalOperationInvalid
1052 error
1053 .
1054 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
1055 (branch
1056 NativePhysicalMachineRoutine
1057 code
1058 arguments
1059 result
1060 .
1061 (nativePhysicalRequireBytes
1062 code
1063 (constructor NativePhysicalErrorCode NativePhysicalMachineCodeEmpty)))
1064 (branch
1065 NativePhysicalFencePoll
1066 address
1067 expected
1068 maximumPolls
1069 .
1070 (nat-eliminate
1071 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1072 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)
1073 (lambda unrestricted predecessor : Nat .
1074 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1075 (constructor
1076 NativePhysicalOperationValidation
1077 NativePhysicalOperationInvalid
1078 (constructor NativePhysicalErrorCode NativePhysicalFencePollCountZero))))
1079 (modelWord64IsZero maximumPolls)))
1080 (branch
1081 NativePhysicalTelemetryAppend
1082 path
1083 record
1084 .
1085 (eliminate
1086 NativePhysicalOperationValidation
1087 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
1088 (family NativePhysicalOperationValidation))
1089 (nativePhysicalRequireBytes
1090 path
1091 (constructor NativePhysicalErrorCode NativePhysicalTelemetryPathEmpty))
1092 (branch
1093 NativePhysicalOperationValid
1094 .
1095 (nativePhysicalRequireBytes
1096 record
1097 (constructor NativePhysicalErrorCode NativePhysicalTelemetryRecordEmpty)))
1098 (branch
1099 NativePhysicalOperationInvalid
1100 error
1101 .
1102 (constructor NativePhysicalOperationValidation NativePhysicalOperationInvalid error))))
1103 (branch
1104 NativePhysicalAssertEqual
1105 left
1106 right
1107 error
1108 .
1109 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1110 (branch
1111 NativePhysicalAssertOneOf
1112 observed
1113 first
1114 second
1115 error
1116 .
1117 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1118 (branch
1119 NativePhysicalHaltSuccess
1120 .
1121 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1122 (branch
1123 NativePhysicalRepeatBegin
1124 count
1125 .
1126 (nat-eliminate
1127 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1128 (constructor
1129 NativePhysicalOperationValidation
1130 NativePhysicalOperationInvalid
1131 (constructor NativePhysicalErrorCode NativePhysicalRepeatCountZero))
1132 (lambda unrestricted predecessor : Nat .
1133 (lambda unrestricted induction : (family NativePhysicalOperationValidation) .
1134 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1135 (naturalIsZero (modelWord64IsZero count))))
1136 (branch
1137 NativePhysicalSkipUnlessEqual
1138 left
1139 right
1140 count
1141 .
1142 (nat-eliminate
1143 (lambda unrestricted valid : Nat . (family NativePhysicalOperationValidation))
1144 (constructor
1145 NativePhysicalOperationValidation
1146 NativePhysicalOperationInvalid
1147 (constructor NativePhysicalErrorCode NativePhysicalBranchTargetInvalid))
1148 (lambda unrestricted previous : Nat .
1149 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1150 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1151 (nativePhysicalBranchWindowValid count rest)))
1152 (branch
1153 NativePhysicalRepeatEnd
1154 .
1155 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1156 (branch
1157 NativePhysicalRepeatEndWhen
1158 observed
1159 expected
1160 .
1161 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1162 (branch
1163 NativePhysicalStoreWord64
1164 destination
1165 value
1166 .
1167 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1168 (branch
1169 NativePhysicalFenceWait
1170 address
1171 expected
1172 maximumPolls
1173 interval
1174 .
1175 (nat-eliminate
1176 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1177 (nat-eliminate
1178 (lambda unrestricted current : Nat . (family NativePhysicalOperationValidation))
1179 (constructor
1180 NativePhysicalOperationValidation
1181 NativePhysicalOperationInvalid
1182 (constructor NativePhysicalErrorCode NativePhysicalFenceWaitIntervalInvalid))
1183 (lambda unrestricted predecessor : Nat .
1184 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1185 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))
1186 (nativePhysicalFenceWaitIntervalValid interval))
1187 (lambda unrestricted predecessor : Nat .
1188 (lambda unrestricted ignored : (family NativePhysicalOperationValidation) .
1189 (constructor
1190 NativePhysicalOperationValidation
1191 NativePhysicalOperationInvalid
1192 (constructor NativePhysicalErrorCode NativePhysicalFenceWaitCountZero))))
1193 (modelWord64IsZero maximumPolls)))
1194 (branch
1195 NativePhysicalRepeatBeginCounted
1196 count
1197 .
1198 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1199 (branch
1200 NativePhysicalAddWord64
1201 destination
1202 left
1203 right
1204 .
1205 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid))
1206 (branch
1207 NativePhysicalFloat64
1208 operation
1209 destination
1210 left
1211 right
1212 .
1213 (constructor NativePhysicalOperationValidation NativePhysicalOperationValid)))))
1214
1215def nativePhysicalValidateCommands =
1216 (lambda unrestricted commands : (family NativePhysicalCommands) .
1217 (eliminate
1218 NativePhysicalCommands
1219 (lambda unrestricted current : (family NativePhysicalCommands) .
1220 (family NativePhysicalCommandsValidation))
1221 commands
1222 (branch
1223 NativePhysicalCommandsEnd
1224 .
1225 (constructor NativePhysicalCommandsValidation NativePhysicalCommandsValid zero))
1226 (branch
1227 NativePhysicalCommandsNext
1228 head
1229 tail
1230 induction
1231 .
1232 (eliminate
1233 NativePhysicalCommand
1234 (lambda unrestricted current : (family NativePhysicalCommand) .
1235 (family NativePhysicalCommandsValidation))
1236 head
1237 (branch
1238 NativePhysicalCommandValue
1239 operation
1240 errorIdentity
1241 .
1242 (eliminate
1243 NativePhysicalOperationValidation
1244 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
1245 (family NativePhysicalCommandsValidation))
1246 (nativePhysicalValidateOperation tail operation)
1247 (branch
1248 NativePhysicalOperationValid
1249 .
1250 (eliminate
1251 NativePhysicalCommandsValidation
1252 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
1253 (family NativePhysicalCommandsValidation))
1254 induction
1255 (branch
1256 NativePhysicalCommandsValid
1257 completed
1258 .
1259 (constructor
1260 NativePhysicalCommandsValidation
1261 NativePhysicalCommandsValid
1262 (succ completed)))
1263 (branch
1264 NativePhysicalCommandsInvalid
1265 error
1266 ordinal
1267 .
1268 (constructor
1269 NativePhysicalCommandsValidation
1270 NativePhysicalCommandsInvalid
1271 error
1272 (succ ordinal)))))
1273 (branch
1274 NativePhysicalOperationInvalid
1275 error
1276 .
1277 (constructor
1278 NativePhysicalCommandsValidation
1279 NativePhysicalCommandsInvalid
1280 error
1281 zero))))))))
1282
1283def nativePhysicalValidationTelemetryFor =
1284 (lambda unrestricted program : (family NativePhysicalProgram) .
1285 (lambda unrestricted failures : Nat .
1286 (lambda unrestricted ordinal : Nat .
1287 (lambda unrestricted code : Bytes .
1288 (eliminate
1289 NativePhysicalProgram
1290 (lambda unrestricted current : (family NativePhysicalProgram) .
1291 (family NativePhysicalValidationTelemetry))
1292 program
1293 (branch
1294 NativePhysicalProgramValue
1295 stateExtent
1296 resultSlots
1297 commands
1298 expected
1299 identity
1300 fallbacks
1301 .
1302 (constructor
1303 NativePhysicalValidationTelemetry
1304 NativePhysicalValidationTelemetryValue
1305 (nativePhysicalCommandsCounts commands)
1306 expected
1307 stateExtent
1308 resultSlots
1309 fallbacks
1310 identity
1311 failures
1312 ordinal
1313 code)))))))
1314
1315def nativePhysicalReject =
1316 (lambda unrestricted program : (family NativePhysicalProgram) .
1317 (lambda unrestricted error : (family NativePhysicalErrorCode) .
1318 (lambda unrestricted ordinal : Nat .
1319 (constructor
1320 NativePhysicalProgramValidation
1321 NativePhysicalProgramRejected
1322 error
1323 (nativePhysicalValidationTelemetryFor
1324 program
1325 (succ zero)
1326 ordinal
1327 (nativePhysicalErrorCodeBytes error))))))
1328
1329def nativePhysicalValidateProgram =
1330 (lambda unrestricted program : (family NativePhysicalProgram) .
1331 (eliminate
1332 NativePhysicalProgram
1333 (lambda unrestricted current : (family NativePhysicalProgram) .
1334 (family NativePhysicalProgramValidation))
1335 program
1336 (branch
1337 NativePhysicalProgramValue
1338 stateExtent
1339 resultSlots
1340 commands
1341 expected
1342 identity
1343 fallbacks
1344 .
1345 (nat-eliminate
1346 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1347 (nativePhysicalReject
1348 program
1349 (constructor NativePhysicalErrorCode NativePhysicalIdentityInvalid)
1350 zero)
1351 (lambda unrestricted identityPredecessor : Nat .
1352 (lambda unrestricted ignoredIdentity : (family NativePhysicalProgramValidation) .
1353 (nat-eliminate
1354 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1355 (nativePhysicalReject
1356 program
1357 (constructor NativePhysicalErrorCode NativePhysicalFallbackObserved)
1358 zero)
1359 (lambda unrestricted fallbackPredecessor : Nat .
1360 (lambda unrestricted ignoredFallback : (family NativePhysicalProgramValidation) .
1361 (nat-eliminate
1362 (lambda unrestricted current : Nat . (family NativePhysicalProgramValidation))
1363 (eliminate
1364 NativePhysicalCommandsValidation
1365 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
1366 (family NativePhysicalProgramValidation))
1367 (nat-eliminate
1368 (lambda unrestricted current : Nat .
1369 (family NativePhysicalCommandsValidation))
1370 (nativePhysicalValidateCommands commands)
1371 (lambda unrestricted predecessor : Nat .
1372 (lambda unrestricted ignoredBalance : (family NativePhysicalCommandsValidation) .
1373 (constructor
1374 NativePhysicalCommandsValidation
1375 NativePhysicalCommandsInvalid
1376 (constructor NativePhysicalErrorCode NativePhysicalRepeatUnbalanced)
1377 zero)))
1378 (nativePhysicalRepeatBalance commands))
1379 (branch
1380 NativePhysicalCommandsValid
1381 completed
1382 .
1383 (nat-eliminate
1384 (lambda unrestricted current : Nat .
1385 (family NativePhysicalProgramValidation))
1386 (nativePhysicalReject
1387 program
1388 (constructor
1389 NativePhysicalErrorCode
1390 NativePhysicalCommandCountMismatch)
1391 zero)
1392 (lambda unrestricted countPredecessor : Nat .
1393 (lambda unrestricted ignoredCount : (family NativePhysicalProgramValidation) .
1394 (nat-eliminate
1395 (lambda unrestricted valid : Nat .
1396 (family NativePhysicalProgramValidation))
1397 (nativePhysicalReject
1398 program
1399 (constructor
1400 NativePhysicalErrorCode
1401 NativePhysicalMemoryExtentInvalid)
1402 zero)
1403 (lambda unrestricted previous : Nat .
1404 (lambda unrestricted ignored : (family NativePhysicalProgramValidation) .
1405 (constructor
1406 NativePhysicalProgramValidation
1407 NativePhysicalProgramValidated
1408 program
1409 (nativePhysicalValidationTelemetryFor program zero zero b""))))
1410 (nativePhysicalMemoryAdmitted
1411 (modelWord64Natural stateExtent)
1412 (modelWord64Natural resultSlots)
1413 (nativePhysicalRepeatMaximumDepth commands)))))
1414 (naturalEqual completed expected)))
1415 (branch
1416 NativePhysicalCommandsInvalid
1417 error
1418 ordinal
1419 .
1420 (nativePhysicalReject program error ordinal)))
1421 (lambda unrestricted statePredecessor : Nat .
1422 (lambda unrestricted ignoredState : (family NativePhysicalProgramValidation) .
1423 (nativePhysicalReject
1424 program
1425 (constructor NativePhysicalErrorCode NativePhysicalStateExtentZero)
1426 zero)))
1427 (modelWord64IsZero stateExtent))))
1428 (naturalEqual fallbacks zero))))
1429 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))))
1430
1431-- Derive the record count from the command spine without evaluating payloads
1432-- or machine routines. Inspection of other counts remains a separate operation.
1433def nativePhysicalProgramFromCommands =
1434 (lambda unrestricted identity : Bytes .
1435 (lambda unrestricted extent : Nat .
1436 (lambda unrestricted slots : Nat .
1437 (lambda unrestricted commands : (family NativePhysicalCommands) .
1438 (constructor
1439 NativePhysicalProgram
1440 NativePhysicalProgramValue
1441 (modelWord64FromNaturalTruncated extent)
1442 (modelWord64FromNaturalTruncated slots)
1443 commands
1444 (nativePhysicalCommandsLength commands)
1445 identity
1446 0)))))
1447
1448-- The interpreter memory ABI owns the byte width of a complete word.
1449def nativePhysicalWordBytes : Nat =
1450 nativePhysicalMemoryWordBytes
1451
1452-- Direct operand scopes for a program before adding private residents/slots.
1453-- This does not sandbox arbitrary syscall or machine-routine memory effects,
1454-- authenticate result-held pointers, or establish runtime argv availability.
1455-- Extent tests subtract from admitted ranges; hostile u64 offsets never add.
1456def nativePhysicalOperandScopeAdmission =
1457 (lambda unrestricted stateBytes : Nat .
1458 (lambda unrestricted slots : Nat .
1459 (lambda unrestricted payloadBytes : Nat .
1460 (lambda unrestricted operand : (family NativePhysicalOperand) .
1461 (eliminate
1462 NativePhysicalOperand
1463 (lambda unrestricted current : (family NativePhysicalOperand) . Nat)
1464 operand
1465 (branch NativePhysicalImmediate value . 1)
1466 (branch
1467 NativePhysicalResultValue
1468 slot
1469 .
1470 (eliminate
1471 NativePhysicalSlot
1472 (lambda unrestricted current : (family NativePhysicalSlot) . Nat)
1473 slot
1474 (branch
1475 NativePhysicalSlotValue
1476 index
1477 .
1478 (naturalLess (modelWord64Natural index) slots))))
1479 (branch
1480 NativePhysicalResultAddress
1481 slot
1482 offset
1483 .
1484 (eliminate
1485 NativePhysicalSlot
1486 (lambda unrestricted current : (family NativePhysicalSlot) . Nat)
1487 slot
1488 (branch
1489 NativePhysicalSlotValue
1490 index
1491 .
1492 (naturalLess (modelWord64Natural index) slots))))
1493 (branch
1494 NativePhysicalStateAddress
1495 offset
1496 .
1497 (naturalLess (modelWord64Natural offset) stateBytes))
1498 (branch
1499 NativePhysicalStateLoad64
1500 offset
1501 .
1502 (naturalAnd
1503 (naturalLessOrEqual nativePhysicalWordBytes stateBytes)
1504 (naturalLessOrEqual
1505 (modelWord64Natural offset)
1506 (naturalSaturatingSubtract stateBytes nativePhysicalWordBytes))))
1507 (branch
1508 NativePhysicalPayloadAddress
1509 offset
1510 .
1511 (naturalLess (modelWord64Natural offset) payloadBytes))
1512 (branch
1513 NativePhysicalPayloadLoad64
1514 offset
1515 .
1516 (naturalAnd
1517 (naturalLessOrEqual nativePhysicalWordBytes payloadBytes)
1518 (naturalLessOrEqual
1519 (modelWord64Natural offset)
1520 (naturalSaturatingSubtract payloadBytes nativePhysicalWordBytes))))
1521 (branch NativePhysicalProcessArgument index . 1)
1522 (branch NativePhysicalLoopAffine base stride . 1))))))
1523
1524def nativePhysicalArgumentsScopeAdmission =
1525 (lambda unrestricted stateBytes : Nat .
1526 (lambda unrestricted slots : Nat .
1527 (lambda unrestricted payloadBytes : Nat .
1528 (lambda unrestricted arguments : (family NativePhysicalArguments) .
1529 (eliminate
1530 NativePhysicalArguments
1531 (lambda unrestricted current : (family NativePhysicalArguments) . Nat)
1532 arguments
1533 (branch
1534 NativePhysicalArgumentsValue
1535 a0
1536 a1
1537 a2
1538 a3
1539 a4
1540 a5
1541 .
1542 (naturalAnd
1543 (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a0)
1544 (naturalAnd
1545 (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a1)
1546 (naturalAnd
1547 (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a2)
1548 (naturalAnd
1549 (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a3)
1550 (naturalAnd
1551 (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a4)
1552 (naturalAnd
1553 (nativePhysicalOperandScopeAdmission stateBytes slots payloadBytes a5)
1554 1))))))))))))
1555
1556def nativePhysicalResultScopeAdmission =
1557 (lambda unrestricted slots : Nat .
1558 (lambda unrestricted result : (family NativePhysicalResultBinding) .
1559 (eliminate
1560 NativePhysicalResultBinding
1561 (lambda unrestricted current : (family NativePhysicalResultBinding) . Nat)
1562 result
1563 (branch NativePhysicalDiscardResult . 1)
1564 (branch
1565 NativePhysicalStoreResult
1566 slot
1567 .
1568 (eliminate
1569 NativePhysicalSlot
1570 (lambda unrestricted current : (family NativePhysicalSlot) . Nat)
1571 slot
1572 (branch NativePhysicalSlotValue index . (naturalLess (modelWord64Natural index) slots)))))))
1573
1574-- A pointer operand's start may be valid while an eight-byte operation at
1575-- it crosses into the next resident. Check known direct ranges at the use's
1576-- width; indirect/result-held pointers retain their explicit primitive trust.
1577def nativePhysicalAddressSpanAdmission =
1578 (lambda unrestricted stateBytes : Nat .
1579 (lambda unrestricted slots : Nat .
1580 (lambda unrestricted width : Nat .
1581 (lambda unrestricted operand : (family NativePhysicalOperand) .
1582 (eliminate NativePhysicalOperand
1583 (lambda unrestricted current : (family NativePhysicalOperand) . Nat) operand
1584 (branch NativePhysicalImmediate value . 1)
1585 (branch NativePhysicalResultValue slot .
1586 (nativePhysicalOperandScopeAdmission stateBytes slots 0 operand))
1587 (branch NativePhysicalResultAddress slot offset .
1588 (nativePhysicalOperandScopeAdmission stateBytes slots 0 operand))
1589 (branch NativePhysicalStateAddress offset .
1590 (naturalAnd (naturalLessOrEqual width stateBytes)
1591 (naturalLessOrEqual (modelWord64Natural offset)
1592 (naturalSaturatingSubtract stateBytes width))))
1593 (branch NativePhysicalStateLoad64 offset .
1594 (nativePhysicalOperandScopeAdmission stateBytes slots 0 operand))
1595 (branch NativePhysicalPayloadAddress offset . 0)
1596 (branch NativePhysicalPayloadLoad64 offset . 0)
1597 (branch NativePhysicalProcessArgument index . 1)
1598 (branch NativePhysicalLoopAffine base stride . 1))))))
1599
1600def nativePhysicalOperationScopeAdmission =
1601 (lambda unrestricted stateBytes : Nat .
1602 (lambda unrestricted slots : Nat .
1603 (lambda unrestricted operation : (family NativePhysicalOperation) .
1604 (eliminate
1605 NativePhysicalOperation
1606 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
1607 operation
1608 (branch
1609 NativePhysicalSystemCall
1610 number
1611 arguments
1612 payload
1613 result
1614 .
1615 (naturalAnd
1616 (nativePhysicalOperandScopeAdmission stateBytes slots 0 number)
1617 (naturalAnd
1618 (nativePhysicalArgumentsScopeAdmission
1619 stateBytes
1620 slots
1621 (bytes-length payload)
1622 arguments)
1623 (naturalAnd (nativePhysicalResultScopeAdmission slots result) 1))))
1624 (branch
1625 NativePhysicalCopyPayloadToState
1626 destination
1627 extent
1628 payload
1629 .
1630 (naturalAnd
1631 (naturalAnd
1632 (naturalLessOrEqual (modelWord64Natural extent) stateBytes)
1633 (naturalLessOrEqual
1634 (modelWord64Natural destination)
1635 (naturalSaturatingSubtract stateBytes (modelWord64Natural extent))))
1636 (naturalAnd (naturalEqual (modelWord64Natural extent) (bytes-length payload)) 1)))
1637 (branch
1638 NativePhysicalMachineRoutine
1639 code
1640 arguments
1641 result
1642 .
1643 (naturalAnd
1644 (nativePhysicalArgumentsScopeAdmission stateBytes slots (bytes-length code) arguments)
1645 (naturalAnd (nativePhysicalResultScopeAdmission slots result) 1)))
1646 (branch
1647 NativePhysicalFencePoll
1648 address
1649 expected
1650 polls
1651 .
1652 (naturalAnd
1653 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes address)
1654 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 expected) 1)))
1655 (branch NativePhysicalTelemetryAppend path record . 1)
1656 (branch
1657 NativePhysicalAssertEqual
1658 left
1659 right
1660 error
1661 .
1662 (naturalAnd
1663 (nativePhysicalOperandScopeAdmission stateBytes slots 0 left)
1664 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 right) 1)))
1665 (branch
1666 NativePhysicalAssertOneOf
1667 observed
1668 first
1669 second
1670 error
1671 .
1672 (naturalAnd
1673 (nativePhysicalOperandScopeAdmission stateBytes slots 0 observed)
1674 (naturalAnd
1675 (nativePhysicalOperandScopeAdmission stateBytes slots 0 first)
1676 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 second) 1))))
1677 (branch NativePhysicalHaltSuccess . 1)
1678 (branch NativePhysicalRepeatBegin count . 1)
1679 (branch
1680 NativePhysicalSkipUnlessEqual
1681 left
1682 right
1683 count
1684 .
1685 (naturalAnd
1686 (nativePhysicalOperandScopeAdmission stateBytes slots 0 left)
1687 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 right) 1)))
1688 (branch NativePhysicalRepeatEnd . 1)
1689 (branch
1690 NativePhysicalRepeatEndWhen
1691 observed
1692 expected
1693 .
1694 (naturalAnd
1695 (nativePhysicalOperandScopeAdmission stateBytes slots 0 observed)
1696 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 expected) 1)))
1697 (branch
1698 NativePhysicalStoreWord64
1699 destination
1700 value
1701 .
1702 (naturalAnd
1703 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes destination)
1704 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 value) 1)))
1705 (branch
1706 NativePhysicalFenceWait
1707 address
1708 expected
1709 polls
1710 interval
1711 .
1712 (naturalAnd
1713 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes address)
1714 (naturalAnd
1715 (nativePhysicalOperandScopeAdmission stateBytes slots 0 expected)
1716 (naturalAnd
1717 1
1718 (naturalAnd 1 1)))))
1719 (branch
1720 NativePhysicalRepeatBeginCounted
1721 count
1722 .
1723 (nativePhysicalOperandScopeAdmission stateBytes slots 0 count))
1724 (branch
1725 NativePhysicalAddWord64
1726 destination
1727 left
1728 right
1729 .
1730 (naturalAnd
1731 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes destination)
1732 (naturalAnd
1733 (nativePhysicalOperandScopeAdmission stateBytes slots 0 left)
1734 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 right) 1))))
1735 (branch
1736 NativePhysicalFloat64
1737 operation
1738 destination
1739 left
1740 right
1741 .
1742 (naturalAnd
1743 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes destination)
1744 (naturalAnd
1745 (nativePhysicalOperandScopeAdmission stateBytes slots 0 left)
1746 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 right) 1))))))))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.