1module Runtime.NativePhysicalImage
2
3import Data.SHA256Digest
4import Model.Config
5import Model.Parameter
6import Runtime.NativePhysicalProgram
7import Runtime.NativePhysicalImagePlan
8import Runtime.NativeTelemetry
9import Std.Natural
10
11family NativePhysicalImageErrorCode : Type 0
12constructor NativePhysicalImageProgramRejected
13field unrestricted nativePhysicalImageRejectedProgramError : (family NativePhysicalErrorCode)
14constructor NativePhysicalImageExtentOverflow
15constructor NativePhysicalImageCommandErrorIdentityEmpty
16constructor NativePhysicalImageCommandCountMismatch
17
18end-family
19
20family NativePhysicalImageResultDescriptor : Type 0
21constructor NativePhysicalImageResultDescriptorValue
22field unrestricted nativePhysicalImageResultKind : (family ModelWord64)
23field unrestricted nativePhysicalImageResultSlot : (family ModelWord64)
24
25end-family
26
27family NativePhysicalEncodedCommand : Type 0
28constructor NativePhysicalEncodedCommandValue
29field unrestricted nativePhysicalEncodedCommandBytes : Bytes
30field unrestricted nativePhysicalEncodedCommandPayloadBytes : Nat
31field unrestricted nativePhysicalEncodedCommandAuxiliaryBytes : Nat
32field unrestricted nativePhysicalEncodedCommandErrorBytes : Nat
33
34end-family
35
36family NativePhysicalEncodedCommandResult : Type 0
37constructor NativePhysicalCommandEncoded
38field unrestricted nativePhysicalEncodedCommand : (family NativePhysicalEncodedCommand)
39constructor NativePhysicalCommandEncodingFailed
40field unrestricted nativePhysicalCommandEncodingError : (family NativePhysicalImageErrorCode)
41
42end-family
43
44family NativePhysicalEncodedCommands : Type 0
45constructor NativePhysicalEncodedCommandsValue
46field unrestricted nativePhysicalEncodedCommandsBytes : Bytes
47field unrestricted nativePhysicalEncodedCommandsCount : Nat
48field unrestricted nativePhysicalEncodedCommandsPayloadBytes : Nat
49field unrestricted nativePhysicalEncodedCommandsAuxiliaryBytes : Nat
50field unrestricted nativePhysicalEncodedCommandsErrorBytes : Nat
51
52end-family
53
54family NativePhysicalEncodedCommandsResult : Type 0
55constructor NativePhysicalCommandsEncoded
56field unrestricted nativePhysicalEncodedCommands : (family NativePhysicalEncodedCommands)
57constructor NativePhysicalCommandsEncodingFailed
58field unrestricted nativePhysicalCommandsEncodingError : (family NativePhysicalImageErrorCode)
59field unrestricted nativePhysicalCommandsEncodingOrdinal : Nat
60
61end-family
62
63family NativePhysicalImageTelemetry : Type 0
64constructor NativePhysicalImageTelemetryValue
65field unrestricted nativePhysicalImageTelemetryCounts : (family NativePhysicalCounts)
66field unrestricted nativePhysicalImageTelemetryPayloadBytes : Nat
67field unrestricted nativePhysicalImageTelemetryAuxiliaryBytes : Nat
68field unrestricted nativePhysicalImageTelemetryErrorIdentityBytes : Nat
69field unrestricted nativePhysicalImageTelemetryBodyBytes : Nat
70field unrestricted nativePhysicalImageTelemetryOutputBytes : Nat
71field unrestricted nativePhysicalImageTelemetryFailures : Nat
72field unrestricted nativePhysicalImageTelemetryFallbacks : Nat
73field unrestricted nativePhysicalImageTelemetryIdentity : Bytes
74field unrestricted nativePhysicalImageTelemetryBodySHA256 : Bytes
75
76end-family
77
78family NativePhysicalImageFailureTelemetry : Type 0
79constructor NativePhysicalImageFailureTelemetryValue
80field unrestricted nativePhysicalImageFailureValidation : (family NativePhysicalValidationTelemetry)
81field unrestricted nativePhysicalImageFailureEncodedCommands : Nat
82field unrestricted nativePhysicalImageFailureBodyBytes : Nat
83field unrestricted nativePhysicalImageFailureCode : Bytes
84
85end-family
86
87family NativePhysicalImage : Type 0
88constructor NativePhysicalImageValue
89field unrestricted nativePhysicalImageBytes : Bytes
90field unrestricted nativePhysicalImageBodySHA256 : Bytes
91field unrestricted nativePhysicalImageProgramIdentity : Bytes
92field unrestricted nativePhysicalImageCommandCount : Nat
93field unrestricted nativePhysicalImageStateExtent : (family ModelWord64)
94field unrestricted nativePhysicalImageResultSlots : (family ModelWord64)
95field unrestricted nativePhysicalImageTelemetry : (family NativePhysicalImageTelemetry)
96
97end-family
98
99family NativePhysicalImageResult : Type 0
100constructor NativePhysicalImageGenerated
101field unrestricted nativePhysicalGeneratedImage : (family NativePhysicalImage)
102field unrestricted nativePhysicalImageSuccessTelemetry : (family NativePhysicalImageTelemetry)
103constructor NativePhysicalImageGenerationFailed
104field unrestricted nativePhysicalImageGenerationError : (family NativePhysicalImageErrorCode)
105field unrestricted nativePhysicalImageGenerationFailureTelemetry : (family NativePhysicalImageFailureTelemetry)
106
107end-family
108
109def nativePhysicalImageErrorCodeBytes =
110 (lambda unrestricted code : (family NativePhysicalImageErrorCode) .
111 (eliminate
112 NativePhysicalImageErrorCode
113 (lambda unrestricted current : (family NativePhysicalImageErrorCode) . Bytes)
114 code
115 (branch
116 NativePhysicalImageProgramRejected
117 programError
118 .
119 (bytes-append
120 b"ALPHA-PHYIMG-001-"
121 (nativePhysicalErrorCodeBytes programError)))
122 (branch
123 NativePhysicalImageExtentOverflow
124 .
125 b"ALPHA-PHYIMG-002")
126 (branch
127 NativePhysicalImageCommandErrorIdentityEmpty
128 .
129 b"ALPHA-PHYIMG-003")
130 (branch
131 NativePhysicalImageCommandCountMismatch
132 .
133 b"ALPHA-PHYIMG-004")))
134
135def nativePhysicalImageMagic : Bytes =
136 b"ALPXPHY2"
137
138def nativePhysicalImageVersion : (family ModelWord64) =
139 2
140
141def nativePhysicalImageZeroWord64 : (family ModelWord64) =
142 0
143
144def nativePhysicalImageWord64 =
145 (lambda unrestricted byte0 : Byte .
146 (constructor
147 ModelWord64
148 ModelWord64Value
149 byte0
150 (byte 0)
151 (byte 0)
152 (byte 0)
153 (byte 0)
154 (byte 0)
155 (byte 0)
156 (byte 0)))
157
158def nativePhysicalImageWord64Bytes =
159 (lambda unrestricted value : (family ModelWord64) .
160 (eliminate
161 ModelWord64
162 (lambda unrestricted current : (family ModelWord64) . Bytes)
163 value
164 (branch
165 ModelWord64Value
166 byte0
167 byte1
168 byte2
169 byte3
170 byte4
171 byte5
172 byte6
173 byte7
174 .
175 (bytes-cons
176 byte0
177 (bytes-cons
178 byte1
179 (bytes-cons
180 byte2
181 (bytes-cons
182 byte3
183 (bytes-cons byte4 (bytes-cons byte5 (bytes-cons byte6 (bytes-cons byte7 b"")))))))))))
184
185def nativePhysicalImageSlotWord =
186 (lambda unrestricted slot : (family NativePhysicalSlot) .
187 (eliminate
188 NativePhysicalSlot
189 (lambda unrestricted current : (family NativePhysicalSlot) . (family ModelWord64))
190 slot
191 (branch NativePhysicalSlotValue index . index)))
192
193def nativePhysicalImageResultDescriptor =
194 (lambda unrestricted binding : (family NativePhysicalResultBinding) .
195 (eliminate
196 NativePhysicalResultBinding
197 (lambda unrestricted current : (family NativePhysicalResultBinding) .
198 (family NativePhysicalImageResultDescriptor))
199 binding
200 (branch
201 NativePhysicalDiscardResult
202 .
203 (constructor
204 NativePhysicalImageResultDescriptor
205 NativePhysicalImageResultDescriptorValue
206 nativePhysicalImageZeroWord64
207 nativePhysicalImageZeroWord64))
208 (branch
209 NativePhysicalStoreResult
210 slot
211 .
212 (constructor
213 NativePhysicalImageResultDescriptor
214 NativePhysicalImageResultDescriptorValue
215 (nativePhysicalImageWord64 (byte 1))
216 (nativePhysicalImageSlotWord slot)))))
217
218def nativePhysicalImageOperandDescriptor =
219 (lambda unrestricted operand : (family NativePhysicalOperand) .
220 (eliminate
221 NativePhysicalOperand
222 (lambda unrestricted current : (family NativePhysicalOperand) . Bytes)
223 operand
224 (branch
225 NativePhysicalImmediate
226 value
227 .
228 (bytes-append
229 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 0)))
230 (bytes-append
231 (nativePhysicalImageWord64Bytes value)
232 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
233 (branch
234 NativePhysicalResultValue
235 slot
236 .
237 (bytes-append
238 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 1)))
239 (bytes-append
240 (nativePhysicalImageWord64Bytes (nativePhysicalImageSlotWord slot))
241 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
242 (branch
243 NativePhysicalResultAddress
244 slot
245 offset
246 .
247 (bytes-append
248 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 2)))
249 (bytes-append
250 (nativePhysicalImageWord64Bytes (nativePhysicalImageSlotWord slot))
251 (nativePhysicalImageWord64Bytes offset))))
252 (branch
253 NativePhysicalStateAddress
254 offset
255 .
256 (bytes-append
257 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 3)))
258 (bytes-append
259 (nativePhysicalImageWord64Bytes offset)
260 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
261 (branch
262 NativePhysicalStateLoad64
263 offset
264 .
265 (bytes-append
266 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 4)))
267 (bytes-append
268 (nativePhysicalImageWord64Bytes offset)
269 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
270 (branch
271 NativePhysicalPayloadAddress
272 offset
273 .
274 (bytes-append
275 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 5)))
276 (bytes-append
277 (nativePhysicalImageWord64Bytes offset)
278 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
279 (branch
280 NativePhysicalPayloadLoad64
281 offset
282 .
283 (bytes-append
284 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 6)))
285 (bytes-append
286 (nativePhysicalImageWord64Bytes offset)
287 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
288 (branch
289 NativePhysicalProcessArgument
290 index
291 .
292 (bytes-append
293 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 7)))
294 (bytes-append
295 (nativePhysicalImageWord64Bytes index)
296 (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))))
297 (branch
298 NativePhysicalLoopAffine
299 base
300 stride
301 .
302 (bytes-append
303 (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 8)))
304 (bytes-append
305 (nativePhysicalImageWord64Bytes base)
306 (nativePhysicalImageWord64Bytes stride))))))
307
308def nativePhysicalImageZeroOperand : (family NativePhysicalOperand) =
309 (constructor NativePhysicalOperand NativePhysicalImmediate nativePhysicalImageZeroWord64)
310
311def nativePhysicalImageSevenOperandBytes =
312 (lambda unrestricted operand0 : (family NativePhysicalOperand) .
313 (lambda unrestricted operand1 : (family NativePhysicalOperand) .
314 (lambda unrestricted operand2 : (family NativePhysicalOperand) .
315 (lambda unrestricted operand3 : (family NativePhysicalOperand) .
316 (lambda unrestricted operand4 : (family NativePhysicalOperand) .
317 (lambda unrestricted operand5 : (family NativePhysicalOperand) .
318 (lambda unrestricted operand6 : (family NativePhysicalOperand) .
319 (bytes-append
320 (nativePhysicalImageOperandDescriptor operand0)
321 (bytes-append
322 (nativePhysicalImageOperandDescriptor operand1)
323 (bytes-append
324 (nativePhysicalImageOperandDescriptor operand2)
325 (bytes-append
326 (nativePhysicalImageOperandDescriptor operand3)
327 (bytes-append
328 (nativePhysicalImageOperandDescriptor operand4)
329 (bytes-append
330 (nativePhysicalImageOperandDescriptor operand5)
331 (nativePhysicalImageOperandDescriptor operand6))))))))))))))
332
333def nativePhysicalImageSystemCallOperandBytes =
334 (lambda unrestricted number : (family NativePhysicalOperand) .
335 (lambda unrestricted arguments : (family NativePhysicalArguments) .
336 (eliminate
337 NativePhysicalArguments
338 (lambda unrestricted current : (family NativePhysicalArguments) . Bytes)
339 arguments
340 (branch
341 NativePhysicalArgumentsValue
342 arg0
343 arg1
344 arg2
345 arg3
346 arg4
347 arg5
348 .
349 (nativePhysicalImageSevenOperandBytes number arg0 arg1 arg2 arg3 arg4 arg5)))))
350
351def nativePhysicalImageRoutineOperandBytes =
352 (lambda unrestricted arguments : (family NativePhysicalArguments) .
353 (eliminate
354 NativePhysicalArguments
355 (lambda unrestricted current : (family NativePhysicalArguments) . Bytes)
356 arguments
357 (branch
358 NativePhysicalArgumentsValue
359 arg0
360 arg1
361 arg2
362 arg3
363 arg4
364 arg5
365 .
366 (nativePhysicalImageSevenOperandBytes
367 arg0
368 arg1
369 arg2
370 arg3
371 arg4
372 arg5
373 nativePhysicalImageZeroOperand))))
374
375def nativePhysicalImageCommandFixedBytes : Nat =
376 (byte-to-nat (byte 232))
377
378def nativePhysicalImageRecordAlignment : Nat =
379 (byte-to-nat (byte 4))
380
381-- Legacy V2 padded syscall payloads, but this does not align every record.
382-- Preserve its bytes for existing x86 artifacts. V3 separately pads the complete
383-- record without altering any content extent; Runtime.NativePhysicalImagePlan
384-- owns that wire contract and the AArch64 runtime requires it.
385def nativePhysicalImageSystemCallPayloadPadding =
386 (lambda unrestricted payloadLength : Nat .
387 (naturalModuloUnchecked
388 (naturalSaturatingSubtract
389 nativePhysicalImageRecordAlignment
390 (naturalModuloUnchecked payloadLength nativePhysicalImageRecordAlignment))
391 nativePhysicalImageRecordAlignment))
392
393def nativePhysicalImageZeroPad =
394 (lambda unrestricted count : Nat .
395 (nat-eliminate
396 (lambda unrestricted current : Nat . Bytes)
397 b""
398 (lambda unrestricted predecessor : Nat .
399 (lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction)))
400 count))
401
402def nativePhysicalImageAlignedSystemCallPayload =
403 (lambda unrestricted payload : Bytes .
404 (bytes-append
405 payload
406 (nativePhysicalImageZeroPad
407 (nativePhysicalImageSystemCallPayloadPadding (bytes-length payload)))))
408
409def nativePhysicalImageMagicFor =
410 (lambda unrestricted format : (family NativePhysicalImageFormat) .
411 (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . Bytes) format
412 (branch NativePhysicalImagePackedV2 . nativePhysicalImageMagic)
413 (branch NativePhysicalImageAlignedV3 . b"ALPXPHY3")))
414
415def nativePhysicalImageVersionFor =
416 (lambda unrestricted format : (family NativePhysicalImageFormat) .
417 (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . (family ModelWord64)) format
418 (branch NativePhysicalImagePackedV2 . nativePhysicalImageVersion)
419 (branch NativePhysicalImageAlignedV3 . (nativePhysicalImageWord64 (byte 3)))))
420
421def nativePhysicalImageRecordExtentFor =
422 (lambda unrestricted format : (family NativePhysicalImageFormat) .
423 (lambda unrestricted extent : Nat .
424 (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . Nat) format
425 (branch NativePhysicalImagePackedV2 . extent)
426 (branch NativePhysicalImageAlignedV3 . (nativePhysicalImageAlignedExtent extent)))))
427
428def nativePhysicalImageRecordPaddingFor =
429 (lambda unrestricted format : (family NativePhysicalImageFormat) .
430 (lambda unrestricted extent : Nat .
431 (naturalSaturatingSubtract (nativePhysicalImageRecordExtentFor format extent) extent)))
432
433def nativePhysicalImageCommandRecordForFormat =
434 (lambda unrestricted format : (family NativePhysicalImageFormat) .
435 (lambda unrestricted tag : Byte .
436 (lambda unrestricted binding : (family NativePhysicalResultBinding) .
437 (lambda unrestricted operands : Bytes .
438 (lambda unrestricted payload : Bytes .
439 (lambda unrestricted auxiliary : Bytes .
440 (lambda unrestricted errorIdentity : Bytes .
441 (nat-eliminate
442 (lambda unrestricted current : Nat . (family NativePhysicalEncodedCommandResult))
443 (constructor
444 NativePhysicalEncodedCommandResult
445 NativePhysicalCommandEncodingFailed
446 (constructor
447 NativePhysicalImageErrorCode
448 NativePhysicalImageCommandErrorIdentityEmpty))
449 (lambda unrestricted errorPredecessor : Nat .
450 (lambda unrestricted ignoredError : (family NativePhysicalEncodedCommandResult) .
451 (eliminate
452 NativeTelemetryCounterResult
453 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
454 (family NativePhysicalEncodedCommandResult))
455 (nativeTelemetryCounterFromNatural (bytes-length payload))
456 (branch
457 NativeTelemetryCounterSucceeded
458 payloadExtent
459 .
460 (eliminate
461 NativeTelemetryCounterResult
462 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
463 (family NativePhysicalEncodedCommandResult))
464 (nativeTelemetryCounterFromNatural (bytes-length auxiliary))
465 (branch
466 NativeTelemetryCounterSucceeded
467 auxiliaryExtent
468 .
469 (eliminate
470 NativeTelemetryCounterResult
471 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
472 (family NativePhysicalEncodedCommandResult))
473 (nativeTelemetryCounterFromNatural (bytes-length errorIdentity))
474 (branch
475 NativeTelemetryCounterSucceeded
476 errorExtent
477 .
478 (eliminate
479 NativeTelemetryCounterResult
480 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
481 (family NativePhysicalEncodedCommandResult))
482 (nativeTelemetryCounterFromNatural
483 (nativePhysicalImageRecordExtentFor format
484 (naturalAdd nativePhysicalImageCommandFixedBytes
485 (naturalAdd (bytes-length payload)
486 (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity))))))
487 (branch
488 NativeTelemetryCounterSucceeded
489 recordExtent
490 .
491 (eliminate
492 NativePhysicalImageResultDescriptor
493 (lambda unrestricted current : (family NativePhysicalImageResultDescriptor) .
494 (family NativePhysicalEncodedCommandResult))
495 (nativePhysicalImageResultDescriptor binding)
496 (branch
497 NativePhysicalImageResultDescriptorValue
498 resultKind
499 resultSlot
500 .
501 (constructor
502 NativePhysicalEncodedCommandResult
503 NativePhysicalCommandEncoded
504 (constructor
505 NativePhysicalEncodedCommand
506 NativePhysicalEncodedCommandValue
507 (bytes-append
508 (nativePhysicalImageWord64Bytes
509 (nativePhysicalImageWord64 tag))
510 (bytes-append
511 (nativePhysicalImageWord64Bytes recordExtent)
512 (bytes-append
513 (nativePhysicalImageWord64Bytes resultKind)
514 (bytes-append
515 (nativePhysicalImageWord64Bytes resultSlot)
516 (bytes-append
517 (nativePhysicalImageWord64Bytes payloadExtent)
518 (bytes-append
519 (nativePhysicalImageWord64Bytes auxiliaryExtent)
520 (bytes-append
521 (nativePhysicalImageWord64Bytes errorExtent)
522 (bytes-append
523 (nativePhysicalImageWord64Bytes
524 nativePhysicalImageZeroWord64)
525 (bytes-append
526 operands
527 (bytes-append
528 payload
529 (bytes-append auxiliary (bytes-append errorIdentity
530 (nativePhysicalImageZeroPad
531 (nativePhysicalImageRecordPaddingFor format
532 (naturalAdd nativePhysicalImageCommandFixedBytes
533 (naturalAdd (bytes-length payload)
534 (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity))))))))))))))))))
535 (bytes-length payload)
536 (bytes-length auxiliary)
537 (bytes-length errorIdentity))))))
538 (branch
539 NativeTelemetryCounterFailed
540 counterError
541 naturalValue
542 .
543 (constructor
544 NativePhysicalEncodedCommandResult
545 NativePhysicalCommandEncodingFailed
546 (constructor
547 NativePhysicalImageErrorCode
548 NativePhysicalImageExtentOverflow)))))
549 (branch
550 NativeTelemetryCounterFailed
551 counterError
552 naturalValue
553 .
554 (constructor
555 NativePhysicalEncodedCommandResult
556 NativePhysicalCommandEncodingFailed
557 (constructor
558 NativePhysicalImageErrorCode
559 NativePhysicalImageExtentOverflow)))))
560 (branch
561 NativeTelemetryCounterFailed
562 counterError
563 naturalValue
564 .
565 (constructor
566 NativePhysicalEncodedCommandResult
567 NativePhysicalCommandEncodingFailed
568 (constructor
569 NativePhysicalImageErrorCode
570 NativePhysicalImageExtentOverflow)))))
571 (branch
572 NativeTelemetryCounterFailed
573 counterError
574 naturalValue
575 .
576 (constructor
577 NativePhysicalEncodedCommandResult
578 NativePhysicalCommandEncodingFailed
579 (constructor
580 NativePhysicalImageErrorCode
581 NativePhysicalImageExtentOverflow))))))
582 (bytes-length errorIdentity)))))))))
583
584def nativePhysicalImageCommandRecord =
585 (nativePhysicalImageCommandRecordForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2))
586
587def nativePhysicalImageDiscardResult : (family NativePhysicalResultBinding) =
588 (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)
589
590-- the binary64 operations' record tags: 14 .. 21, in the family's order
591def nativePhysicalImageFloat64Tag =
592 (lambda unrestricted kind : (family NativePhysicalFloat64Operation) .
593 (eliminate NativePhysicalFloat64Operation
594 (lambda unrestricted current : (family NativePhysicalFloat64Operation) . Byte)
595 kind
596 (branch NativePhysicalFloat64Add . (byte 14))
597 (branch NativePhysicalFloat64Subtract . (byte 15))
598 (branch NativePhysicalFloat64Multiply . (byte 16))
599 (branch NativePhysicalFloat64Divide . (byte 17))
600 (branch NativePhysicalFloat64SquareRoot . (byte 18))
601 (branch NativePhysicalFloat64FromNatural . (byte 19))
602 (branch NativePhysicalFloat64ToBinary32 . (byte 20))
603 (branch NativePhysicalFloat64FromBinary32 . (byte 21))))
604
605def nativePhysicalImageEncodeOperationForFormat =
606 (lambda unrestricted format : (family NativePhysicalImageFormat) .
607 (lambda unrestricted operation : (family NativePhysicalOperation) .
608 (lambda unrestricted errorIdentity : Bytes .
609 (eliminate
610 NativePhysicalOperation
611 (lambda unrestricted current : (family NativePhysicalOperation) .
612 (family NativePhysicalEncodedCommandResult))
613 operation
614 (branch
615 NativePhysicalSystemCall
616 number
617 arguments
618 payload
619 result
620 .
621 (nativePhysicalImageCommandRecordForFormat format
622 (byte 1)
623 result
624 (nativePhysicalImageSystemCallOperandBytes number arguments)
625 (nativePhysicalImageAlignedSystemCallPayload payload)
626 b""
627 errorIdentity))
628 (branch
629 NativePhysicalCopyPayloadToState
630 destination
631 extent
632 payload
633 .
634 (nativePhysicalImageCommandRecordForFormat format
635 (byte 2)
636 nativePhysicalImageDiscardResult
637 (nativePhysicalImageSevenOperandBytes
638 (constructor NativePhysicalOperand NativePhysicalImmediate destination)
639 (constructor NativePhysicalOperand NativePhysicalImmediate extent)
640 nativePhysicalImageZeroOperand
641 nativePhysicalImageZeroOperand
642 nativePhysicalImageZeroOperand
643 nativePhysicalImageZeroOperand
644 nativePhysicalImageZeroOperand)
645 payload
646 b""
647 errorIdentity))
648 (branch
649 NativePhysicalMachineRoutine
650 code
651 arguments
652 result
653 .
654 (nativePhysicalImageCommandRecordForFormat format
655 (byte 3)
656 result
657 (nativePhysicalImageRoutineOperandBytes arguments)
658 code
659 b""
660 errorIdentity))
661 (branch
662 NativePhysicalFencePoll
663 address
664 expected
665 maximumPolls
666 .
667 (nativePhysicalImageCommandRecordForFormat format
668 (byte 4)
669 nativePhysicalImageDiscardResult
670 (nativePhysicalImageSevenOperandBytes
671 address
672 expected
673 (constructor NativePhysicalOperand NativePhysicalImmediate maximumPolls)
674 nativePhysicalImageZeroOperand
675 nativePhysicalImageZeroOperand
676 nativePhysicalImageZeroOperand
677 nativePhysicalImageZeroOperand)
678 b""
679 b""
680 errorIdentity))
681 (branch
682 NativePhysicalTelemetryAppend
683 path
684 record
685 .
686 (nativePhysicalImageCommandRecordForFormat format
687 (byte 5)
688 nativePhysicalImageDiscardResult
689 (nativePhysicalImageSevenOperandBytes
690 nativePhysicalImageZeroOperand
691 nativePhysicalImageZeroOperand
692 nativePhysicalImageZeroOperand
693 nativePhysicalImageZeroOperand
694 nativePhysicalImageZeroOperand
695 nativePhysicalImageZeroOperand
696 nativePhysicalImageZeroOperand)
697 path
698 record
699 errorIdentity))
700 (branch
701 NativePhysicalAssertEqual
702 left
703 right
704 error
705 .
706 (nativePhysicalImageCommandRecordForFormat format
707 (byte 6)
708 nativePhysicalImageDiscardResult
709 (nativePhysicalImageSevenOperandBytes
710 left
711 right
712 nativePhysicalImageZeroOperand
713 nativePhysicalImageZeroOperand
714 nativePhysicalImageZeroOperand
715 nativePhysicalImageZeroOperand
716 nativePhysicalImageZeroOperand)
717 b""
718 (nativePhysicalErrorCodeBytes error)
719 errorIdentity))
720 (branch
721 NativePhysicalAssertOneOf
722 observed
723 first
724 second
725 error
726 .
727 (nativePhysicalImageCommandRecordForFormat format
728 (byte 8)
729 nativePhysicalImageDiscardResult
730 (nativePhysicalImageSevenOperandBytes
731 observed
732 first
733 second
734 nativePhysicalImageZeroOperand
735 nativePhysicalImageZeroOperand
736 nativePhysicalImageZeroOperand
737 nativePhysicalImageZeroOperand)
738 b""
739 (nativePhysicalErrorCodeBytes error)
740 errorIdentity))
741 (branch
742 NativePhysicalHaltSuccess
743 .
744 (nativePhysicalImageCommandRecordForFormat format
745 (byte 7)
746 nativePhysicalImageDiscardResult
747 (nativePhysicalImageSevenOperandBytes
748 nativePhysicalImageZeroOperand
749 nativePhysicalImageZeroOperand
750 nativePhysicalImageZeroOperand
751 nativePhysicalImageZeroOperand
752 nativePhysicalImageZeroOperand
753 nativePhysicalImageZeroOperand
754 nativePhysicalImageZeroOperand)
755 b""
756 b""
757 errorIdentity))
758 (branch
759 NativePhysicalRepeatBegin
760 count
761 .
762 (nativePhysicalImageCommandRecordForFormat format
763 (byte 9)
764 nativePhysicalImageDiscardResult
765 (nativePhysicalImageSevenOperandBytes
766 (constructor NativePhysicalOperand NativePhysicalImmediate count)
767 nativePhysicalImageZeroOperand
768 nativePhysicalImageZeroOperand
769 nativePhysicalImageZeroOperand
770 nativePhysicalImageZeroOperand
771 nativePhysicalImageZeroOperand
772 nativePhysicalImageZeroOperand)
773 b""
774 b""
775 errorIdentity))
776 (branch
777 NativePhysicalRepeatEnd
778 .
779 (nativePhysicalImageCommandRecordForFormat format
780 (byte 10)
781 nativePhysicalImageDiscardResult
782 (nativePhysicalImageSevenOperandBytes
783 nativePhysicalImageZeroOperand
784 nativePhysicalImageZeroOperand
785 nativePhysicalImageZeroOperand
786 nativePhysicalImageZeroOperand
787 nativePhysicalImageZeroOperand
788 nativePhysicalImageZeroOperand
789 nativePhysicalImageZeroOperand)
790 b""
791 b""
792 errorIdentity))
793 (branch
794 NativePhysicalStoreWord64
795 destination
796 value
797 .
798 (nativePhysicalImageCommandRecordForFormat format
799 (byte 11)
800 nativePhysicalImageDiscardResult
801 (nativePhysicalImageSevenOperandBytes
802 destination
803 value
804 nativePhysicalImageZeroOperand
805 nativePhysicalImageZeroOperand
806 nativePhysicalImageZeroOperand
807 nativePhysicalImageZeroOperand
808 nativePhysicalImageZeroOperand)
809 b""
810 b""
811 errorIdentity))
812 (branch
813 NativePhysicalFenceWait
814 address
815 expected
816 maximumPolls
817 interval
818 .
819 (nativePhysicalImageCommandRecordForFormat format
820 (byte 12)
821 nativePhysicalImageDiscardResult
822 (nativePhysicalImageSevenOperandBytes
823 address
824 expected
825 (constructor NativePhysicalOperand NativePhysicalImmediate maximumPolls)
826 (constructor NativePhysicalOperand NativePhysicalImmediate interval)
827 nativePhysicalImageZeroOperand
828 nativePhysicalImageZeroOperand
829 nativePhysicalImageZeroOperand)
830 b""
831 b""
832 errorIdentity))
833 (branch
834 NativePhysicalRepeatBeginCounted
835 count
836 .
837 (nativePhysicalImageCommandRecordForFormat format
838 (byte 9)
839 nativePhysicalImageDiscardResult
840 (nativePhysicalImageSevenOperandBytes
841 count
842 nativePhysicalImageZeroOperand
843 nativePhysicalImageZeroOperand
844 nativePhysicalImageZeroOperand
845 nativePhysicalImageZeroOperand
846 nativePhysicalImageZeroOperand
847 nativePhysicalImageZeroOperand)
848 b""
849 b""
850 errorIdentity))
851 (branch
852 NativePhysicalAddWord64
853 destination
854 left
855 right
856 .
857 (nativePhysicalImageCommandRecordForFormat format
858 (byte 13)
859 nativePhysicalImageDiscardResult
860 (nativePhysicalImageSevenOperandBytes
861 destination
862 left
863 right
864 nativePhysicalImageZeroOperand
865 nativePhysicalImageZeroOperand
866 nativePhysicalImageZeroOperand
867 nativePhysicalImageZeroOperand)
868 b""
869 b""
870 errorIdentity))
871 (branch
872 NativePhysicalFloat64
873 kind
874 destination
875 left
876 right
877 .
878 (nativePhysicalImageCommandRecordForFormat format
879 (nativePhysicalImageFloat64Tag kind)
880 nativePhysicalImageDiscardResult
881 (nativePhysicalImageSevenOperandBytes
882 destination
883 left
884 right
885 nativePhysicalImageZeroOperand
886 nativePhysicalImageZeroOperand
887 nativePhysicalImageZeroOperand
888 nativePhysicalImageZeroOperand)
889 b""
890 b""
891 errorIdentity))))))
892
893def nativePhysicalImageEncodeOperation =
894 (nativePhysicalImageEncodeOperationForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2))
895
896def nativePhysicalImageEncodeCommandForFormat =
897 (lambda unrestricted format : (family NativePhysicalImageFormat) .
898 (lambda unrestricted command : (family NativePhysicalCommand) .
899 (eliminate
900 NativePhysicalCommand
901 (lambda unrestricted current : (family NativePhysicalCommand) .
902 (family NativePhysicalEncodedCommandResult))
903 command
904 (branch
905 NativePhysicalCommandValue
906 operation
907 errorIdentity
908 .
909 (nativePhysicalImageEncodeOperationForFormat format operation errorIdentity)))))
910
911def nativePhysicalImageEncodeCommand =
912 (nativePhysicalImageEncodeCommandForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2))
913
914def nativePhysicalImageEncodeCommandsForFormat =
915 (lambda unrestricted format : (family NativePhysicalImageFormat) .
916 (lambda unrestricted commands : (family NativePhysicalCommands) .
917 (eliminate
918 NativePhysicalCommands
919 (lambda unrestricted current : (family NativePhysicalCommands) .
920 (family NativePhysicalEncodedCommandsResult))
921 commands
922 (branch
923 NativePhysicalCommandsEnd
924 .
925 (constructor
926 NativePhysicalEncodedCommandsResult
927 NativePhysicalCommandsEncoded
928 (constructor
929 NativePhysicalEncodedCommands
930 NativePhysicalEncodedCommandsValue
931 b""
932 zero
933 zero
934 zero
935 zero)))
936 (branch
937 NativePhysicalCommandsNext
938 head
939 tail
940 induction
941 .
942 (eliminate
943 NativePhysicalEncodedCommandResult
944 (lambda unrestricted current : (family NativePhysicalEncodedCommandResult) .
945 (family NativePhysicalEncodedCommandsResult))
946 (nativePhysicalImageEncodeCommandForFormat format head)
947 (branch
948 NativePhysicalCommandEncoded
949 encoded
950 .
951 (eliminate
952 NativePhysicalEncodedCommandsResult
953 (lambda unrestricted current : (family NativePhysicalEncodedCommandsResult) .
954 (family NativePhysicalEncodedCommandsResult))
955 induction
956 (branch
957 NativePhysicalCommandsEncoded
958 encodedTail
959 .
960 (eliminate
961 NativePhysicalEncodedCommand
962 (lambda unrestricted current : (family NativePhysicalEncodedCommand) .
963 (family NativePhysicalEncodedCommandsResult))
964 encoded
965 (branch
966 NativePhysicalEncodedCommandValue
967 bytes
968 payloadBytes
969 auxiliaryBytes
970 errorBytes
971 .
972 (eliminate
973 NativePhysicalEncodedCommands
974 (lambda unrestricted current : (family NativePhysicalEncodedCommands) .
975 (family NativePhysicalEncodedCommandsResult))
976 encodedTail
977 (branch
978 NativePhysicalEncodedCommandsValue
979 tailBytes
980 tailCount
981 tailPayload
982 tailAuxiliary
983 tailError
984 .
985 (constructor
986 NativePhysicalEncodedCommandsResult
987 NativePhysicalCommandsEncoded
988 (constructor
989 NativePhysicalEncodedCommands
990 NativePhysicalEncodedCommandsValue
991 (bytes-append bytes tailBytes)
992 (succ tailCount)
993 (naturalAdd payloadBytes tailPayload)
994 (naturalAdd auxiliaryBytes tailAuxiliary)
995 (naturalAdd errorBytes tailError))))))))
996 (branch
997 NativePhysicalCommandsEncodingFailed
998 error
999 ordinal
1000 .
1001 (constructor
1002 NativePhysicalEncodedCommandsResult
1003 NativePhysicalCommandsEncodingFailed
1004 error
1005 (succ ordinal)))))
1006 (branch
1007 NativePhysicalCommandEncodingFailed
1008 error
1009 .
1010 (constructor
1011 NativePhysicalEncodedCommandsResult
1012 NativePhysicalCommandsEncodingFailed
1013 error
1014 zero)))))))
1015
1016-- The extent of the record nativePhysicalImageEncodeCommand writes for a
1017-- command: the fixed 232 bytes, the (aligned) payload, the auxiliary bytes and
1018-- the error identity -- the same fields, measured instead of written. Where a
1019-- MachineRoutine's code lands follows from these (see
1020-- nativePhysicalImageRecordAlignment).
1021def nativePhysicalImageCommandExtent =
1022 (lambda unrestricted command : (family NativePhysicalCommand) .
1023 (eliminate
1024 NativePhysicalCommand
1025 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
1026 command
1027 (branch NativePhysicalCommandValue operation errorIdentity .
1028 (naturalAdd nativePhysicalImageCommandFixedBytes
1029 (naturalAdd (bytes-length errorIdentity)
1030 (eliminate
1031 NativePhysicalOperation
1032 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
1033 operation
1034 (branch NativePhysicalSystemCall number arguments payload result .
1035 (naturalAdd (bytes-length payload) (nativePhysicalImageSystemCallPayloadPadding (bytes-length payload))))
1036 (branch NativePhysicalCopyPayloadToState destination extent payload . (bytes-length payload))
1037 (branch NativePhysicalMachineRoutine code arguments result . (bytes-length code))
1038 (branch NativePhysicalFencePoll address expected polls . zero)
1039 (branch NativePhysicalTelemetryAppend path record . (naturalAdd (bytes-length path) (bytes-length record)))
1040 (branch NativePhysicalAssertEqual left right error . (bytes-length (nativePhysicalErrorCodeBytes error)))
1041 (branch NativePhysicalAssertOneOf observed first second error . (bytes-length (nativePhysicalErrorCodeBytes error)))
1042 (branch NativePhysicalHaltSuccess . zero)
1043 (branch NativePhysicalRepeatBegin count . zero)
1044 (branch NativePhysicalRepeatEnd . zero)
1045 (branch NativePhysicalStoreWord64 destination value . zero)
1046 (branch NativePhysicalFenceWait address expected polls interval . zero)
1047 (branch NativePhysicalRepeatBeginCounted count . zero)
1048 (branch NativePhysicalAddWord64 destination left right . zero)
1049 (branch NativePhysicalFloat64 kind destination left right . zero)))))))
1050
1051def nativePhysicalImageEncodeCommands =
1052 (nativePhysicalImageEncodeCommandsForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2))
1053
1054def nativePhysicalImageFailureTelemetryFor =
1055 (lambda unrestricted validation : (family NativePhysicalValidationTelemetry) .
1056 (lambda unrestricted encoded : Nat .
1057 (lambda unrestricted bodyBytes : Nat .
1058 (lambda unrestricted error : (family NativePhysicalImageErrorCode) .
1059 (constructor
1060 NativePhysicalImageFailureTelemetry
1061 NativePhysicalImageFailureTelemetryValue
1062 validation
1063 encoded
1064 bodyBytes
1065 (nativePhysicalImageErrorCodeBytes error))))))
1066
1067def nativePhysicalImageFail =
1068 (lambda unrestricted validation : (family NativePhysicalValidationTelemetry) .
1069 (lambda unrestricted encoded : Nat .
1070 (lambda unrestricted bodyBytes : Nat .
1071 (lambda unrestricted error : (family NativePhysicalImageErrorCode) .
1072 (constructor
1073 NativePhysicalImageResult
1074 NativePhysicalImageGenerationFailed
1075 error
1076 (nativePhysicalImageFailureTelemetryFor validation encoded bodyBytes error))))))
1077
1078def nativePhysicalImageTelemetryFor =
1079 (lambda unrestricted counts : (family NativePhysicalCounts) .
1080 (lambda unrestricted payloadBytes : Nat .
1081 (lambda unrestricted auxiliaryBytes : Nat .
1082 (lambda unrestricted errorBytes : Nat .
1083 (lambda unrestricted bodyBytes : Nat .
1084 (lambda unrestricted outputBytes : Nat .
1085 (lambda unrestricted fallbacks : Nat .
1086 (lambda unrestricted identity : Bytes .
1087 (lambda unrestricted digest : Bytes .
1088 (constructor
1089 NativePhysicalImageTelemetry
1090 NativePhysicalImageTelemetryValue
1091 counts
1092 payloadBytes
1093 auxiliaryBytes
1094 errorBytes
1095 bodyBytes
1096 outputBytes
1097 zero
1098 fallbacks
1099 identity
1100 digest))))))))))
1101
1102-- Body-digest strategy is now a parameter so the FAST (GPU bring-up) ELF path
1103-- can supply a stub instead of paying for a real SHA-256 of the image body.
1104-- The digest lives in the image header's telemetry region [112,176); the native
1105-- loader jumps straight to the body at offset 176 (NativePhysicalNative.alpha,
1106-- "byte 176") and never reads or verifies it, so the choice of digest does not
1107-- change what the emitted ELF executes
1108
1109def nativePhysicalGenerateImageWithBodyDigestForFormat =
1110 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1111 (lambda unrestricted digestOfBody : (pi unrestricted bodyInput : Bytes . Bytes) .
1112 (lambda unrestricted inputProgram : (family NativePhysicalProgram) .
1113 (eliminate
1114 NativePhysicalProgramValidation
1115 (lambda unrestricted current : (family NativePhysicalProgramValidation) .
1116 (family NativePhysicalImageResult))
1117 (nativePhysicalValidateProgram inputProgram)
1118 (branch
1119 NativePhysicalProgramValidated
1120 program
1121 validation
1122 .
1123 (eliminate
1124 NativePhysicalProgram
1125 (lambda unrestricted current : (family NativePhysicalProgram) .
1126 (family NativePhysicalImageResult))
1127 program
1128 (branch
1129 NativePhysicalProgramValue
1130 stateExtent
1131 resultSlots
1132 commands
1133 expected
1134 identity
1135 fallbacks
1136 .
1137 (eliminate
1138 NativePhysicalEncodedCommandsResult
1139 (lambda unrestricted current : (family NativePhysicalEncodedCommandsResult) .
1140 (family NativePhysicalImageResult))
1141 (nativePhysicalImageEncodeCommandsForFormat format commands)
1142 (branch
1143 NativePhysicalCommandsEncoded
1144 encoded
1145 .
1146 (eliminate
1147 NativePhysicalEncodedCommands
1148 (lambda unrestricted current : (family NativePhysicalEncodedCommands) .
1149 (family NativePhysicalImageResult))
1150 encoded
1151 (branch
1152 NativePhysicalEncodedCommandsValue
1153 body
1154 commandCount
1155 payloadBytes
1156 auxiliaryBytes
1157 errorBytes
1158 .
1159 (nat-eliminate
1160 (lambda unrestricted current : Nat . (family NativePhysicalImageResult))
1161 (nativePhysicalImageFail
1162 validation
1163 commandCount
1164 (bytes-length body)
1165 (constructor
1166 NativePhysicalImageErrorCode
1167 NativePhysicalImageCommandCountMismatch))
1168 (lambda unrestricted countPredecessor : Nat .
1169 (lambda unrestricted ignoredCount : (family NativePhysicalImageResult) .
1170 (eliminate
1171 NativeTelemetryCounterResult
1172 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
1173 (family NativePhysicalImageResult))
1174 (nativeTelemetryCounterFromNatural commandCount)
1175 (branch
1176 NativeTelemetryCounterSucceeded
1177 commandCountWord
1178 .
1179 (eliminate
1180 NativeTelemetryCounterResult
1181 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
1182 (family NativePhysicalImageResult))
1183 (nativeTelemetryCounterFromNatural (bytes-length body))
1184 (branch
1185 NativeTelemetryCounterSucceeded
1186 bodyExtent
1187 .
1188 (app
1189 (lambda unrestricted bodyDigest : Bytes .
1190 (app
1191 (lambda unrestricted output : Bytes .
1192 (app
1193 (lambda unrestricted telemetry : (family NativePhysicalImageTelemetry) .
1194 (constructor
1195 NativePhysicalImageResult
1196 NativePhysicalImageGenerated
1197 (constructor
1198 NativePhysicalImage
1199 NativePhysicalImageValue
1200 output
1201 bodyDigest
1202 identity
1203 commandCount
1204 stateExtent
1205 resultSlots
1206 telemetry)
1207 telemetry))
1208 (nativePhysicalImageTelemetryFor
1209 (nativePhysicalCommandsCounts commands)
1210 payloadBytes
1211 auxiliaryBytes
1212 errorBytes
1213 (bytes-length body)
1214 (bytes-length output)
1215 fallbacks
1216 identity
1217 bodyDigest)))
1218 (bytes-append
1219 (nativePhysicalImageMagicFor format)
1220 (bytes-append
1221 (nativePhysicalImageWord64Bytes (nativePhysicalImageVersionFor format))
1222 (bytes-append
1223 (nativePhysicalImageWord64Bytes commandCountWord)
1224 (bytes-append
1225 (nativePhysicalImageWord64Bytes stateExtent)
1226 (bytes-append
1227 (nativePhysicalImageWord64Bytes resultSlots)
1228 (bytes-append
1229 (nativePhysicalImageWord64Bytes bodyExtent)
1230 (bytes-append identity (bytes-append bodyDigest body))))))))))
1231 (digestOfBody body)))
1232 (branch
1233 NativeTelemetryCounterFailed
1234 counterError
1235 naturalValue
1236 .
1237 (nativePhysicalImageFail
1238 validation
1239 commandCount
1240 (bytes-length body)
1241 (constructor
1242 NativePhysicalImageErrorCode
1243 NativePhysicalImageExtentOverflow)))))
1244 (branch
1245 NativeTelemetryCounterFailed
1246 counterError
1247 naturalValue
1248 .
1249 (nativePhysicalImageFail
1250 validation
1251 commandCount
1252 (bytes-length body)
1253 (constructor
1254 NativePhysicalImageErrorCode
1255 NativePhysicalImageExtentOverflow))))))
1256 (naturalEqual commandCount expected)))))
1257 (branch
1258 NativePhysicalCommandsEncodingFailed
1259 error
1260 ordinal
1261 .
1262 (nativePhysicalImageFail validation ordinal zero error))))))
1263 (branch
1264 NativePhysicalProgramRejected
1265 programError
1266 validation
1267 .
1268 (nativePhysicalImageFail
1269 validation
1270 zero
1271 zero
1272 (constructor
1273 NativePhysicalImageErrorCode
1274 NativePhysicalImageProgramRejected
1275 programError)))))))
1276
1277-- Real body digest: the SHA-256 hex of the image body (unchanged behaviour for
1278-- every non-fast caller, e.g. Training/Inference receipt ELFs).
1279
1280def nativePhysicalGenerateImageWithBodyDigest =
1281 (nativePhysicalGenerateImageWithBodyDigestForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2))
1282
1283def nativePhysicalImageRealBodyDigest =
1284 (lambda unrestricted bodyInput : Bytes . (sha256HexBytesOrEmpty (sha256Hex bodyInput)))
1285
1286-- Stub body digest for the FAST path: 64 zero bytes, matching the exact width of
1287-- the real 64-hex-char digest so the image layout (and the body offset 176 that
1288-- the loader jumps to) is byte-identical; only the inert digest field differs.
1289def nativePhysicalImageStubBodyDigest =
1290 (lambda unrestricted bodyInput : Bytes .
1291 (bytes
1292 0
1293 0
1294 0
1295 0
1296 0
1297 0
1298 0
1299 0
1300 0
1301 0
1302 0
1303 0
1304 0
1305 0
1306 0
1307 0
1308 0
1309 0
1310 0
1311 0
1312 0
1313 0
1314 0
1315 0
1316 0
1317 0
1318 0
1319 0
1320 0
1321 0
1322 0
1323 0
1324 0
1325 0
1326 0
1327 0
1328 0
1329 0
1330 0
1331 0
1332 0
1333 0
1334 0
1335 0
1336 0
1337 0
1338 0
1339 0
1340 0
1341 0
1342 0
1343 0
1344 0
1345 0
1346 0
1347 0
1348 0
1349 0
1350 0
1351 0
1352 0
1353 0
1354 0
1355 0))
1356
1357def nativePhysicalGenerateImage =
1358 (lambda unrestricted inputProgram : (family NativePhysicalProgram) .
1359 (nativePhysicalGenerateImageWithBodyDigest nativePhysicalImageRealBodyDigest inputProgram))
1360
1361def nativePhysicalGenerateImageFast =
1362 (lambda unrestricted inputProgram : (family NativePhysicalProgram) .
1363 (nativePhysicalGenerateImageWithBodyDigest nativePhysicalImageStubBodyDigest inputProgram))
1364
1365-- Reference encoder for native AArch64 programs (already in the target ABI).
1366def nativePhysicalGenerateImageAlignedFast =
1367 (nativePhysicalGenerateImageWithBodyDigestForFormat
1368 (constructor NativePhysicalImageFormat NativePhysicalImageAlignedV3)
1369 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.