1module Runtime.NativePhysicalNativeELF
2
3import Compiler.ELF
4import Compiler.MachineX86NativeAssembly
5import Data.Bytes
6import Data.SHA256Digest
7import Runtime.NativePhysicalImage
8import Runtime.NativePhysicalImagePlan
9import Runtime.NativePhysicalNative
10import Runtime.NativePhysicalProgram
11import Runtime.NativeResourcePlan
12import Std.Natural
13
14family NativePhysicalNativeELFErrorCode : Type 0
15constructor NativePhysicalNativeELFImageGenerationFailed
16field unrestricted nativePhysicalNativeELFImageError : (family NativePhysicalImageErrorCode)
17constructor NativePhysicalNativeELFDuplicateLabel
18field unrestricted nativePhysicalNativeELFDuplicateLabelName : Bytes
19constructor NativePhysicalNativeELFAssemblyOffsetOverflow
20constructor NativePhysicalNativeELFMissingLabel
21field unrestricted nativePhysicalNativeELFMissingLabelName : Bytes
22constructor NativePhysicalNativeELFDisplacementOutOfRange
23field unrestricted nativePhysicalNativeELFDistantLabelName : Bytes
24
25end-family
26
27family NativePhysicalNativeELFTelemetry : Type 0
28constructor NativePhysicalNativeELFTelemetryValue
29field unrestricted nativePhysicalNativeELFTelemetryCodeBytes : Nat
30field unrestricted nativePhysicalNativeELFTelemetryImageBytes : Nat
31field unrestricted nativePhysicalNativeELFTelemetryMachineBytes : Nat
32field unrestricted nativePhysicalNativeELFTelemetryELFBytes : Nat
33field unrestricted nativePhysicalNativeELFTelemetryFailures : Nat
34field unrestricted nativePhysicalNativeELFTelemetryFallbacks : Nat
35field unrestricted nativePhysicalNativeELFTelemetryProgramIdentity : Bytes
36field unrestricted nativePhysicalNativeELFTelemetryCodeSHA256 : Bytes
37field unrestricted nativePhysicalNativeELFTelemetryImageSHA256 : Bytes
38field unrestricted nativePhysicalNativeELFTelemetryMachineSHA256 : Bytes
39field unrestricted nativePhysicalNativeELFTelemetryELFSHA256 : Bytes
40
41end-family
42
43family NativePhysicalNativeELFFailureTelemetry : Type 0
44constructor NativePhysicalNativeELFFailureTelemetryValue
45field unrestricted nativePhysicalNativeELFFailurePhase : Bytes
46field unrestricted nativePhysicalNativeELFFailureCode : Bytes
47field unrestricted nativePhysicalNativeELFFailureImageTelemetry : Bytes
48field unrestricted nativePhysicalNativeELFFailureAssemblySubject : Bytes
49field unrestricted nativePhysicalNativeELFFailureCount : Nat
50field unrestricted nativePhysicalNativeELFFailureFallbacks : Nat
51
52end-family
53
54family NativePhysicalNativeELFArtifact : Type 0
55constructor NativePhysicalNativeELFArtifactValue
56field unrestricted nativePhysicalNativeELFBytes : Bytes
57field unrestricted nativePhysicalNativeCodeBytes : Bytes
58field unrestricted nativePhysicalNativeImageBytes : Bytes
59field unrestricted nativePhysicalNativeMachineBytes : Bytes
60field unrestricted nativePhysicalNativeProgramIdentity : Bytes
61field unrestricted nativePhysicalNativeCodeSHA256 : Bytes
62field unrestricted nativePhysicalNativeImageSHA256 : Bytes
63field unrestricted nativePhysicalNativeMachineSHA256 : Bytes
64field unrestricted nativePhysicalNativeELFSHA256 : Bytes
65field unrestricted nativePhysicalNativeCommandCount : Nat
66field unrestricted nativePhysicalNativeELFTelemetry : (family NativePhysicalNativeELFTelemetry)
67
68end-family
69
70family NativePhysicalNativeELFResult : Type 0
71constructor NativePhysicalNativeELFGenerated
72field unrestricted nativePhysicalNativeELFArtifact : (family NativePhysicalNativeELFArtifact)
73field unrestricted nativePhysicalNativeELFSuccessTelemetry : (family NativePhysicalNativeELFTelemetry)
74constructor NativePhysicalNativeELFGenerationFailed
75field unrestricted nativePhysicalNativeELFGenerationError : (family NativePhysicalNativeELFErrorCode)
76field unrestricted nativePhysicalNativeELFFailureTelemetry : (family NativePhysicalNativeELFFailureTelemetry)
77
78end-family
79
80def nativePhysicalNativeELFErrorCodeBytes =
81 (lambda unrestricted code : (family NativePhysicalNativeELFErrorCode) .
82 (eliminate
83 NativePhysicalNativeELFErrorCode
84 (lambda unrestricted current : (family NativePhysicalNativeELFErrorCode) . Bytes)
85 code
86 (branch
87 NativePhysicalNativeELFImageGenerationFailed
88 imageError
89 .
90 (bytes-append b"ALPHA-NELF-001-" (nativePhysicalImageErrorCodeBytes imageError)))
91 (branch
92 NativePhysicalNativeELFDuplicateLabel
93 labelName
94 .
95 (bytes-append b"ALPHA-NELF-002-" labelName))
96 (branch NativePhysicalNativeELFAssemblyOffsetOverflow . b"ALPHA-NELF-003")
97 (branch
98 NativePhysicalNativeELFMissingLabel
99 labelName
100 .
101 (bytes-append b"ALPHA-NELF-004-" labelName))
102 (branch
103 NativePhysicalNativeELFDisplacementOutOfRange
104 labelName
105 .
106 (bytes-append b"ALPHA-NELF-005-" labelName))))
107
108def nativePhysicalNativeELFImageFailurePhase : Bytes =
109 b"image-generation"
110
111def nativePhysicalNativeELFAssemblyFailurePhase : Bytes =
112 b"x86-assembly"
113
114def nativePhysicalNativeELFEncodeValidationTelemetry =
115 (lambda unrestricted telemetry : (family NativePhysicalValidationTelemetry) .
116 (eliminate
117 NativePhysicalValidationTelemetry
118 (lambda unrestricted current : (family NativePhysicalValidationTelemetry) . Bytes)
119 telemetry
120 (branch
121 NativePhysicalValidationTelemetryValue
122 counts
123 expected
124 stateExtent
125 resultSlots
126 fallbacks
127 identity
128 failures
129 ordinal
130 code
131 .
132 (bytes-append
133 identity
134 (bytes-append
135 (bytes 0)
136 (bytes-append
137 code
138 (bytes-append
139 (bytes 0)
140 (bytes
141 (nat-to-byte expected)
142 (nat-to-byte fallbacks)
143 (nat-to-byte failures)
144 (nat-to-byte ordinal)))))))))
145
146def nativePhysicalNativeELFEncodeImageFailureTelemetry =
147 (lambda unrestricted telemetry : (family NativePhysicalImageFailureTelemetry) .
148 (eliminate
149 NativePhysicalImageFailureTelemetry
150 (lambda unrestricted current : (family NativePhysicalImageFailureTelemetry) . Bytes)
151 telemetry
152 (branch
153 NativePhysicalImageFailureTelemetryValue
154 validation
155 encoded
156 bodyBytes
157 code
158 .
159 (bytes-append
160 (nativePhysicalNativeELFEncodeValidationTelemetry validation)
161 (bytes-append (bytes 0) code)))))
162
163def nativePhysicalNativeELFFailureTelemetryFor =
164 (lambda unrestricted phase : Bytes .
165 (lambda unrestricted code : (family NativePhysicalNativeELFErrorCode) .
166 (lambda unrestricted imageTelemetry : Bytes .
167 (lambda unrestricted subject : Bytes .
168 (constructor
169 NativePhysicalNativeELFFailureTelemetry
170 NativePhysicalNativeELFFailureTelemetryValue
171 phase
172 (nativePhysicalNativeELFErrorCodeBytes code)
173 imageTelemetry
174 subject
175 (succ zero)
176 zero)))))
177
178def nativePhysicalNativeELFFail =
179 (lambda unrestricted phase : Bytes .
180 (lambda unrestricted code : (family NativePhysicalNativeELFErrorCode) .
181 (lambda unrestricted imageTelemetry : Bytes .
182 (lambda unrestricted subject : Bytes .
183 (constructor
184 NativePhysicalNativeELFResult
185 NativePhysicalNativeELFGenerationFailed
186 code
187 (nativePhysicalNativeELFFailureTelemetryFor phase code imageTelemetry subject))))))
188
189def nativePhysicalNativeELFTelemetryFor =
190 (lambda unrestricted code : Bytes .
191 (lambda unrestricted image : Bytes .
192 (lambda unrestricted machine : Bytes .
193 (lambda unrestricted elf : Bytes .
194 (lambda unrestricted identity : Bytes .
195 (lambda unrestricted codeDigest : Bytes .
196 (lambda unrestricted imageDigest : Bytes .
197 (lambda unrestricted machineDigest : Bytes .
198 (lambda unrestricted elfDigest : Bytes .
199 (constructor
200 NativePhysicalNativeELFTelemetry
201 NativePhysicalNativeELFTelemetryValue
202 (bytes-length code)
203 (bytes-length image)
204 (bytes-length machine)
205 (bytes-length elf)
206 zero
207 zero
208 identity
209 codeDigest
210 imageDigest
211 machineDigest
212 elfDigest))))))))))
213
214def nativePhysicalGenerateNativeELF =
215 (lambda unrestricted program : (family NativePhysicalProgram) .
216 (eliminate
217 NativePhysicalImageResult
218 (lambda unrestricted current : (family NativePhysicalImageResult) .
219 (family NativePhysicalNativeELFResult))
220 (nativePhysicalGenerateImage program)
221 (branch
222 NativePhysicalImageGenerated
223 image
224 imageTelemetry
225 .
226 (eliminate
227 NativePhysicalImage
228 (lambda unrestricted current : (family NativePhysicalImage) .
229 (family NativePhysicalNativeELFResult))
230 image
231 (branch
232 NativePhysicalImageValue
233 imageBytes
234 bodyDigest
235 identity
236 commandCount
237 stateExtent
238 resultSlots
239 telemetry
240 .
241 (eliminate
242 X86NativeAssemblyResult
243 (lambda unrestricted current : (family X86NativeAssemblyResult) .
244 (family NativePhysicalNativeELFResult))
245 (x86NativeAssemble nativePhysicalNativeAssembly)
246 (branch
247 X86NativeAssemblyEncoded
248 codeBytes
249 .
250 (app
251 (lambda unrestricted machineBytes : Bytes .
252 (app
253 (lambda unrestricted elfBytes : Bytes .
254 (app
255 (lambda unrestricted codeSHA256 : Bytes .
256 (app
257 (lambda unrestricted imageSHA256 : Bytes .
258 (app
259 (lambda unrestricted machineSHA256 : Bytes .
260 (app
261 (lambda unrestricted elfSHA256 : Bytes .
262 (app
263 (lambda unrestricted artifactTelemetry : (family NativePhysicalNativeELFTelemetry) .
264 (constructor
265 NativePhysicalNativeELFResult
266 NativePhysicalNativeELFGenerated
267 (constructor
268 NativePhysicalNativeELFArtifact
269 NativePhysicalNativeELFArtifactValue
270 elfBytes
271 codeBytes
272 imageBytes
273 machineBytes
274 identity
275 codeSHA256
276 imageSHA256
277 machineSHA256
278 elfSHA256
279 commandCount
280 artifactTelemetry)
281 artifactTelemetry))
282 (nativePhysicalNativeELFTelemetryFor
283 codeBytes
284 imageBytes
285 machineBytes
286 elfBytes
287 identity
288 codeSHA256
289 imageSHA256
290 machineSHA256
291 elfSHA256)))
292 (sha256HexBytesOrEmpty (sha256Hex elfBytes))))
293 (sha256HexBytesOrEmpty (sha256Hex machineBytes))))
294 (sha256HexBytesOrEmpty (sha256Hex imageBytes))))
295 (sha256HexBytesOrEmpty (sha256Hex codeBytes))))
296 (wrapMachineCodeSparseLarge machineBytes)))
297 (bytes-append codeBytes imageBytes)))
298 (branch
299 X86NativeAssemblyEncodeDuplicateLabel
300 duplicateName
301 .
302 (nativePhysicalNativeELFFail
303 nativePhysicalNativeELFAssemblyFailurePhase
304 (constructor
305 NativePhysicalNativeELFErrorCode
306 NativePhysicalNativeELFDuplicateLabel
307 duplicateName)
308 b""
309 duplicateName))
310 (branch
311 X86NativeAssemblyEncodeOffsetOverflow
312 .
313 (nativePhysicalNativeELFFail
314 nativePhysicalNativeELFAssemblyFailurePhase
315 (constructor
316 NativePhysicalNativeELFErrorCode
317 NativePhysicalNativeELFAssemblyOffsetOverflow)
318 b""
319 b""))
320 (branch
321 X86NativeAssemblyMissingLabel
322 missingName
323 .
324 (nativePhysicalNativeELFFail
325 nativePhysicalNativeELFAssemblyFailurePhase
326 (constructor
327 NativePhysicalNativeELFErrorCode
328 NativePhysicalNativeELFMissingLabel
329 missingName)
330 b""
331 missingName))
332 (branch
333 X86NativeAssemblyDisplacementOutOfRange
334 distantName
335 .
336 (nativePhysicalNativeELFFail
337 nativePhysicalNativeELFAssemblyFailurePhase
338 (constructor
339 NativePhysicalNativeELFErrorCode
340 NativePhysicalNativeELFDisplacementOutOfRange
341 distantName)
342 b""
343 distantName))))))
344 (branch
345 NativePhysicalImageGenerationFailed
346 imageError
347 failureTelemetry
348 .
349 (nativePhysicalNativeELFFail
350 nativePhysicalNativeELFImageFailurePhase
351 (constructor
352 NativePhysicalNativeELFErrorCode
353 NativePhysicalNativeELFImageGenerationFailed
354 imageError)
355 (nativePhysicalNativeELFEncodeImageFailureTelemetry failureTelemetry)
356 b""))))
357
358-- FAST EMIT (GPU bring-up): runnable ELF, all SHA-256 digests stubbed so the
359-- emit is seconds instead of tens of minutes. The four receipt digests are
360-- separate telemetry fields (never in the elfBytes). The image BODY digest IS
361-- embedded in the elfBytes, but it sits in the inert header region [112,176)
362-- that the native loader skips (it jumps to the body at offset 176), so
363-- stubbing it (via nativePhysicalGenerateImageFast) leaves a byte-for-byte
364-- identical executable code+body -- only that inert 64-byte digest field is
365-- zeroed. sha256Hex over the body was the whole remaining cost (~54s per
366-- 512-bit block); everything else in the emit is already first-order (<3s).
367def nativePhysicalGenerateNativeELFFast =
368 (lambda unrestricted program : (family NativePhysicalProgram) .
369 (eliminate
370 NativePhysicalImageResult
371 (lambda unrestricted current : (family NativePhysicalImageResult) .
372 (family NativePhysicalNativeELFResult))
373 (nativePhysicalGenerateImageFast program)
374 (branch
375 NativePhysicalImageGenerated
376 image
377 imageTelemetry
378 .
379 (eliminate
380 NativePhysicalImage
381 (lambda unrestricted current : (family NativePhysicalImage) .
382 (family NativePhysicalNativeELFResult))
383 image
384 (branch
385 NativePhysicalImageValue
386 imageBytes
387 bodyDigest
388 identity
389 commandCount
390 stateExtent
391 resultSlots
392 telemetry
393 .
394 (eliminate
395 X86NativeAssemblyResult
396 (lambda unrestricted current : (family X86NativeAssemblyResult) .
397 (family NativePhysicalNativeELFResult))
398 (x86NativeAssemble nativePhysicalNativeAssembly)
399 (branch
400 X86NativeAssemblyEncoded
401 codeBytes
402 .
403 (app
404 (lambda unrestricted machineBytes : Bytes .
405 (app
406 (lambda unrestricted elfBytes : Bytes .
407 (app
408 (lambda unrestricted codeSHA256 : Bytes .
409 (app
410 (lambda unrestricted imageSHA256 : Bytes .
411 (app
412 (lambda unrestricted machineSHA256 : Bytes .
413 (app
414 (lambda unrestricted elfSHA256 : Bytes .
415 (app
416 (lambda unrestricted artifactTelemetry : (family NativePhysicalNativeELFTelemetry) .
417 (constructor
418 NativePhysicalNativeELFResult
419 NativePhysicalNativeELFGenerated
420 (constructor
421 NativePhysicalNativeELFArtifact
422 NativePhysicalNativeELFArtifactValue
423 elfBytes
424 codeBytes
425 imageBytes
426 machineBytes
427 identity
428 codeSHA256
429 imageSHA256
430 machineSHA256
431 elfSHA256
432 commandCount
433 artifactTelemetry)
434 artifactTelemetry))
435 (nativePhysicalNativeELFTelemetryFor
436 codeBytes
437 imageBytes
438 machineBytes
439 elfBytes
440 identity
441 codeSHA256
442 imageSHA256
443 machineSHA256
444 elfSHA256)))
445 b""))
446 b""))
447 b""))
448 b""))
449 (wrapMachineCodeSparseLarge machineBytes)))
450 (bytes-append codeBytes imageBytes)))
451 (branch
452 X86NativeAssemblyEncodeDuplicateLabel
453 duplicateName
454 .
455 (nativePhysicalNativeELFFail
456 nativePhysicalNativeELFAssemblyFailurePhase
457 (constructor
458 NativePhysicalNativeELFErrorCode
459 NativePhysicalNativeELFDuplicateLabel
460 duplicateName)
461 b""
462 duplicateName))
463 (branch
464 X86NativeAssemblyEncodeOffsetOverflow
465 .
466 (nativePhysicalNativeELFFail
467 nativePhysicalNativeELFAssemblyFailurePhase
468 (constructor
469 NativePhysicalNativeELFErrorCode
470 NativePhysicalNativeELFAssemblyOffsetOverflow)
471 b""
472 b""))
473 (branch
474 X86NativeAssemblyMissingLabel
475 missingName
476 .
477 (nativePhysicalNativeELFFail
478 nativePhysicalNativeELFAssemblyFailurePhase
479 (constructor
480 NativePhysicalNativeELFErrorCode
481 NativePhysicalNativeELFMissingLabel
482 missingName)
483 b""
484 missingName))
485 (branch
486 X86NativeAssemblyDisplacementOutOfRange
487 distantName
488 .
489 (nativePhysicalNativeELFFail
490 nativePhysicalNativeELFAssemblyFailurePhase
491 (constructor
492 NativePhysicalNativeELFErrorCode
493 NativePhysicalNativeELFDisplacementOutOfRange
494 distantName)
495 b""
496 distantName))))))
497 (branch
498 NativePhysicalImageGenerationFailed
499 imageError
500 failureTelemetry
501 .
502 (nativePhysicalNativeELFFail
503 nativePhysicalNativeELFImageFailurePhase
504 (constructor
505 NativePhysicalNativeELFErrorCode
506 NativePhysicalNativeELFImageGenerationFailed
507 imageError)
508 (nativePhysicalNativeELFEncodeImageFailureTelemetry failureTelemetry)
509 b""))))
510
511-- Whole-program publication path. The NativePhysicalProgram remains a
512-- checked Alpha value, while the compiler lowers its constructor tree to the
513-- ALPXPHY4 records in one backend operation. This is semantically the fast
514-- image encoder above (including the inert 64-byte zero digest), but avoids
515-- interpreting thousands of byte-building eliminators during compilation.
516-- The image is packed (Runtime.NativePhysicalImagePlan): the executable
517-- carries it compressed, and its load segment reserves the pages the
518-- interpreter unpacks it into, so nothing executes differently.
519def nativePhysicalPackedImageWord =
520 (lambda unrestricted container : Bytes .
521 (lambda unrestricted at : Nat .
522 (byte-to-nat (dataBytesByteAtValidated container at))))
523
524-- the unpacked image's length (container bytes 16 .. 23), page-rounded
525def nativePhysicalPackedImageReserve =
526 (lambda unrestricted container : Bytes .
527 (let unrestricted unpacked =
528 (naturalAdd (nativePhysicalPackedImageWord container 16)
529 (naturalAdd (naturalMultiply 256 (nativePhysicalPackedImageWord container 17))
530 (naturalAdd (naturalMultiply 65536 (nativePhysicalPackedImageWord container 18))
531 (naturalAdd (naturalMultiply 16777216 (nativePhysicalPackedImageWord container 19))
532 (naturalAdd (naturalMultiply 4294967296 (nativePhysicalPackedImageWord container 20))
533 (naturalAdd (naturalMultiply 1099511627776 (nativePhysicalPackedImageWord container 21))
534 (naturalAdd (naturalMultiply 281474976710656 (nativePhysicalPackedImageWord container 22))
535 (naturalMultiply 72057594037927936 (nativePhysicalPackedImageWord container 23)))))))))
536 in
537 (naturalMultiply elfPageBytes
538 (naturalDivideUnchecked (naturalAdd unpacked (naturalSaturatingSubtract elfPageBytes 1)) elfPageBytes))))
539
540def nativePhysicalGenerateNativeELFBytesDirect =
541 (lambda unrestricted program : (family NativePhysicalProgram) .
542 (let unrestricted container =
543 (compiler-native-encode
544 (family NativePhysicalPackedImage)
545 (constructor NativePhysicalPackedImage NativePhysicalPackedImageOf program))
546 in
547 (wrapMachineCodeSparseLargeReserving
548 (nativePhysicalPackedImageReserve container)
549 (bytes-append
550 (compiler-native-encode (family X86NativeAssembly) nativePhysicalNativeAssembly)
551 container))))
552
553-- The same executable with its image stored in place, uncompressed: for tests
554-- that alter individual command records in the file to exercise the
555-- interpreter's record validation.
556def nativePhysicalGenerateNativeELFBytesDirectUnpacked =
557 (lambda unrestricted program : (family NativePhysicalProgram) .
558 (wrapMachineCodeSparseLarge
559 (bytes-append
560 (compiler-native-encode (family X86NativeAssembly) nativePhysicalNativeAssembly)
561 (compiler-native-encode (family NativePhysicalProgram) program))))
562
563-- Final projection used by whole-program artifact roots. Failure stays
564-- fail-closed: the compiler's direct artifact writer rejects the empty value
565-- as a non-ELF instead of executing a generated emitter to discover it later.
566def nativePhysicalNativeELFResultBytes =
567 (lambda unrestricted result : (family NativePhysicalNativeELFResult) .
568 (eliminate
569 NativePhysicalNativeELFResult
570 (lambda unrestricted current : (family NativePhysicalNativeELFResult) . Bytes)
571 result
572 (branch
573 NativePhysicalNativeELFGenerated
574 artifact
575 successTelemetry
576 .
577 (eliminate
578 NativePhysicalNativeELFArtifact
579 (lambda unrestricted current : (family NativePhysicalNativeELFArtifact) . Bytes)
580 artifact
581 (branch
582 NativePhysicalNativeELFArtifactValue
583 elfBytes
584 codeBytes
585 imageBytes
586 machineBytes
587 identity
588 codeSHA
589 imageSHA
590 machineSHA
591 elfSHA
592 commandCount
593 telemetry
594 .
595 elfBytes)))
596 (branch NativePhysicalNativeELFGenerationFailed error telemetry . b"")))
597
598-- Deployment capacity admission precedes emission. The program remains the
599-- only source of state, result-slot and scratch sizes; the caller cannot
600-- substitute a smaller declared interpreter allocation.
601def nativePhysicalGenerateResourceELFBytesDirect =
602 (lambda unrestricted resources : (family NativeResourceContext) .
603 (lambda unrestricted program : (family NativePhysicalProgram) .
604 (nat-eliminate
605 (lambda unrestricted valid : Nat . Bytes)
606 b""
607 (lambda unrestricted prior : Nat .
608 (lambda unrestricted ignored : Bytes .
609 (nativePhysicalGenerateNativeELFBytesDirect program)))
610 (nativePhysicalResourcesAdmitted resources program))))
611
612-- The admitted executable with its image stored in place (record-mutation tests).
613def nativePhysicalGenerateResourceELFBytesDirectUnpacked =
614 (lambda unrestricted resources : (family NativeResourceContext) .
615 (lambda unrestricted program : (family NativePhysicalProgram) .
616 (nat-eliminate
617 (lambda unrestricted valid : Nat . Bytes)
618 b""
619 (lambda unrestricted prior : Nat .
620 (lambda unrestricted ignored : Bytes .
621 (nativePhysicalGenerateNativeELFBytesDirectUnpacked program)))
622 (nativePhysicalResourcesAdmitted resources program))))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.