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