1module Runtime.NativePhysicalImage
2
3import Data.SHA256Digest
4import Model.Config
5import Model.Parameter
6import Runtime.NativePhysicalProgram
7import Runtime.NativePhysicalImagePlan
8import Runtime.NativeTelemetry
9import Std.List
10import Std.Natural
11
12family NativePhysicalImageErrorCode : Type 0
13constructor NativePhysicalImageProgramRejected
14field unrestricted nativePhysicalImageRejectedProgramError : (family NativePhysicalErrorCode)
15constructor NativePhysicalImageExtentOverflow
16constructor NativePhysicalImageCommandErrorIdentityEmpty
17constructor NativePhysicalImageCommandCountMismatch
18
19end-family
20
21family NativePhysicalImageResultDescriptor : Type 0
22constructor NativePhysicalImageResultDescriptorValue
23field unrestricted nativePhysicalImageResultKind : (family ModelWord64)
24field unrestricted nativePhysicalImageResultSlot : (family ModelWord64)
25
26end-family
27
28family NativePhysicalEncodedCommand : Type 0
29constructor NativePhysicalEncodedCommandValue
30field unrestricted nativePhysicalEncodedCommandBytes : Bytes
31field unrestricted nativePhysicalEncodedCommandPayloadBytes : Nat
32field unrestricted nativePhysicalEncodedCommandAuxiliaryBytes : Nat
33field unrestricted nativePhysicalEncodedCommandErrorBytes : Nat
34
35end-family
36
37family NativePhysicalEncodedCommandResult : Type 0
38constructor NativePhysicalCommandEncoded
39field unrestricted nativePhysicalEncodedCommand : (family NativePhysicalEncodedCommand)
40constructor NativePhysicalCommandEncodingFailed
41field unrestricted nativePhysicalCommandEncodingError : (family NativePhysicalImageErrorCode)
42
43end-family
44
45family NativePhysicalEncodedCommands : Type 0
46constructor NativePhysicalEncodedCommandsValue
47field unrestricted nativePhysicalEncodedCommandsBytes : Bytes
48field unrestricted nativePhysicalEncodedCommandsCount : Nat
49field unrestricted nativePhysicalEncodedCommandsPayloadBytes : Nat
50field unrestricted nativePhysicalEncodedCommandsAuxiliaryBytes : Nat
51field unrestricted nativePhysicalEncodedCommandsErrorBytes : Nat
52
53end-family
54
55family NativePhysicalEncodedCommandsResult : Type 0
56constructor NativePhysicalCommandsEncoded
57field unrestricted nativePhysicalEncodedCommands : (family NativePhysicalEncodedCommands)
58constructor NativePhysicalCommandsEncodingFailed
59field unrestricted nativePhysicalCommandsEncodingError : (family NativePhysicalImageErrorCode)
60field unrestricted nativePhysicalCommandsEncodingOrdinal : Nat
61
62end-family
63
64family NativePhysicalImageTelemetry : Type 0
65constructor NativePhysicalImageTelemetryValue
66field unrestricted nativePhysicalImageTelemetryCounts : (family NativePhysicalCounts)
67field unrestricted nativePhysicalImageTelemetryPayloadBytes : Nat
68field unrestricted nativePhysicalImageTelemetryAuxiliaryBytes : Nat
69field unrestricted nativePhysicalImageTelemetryErrorIdentityBytes : Nat
70field unrestricted nativePhysicalImageTelemetryBodyBytes : Nat
71field unrestricted nativePhysicalImageTelemetryOutputBytes : Nat
72field unrestricted nativePhysicalImageTelemetryFailures : Nat
73field unrestricted nativePhysicalImageTelemetryFallbacks : Nat
74field unrestricted nativePhysicalImageTelemetryIdentity : Bytes
75field unrestricted nativePhysicalImageTelemetryBodySHA256 : Bytes
76
77end-family
78
79family NativePhysicalImageFailureTelemetry : Type 0
80constructor NativePhysicalImageFailureTelemetryValue
81field unrestricted nativePhysicalImageFailureValidation : (family NativePhysicalValidationTelemetry)
82field unrestricted nativePhysicalImageFailureEncodedCommands : Nat
83field unrestricted nativePhysicalImageFailureBodyBytes : Nat
84field unrestricted nativePhysicalImageFailureCode : Bytes
85
86end-family
87
88family NativePhysicalImage : Type 0
89constructor NativePhysicalImageValue
90field unrestricted nativePhysicalImageBytes : Bytes
91field unrestricted nativePhysicalImageBodySHA256 : Bytes
92field unrestricted nativePhysicalImageProgramIdentity : Bytes
93field unrestricted nativePhysicalImageCommandCount : Nat
94field unrestricted nativePhysicalImageStateExtent : (family ModelWord64)
95field unrestricted nativePhysicalImageResultSlots : (family ModelWord64)
96field unrestricted nativePhysicalImageTelemetry : (family NativePhysicalImageTelemetry)
97
98end-family
99
100family NativePhysicalImageResult : Type 0
101constructor NativePhysicalImageGenerated
102field unrestricted nativePhysicalGeneratedImage : (family NativePhysicalImage)
103field unrestricted nativePhysicalImageSuccessTelemetry : (family NativePhysicalImageTelemetry)
104constructor NativePhysicalImageGenerationFailed
105field unrestricted nativePhysicalImageGenerationError : (family NativePhysicalImageErrorCode)
106field unrestricted nativePhysicalImageGenerationFailureTelemetry : (family NativePhysicalImageFailureTelemetry)
107
108end-family
109
110-- Code the image already holds, and the body offset where it begins.
111family NativePhysicalImageRoutineCode : Type 0
112constructor NativePhysicalImageRoutineCodeValue
113field unrestricted nativePhysicalImageRoutineCodeBytes : Bytes
114field unrestricted nativePhysicalImageRoutineCodeAt : Nat
115
116end-family
117
118family NativePhysicalImageSharedEncoding : Type 0
119constructor NativePhysicalImageSharedEncodingValue
120field unrestricted nativePhysicalImageSharedEncodingResult : (family NativePhysicalEncodedCommandResult)
121field unrestricted nativePhysicalImageSharedEncodingHeld : (family StdList (family NativePhysicalImageRoutineCode))
122
123end-family
124
125def nativePhysicalImageErrorCodeBytes =
126 (lambda unrestricted code : (family NativePhysicalImageErrorCode) .
127 (eliminate
128 NativePhysicalImageErrorCode
129 (lambda unrestricted current : (family NativePhysicalImageErrorCode) . Bytes)
130 code
131 (branch
132 NativePhysicalImageProgramRejected
133 programError
134 .
135 (bytes-append
136 b"ALPHA-PHYIMG-001-"
137 (nativePhysicalErrorCodeBytes programError)))
138 (branch
139 NativePhysicalImageExtentOverflow
140 .
141 b"ALPHA-PHYIMG-002")
142 (branch
143 NativePhysicalImageCommandErrorIdentityEmpty
144 .
145 b"ALPHA-PHYIMG-003")
146 (branch
147 NativePhysicalImageCommandCountMismatch
148 .
149 b"ALPHA-PHYIMG-004")))
150
151def nativePhysicalImageMagic : Bytes =
152 b"ALPXPHY4"
153
154def nativePhysicalImageVersion : (family ModelWord64) =
155 4
156
157def nativePhysicalImageZeroWord64 : (family ModelWord64) =
158 0
159
160def nativePhysicalImageWord64 =
161 (lambda unrestricted byte0 : Byte .
162 (constructor
163 ModelWord64
164 ModelWord64Value
165 byte0
166 (byte 0)
167 (byte 0)
168 (byte 0)
169 (byte 0)
170 (byte 0)
171 (byte 0)
172 (byte 0)))
173
174def nativePhysicalImageWord64Bytes =
175 (lambda unrestricted value : (family ModelWord64) .
176 (eliminate
177 ModelWord64
178 (lambda unrestricted current : (family ModelWord64) . Bytes)
179 value
180 (branch
181 ModelWord64Value
182 byte0
183 byte1
184 byte2
185 byte3
186 byte4
187 byte5
188 byte6
189 byte7
190 .
191 (bytes-cons
192 byte0
193 (bytes-cons
194 byte1
195 (bytes-cons
196 byte2
197 (bytes-cons
198 byte3
199 (bytes-cons byte4 (bytes-cons byte5 (bytes-cons byte6 (bytes-cons byte7 b"")))))))))))
200
201def nativePhysicalImageSlotWord =
202 (lambda unrestricted slot : (family NativePhysicalSlot) .
203 (eliminate
204 NativePhysicalSlot
205 (lambda unrestricted current : (family NativePhysicalSlot) . (family ModelWord64))
206 slot
207 (branch NativePhysicalSlotValue index . index)))
208
209def nativePhysicalImageResultDescriptor =
210 (lambda unrestricted binding : (family NativePhysicalResultBinding) .
211 (eliminate
212 NativePhysicalResultBinding
213 (lambda unrestricted current : (family NativePhysicalResultBinding) .
214 (family NativePhysicalImageResultDescriptor))
215 binding
216 (branch
217 NativePhysicalDiscardResult
218 .
219 (constructor
220 NativePhysicalImageResultDescriptor
221 NativePhysicalImageResultDescriptorValue
222 nativePhysicalImageZeroWord64
223 nativePhysicalImageZeroWord64))
224 (branch
225 NativePhysicalStoreResult
226 slot
227 .
228 (constructor
229 NativePhysicalImageResultDescriptor
230 NativePhysicalImageResultDescriptorValue
231 (nativePhysicalImageWord64 (byte 1))
232 (nativePhysicalImageSlotWord slot)))))
233
234def nativePhysicalImageOperandDescriptor =
235 (lambda unrestricted operand : (family NativePhysicalOperand) .
236 (eliminate
237 NativePhysicalOperand
238 (lambda unrestricted current : (family NativePhysicalOperand) . Bytes)
239 operand
240 (branch
241 NativePhysicalImmediate
242 value
243 .
244 (bytes-append
245 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 0)))
246 (bytes-append
247 (nativePhysicalImageWord64Bytes value)
248 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
249 (branch
250 NativePhysicalResultValue
251 slot
252 .
253 (bytes-append
254 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 1)))
255 (bytes-append
256 (nativePhysicalImageWord64Bytes (nativePhysicalImageSlotWord slot))
257 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
258 (branch
259 NativePhysicalResultAddress
260 slot
261 offset
262 .
263 (bytes-append
264 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 2)))
265 (bytes-append
266 (nativePhysicalImageWord64Bytes (nativePhysicalImageSlotWord slot))
267 (nativePhysicalImageWord64Bytes offset))))
268 (branch
269 NativePhysicalStateAddress
270 offset
271 .
272 (bytes-append
273 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 3)))
274 (bytes-append
275 (nativePhysicalImageWord64Bytes offset)
276 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
277 (branch
278 NativePhysicalStateLoad64
279 offset
280 .
281 (bytes-append
282 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 4)))
283 (bytes-append
284 (nativePhysicalImageWord64Bytes offset)
285 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
286 (branch
287 NativePhysicalPayloadAddress
288 offset
289 .
290 (bytes-append
291 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 5)))
292 (bytes-append
293 (nativePhysicalImageWord64Bytes offset)
294 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
295 (branch
296 NativePhysicalPayloadLoad64
297 offset
298 .
299 (bytes-append
300 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 6)))
301 (bytes-append
302 (nativePhysicalImageWord64Bytes offset)
303 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
304 (branch
305 NativePhysicalProcessArgument
306 index
307 .
308 (bytes-append
309 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 7)))
310 (bytes-append
311 (nativePhysicalImageWord64Bytes index)
312 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
313 (branch
314 NativePhysicalLoopAffine
315 base
316 stride
317 .
318 (bytes-append
319 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 8)))
320 (bytes-append
321 (nativePhysicalImageWord64Bytes base)
322 (nativePhysicalImageWord64Bytes stride))))))
323
324def nativePhysicalImageZeroOperand : (family NativePhysicalOperand) =
325 (constructor NativePhysicalOperand NativePhysicalImmediate nativePhysicalImageZeroWord64)
326
327-- Seven operand slots, without the trailing slots that are the zero
328-- immediate. An omitted slot reads as the zero immediate (Runtime.
329-- NativePhysicalNative resolves a slot past a record's stored operands to 0),
330-- so trimming never changes an operand's value; it only drops the zero
331-- padding most commands carry. The aligned format restores all seven.
332def nativePhysicalImageKeepOperand =
333 (lambda unrestricted descriptor : Bytes .
334 (lambda unrestricted later : Bytes .
335 (nat-eliminate
336 (lambda unrestricted current : Nat . Bytes)
337 (bytes-append descriptor later)
338 (lambda unrestricted predecessor : Nat .
339 (lambda unrestricted ignored : Bytes . b""))
340 (naturalAnd
341 (bytes-equal later b"")
342 (bytes-equal descriptor (nativePhysicalImageOperandDescriptor nativePhysicalImageZeroOperand))))))
343
344def nativePhysicalImageSevenOperandBytes =
345 (lambda unrestricted operand0 : (family NativePhysicalOperand) .
346 (lambda unrestricted operand1 : (family NativePhysicalOperand) .
347 (lambda unrestricted operand2 : (family NativePhysicalOperand) .
348 (lambda unrestricted operand3 : (family NativePhysicalOperand) .
349 (lambda unrestricted operand4 : (family NativePhysicalOperand) .
350 (lambda unrestricted operand5 : (family NativePhysicalOperand) .
351 (lambda unrestricted operand6 : (family NativePhysicalOperand) .
352 (nativePhysicalImageKeepOperand
353 (nativePhysicalImageOperandDescriptor operand0)
354 (nativePhysicalImageKeepOperand
355 (nativePhysicalImageOperandDescriptor operand1)
356 (nativePhysicalImageKeepOperand
357 (nativePhysicalImageOperandDescriptor operand2)
358 (nativePhysicalImageKeepOperand
359 (nativePhysicalImageOperandDescriptor operand3)
360 (nativePhysicalImageKeepOperand
361 (nativePhysicalImageOperandDescriptor operand4)
362 (nativePhysicalImageKeepOperand
363 (nativePhysicalImageOperandDescriptor operand5)
364 (nativePhysicalImageKeepOperand
365 (nativePhysicalImageOperandDescriptor operand6)
366 b""))))))))))))))
367
368def nativePhysicalImageSystemCallOperandBytes =
369 (lambda unrestricted number : (family NativePhysicalOperand) .
370 (lambda unrestricted arguments : (family NativePhysicalArguments) .
371 (eliminate
372 NativePhysicalArguments
373 (lambda unrestricted current : (family NativePhysicalArguments) . Bytes)
374 arguments
375 (branch
376 NativePhysicalArgumentsValue
377 arg0
378 arg1
379 arg2
380 arg3
381 arg4
382 arg5
383 .
384 (nativePhysicalImageSevenOperandBytes number arg0 arg1 arg2 arg3 arg4 arg5)))))
385
386def nativePhysicalImageRoutineOperandBytes =
387 (lambda unrestricted arguments : (family NativePhysicalArguments) .
388 (eliminate
389 NativePhysicalArguments
390 (lambda unrestricted current : (family NativePhysicalArguments) . Bytes)
391 arguments
392 (branch
393 NativePhysicalArgumentsValue
394 arg0
395 arg1
396 arg2
397 arg3
398 arg4
399 arg5
400 .
401 (nativePhysicalImageSevenOperandBytes
402 arg0
403 arg1
404 arg2
405 arg3
406 arg4
407 arg5
408 nativePhysicalImageZeroOperand))))
409
410-- A record's fixed part: eight header words, then seven 24-byte operand
411-- slots. The compact format stores only a prefix of the slots and records
412-- how many bytes it omitted in header word 7; the aligned format stores all.
413def nativePhysicalImageCommandFixedBytes : Nat =
414 (byte-to-nat (byte 232))
415
416def nativePhysicalImageCommandHeaderBytes : Nat =
417 (byte-to-nat (byte 64))
418
419def nativePhysicalImageCommandOperandBytes : Nat =
420 (byte-to-nat (byte 168))
421
422def nativePhysicalImageRecordAlignment : Nat =
423 (byte-to-nat (byte 4))
424
425-- Legacy V2 padded syscall payloads, but this does not align every record.
426-- Preserve its bytes for existing x86 artifacts. V3 separately pads the complete
427-- record without altering any content extent; Runtime.NativePhysicalImagePlan
428-- owns that wire contract and the AArch64 runtime requires it.
429def nativePhysicalImageSystemCallPayloadPadding =
430 (lambda unrestricted payloadLength : Nat .
431 (naturalModuloUnchecked
432 (naturalSaturatingSubtract
433 nativePhysicalImageRecordAlignment
434 (naturalModuloUnchecked payloadLength nativePhysicalImageRecordAlignment))
435 nativePhysicalImageRecordAlignment))
436
437def nativePhysicalImageZeroPad =
438 (lambda unrestricted count : Nat .
439 (nat-eliminate
440 (lambda unrestricted current : Nat . Bytes)
441 b""
442 (lambda unrestricted predecessor : Nat .
443 (lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction)))
444 count))
445
446def nativePhysicalImageAlignedSystemCallPayload =
447 (lambda unrestricted payload : Bytes .
448 (bytes-append
449 payload
450 (nativePhysicalImageZeroPad
451 (nativePhysicalImageSystemCallPayloadPadding (bytes-length payload)))))
452
453def nativePhysicalImageMagicFor =
454 (lambda unrestricted format : (family NativePhysicalImageFormat) .
455 (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . Bytes) format
456 (branch NativePhysicalImageCompactV4 . nativePhysicalImageMagic)
457 (branch NativePhysicalImageAlignedV3 . b"ALPXPHY3")))
458
459def nativePhysicalImageVersionFor =
460 (lambda unrestricted format : (family NativePhysicalImageFormat) .
461 (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . (family ModelWord64)) format
462 (branch NativePhysicalImageCompactV4 . nativePhysicalImageVersion)
463 (branch NativePhysicalImageAlignedV3 . (nativePhysicalImageWord64 (byte 3)))))
464
465def nativePhysicalImageRecordExtentFor =
466 (lambda unrestricted format : (family NativePhysicalImageFormat) .
467 (lambda unrestricted extent : Nat .
468 (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . Nat) format
469 (branch NativePhysicalImageCompactV4 . extent)
470 (branch NativePhysicalImageAlignedV3 . (nativePhysicalImageAlignedExtent extent)))))
471
472def nativePhysicalImageRecordPaddingFor =
473 (lambda unrestricted format : (family NativePhysicalImageFormat) .
474 (lambda unrestricted extent : Nat .
475 (naturalSaturatingSubtract (nativePhysicalImageRecordExtentFor format extent) extent)))
476
477-- The operand slots a record stores: the trimmed prefix in the compact
478-- format; all seven in the aligned format (its reader has fixed offsets).
479def nativePhysicalImageStoredOperands =
480 (lambda unrestricted format : (family NativePhysicalImageFormat) .
481 (lambda unrestricted operands : Bytes .
482 (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . Bytes) format
483 (branch NativePhysicalImageCompactV4 . operands)
484 (branch NativePhysicalImageAlignedV3 .
485 (bytes-append operands
486 (nativePhysicalImageZeroPad
487 (naturalSaturatingSubtract nativePhysicalImageCommandOperandBytes (bytes-length operands))))))))
488
489-- Header word 7: the operand bytes a record omits. Its payload begins at
490-- nativePhysicalImageCommandFixedBytes minus this.
491def nativePhysicalImageOmittedOperandBytes =
492 (lambda unrestricted format : (family NativePhysicalImageFormat) .
493 (lambda unrestricted operands : Bytes .
494 (naturalSaturatingSubtract nativePhysicalImageCommandOperandBytes
495 (bytes-length (nativePhysicalImageStoredOperands format operands)))))
496
497def nativePhysicalImageCommandRecordForFormat =
498 (lambda unrestricted format : (family NativePhysicalImageFormat) .
499 (lambda unrestricted tag : Byte .
500 (lambda unrestricted binding : (family NativePhysicalResultBinding) .
501 (lambda unrestricted operands : Bytes .
502 (lambda unrestricted payload : Bytes .
503 (lambda unrestricted auxiliary : Bytes .
504 (lambda unrestricted errorIdentity : Bytes .
505 (nat-eliminate
506 (lambda unrestricted current : Nat . (family NativePhysicalEncodedCommandResult))
507 (constructor
508 NativePhysicalEncodedCommandResult
509 NativePhysicalCommandEncodingFailed
510 (constructor
511 NativePhysicalImageErrorCode
512 NativePhysicalImageCommandErrorIdentityEmpty))
513 (lambda unrestricted errorPredecessor : Nat .
514 (lambda unrestricted ignoredError : (family NativePhysicalEncodedCommandResult) .
515 (eliminate
516 NativeTelemetryCounterResult
517 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
518 (family NativePhysicalEncodedCommandResult))
519 (nativeTelemetryCounterFromNatural (bytes-length payload))
520 (branch
521 NativeTelemetryCounterSucceeded
522 payloadExtent
523 .
524 (eliminate
525 NativeTelemetryCounterResult
526 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
527 (family NativePhysicalEncodedCommandResult))
528 (nativeTelemetryCounterFromNatural (bytes-length auxiliary))
529 (branch
530 NativeTelemetryCounterSucceeded
531 auxiliaryExtent
532 .
533 (eliminate
534 NativeTelemetryCounterResult
535 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
536 (family NativePhysicalEncodedCommandResult))
537 (nativeTelemetryCounterFromNatural (bytes-length errorIdentity))
538 (branch
539 NativeTelemetryCounterSucceeded
540 errorExtent
541 .
542 (eliminate
543 NativeTelemetryCounterResult
544 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
545 (family NativePhysicalEncodedCommandResult))
546 (nativeTelemetryCounterFromNatural
547 (nativePhysicalImageRecordExtentFor format
548 (naturalAdd
549 (naturalSaturatingSubtract nativePhysicalImageCommandFixedBytes
550 (nativePhysicalImageOmittedOperandBytes format operands))
551 (naturalAdd (bytes-length payload)
552 (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity))))))
553 (branch
554 NativeTelemetryCounterSucceeded
555 recordExtent
556 .
557 (eliminate
558 NativePhysicalImageResultDescriptor
559 (lambda unrestricted current : (family NativePhysicalImageResultDescriptor) .
560 (family NativePhysicalEncodedCommandResult))
561 (nativePhysicalImageResultDescriptor binding)
562 (branch
563 NativePhysicalImageResultDescriptorValue
564 resultKind
565 resultSlot
566 .
567 (constructor
568 NativePhysicalEncodedCommandResult
569 NativePhysicalCommandEncoded
570 (constructor
571 NativePhysicalEncodedCommand
572 NativePhysicalEncodedCommandValue
573 (bytes-append
574 (nativePhysicalImageWord64Bytes
575 (nativePhysicalImageWord64 tag))
576 (bytes-append
577 (nativePhysicalImageWord64Bytes recordExtent)
578 (bytes-append
579 (nativePhysicalImageWord64Bytes resultKind)
580 (bytes-append
581 (nativePhysicalImageWord64Bytes resultSlot)
582 (bytes-append
583 (nativePhysicalImageWord64Bytes payloadExtent)
584 (bytes-append
585 (nativePhysicalImageWord64Bytes auxiliaryExtent)
586 (bytes-append
587 (nativePhysicalImageWord64Bytes errorExtent)
588 (bytes-append
589 (nativePhysicalImageWord64Bytes
590 (nativePhysicalImageWord64
591 (nat-to-byte (nativePhysicalImageOmittedOperandBytes format operands))))
592 (bytes-append
593 (nativePhysicalImageStoredOperands format operands)
594 (bytes-append
595 payload
596 (bytes-append auxiliary (bytes-append errorIdentity
597 (nativePhysicalImageZeroPad
598 (nativePhysicalImageRecordPaddingFor format
599 (naturalAdd
600 (naturalSaturatingSubtract nativePhysicalImageCommandFixedBytes
601 (nativePhysicalImageOmittedOperandBytes format operands))
602 (naturalAdd (bytes-length payload)
603 (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity))))))))))))))))))
604 (bytes-length payload)
605 (bytes-length auxiliary)
606 (bytes-length errorIdentity))))))
607 (branch
608 NativeTelemetryCounterFailed
609 counterError
610 naturalValue
611 .
612 (constructor
613 NativePhysicalEncodedCommandResult
614 NativePhysicalCommandEncodingFailed
615 (constructor
616 NativePhysicalImageErrorCode
617 NativePhysicalImageExtentOverflow)))))
618 (branch
619 NativeTelemetryCounterFailed
620 counterError
621 naturalValue
622 .
623 (constructor
624 NativePhysicalEncodedCommandResult
625 NativePhysicalCommandEncodingFailed
626 (constructor
627 NativePhysicalImageErrorCode
628 NativePhysicalImageExtentOverflow)))))
629 (branch
630 NativeTelemetryCounterFailed
631 counterError
632 naturalValue
633 .
634 (constructor
635 NativePhysicalEncodedCommandResult
636 NativePhysicalCommandEncodingFailed
637 (constructor
638 NativePhysicalImageErrorCode
639 NativePhysicalImageExtentOverflow)))))
640 (branch
641 NativeTelemetryCounterFailed
642 counterError
643 naturalValue
644 .
645 (constructor
646 NativePhysicalEncodedCommandResult
647 NativePhysicalCommandEncodingFailed
648 (constructor
649 NativePhysicalImageErrorCode
650 NativePhysicalImageExtentOverflow))))))
651 (bytes-length errorIdentity)))))))))
652
653def nativePhysicalImageCommandRecord =
654 (nativePhysicalImageCommandRecordForFormat (constructor NativePhysicalImageFormat NativePhysicalImageCompactV4))
655
656def nativePhysicalImageDiscardResult : (family NativePhysicalResultBinding) =
657 (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)
658
659-- the binary64 operations' record tags: 14 .. 21, in the family's order
660def nativePhysicalImageFloat64Tag =
661 (lambda unrestricted kind : (family NativePhysicalFloat64Operation) .
662 (eliminate NativePhysicalFloat64Operation
663 (lambda unrestricted current : (family NativePhysicalFloat64Operation) . Byte)
664 kind
665 (branch NativePhysicalFloat64Add . (byte 14))
666 (branch NativePhysicalFloat64Subtract . (byte 15))
667 (branch NativePhysicalFloat64Multiply . (byte 16))
668 (branch NativePhysicalFloat64Divide . (byte 17))
669 (branch NativePhysicalFloat64SquareRoot . (byte 18))
670 (branch NativePhysicalFloat64FromNatural . (byte 19))
671 (branch NativePhysicalFloat64ToBinary32 . (byte 20))
672 (branch NativePhysicalFloat64FromBinary32 . (byte 21))))
673
674def nativePhysicalImageEncodeOperationForFormat =
675 (lambda unrestricted format : (family NativePhysicalImageFormat) .
676 (lambda unrestricted operation : (family NativePhysicalOperation) .
677 (lambda unrestricted errorIdentity : Bytes .
678 (eliminate
679 NativePhysicalOperation
680 (lambda unrestricted current : (family NativePhysicalOperation) .
681 (family NativePhysicalEncodedCommandResult))
682 operation
683 (branch
684 NativePhysicalSystemCall
685 number
686 arguments
687 payload
688 result
689 .
690 (nativePhysicalImageCommandRecordForFormat
691 format
692 (byte 1)
693 result
694 (nativePhysicalImageSystemCallOperandBytes number arguments)
695 (nativePhysicalImageAlignedSystemCallPayload payload)
696 b""
697 errorIdentity))
698 (branch
699 NativePhysicalCopyPayloadToState
700 destination
701 extent
702 payload
703 .
704 (nativePhysicalImageCommandRecordForFormat
705 format
706 (byte 2)
707 nativePhysicalImageDiscardResult
708 (nativePhysicalImageSevenOperandBytes
709 (constructor NativePhysicalOperand NativePhysicalImmediate destination)
710 (constructor NativePhysicalOperand NativePhysicalImmediate extent)
711 nativePhysicalImageZeroOperand
712 nativePhysicalImageZeroOperand
713 nativePhysicalImageZeroOperand
714 nativePhysicalImageZeroOperand
715 nativePhysicalImageZeroOperand)
716 payload
717 b""
718 errorIdentity))
719 (branch
720 NativePhysicalMachineRoutine
721 code
722 arguments
723 result
724 .
725 (nativePhysicalImageCommandRecordForFormat
726 format
727 (byte 3)
728 result
729 (nativePhysicalImageRoutineOperandBytes arguments)
730 code
731 b""
732 errorIdentity))
733 (branch
734 NativePhysicalFencePoll
735 address
736 expected
737 maximumPolls
738 .
739 (nativePhysicalImageCommandRecordForFormat
740 format
741 (byte 4)
742 nativePhysicalImageDiscardResult
743 (nativePhysicalImageSevenOperandBytes
744 address
745 expected
746 (constructor NativePhysicalOperand NativePhysicalImmediate maximumPolls)
747 nativePhysicalImageZeroOperand
748 nativePhysicalImageZeroOperand
749 nativePhysicalImageZeroOperand
750 nativePhysicalImageZeroOperand)
751 b""
752 b""
753 errorIdentity))
754 (branch
755 NativePhysicalTelemetryAppend
756 path
757 record
758 .
759 (nativePhysicalImageCommandRecordForFormat
760 format
761 (byte 5)
762 nativePhysicalImageDiscardResult
763 (nativePhysicalImageSevenOperandBytes
764 nativePhysicalImageZeroOperand
765 nativePhysicalImageZeroOperand
766 nativePhysicalImageZeroOperand
767 nativePhysicalImageZeroOperand
768 nativePhysicalImageZeroOperand
769 nativePhysicalImageZeroOperand
770 nativePhysicalImageZeroOperand)
771 path
772 record
773 errorIdentity))
774 (branch
775 NativePhysicalAssertEqual
776 left
777 right
778 error
779 .
780 (nativePhysicalImageCommandRecordForFormat
781 format
782 (byte 6)
783 nativePhysicalImageDiscardResult
784 (nativePhysicalImageSevenOperandBytes
785 left
786 right
787 nativePhysicalImageZeroOperand
788 nativePhysicalImageZeroOperand
789 nativePhysicalImageZeroOperand
790 nativePhysicalImageZeroOperand
791 nativePhysicalImageZeroOperand)
792 b""
793 (nativePhysicalErrorCodeBytes error)
794 errorIdentity))
795 (branch
796 NativePhysicalAssertOneOf
797 observed
798 first
799 second
800 error
801 .
802 (nativePhysicalImageCommandRecordForFormat
803 format
804 (byte 8)
805 nativePhysicalImageDiscardResult
806 (nativePhysicalImageSevenOperandBytes
807 observed
808 first
809 second
810 nativePhysicalImageZeroOperand
811 nativePhysicalImageZeroOperand
812 nativePhysicalImageZeroOperand
813 nativePhysicalImageZeroOperand)
814 b""
815 (nativePhysicalErrorCodeBytes error)
816 errorIdentity))
817 (branch
818 NativePhysicalHaltSuccess
819 .
820 (nativePhysicalImageCommandRecordForFormat
821 format
822 (byte 7)
823 nativePhysicalImageDiscardResult
824 (nativePhysicalImageSevenOperandBytes
825 nativePhysicalImageZeroOperand
826 nativePhysicalImageZeroOperand
827 nativePhysicalImageZeroOperand
828 nativePhysicalImageZeroOperand
829 nativePhysicalImageZeroOperand
830 nativePhysicalImageZeroOperand
831 nativePhysicalImageZeroOperand)
832 b""
833 b""
834 errorIdentity))
835 (branch
836 NativePhysicalRepeatBegin
837 count
838 .
839 (nativePhysicalImageCommandRecordForFormat
840 format
841 (byte 9)
842 nativePhysicalImageDiscardResult
843 (nativePhysicalImageSevenOperandBytes
844 (constructor NativePhysicalOperand NativePhysicalImmediate count)
845 nativePhysicalImageZeroOperand
846 nativePhysicalImageZeroOperand
847 nativePhysicalImageZeroOperand
848 nativePhysicalImageZeroOperand
849 nativePhysicalImageZeroOperand
850 nativePhysicalImageZeroOperand)
851 b""
852 b""
853 errorIdentity))
854 (branch
855 NativePhysicalSkipUnlessEqual
856 left
857 right
858 count
859 .
860 (nativePhysicalImageCommandRecordForFormat
861 format
862 (byte 23)
863 nativePhysicalImageDiscardResult
864 (nativePhysicalImageSevenOperandBytes
865 left
866 right
867 (constructor NativePhysicalOperand NativePhysicalImmediate count)
868 nativePhysicalImageZeroOperand
869 nativePhysicalImageZeroOperand
870 nativePhysicalImageZeroOperand
871 nativePhysicalImageZeroOperand)
872 b""
873 b""
874 errorIdentity))
875 (branch
876 NativePhysicalRepeatEnd
877 .
878 (nativePhysicalImageCommandRecordForFormat
879 format
880 (byte 10)
881 nativePhysicalImageDiscardResult
882 (nativePhysicalImageSevenOperandBytes
883 nativePhysicalImageZeroOperand
884 nativePhysicalImageZeroOperand
885 nativePhysicalImageZeroOperand
886 nativePhysicalImageZeroOperand
887 nativePhysicalImageZeroOperand
888 nativePhysicalImageZeroOperand
889 nativePhysicalImageZeroOperand)
890 b""
891 b""
892 errorIdentity))
893 (branch
894 NativePhysicalRepeatEndWhen
895 observed
896 expected
897 .
898 (nativePhysicalImageCommandRecordForFormat
899 format
900 (byte 22)
901 nativePhysicalImageDiscardResult
902 (nativePhysicalImageSevenOperandBytes
903 observed
904 expected
905 nativePhysicalImageZeroOperand
906 nativePhysicalImageZeroOperand
907 nativePhysicalImageZeroOperand
908 nativePhysicalImageZeroOperand
909 nativePhysicalImageZeroOperand)
910 b""
911 b""
912 errorIdentity))
913 (branch
914 NativePhysicalStoreWord64
915 destination
916 value
917 .
918 (nativePhysicalImageCommandRecordForFormat
919 format
920 (byte 11)
921 nativePhysicalImageDiscardResult
922 (nativePhysicalImageSevenOperandBytes
923 destination
924 value
925 nativePhysicalImageZeroOperand
926 nativePhysicalImageZeroOperand
927 nativePhysicalImageZeroOperand
928 nativePhysicalImageZeroOperand
929 nativePhysicalImageZeroOperand)
930 b""
931 b""
932 errorIdentity))
933 (branch
934 NativePhysicalFenceWait
935 address
936 expected
937 maximumPolls
938 interval
939 .
940 (nativePhysicalImageCommandRecordForFormat
941 format
942 (byte 12)
943 nativePhysicalImageDiscardResult
944 (nativePhysicalImageSevenOperandBytes
945 address
946 expected
947 (constructor NativePhysicalOperand NativePhysicalImmediate maximumPolls)
948 (constructor NativePhysicalOperand NativePhysicalImmediate interval)
949 nativePhysicalImageZeroOperand
950 nativePhysicalImageZeroOperand
951 nativePhysicalImageZeroOperand)
952 b""
953 b""
954 errorIdentity))
955 (branch
956 NativePhysicalRepeatBeginCounted
957 count
958 .
959 (nativePhysicalImageCommandRecordForFormat
960 format
961 (byte 9)
962 nativePhysicalImageDiscardResult
963 (nativePhysicalImageSevenOperandBytes
964 count
965 nativePhysicalImageZeroOperand
966 nativePhysicalImageZeroOperand
967 nativePhysicalImageZeroOperand
968 nativePhysicalImageZeroOperand
969 nativePhysicalImageZeroOperand
970 nativePhysicalImageZeroOperand)
971 b""
972 b""
973 errorIdentity))
974 (branch
975 NativePhysicalAddWord64
976 destination
977 left
978 right
979 .
980 (nativePhysicalImageCommandRecordForFormat
981 format
982 (byte 13)
983 nativePhysicalImageDiscardResult
984 (nativePhysicalImageSevenOperandBytes
985 destination
986 left
987 right
988 nativePhysicalImageZeroOperand
989 nativePhysicalImageZeroOperand
990 nativePhysicalImageZeroOperand
991 nativePhysicalImageZeroOperand)
992 b""
993 b""
994 errorIdentity))
995 (branch
996 NativePhysicalFloat64
997 kind
998 destination
999 left
1000 right
1001 .
1002 (nativePhysicalImageCommandRecordForFormat
1003 format
1004 (nativePhysicalImageFloat64Tag kind)
1005 nativePhysicalImageDiscardResult
1006 (nativePhysicalImageSevenOperandBytes
1007 destination
1008 left
1009 right
1010 nativePhysicalImageZeroOperand
1011 nativePhysicalImageZeroOperand
1012 nativePhysicalImageZeroOperand
1013 nativePhysicalImageZeroOperand)
1014 b""
1015 b""
1016 errorIdentity))))))
1017
1018def nativePhysicalImageEncodeOperation =
1019 (nativePhysicalImageEncodeOperationForFormat (constructor NativePhysicalImageFormat NativePhysicalImageCompactV4))
1020
1021def nativePhysicalImageEncodeCommandForFormat =
1022 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1023 (lambda unrestricted command : (family NativePhysicalCommand) .
1024 (eliminate
1025 NativePhysicalCommand
1026 (lambda unrestricted current : (family NativePhysicalCommand) .
1027 (family NativePhysicalEncodedCommandResult))
1028 command
1029 (branch
1030 NativePhysicalCommandValue
1031 operation
1032 errorIdentity
1033 .
1034 (nativePhysicalImageEncodeOperationForFormat format operation errorIdentity)))))
1035
1036def nativePhysicalImageEncodeCommand =
1037 (nativePhysicalImageEncodeCommandForFormat (constructor NativePhysicalImageFormat NativePhysicalImageCompactV4))
1038
1039-- ---- shared routine code ----
1040-- A machine routine whose code repeats an earlier routine's exactly stores a
1041-- one-instruction branch to that earlier code instead of a copy (the format's
1042-- jump: x86 jmp rel32, AArch64 B). The interpreter calls the routine record
1043-- as before; the branch reaches the same code with the same argument
1044-- registers and return address, so behaviour is unchanged. A routine that
1045-- passes an operand into its own payload keeps its copy: that operand would
1046-- otherwise address the branch. Runtime.NativePhysicalImagePlan states the
1047-- wire contract; the compiler's encoder applies the same rule.
1048
1049-- Where `code` begins if the image already holds it, otherwise 0 (no code
1050-- begins at body offset 0: a record header precedes every payload).
1051def nativePhysicalImageHeldRoutineAt =
1052 (lambda unrestricted code : Bytes .
1053 (lambda unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1054 (eliminate
1055 StdList
1056 (lambda unrestricted current : (family StdList (family NativePhysicalImageRoutineCode)) . Nat)
1057 held
1058 (branch StdListEmpty . zero)
1059 (branch
1060 StdListCons
1061 head
1062 tail
1063 induction
1064 .
1065 (eliminate
1066 NativePhysicalImageRoutineCode
1067 (lambda unrestricted current : (family NativePhysicalImageRoutineCode) . Nat)
1068 head
1069 (branch
1070 NativePhysicalImageRoutineCodeValue
1071 bytes
1072 at
1073 .
1074 (nat-eliminate
1075 (lambda unrestricted current : Nat . Nat)
1076 induction
1077 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . at))
1078 (bytes-equal bytes code))))))))
1079
1080-- 1 when the operand addresses its own record's payload.
1081def nativePhysicalImageOperandReadsPayload =
1082 (lambda unrestricted operand : (family NativePhysicalOperand) .
1083 (eliminate
1084 NativePhysicalOperand
1085 (lambda unrestricted current : (family NativePhysicalOperand) . Nat)
1086 operand
1087 (branch NativePhysicalImmediate value . zero)
1088 (branch NativePhysicalResultValue slot . zero)
1089 (branch NativePhysicalResultAddress slot offset . zero)
1090 (branch NativePhysicalStateAddress offset . zero)
1091 (branch NativePhysicalStateLoad64 offset . zero)
1092 (branch NativePhysicalPayloadAddress offset . (succ zero))
1093 (branch NativePhysicalPayloadLoad64 offset . (succ zero))
1094 (branch NativePhysicalProcessArgument index . zero)
1095 (branch NativePhysicalLoopAffine base stride . zero)))
1096
1097def nativePhysicalImageArgumentsReadPayload =
1098 (lambda unrestricted arguments : (family NativePhysicalArguments) .
1099 (eliminate
1100 NativePhysicalArguments
1101 (lambda unrestricted current : (family NativePhysicalArguments) . Nat)
1102 arguments
1103 (branch
1104 NativePhysicalArgumentsValue
1105 arg0
1106 arg1
1107 arg2
1108 arg3
1109 arg4
1110 arg5
1111 .
1112 (naturalOr (nativePhysicalImageOperandReadsPayload arg0)
1113 (naturalOr (nativePhysicalImageOperandReadsPayload arg1)
1114 (naturalOr (nativePhysicalImageOperandReadsPayload arg2)
1115 (naturalOr (nativePhysicalImageOperandReadsPayload arg3)
1116 (naturalOr (nativePhysicalImageOperandReadsPayload arg4)
1117 (nativePhysicalImageOperandReadsPayload arg5)))))))))
1118
1119-- Where a routine record's code begins inside the record.
1120def nativePhysicalImageRoutineCodeOffset =
1121 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1122 (lambda unrestricted arguments : (family NativePhysicalArguments) .
1123 (naturalSaturatingSubtract nativePhysicalImageCommandFixedBytes
1124 (nativePhysicalImageOmittedOperandBytes format
1125 (nativePhysicalImageRoutineOperandBytes arguments)))))
1126
1127def nativePhysicalImageRoutineBranchBytes =
1128 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1129 (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . Nat) format
1130 (branch NativePhysicalImageCompactV4 . 5)
1131 (branch NativePhysicalImageAlignedV3 . 4)))
1132
1133def nativePhysicalImageLittleEndian32 =
1134 (lambda unrestricted value : Nat .
1135 (bytes-cons (nat-to-byte (naturalModuloUnchecked value 256))
1136 (bytes-cons (nat-to-byte (naturalModuloUnchecked (naturalDivideUnchecked value 256) 256))
1137 (bytes-cons (nat-to-byte (naturalModuloUnchecked (naturalDivideUnchecked value 65536) 256))
1138 (bytes-cons (nat-to-byte (naturalModuloUnchecked (naturalDivideUnchecked value 16777216) 256))
1139 b"")))))
1140
1141-- The branch at body offset `here` to the earlier code at `at` (at < here).
1142-- x86 jmp rel32 (E9) measures from the next instruction; AArch64 B (imm26
1143-- words, opcode 0x14000000) from itself. Both displacements are negative.
1144def nativePhysicalImageRoutineBranch =
1145 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1146 (lambda unrestricted at : Nat .
1147 (lambda unrestricted here : Nat .
1148 (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . Bytes) format
1149 (branch NativePhysicalImageCompactV4 .
1150 (bytes-append (bytes 233)
1151 (nativePhysicalImageLittleEndian32
1152 (naturalSaturatingSubtract 4294967296
1153 (naturalSaturatingSubtract (naturalAdd here 5) at)))))
1154 (branch NativePhysicalImageAlignedV3 .
1155 (nativePhysicalImageLittleEndian32
1156 (naturalAdd 335544320
1157 (naturalSaturatingSubtract 67108864
1158 (naturalDivideUnchecked (naturalSaturatingSubtract here at) 4)))))))))
1159
1160def nativePhysicalImageSharedPlain =
1161 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1162 (lambda unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1163 (lambda unrestricted operation : (family NativePhysicalOperation) .
1164 (lambda unrestricted errorIdentity : Bytes .
1165 (constructor
1166 NativePhysicalImageSharedEncoding
1167 NativePhysicalImageSharedEncodingValue
1168 (nativePhysicalImageEncodeOperationForFormat format operation errorIdentity)
1169 held)))))
1170
1171-- Encode one command whose record begins at body offset `offset`, given the
1172-- routine code already held, and the code held after it.
1173def nativePhysicalImageEncodeShared =
1174 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1175 (lambda unrestricted offset : Nat .
1176 (lambda unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1177 (lambda unrestricted operation : (family NativePhysicalOperation) .
1178 (lambda unrestricted errorIdentity : Bytes .
1179 (eliminate
1180 NativePhysicalOperation
1181 (lambda unrestricted current : (family NativePhysicalOperation) .
1182 (family NativePhysicalImageSharedEncoding))
1183 operation
1184 (branch NativePhysicalSystemCall number arguments payload result .
1185 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1186 (branch NativePhysicalCopyPayloadToState destination extent payload .
1187 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1188 (branch
1189 NativePhysicalMachineRoutine
1190 code
1191 arguments
1192 result
1193 .
1194 (app
1195 (lambda unrestricted at : Nat .
1196 (app
1197 (lambda unrestricted here : Nat .
1198 (nat-eliminate
1199 (lambda unrestricted current : Nat . (family NativePhysicalImageSharedEncoding))
1200 (constructor
1201 NativePhysicalImageSharedEncoding
1202 NativePhysicalImageSharedEncodingValue
1203 (nativePhysicalImageEncodeOperationForFormat format operation errorIdentity)
1204 (nat-eliminate
1205 (lambda unrestricted current : Nat .
1206 (family StdList (family NativePhysicalImageRoutineCode)))
1207 (constructor
1208 StdList
1209 StdListCons
1210 (family NativePhysicalImageRoutineCode)
1211 (constructor
1212 NativePhysicalImageRoutineCode
1213 NativePhysicalImageRoutineCodeValue
1214 code
1215 here)
1216 held)
1217 (lambda unrestricted predecessor : Nat .
1218 (lambda unrestricted ignored : (family StdList (family NativePhysicalImageRoutineCode)) .
1219 held))
1220 at))
1221 (lambda unrestricted predecessor : Nat .
1222 (lambda unrestricted ignored : (family NativePhysicalImageSharedEncoding) .
1223 (constructor
1224 NativePhysicalImageSharedEncoding
1225 NativePhysicalImageSharedEncodingValue
1226 (nativePhysicalImageEncodeOperationForFormat
1227 format
1228 (constructor
1229 NativePhysicalOperation
1230 NativePhysicalMachineRoutine
1231 (nativePhysicalImageRoutineBranch format at here)
1232 arguments
1233 result)
1234 errorIdentity)
1235 held)))
1236 (naturalAnd
1237 (naturalLess zero at)
1238 (naturalAnd
1239 (naturalIsZero (nativePhysicalImageArgumentsReadPayload arguments))
1240 (naturalLess
1241 (nativePhysicalImageRoutineBranchBytes format)
1242 (bytes-length code))))))
1243 (naturalAdd offset (nativePhysicalImageRoutineCodeOffset format arguments))))
1244 (nativePhysicalImageHeldRoutineAt code held)))
1245 (branch NativePhysicalFencePoll address expected polls .
1246 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1247 (branch NativePhysicalTelemetryAppend path record .
1248 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1249 (branch NativePhysicalAssertEqual left right error .
1250 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1251 (branch NativePhysicalAssertOneOf observed first second error .
1252 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1253 (branch NativePhysicalHaltSuccess .
1254 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1255 (branch NativePhysicalRepeatBegin count .
1256 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1257 (branch NativePhysicalSkipUnlessEqual left right count .
1258 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1259 (branch NativePhysicalRepeatEnd .
1260 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1261 (branch NativePhysicalRepeatEndWhen observed expected .
1262 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1263 (branch NativePhysicalStoreWord64 destination value .
1264 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1265 (branch NativePhysicalFenceWait address expected polls interval .
1266 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1267 (branch NativePhysicalRepeatBeginCounted count .
1268 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1269 (branch NativePhysicalAddWord64 destination left right .
1270 (nativePhysicalImageSharedPlain format held operation errorIdentity))
1271 (branch NativePhysicalFloat64 kind destination left right .
1272 (nativePhysicalImageSharedPlain format held operation errorIdentity))))))))
1273
1274-- The commands from body offset `offset`, in order: each record's offset is
1275-- the length of those before it, so shared routine code can be addressed.
1276def nativePhysicalImageEncodeCommandsFrom =
1277 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1278 (lambda unrestricted commands : (family NativePhysicalCommands) .
1279 (eliminate
1280 NativePhysicalCommands
1281 (lambda unrestricted current : (family NativePhysicalCommands) .
1282 (pi unrestricted offset : Nat .
1283 (pi unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1284 (family NativePhysicalEncodedCommandsResult))))
1285 commands
1286 (branch
1287 NativePhysicalCommandsEnd
1288 .
1289 (lambda unrestricted offset : Nat .
1290 (lambda unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1291 (constructor
1292 NativePhysicalEncodedCommandsResult
1293 NativePhysicalCommandsEncoded
1294 (constructor
1295 NativePhysicalEncodedCommands
1296 NativePhysicalEncodedCommandsValue
1297 b""
1298 zero
1299 zero
1300 zero
1301 zero)))))
1302 (branch
1303 NativePhysicalCommandsNext
1304 head
1305 tail
1306 induction
1307 .
1308 (lambda unrestricted offset : Nat .
1309 (lambda unrestricted held : (family StdList (family NativePhysicalImageRoutineCode)) .
1310 (eliminate
1311 NativePhysicalCommand
1312 (lambda unrestricted current : (family NativePhysicalCommand) .
1313 (family NativePhysicalEncodedCommandsResult))
1314 head
1315 (branch
1316 NativePhysicalCommandValue
1317 operation
1318 errorIdentity
1319 .
1320 (eliminate
1321 NativePhysicalImageSharedEncoding
1322 (lambda unrestricted current : (family NativePhysicalImageSharedEncoding) .
1323 (family NativePhysicalEncodedCommandsResult))
1324 (nativePhysicalImageEncodeShared format offset held operation errorIdentity)
1325 (branch
1326 NativePhysicalImageSharedEncodingValue
1327 headResult
1328 heldAfter
1329 .
1330 (eliminate
1331 NativePhysicalEncodedCommandResult
1332 (lambda unrestricted current : (family NativePhysicalEncodedCommandResult) .
1333 (family NativePhysicalEncodedCommandsResult))
1334 headResult
1335 (branch
1336 NativePhysicalCommandEncoded
1337 encoded
1338 .
1339 (eliminate
1340 NativePhysicalEncodedCommand
1341 (lambda unrestricted current : (family NativePhysicalEncodedCommand) .
1342 (family NativePhysicalEncodedCommandsResult))
1343 encoded
1344 (branch
1345 NativePhysicalEncodedCommandValue
1346 bytes
1347 payloadBytes
1348 auxiliaryBytes
1349 errorBytes
1350 .
1351 (eliminate
1352 NativePhysicalEncodedCommandsResult
1353 (lambda unrestricted current : (family NativePhysicalEncodedCommandsResult) .
1354 (family NativePhysicalEncodedCommandsResult))
1355 (induction (naturalAdd offset (bytes-length bytes)) heldAfter)
1356 (branch
1357 NativePhysicalCommandsEncoded
1358 encodedTail
1359 .
1360 (eliminate
1361 NativePhysicalEncodedCommands
1362 (lambda unrestricted current : (family NativePhysicalEncodedCommands) .
1363 (family NativePhysicalEncodedCommandsResult))
1364 encodedTail
1365 (branch
1366 NativePhysicalEncodedCommandsValue
1367 tailBytes
1368 tailCount
1369 tailPayload
1370 tailAuxiliary
1371 tailError
1372 .
1373 (constructor
1374 NativePhysicalEncodedCommandsResult
1375 NativePhysicalCommandsEncoded
1376 (constructor
1377 NativePhysicalEncodedCommands
1378 NativePhysicalEncodedCommandsValue
1379 (bytes-append bytes tailBytes)
1380 (succ tailCount)
1381 (naturalAdd payloadBytes tailPayload)
1382 (naturalAdd auxiliaryBytes tailAuxiliary)
1383 (naturalAdd errorBytes tailError))))))
1384 (branch
1385 NativePhysicalCommandsEncodingFailed
1386 error
1387 ordinal
1388 .
1389 (constructor
1390 NativePhysicalEncodedCommandsResult
1391 NativePhysicalCommandsEncodingFailed
1392 error
1393 (succ ordinal)))))))
1394 (branch
1395 NativePhysicalCommandEncodingFailed
1396 error
1397 .
1398 (constructor
1399 NativePhysicalEncodedCommandsResult
1400 NativePhysicalCommandsEncodingFailed
1401 error
1402 zero)))))))))))))
1403
1404def nativePhysicalImageEncodeCommandsForFormat =
1405 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1406 (lambda unrestricted commands : (family NativePhysicalCommands) .
1407 (nativePhysicalImageEncodeCommandsFrom
1408 format
1409 commands
1410 zero
1411 (constructor StdList StdListEmpty (family NativePhysicalImageRoutineCode)))))
1412
1413-- The extent of the record nativePhysicalImageEncodeCommand writes for a
1414-- command, measured from that encoding (so it cannot drift from the record
1415-- layout); 0 for a command that cannot be encoded. Shared routine code is a
1416-- property of a whole image, not of one command, and is not applied here.
1417def nativePhysicalImageCommandExtent =
1418 (lambda unrestricted command : (family NativePhysicalCommand) .
1419 (eliminate
1420 NativePhysicalEncodedCommandResult
1421 (lambda unrestricted current : (family NativePhysicalEncodedCommandResult) . Nat)
1422 (nativePhysicalImageEncodeCommand command)
1423 (branch
1424 NativePhysicalCommandEncoded
1425 encoded
1426 .
1427 (eliminate
1428 NativePhysicalEncodedCommand
1429 (lambda unrestricted current : (family NativePhysicalEncodedCommand) . Nat)
1430 encoded
1431 (branch NativePhysicalEncodedCommandValue bytes payloadBytes auxiliaryBytes errorBytes . (bytes-length bytes))))
1432 (branch NativePhysicalCommandEncodingFailed error . zero)))
1433
1434def nativePhysicalImageEncodeCommands =
1435 (nativePhysicalImageEncodeCommandsForFormat (constructor NativePhysicalImageFormat NativePhysicalImageCompactV4))
1436
1437def nativePhysicalImageFailureTelemetryFor =
1438 (lambda unrestricted validation : (family NativePhysicalValidationTelemetry) .
1439 (lambda unrestricted encoded : Nat .
1440 (lambda unrestricted bodyBytes : Nat .
1441 (lambda unrestricted error : (family NativePhysicalImageErrorCode) .
1442 (constructor
1443 NativePhysicalImageFailureTelemetry
1444 NativePhysicalImageFailureTelemetryValue
1445 validation
1446 encoded
1447 bodyBytes
1448 (nativePhysicalImageErrorCodeBytes error))))))
1449
1450def nativePhysicalImageFail =
1451 (lambda unrestricted validation : (family NativePhysicalValidationTelemetry) .
1452 (lambda unrestricted encoded : Nat .
1453 (lambda unrestricted bodyBytes : Nat .
1454 (lambda unrestricted error : (family NativePhysicalImageErrorCode) .
1455 (constructor
1456 NativePhysicalImageResult
1457 NativePhysicalImageGenerationFailed
1458 error
1459 (nativePhysicalImageFailureTelemetryFor validation encoded bodyBytes error))))))
1460
1461def nativePhysicalImageTelemetryFor =
1462 (lambda unrestricted counts : (family NativePhysicalCounts) .
1463 (lambda unrestricted payloadBytes : Nat .
1464 (lambda unrestricted auxiliaryBytes : Nat .
1465 (lambda unrestricted errorBytes : Nat .
1466 (lambda unrestricted bodyBytes : Nat .
1467 (lambda unrestricted outputBytes : Nat .
1468 (lambda unrestricted fallbacks : Nat .
1469 (lambda unrestricted identity : Bytes .
1470 (lambda unrestricted digest : Bytes .
1471 (constructor
1472 NativePhysicalImageTelemetry
1473 NativePhysicalImageTelemetryValue
1474 counts
1475 payloadBytes
1476 auxiliaryBytes
1477 errorBytes
1478 bodyBytes
1479 outputBytes
1480 zero
1481 fallbacks
1482 identity
1483 digest))))))))))
1484
1485-- Body-digest strategy is now a parameter so the FAST (GPU bring-up) ELF path
1486-- can supply a stub instead of paying for a real SHA-256 of the image body.
1487-- The digest lives in the image header's telemetry region [112,176); the native
1488-- loader jumps straight to the body at offset 176 (NativePhysicalNative.alpha,
1489-- "byte 176") and never reads or verifies it, so the choice of digest does not
1490-- change what the emitted ELF executes
1491
1492def nativePhysicalGenerateImageWithBodyDigestForFormat =
1493 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1494 (lambda unrestricted digestOfBody : (pi unrestricted bodyInput : Bytes . Bytes) .
1495 (lambda unrestricted inputProgram : (family NativePhysicalProgram) .
1496 (eliminate
1497 NativePhysicalProgramValidation
1498 (lambda unrestricted current : (family NativePhysicalProgramValidation) .
1499 (family NativePhysicalImageResult))
1500 (nativePhysicalValidateProgram inputProgram)
1501 (branch
1502 NativePhysicalProgramValidated
1503 program
1504 validation
1505 .
1506 (eliminate
1507 NativePhysicalProgram
1508 (lambda unrestricted current : (family NativePhysicalProgram) .
1509 (family NativePhysicalImageResult))
1510 program
1511 (branch
1512 NativePhysicalProgramValue
1513 stateExtent
1514 resultSlots
1515 commands
1516 expected
1517 identity
1518 fallbacks
1519 .
1520 (eliminate
1521 NativePhysicalEncodedCommandsResult
1522 (lambda unrestricted current : (family NativePhysicalEncodedCommandsResult) .
1523 (family NativePhysicalImageResult))
1524 (nativePhysicalImageEncodeCommandsForFormat format commands)
1525 (branch
1526 NativePhysicalCommandsEncoded
1527 encoded
1528 .
1529 (eliminate
1530 NativePhysicalEncodedCommands
1531 (lambda unrestricted current : (family NativePhysicalEncodedCommands) .
1532 (family NativePhysicalImageResult))
1533 encoded
1534 (branch
1535 NativePhysicalEncodedCommandsValue
1536 body
1537 commandCount
1538 payloadBytes
1539 auxiliaryBytes
1540 errorBytes
1541 .
1542 (nat-eliminate
1543 (lambda unrestricted current : Nat . (family NativePhysicalImageResult))
1544 (nativePhysicalImageFail
1545 validation
1546 commandCount
1547 (bytes-length body)
1548 (constructor
1549 NativePhysicalImageErrorCode
1550 NativePhysicalImageCommandCountMismatch))
1551 (lambda unrestricted countPredecessor : Nat .
1552 (lambda unrestricted ignoredCount : (family NativePhysicalImageResult) .
1553 (eliminate
1554 NativeTelemetryCounterResult
1555 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
1556 (family NativePhysicalImageResult))
1557 (nativeTelemetryCounterFromNatural commandCount)
1558 (branch
1559 NativeTelemetryCounterSucceeded
1560 commandCountWord
1561 .
1562 (eliminate
1563 NativeTelemetryCounterResult
1564 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
1565 (family NativePhysicalImageResult))
1566 (nativeTelemetryCounterFromNatural (bytes-length body))
1567 (branch
1568 NativeTelemetryCounterSucceeded
1569 bodyExtent
1570 .
1571 (app
1572 (lambda unrestricted bodyDigest : Bytes .
1573 (app
1574 (lambda unrestricted output : Bytes .
1575 (app
1576 (lambda unrestricted telemetry : (family NativePhysicalImageTelemetry) .
1577 (constructor
1578 NativePhysicalImageResult
1579 NativePhysicalImageGenerated
1580 (constructor
1581 NativePhysicalImage
1582 NativePhysicalImageValue
1583 output
1584 bodyDigest
1585 identity
1586 commandCount
1587 stateExtent
1588 resultSlots
1589 telemetry)
1590 telemetry))
1591 (nativePhysicalImageTelemetryFor
1592 (nativePhysicalCommandsCounts commands)
1593 payloadBytes
1594 auxiliaryBytes
1595 errorBytes
1596 (bytes-length body)
1597 (bytes-length output)
1598 fallbacks
1599 identity
1600 bodyDigest)))
1601 (bytes-append
1602 (nativePhysicalImageMagicFor format)
1603 (bytes-append
1604 (nativePhysicalImageWord64Bytes (nativePhysicalImageVersionFor format))
1605 (bytes-append
1606 (nativePhysicalImageWord64Bytes commandCountWord)
1607 (bytes-append
1608 (nativePhysicalImageWord64Bytes stateExtent)
1609 (bytes-append
1610 (nativePhysicalImageWord64Bytes resultSlots)
1611 (bytes-append
1612 (nativePhysicalImageWord64Bytes bodyExtent)
1613 (bytes-append identity (bytes-append bodyDigest body))))))))))
1614 (digestOfBody body)))
1615 (branch
1616 NativeTelemetryCounterFailed
1617 counterError
1618 naturalValue
1619 .
1620 (nativePhysicalImageFail
1621 validation
1622 commandCount
1623 (bytes-length body)
1624 (constructor
1625 NativePhysicalImageErrorCode
1626 NativePhysicalImageExtentOverflow)))))
1627 (branch
1628 NativeTelemetryCounterFailed
1629 counterError
1630 naturalValue
1631 .
1632 (nativePhysicalImageFail
1633 validation
1634 commandCount
1635 (bytes-length body)
1636 (constructor
1637 NativePhysicalImageErrorCode
1638 NativePhysicalImageExtentOverflow))))))
1639 (naturalEqual commandCount expected)))))
1640 (branch
1641 NativePhysicalCommandsEncodingFailed
1642 error
1643 ordinal
1644 .
1645 (nativePhysicalImageFail validation ordinal zero error))))))
1646 (branch
1647 NativePhysicalProgramRejected
1648 programError
1649 validation
1650 .
1651 (nativePhysicalImageFail
1652 validation
1653 zero
1654 zero
1655 (constructor
1656 NativePhysicalImageErrorCode
1657 NativePhysicalImageProgramRejected
1658 programError)))))))
1659
1660-- Real body digest: the SHA-256 hex of the image body (unchanged behaviour for
1661-- every non-fast caller, e.g. Training/Inference receipt ELFs).
1662
1663def nativePhysicalGenerateImageWithBodyDigest =
1664 (nativePhysicalGenerateImageWithBodyDigestForFormat (constructor NativePhysicalImageFormat NativePhysicalImageCompactV4))
1665
1666def nativePhysicalImageRealBodyDigest =
1667 (lambda unrestricted bodyInput : Bytes . (sha256HexBytesOrEmpty (sha256Hex bodyInput)))
1668
1669-- Stub body digest for the FAST path: 64 zero bytes, matching the exact width of
1670-- the real 64-hex-char digest so the image layout (and the body offset 176 that
1671-- the loader jumps to) is byte-identical; only the inert digest field differs.
1672def nativePhysicalImageStubBodyDigest =
1673 (lambda unrestricted bodyInput : Bytes .
1674 (bytes
1675 0
1676 0
1677 0
1678 0
1679 0
1680 0
1681 0
1682 0
1683 0
1684 0
1685 0
1686 0
1687 0
1688 0
1689 0
1690 0
1691 0
1692 0
1693 0
1694 0
1695 0
1696 0
1697 0
1698 0
1699 0
1700 0
1701 0
1702 0
1703 0
1704 0
1705 0
1706 0
1707 0
1708 0
1709 0
1710 0
1711 0
1712 0
1713 0
1714 0
1715 0
1716 0
1717 0
1718 0
1719 0
1720 0
1721 0
1722 0
1723 0
1724 0
1725 0
1726 0
1727 0
1728 0
1729 0
1730 0
1731 0
1732 0
1733 0
1734 0
1735 0
1736 0
1737 0
1738 0))
1739
1740def nativePhysicalGenerateImage =
1741 (lambda unrestricted inputProgram : (family NativePhysicalProgram) .
1742 (nativePhysicalGenerateImageWithBodyDigest nativePhysicalImageRealBodyDigest inputProgram))
1743
1744def nativePhysicalGenerateImageFast =
1745 (lambda unrestricted inputProgram : (family NativePhysicalProgram) .
1746 (nativePhysicalGenerateImageWithBodyDigest nativePhysicalImageStubBodyDigest inputProgram))
1747
1748-- Reference encoder for native AArch64 programs (already in the target ABI).
1749def nativePhysicalGenerateImageAlignedFast =
1750 (nativePhysicalGenerateImageWithBodyDigestForFormat
1751 (constructor NativePhysicalImageFormat NativePhysicalImageAlignedV3)
1752 nativePhysicalImageStubBodyDigest)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.