1module Runtime.NativePhysicalEmbeddedArtifact
2
3import Data.Bytes
4import Model.Config
5import Model.Word32
6import Std.Natural
7
8-- Versioned envelope for a native ELF and the GPU artifacts it owns.
9-- Large materials remain runtime Bytes values and are joined through the
10-- runtime byte builder. No component is expanded into source-level literals.
11
12family NativePhysicalEmbeddedComponentKind : Type 0
13constructor NativePhysicalEmbeddedHostELF
14constructor NativePhysicalEmbeddedProgramTable
15constructor NativePhysicalEmbeddedQMDTable
16constructor NativePhysicalEmbeddedPushbuffer
17constructor NativePhysicalEmbeddedGPFIFO
18
19end-family
20
21family NativePhysicalEmbeddedPayload : Type 0
22constructor NativePhysicalEmbeddedPayloadValue
23field unrestricted nativePhysicalEmbeddedPayloadBytes : Bytes
24field unrestricted nativePhysicalEmbeddedPayloadIdentity : Bytes
25field unrestricted nativePhysicalEmbeddedPayloadSHA256 : Bytes
26
27end-family
28
29family NativePhysicalEmbeddedDescriptor : Type 0
30constructor NativePhysicalEmbeddedDescriptorValue
31field unrestricted nativePhysicalEmbeddedDescriptorKind : (family NativePhysicalEmbeddedComponentKind)
32field unrestricted nativePhysicalEmbeddedDescriptorOffset : Nat
33field unrestricted nativePhysicalEmbeddedDescriptorLength : Nat
34field unrestricted nativePhysicalEmbeddedDescriptorIdentity : Bytes
35field unrestricted nativePhysicalEmbeddedDescriptorSHA256 : Bytes
36
37end-family
38
39family NativePhysicalEmbeddedManifest : Type 0
40constructor NativePhysicalEmbeddedManifestValue
41field unrestricted nativePhysicalEmbeddedManifestVersion : Nat
42field unrestricted nativePhysicalEmbeddedManifestHost : (family NativePhysicalEmbeddedDescriptor)
43field unrestricted nativePhysicalEmbeddedManifestProgram : (family NativePhysicalEmbeddedDescriptor)
44field unrestricted nativePhysicalEmbeddedManifestQMD : (family NativePhysicalEmbeddedDescriptor)
45field unrestricted nativePhysicalEmbeddedManifestPushbuffer : (family NativePhysicalEmbeddedDescriptor)
46field unrestricted nativePhysicalEmbeddedManifestGPFIFO : (family NativePhysicalEmbeddedDescriptor)
47field unrestricted nativePhysicalEmbeddedManifestBytes : Bytes
48field unrestricted nativePhysicalEmbeddedManifestOffset : Nat
49field unrestricted nativePhysicalEmbeddedManifestArtifactLength : Nat
50
51end-family
52
53family NativePhysicalEmbeddedArtifact : Type 0
54constructor NativePhysicalEmbeddedArtifactValue
55field unrestricted nativePhysicalEmbeddedArtifactBytes : Bytes
56field unrestricted nativePhysicalEmbeddedArtifactManifest : (family NativePhysicalEmbeddedManifest)
57
58end-family
59
60-- Digests are observed independently by the native runtime hasher. The
61-- manifest parser never treats its own embedded claims as observations.
62family NativePhysicalEmbeddedObservedDigests : Type 0
63constructor NativePhysicalEmbeddedObservedDigestsValue
64field unrestricted nativePhysicalEmbeddedObservedHostSHA256 : Bytes
65field unrestricted nativePhysicalEmbeddedObservedProgramSHA256 : Bytes
66field unrestricted nativePhysicalEmbeddedObservedQMDSHA256 : Bytes
67field unrestricted nativePhysicalEmbeddedObservedPushbufferSHA256 : Bytes
68field unrestricted nativePhysicalEmbeddedObservedGPFIFOSHA256 : Bytes
69
70end-family
71
72family NativePhysicalEmbeddedErrorCode : Type 0
73constructor NativePhysicalEmbeddedBuildInputsInvalid
74constructor NativePhysicalEmbeddedLengthOverflow
75constructor NativePhysicalEmbeddedFooterInvalid
76constructor NativePhysicalEmbeddedManifestInvalid
77constructor NativePhysicalEmbeddedBoundsInvalid
78constructor NativePhysicalEmbeddedComponentHashMismatch
79
80end-family
81
82family NativePhysicalEmbeddedBuildResult : Type 0
83constructor NativePhysicalEmbeddedBuildSucceeded
84field unrestricted nativePhysicalEmbeddedBuiltArtifact : (family NativePhysicalEmbeddedArtifact)
85constructor NativePhysicalEmbeddedBuildFailed
86field unrestricted nativePhysicalEmbeddedBuildError : (family NativePhysicalEmbeddedErrorCode)
87
88end-family
89
90family NativePhysicalEmbeddedLoadResult : Type 0
91constructor NativePhysicalEmbeddedLoadSucceeded
92field unrestricted nativePhysicalEmbeddedLoadedArtifact : (family NativePhysicalEmbeddedArtifact)
93field unrestricted nativePhysicalEmbeddedLoadedHostELF : Bytes
94field unrestricted nativePhysicalEmbeddedLoadedProgramTable : Bytes
95field unrestricted nativePhysicalEmbeddedLoadedQMDTable : Bytes
96field unrestricted nativePhysicalEmbeddedLoadedPushbuffer : Bytes
97field unrestricted nativePhysicalEmbeddedLoadedGPFIFO : Bytes
98constructor NativePhysicalEmbeddedLoadFailed
99field unrestricted nativePhysicalEmbeddedLoadError : (family NativePhysicalEmbeddedErrorCode)
100
101end-family
102
103-- Eight-byte manifest magic: "ALPHAEMB".
104def nativePhysicalEmbeddedManifestMagic : Bytes =
105 b"ALPHAEMB"
106
107-- Eight-byte EOF footer magic: "ALPHAFTR".
108def nativePhysicalEmbeddedFooterMagic : Bytes =
109 b"ALPHAFTR"
110
111-- Canonical envelope version.
112def nativePhysicalEmbeddedVersion : Nat =
113 (succ zero)
114
115-- Owner identities remain the established 64-byte identity representation.
116def nativePhysicalEmbeddedIdentityLength : Nat =
117 (byte-to-nat (byte 64))
118
119-- SHA-256 is stored as its raw 32-byte digest.
120def nativePhysicalEmbeddedDigestLength : Nat =
121 (byte-to-nat (byte 32))
122
123-- Component digests are optional runtime evidence. Whole-program builds use
124-- this explicit sentinel rather than spending evaluator time hashing payloads
125-- that the Haskell artifact writer and receipt hash again after linking.
126def nativePhysicalEmbeddedDigestOmitted : Bytes =
127 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
128
129-- In-memory payload constructor for direct whole-program linking. The stable
130-- identity is kept typed and the material never becomes a path or temporary
131-- file.
132def nativePhysicalEmbeddedPayloadInMemory =
133 (lambda unrestricted identity : Bytes .
134 (lambda unrestricted material : Bytes .
135 (constructor
136 NativePhysicalEmbeddedPayload
137 NativePhysicalEmbeddedPayloadValue
138 material
139 identity
140 nativePhysicalEmbeddedDigestOmitted)))
141
142-- tag:u32 + offset:u32 + length:u32 + identity[64] + sha256[32].
143def nativePhysicalEmbeddedDescriptorLength : Nat =
144 (byte-to-nat (byte 108))
145
146-- magic[8] + version:u32 + five 108-byte component descriptors.
147def nativePhysicalEmbeddedManifestLength : Nat =
148 552
149
150-- magic[8] + manifest-offset:u32 + manifest-length:u32.
151def nativePhysicalEmbeddedFooterLength : Nat =
152 (byte-to-nat (byte 16))
153
154-- Version 1 uses canonical unsigned 32-bit offsets and lengths.
155def nativePhysicalEmbeddedMaximumLength : Nat =
156 4294967295
157
158-- Stable descriptor tags, in physical layout order.
159def nativePhysicalEmbeddedComponentTag =
160 (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) .
161 (eliminate
162 NativePhysicalEmbeddedComponentKind
163 (lambda unrestricted current : (family NativePhysicalEmbeddedComponentKind) . Nat)
164 kind
165 (branch NativePhysicalEmbeddedHostELF . (succ zero))
166 (branch NativePhysicalEmbeddedProgramTable . (byte-to-nat (byte 2)))
167 (branch NativePhysicalEmbeddedQMDTable . (byte-to-nat (byte 3)))
168 (branch NativePhysicalEmbeddedPushbuffer . (byte-to-nat (byte 4)))
169 (branch NativePhysicalEmbeddedGPFIFO . (byte-to-nat (byte 5)))))
170
171-- Canonical little-endian u32 encoder for bounded manifest fields.
172def nativePhysicalEmbeddedWord32Bytes =
173 (lambda unrestricted value : Nat .
174 (dataBytesWord32LE (modelWord32FromNaturalTruncated value)))
175
176-- Efficiently joins two immutable byte values without source expansion.
177def nativePhysicalEmbeddedJoin =
178 (lambda unrestricted left : Bytes .
179 (lambda unrestricted right : Bytes .
180 (bytes-builder-build
181 (bytes-builder-append
182 (bytes-builder-chunk left)
183 (bytes-builder-chunk right)))))
184
185-- Returns the material bytes of a payload.
186def nativePhysicalEmbeddedPayloadMaterial =
187 (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) .
188 (eliminate
189 NativePhysicalEmbeddedPayload
190 (lambda unrestricted current : (family NativePhysicalEmbeddedPayload) . Bytes)
191 payload
192 (branch NativePhysicalEmbeddedPayloadValue material identity digest . material)))
193
194-- Returns the stable owner identity of a payload.
195def nativePhysicalEmbeddedPayloadIdentityValue =
196 (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) .
197 (eliminate
198 NativePhysicalEmbeddedPayload
199 (lambda unrestricted current : (family NativePhysicalEmbeddedPayload) . Bytes)
200 payload
201 (branch NativePhysicalEmbeddedPayloadValue material identity digest . identity)))
202
203-- Returns the independently established raw SHA-256 of a payload.
204def nativePhysicalEmbeddedPayloadDigestValue =
205 (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) .
206 (eliminate
207 NativePhysicalEmbeddedPayload
208 (lambda unrestricted current : (family NativePhysicalEmbeddedPayload) . Bytes)
209 payload
210 (branch NativePhysicalEmbeddedPayloadValue material identity digest . digest)))
211
212-- Payload admission is non-empty and fixes identity/hash widths.
213def nativePhysicalEmbeddedPayloadValid =
214 (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) .
215 (naturalAnd
216 (naturalNonzero (bytes-length (nativePhysicalEmbeddedPayloadMaterial payload)))
217 (naturalAnd
218 (naturalEqual
219 (bytes-length (nativePhysicalEmbeddedPayloadIdentityValue payload))
220 nativePhysicalEmbeddedIdentityLength)
221 (naturalEqual
222 (bytes-length (nativePhysicalEmbeddedPayloadDigestValue payload))
223 nativePhysicalEmbeddedDigestLength))))
224
225-- Constructs a typed descriptor from an admitted payload and physical offset.
226def nativePhysicalEmbeddedMakeDescriptor =
227 (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) .
228 (lambda unrestricted offset : Nat .
229 (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) .
230 (constructor
231 NativePhysicalEmbeddedDescriptor
232 NativePhysicalEmbeddedDescriptorValue
233 kind
234 offset
235 (bytes-length (nativePhysicalEmbeddedPayloadMaterial payload))
236 (nativePhysicalEmbeddedPayloadIdentityValue payload)
237 (nativePhysicalEmbeddedPayloadDigestValue payload)))))
238
239-- Canonical fixed-width descriptor encoding.
240def nativePhysicalEmbeddedDescriptorBytes =
241 (lambda unrestricted descriptor : (family NativePhysicalEmbeddedDescriptor) .
242 (eliminate
243 NativePhysicalEmbeddedDescriptor
244 (lambda unrestricted current : (family NativePhysicalEmbeddedDescriptor) . Bytes)
245 descriptor
246 (branch
247 NativePhysicalEmbeddedDescriptorValue
248 kind
249 offset
250 length
251 identity
252 digest
253 .
254 (bytes-builder-build
255 (bytes-builder-append
256 (bytes-builder-chunk
257 (nativePhysicalEmbeddedWord32Bytes (nativePhysicalEmbeddedComponentTag kind)))
258 (bytes-builder-append
259 (bytes-builder-chunk (nativePhysicalEmbeddedWord32Bytes offset))
260 (bytes-builder-append
261 (bytes-builder-chunk (nativePhysicalEmbeddedWord32Bytes length))
262 (bytes-builder-append
263 (bytes-builder-chunk identity)
264 (bytes-builder-chunk digest)))))))))
265
266-- Fixed-width descriptor encoding for large-artifact packagers. Callers that
267-- already proved their u32 bounds can supply the canonical words directly and
268-- avoid reducing million-sized offsets through unary Nat arithmetic.
269def nativePhysicalEmbeddedDescriptorFixedWidthBytes =
270 (lambda unrestricted tag : (family ModelWord32) .
271 (lambda unrestricted offset : (family ModelWord32) .
272 (lambda unrestricted length : (family ModelWord32) .
273 (lambda unrestricted identity : Bytes .
274 (lambda unrestricted digest : Bytes .
275 (bytes-builder-build
276 (bytes-builder-append
277 (bytes-builder-chunk (dataBytesWord32LE tag))
278 (bytes-builder-append
279 (bytes-builder-chunk (dataBytesWord32LE offset))
280 (bytes-builder-append
281 (bytes-builder-chunk (dataBytesWord32LE length))
282 (bytes-builder-append
283 (bytes-builder-chunk identity)
284 (bytes-builder-chunk digest)))))))))))
285
286-- Fixed-width canonical manifest assembly. Each input is one canonical
287-- 108-byte descriptor produced by the function above.
288def nativePhysicalEmbeddedManifestFixedWidthBytes =
289 (lambda unrestricted host : Bytes .
290 (lambda unrestricted program : Bytes .
291 (lambda unrestricted qmd : Bytes .
292 (lambda unrestricted pushbuffer : Bytes .
293 (lambda unrestricted gpfifo : Bytes .
294 (bytes-builder-build
295 (bytes-builder-append
296 (bytes-builder-chunk nativePhysicalEmbeddedManifestMagic)
297 (bytes-builder-append
298 (bytes-builder-chunk (dataBytesWord32LE modelWord32One))
299 (bytes-builder-append
300 (bytes-builder-chunk host)
301 (bytes-builder-append
302 (bytes-builder-chunk program)
303 (bytes-builder-append
304 (bytes-builder-chunk qmd)
305 (bytes-builder-append
306 (bytes-builder-chunk pushbuffer)
307 (bytes-builder-chunk gpfifo)))))))))))))
308
309-- Canonical version-1 manifest encoding.
310def nativePhysicalEmbeddedManifestCanonicalBytes =
311 (lambda unrestricted host : (family NativePhysicalEmbeddedDescriptor) .
312 (lambda unrestricted program : (family NativePhysicalEmbeddedDescriptor) .
313 (lambda unrestricted qmd : (family NativePhysicalEmbeddedDescriptor) .
314 (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedDescriptor) .
315 (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedDescriptor) .
316 (bytes-builder-build
317 (bytes-builder-append
318 (bytes-builder-chunk nativePhysicalEmbeddedManifestMagic)
319 (bytes-builder-append
320 (bytes-builder-chunk
321 (nativePhysicalEmbeddedWord32Bytes nativePhysicalEmbeddedVersion))
322 (bytes-builder-append
323 (bytes-builder-chunk (nativePhysicalEmbeddedDescriptorBytes host))
324 (bytes-builder-append
325 (bytes-builder-chunk (nativePhysicalEmbeddedDescriptorBytes program))
326 (bytes-builder-append
327 (bytes-builder-chunk (nativePhysicalEmbeddedDescriptorBytes qmd))
328 (bytes-builder-append
329 (bytes-builder-chunk (nativePhysicalEmbeddedDescriptorBytes pushbuffer))
330 (bytes-builder-chunk
331 (nativePhysicalEmbeddedDescriptorBytes gpfifo))))))))))))))
332
333-- Canonical EOF locator encoding.
334def nativePhysicalEmbeddedFooterBytes =
335 (lambda unrestricted manifestOffset : Nat .
336 (bytes-builder-build
337 (bytes-builder-append
338 (bytes-builder-chunk nativePhysicalEmbeddedFooterMagic)
339 (bytes-builder-append
340 (bytes-builder-chunk (nativePhysicalEmbeddedWord32Bytes manifestOffset))
341 (bytes-builder-chunk
342 (nativePhysicalEmbeddedWord32Bytes nativePhysicalEmbeddedManifestLength))))))
343
344-- Fixed-width EOF locator matching nativePhysicalEmbeddedFooterBytes without
345-- a large Nat-to-Word32 reduction in the packager evaluator.
346def nativePhysicalEmbeddedFooterFixedWidthBytes =
347 (lambda unrestricted manifestOffset : (family ModelWord32) .
348 (bytes-builder-build
349 (bytes-builder-append
350 (bytes-builder-chunk nativePhysicalEmbeddedFooterMagic)
351 (bytes-builder-append
352 (bytes-builder-chunk (dataBytesWord32LE manifestOffset))
353 (bytes-builder-chunk
354 (dataBytesWord32LE
355 (constructor
356 ModelWord32
357 ModelWord32Value
358 (byte 40) (byte 2) (byte 0) (byte 0))))))))
359
360-- Assembles already-admitted payloads without re-copying them through source
361-- syntax. The runtime builder performs one final materialization.
362def nativePhysicalEmbeddedAssemble =
363 (lambda unrestricted host : (family NativePhysicalEmbeddedPayload) .
364 (lambda unrestricted program : (family NativePhysicalEmbeddedPayload) .
365 (lambda unrestricted qmd : (family NativePhysicalEmbeddedPayload) .
366 (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedPayload) .
367 (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedPayload) .
368 (let unrestricted hostLength =
369 (bytes-length (nativePhysicalEmbeddedPayloadMaterial host))
370 in
371 (let unrestricted programOffset = hostLength in
372 (let unrestricted qmdOffset =
373 (naturalAdd
374 programOffset
375 (bytes-length (nativePhysicalEmbeddedPayloadMaterial program)))
376 in
377 (let unrestricted pushbufferOffset =
378 (naturalAdd
379 qmdOffset
380 (bytes-length (nativePhysicalEmbeddedPayloadMaterial qmd)))
381 in
382 (let unrestricted gpfifoOffset =
383 (naturalAdd
384 pushbufferOffset
385 (bytes-length (nativePhysicalEmbeddedPayloadMaterial pushbuffer)))
386 in
387 (let unrestricted manifestOffset =
388 (naturalAdd
389 gpfifoOffset
390 (bytes-length (nativePhysicalEmbeddedPayloadMaterial gpfifo)))
391 in
392 (let unrestricted artifactLength =
393 (naturalAdd
394 manifestOffset
395 (naturalAdd
396 nativePhysicalEmbeddedManifestLength
397 nativePhysicalEmbeddedFooterLength))
398 in
399 (let unrestricted hostDescriptor =
400 (nativePhysicalEmbeddedMakeDescriptor
401 (constructor
402 NativePhysicalEmbeddedComponentKind
403 NativePhysicalEmbeddedHostELF)
404 zero
405 host)
406 in
407 (let unrestricted programDescriptor =
408 (nativePhysicalEmbeddedMakeDescriptor
409 (constructor
410 NativePhysicalEmbeddedComponentKind
411 NativePhysicalEmbeddedProgramTable)
412 programOffset
413 program)
414 in
415 (let unrestricted qmdDescriptor =
416 (nativePhysicalEmbeddedMakeDescriptor
417 (constructor
418 NativePhysicalEmbeddedComponentKind
419 NativePhysicalEmbeddedQMDTable)
420 qmdOffset
421 qmd)
422 in
423 (let unrestricted pushbufferDescriptor =
424 (nativePhysicalEmbeddedMakeDescriptor
425 (constructor
426 NativePhysicalEmbeddedComponentKind
427 NativePhysicalEmbeddedPushbuffer)
428 pushbufferOffset
429 pushbuffer)
430 in
431 (let unrestricted gpfifoDescriptor =
432 (nativePhysicalEmbeddedMakeDescriptor
433 (constructor
434 NativePhysicalEmbeddedComponentKind
435 NativePhysicalEmbeddedGPFIFO)
436 gpfifoOffset
437 gpfifo)
438 in
439 (let unrestricted manifestBytes =
440 (nativePhysicalEmbeddedManifestCanonicalBytes
441 hostDescriptor
442 programDescriptor
443 qmdDescriptor
444 pushbufferDescriptor
445 gpfifoDescriptor)
446 in
447 (let unrestricted footerBytes =
448 (nativePhysicalEmbeddedFooterBytes manifestOffset)
449 in
450 (let unrestricted artifactBytes =
451 (bytes-builder-build
452 (bytes-builder-append
453 (bytes-builder-chunk
454 (nativePhysicalEmbeddedPayloadMaterial host))
455 (bytes-builder-append
456 (bytes-builder-chunk
457 (nativePhysicalEmbeddedPayloadMaterial program))
458 (bytes-builder-append
459 (bytes-builder-chunk
460 (nativePhysicalEmbeddedPayloadMaterial qmd))
461 (bytes-builder-append
462 (bytes-builder-chunk
463 (nativePhysicalEmbeddedPayloadMaterial pushbuffer))
464 (bytes-builder-append
465 (bytes-builder-chunk
466 (nativePhysicalEmbeddedPayloadMaterial gpfifo))
467 (bytes-builder-append
468 (bytes-builder-chunk manifestBytes)
469 (bytes-builder-chunk footerBytes))))))))
470 in
471 (let unrestricted manifest =
472 (constructor
473 NativePhysicalEmbeddedManifest
474 NativePhysicalEmbeddedManifestValue
475 nativePhysicalEmbeddedVersion
476 hostDescriptor
477 programDescriptor
478 qmdDescriptor
479 pushbufferDescriptor
480 gpfifoDescriptor
481 manifestBytes
482 manifestOffset
483 artifactLength)
484 in
485 (constructor
486 NativePhysicalEmbeddedBuildResult
487 NativePhysicalEmbeddedBuildSucceeded
488 (constructor
489 NativePhysicalEmbeddedArtifact
490 NativePhysicalEmbeddedArtifactValue
491 artifactBytes
492 manifest)))))))))))))))))))))))
493
494-- Validates every fixed-width input before assembling the artifact.
495def nativePhysicalEmbeddedBuild =
496 (lambda unrestricted host : (family NativePhysicalEmbeddedPayload) .
497 (lambda unrestricted program : (family NativePhysicalEmbeddedPayload) .
498 (lambda unrestricted qmd : (family NativePhysicalEmbeddedPayload) .
499 (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedPayload) .
500 (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedPayload) .
501 (let unrestricted totalLength =
502 (naturalAdd
503 (bytes-length (nativePhysicalEmbeddedPayloadMaterial host))
504 (naturalAdd
505 (bytes-length (nativePhysicalEmbeddedPayloadMaterial program))
506 (naturalAdd
507 (bytes-length (nativePhysicalEmbeddedPayloadMaterial qmd))
508 (naturalAdd
509 (bytes-length (nativePhysicalEmbeddedPayloadMaterial pushbuffer))
510 (naturalAdd
511 (bytes-length (nativePhysicalEmbeddedPayloadMaterial gpfifo))
512 (naturalAdd
513 nativePhysicalEmbeddedManifestLength
514 nativePhysicalEmbeddedFooterLength))))))
515 in
516 (let unrestricted inputsValid =
517 (naturalAnd
518 (nativePhysicalEmbeddedPayloadValid host)
519 (naturalAnd
520 (nativePhysicalEmbeddedPayloadValid program)
521 (naturalAnd
522 (nativePhysicalEmbeddedPayloadValid qmd)
523 (naturalAnd
524 (nativePhysicalEmbeddedPayloadValid pushbuffer)
525 (nativePhysicalEmbeddedPayloadValid gpfifo)))))
526 in
527 (nat-eliminate
528 (lambda unrestricted current : Nat . (family NativePhysicalEmbeddedBuildResult))
529 (constructor
530 NativePhysicalEmbeddedBuildResult
531 NativePhysicalEmbeddedBuildFailed
532 (constructor
533 NativePhysicalEmbeddedErrorCode
534 NativePhysicalEmbeddedBuildInputsInvalid))
535 (lambda unrestricted inputsPredecessor : Nat .
536 (lambda unrestricted inputsInduction : (family NativePhysicalEmbeddedBuildResult) .
537 (nat-eliminate
538 (lambda unrestricted current : Nat . (family NativePhysicalEmbeddedBuildResult))
539 (constructor
540 NativePhysicalEmbeddedBuildResult
541 NativePhysicalEmbeddedBuildFailed
542 (constructor
543 NativePhysicalEmbeddedErrorCode
544 NativePhysicalEmbeddedLengthOverflow))
545 (lambda unrestricted lengthPredecessor : Nat .
546 (lambda unrestricted lengthInduction : (family NativePhysicalEmbeddedBuildResult) .
547 (nativePhysicalEmbeddedAssemble host program qmd pushbuffer gpfifo)))
548 (naturalLessOrEqual totalLength nativePhysicalEmbeddedMaximumLength))))
549 inputsValid))))))))
550
551-- Direct artifact projection. An invalid component set becomes empty bytes,
552-- which the compiler's ELF writer rejects without running an intermediate
553-- packager executable.
554def nativePhysicalEmbeddedBuildResultBytes =
555 (lambda unrestricted result : (family NativePhysicalEmbeddedBuildResult) .
556 (eliminate
557 NativePhysicalEmbeddedBuildResult
558 (lambda unrestricted current : (family NativePhysicalEmbeddedBuildResult) . Bytes)
559 result
560 (branch
561 NativePhysicalEmbeddedBuildSucceeded
562 artifact
563 .
564 (eliminate
565 NativePhysicalEmbeddedArtifact
566 (lambda unrestricted current : (family NativePhysicalEmbeddedArtifact) . Bytes)
567 artifact
568 (branch NativePhysicalEmbeddedArtifactValue bytes manifest . bytes)))
569 (branch NativePhysicalEmbeddedBuildFailed error . b"")))
570
571-- Bounded exact slice used by the manifest decoder. Empty means failure;
572-- admitted components are non-empty, so the sentinel is unambiguous.
573def nativePhysicalEmbeddedSliceOrEmpty =
574 (lambda unrestricted input : Bytes .
575 (lambda unrestricted offset : Nat .
576 (lambda unrestricted length : Nat .
577 (eliminate
578 DataBytesSliceResult
579 (lambda unrestricted current : (family DataBytesSliceResult) . Bytes)
580 (dataBytesSlice input offset length)
581 (branch
582 DataBytesSliceSucceeded
583 slice
584 telemetry
585 .
586 (eliminate
587 DataBytesResult
588 (lambda unrestricted current : (family DataBytesResult) . Bytes)
589 (dataBytesSliceToBytes slice)
590 (branch DataBytesSucceeded value materialTelemetry . value)
591 (branch DataBytesFailed code materialTelemetry . b"")))
592 (branch DataBytesSliceFailed code telemetry . b"")))))
593
594-- Bounded little-endian u32 reader; zero is a fail-closed sentinel.
595def nativePhysicalEmbeddedWord32At =
596 (lambda unrestricted input : Bytes .
597 (lambda unrestricted offset : Nat .
598 (eliminate
599 DataBytesWord32ExactDecodeResult
600 (lambda unrestricted current : (family DataBytesWord32ExactDecodeResult) . Nat)
601 (dataBytesDecodeWord32LEExact
602 (nativePhysicalEmbeddedSliceOrEmpty input offset (byte-to-nat (byte 4))))
603 (branch DataBytesWord32ExactlyDecoded value telemetry . (modelWord32ToNatural value))
604 (branch DataBytesWord32ExactDecodeFailed code telemetry . zero))))
605
606-- Decodes one descriptor at its fixed manifest offset.
607def nativePhysicalEmbeddedDescriptorAt =
608 (lambda unrestricted manifestBytes : Bytes .
609 (lambda unrestricted descriptorOffset : Nat .
610 (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) .
611 (constructor
612 NativePhysicalEmbeddedDescriptor
613 NativePhysicalEmbeddedDescriptorValue
614 kind
615 (nativePhysicalEmbeddedWord32At
616 manifestBytes
617 (naturalAdd descriptorOffset (byte-to-nat (byte 4))))
618 (nativePhysicalEmbeddedWord32At
619 manifestBytes
620 (naturalAdd descriptorOffset (byte-to-nat (byte 8))))
621 (nativePhysicalEmbeddedSliceOrEmpty
622 manifestBytes
623 (naturalAdd descriptorOffset (byte-to-nat (byte 12)))
624 nativePhysicalEmbeddedIdentityLength)
625 (nativePhysicalEmbeddedSliceOrEmpty
626 manifestBytes
627 (naturalAdd descriptorOffset (byte-to-nat (byte 76)))
628 nativePhysicalEmbeddedDigestLength)))))
629
630-- Descriptor field projections used by bounds and hash validation.
631def nativePhysicalEmbeddedDescriptorOffsetValue =
632 (lambda unrestricted descriptor : (family NativePhysicalEmbeddedDescriptor) .
633 (eliminate
634 NativePhysicalEmbeddedDescriptor
635 (lambda unrestricted current : (family NativePhysicalEmbeddedDescriptor) . Nat)
636 descriptor
637 (branch NativePhysicalEmbeddedDescriptorValue kind offset length identity digest . offset)))
638
639def nativePhysicalEmbeddedDescriptorLengthValue =
640 (lambda unrestricted descriptor : (family NativePhysicalEmbeddedDescriptor) .
641 (eliminate
642 NativePhysicalEmbeddedDescriptor
643 (lambda unrestricted current : (family NativePhysicalEmbeddedDescriptor) . Nat)
644 descriptor
645 (branch NativePhysicalEmbeddedDescriptorValue kind offset length identity digest . length)))
646
647def nativePhysicalEmbeddedDescriptorDigestValue =
648 (lambda unrestricted descriptor : (family NativePhysicalEmbeddedDescriptor) .
649 (eliminate
650 NativePhysicalEmbeddedDescriptor
651 (lambda unrestricted current : (family NativePhysicalEmbeddedDescriptor) . Bytes)
652 descriptor
653 (branch NativePhysicalEmbeddedDescriptorValue kind offset length identity digest . digest)))
654
655def nativePhysicalEmbeddedDescriptorTagAt =
656 (lambda unrestricted manifestBytes : Bytes .
657 (lambda unrestricted descriptorOffset : Nat .
658 (nativePhysicalEmbeddedWord32At manifestBytes descriptorOffset)))
659
660-- Version-1 descriptors must be contiguous and end exactly at the manifest.
661def nativePhysicalEmbeddedLayoutValid =
662 (lambda unrestricted host : (family NativePhysicalEmbeddedDescriptor) .
663 (lambda unrestricted program : (family NativePhysicalEmbeddedDescriptor) .
664 (lambda unrestricted qmd : (family NativePhysicalEmbeddedDescriptor) .
665 (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedDescriptor) .
666 (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedDescriptor) .
667 (lambda unrestricted manifestOffset : Nat .
668 (naturalAnd
669 (naturalNonzero (nativePhysicalEmbeddedDescriptorLengthValue host))
670 (naturalAnd
671 (naturalEqual (nativePhysicalEmbeddedDescriptorOffsetValue host) zero)
672 (naturalAnd
673 (naturalEqual
674 (nativePhysicalEmbeddedDescriptorOffsetValue program)
675 (nativePhysicalEmbeddedDescriptorLengthValue host))
676 (naturalAnd
677 (naturalEqual
678 (nativePhysicalEmbeddedDescriptorOffsetValue qmd)
679 (naturalAdd
680 (nativePhysicalEmbeddedDescriptorOffsetValue program)
681 (nativePhysicalEmbeddedDescriptorLengthValue program)))
682 (naturalAnd
683 (naturalEqual
684 (nativePhysicalEmbeddedDescriptorOffsetValue pushbuffer)
685 (naturalAdd
686 (nativePhysicalEmbeddedDescriptorOffsetValue qmd)
687 (nativePhysicalEmbeddedDescriptorLengthValue qmd)))
688 (naturalAnd
689 (naturalEqual
690 (nativePhysicalEmbeddedDescriptorOffsetValue gpfifo)
691 (naturalAdd
692 (nativePhysicalEmbeddedDescriptorOffsetValue pushbuffer)
693 (nativePhysicalEmbeddedDescriptorLengthValue pushbuffer)))
694 (naturalEqual
695 manifestOffset
696 (naturalAdd
697 (nativePhysicalEmbeddedDescriptorOffsetValue gpfifo)
698 (nativePhysicalEmbeddedDescriptorLengthValue gpfifo)))))))))))))))
699
700-- Compares manifest claims only with independently observed raw digests.
701def nativePhysicalEmbeddedHashesValid =
702 (lambda unrestricted host : (family NativePhysicalEmbeddedDescriptor) .
703 (lambda unrestricted program : (family NativePhysicalEmbeddedDescriptor) .
704 (lambda unrestricted qmd : (family NativePhysicalEmbeddedDescriptor) .
705 (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedDescriptor) .
706 (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedDescriptor) .
707 (lambda unrestricted observed : (family NativePhysicalEmbeddedObservedDigests) .
708 (eliminate
709 NativePhysicalEmbeddedObservedDigests
710 (lambda unrestricted current : (family NativePhysicalEmbeddedObservedDigests) . Nat)
711 observed
712 (branch
713 NativePhysicalEmbeddedObservedDigestsValue
714 hostDigest
715 programDigest
716 qmdDigest
717 pushbufferDigest
718 gpfifoDigest
719 .
720 (naturalAnd
721 (naturalEqual (bytes-length hostDigest) nativePhysicalEmbeddedDigestLength)
722 (naturalAnd
723 (bytes-equal
724 (nativePhysicalEmbeddedDescriptorDigestValue host)
725 hostDigest)
726 (naturalAnd
727 (bytes-equal
728 (nativePhysicalEmbeddedDescriptorDigestValue program)
729 programDigest)
730 (naturalAnd
731 (bytes-equal
732 (nativePhysicalEmbeddedDescriptorDigestValue qmd)
733 qmdDigest)
734 (naturalAnd
735 (bytes-equal
736 (nativePhysicalEmbeddedDescriptorDigestValue pushbuffer)
737 pushbufferDigest)
738 (bytes-equal
739 (nativePhysicalEmbeddedDescriptorDigestValue gpfifo)
740 gpfifoDigest))))))))))))))
741
742-- Decodes and validates an artifact after the native hasher has supplied all
743-- five observations. No bytes reach GPU submission through a failed result.
744def nativePhysicalEmbeddedLoad =
745 (lambda unrestricted artifactBytes : Bytes .
746 (lambda unrestricted observed : (family NativePhysicalEmbeddedObservedDigests) .
747 (let unrestricted artifactLength = (bytes-length artifactBytes) in
748 (let unrestricted footerOffset =
749 (naturalSaturatingSubtract artifactLength nativePhysicalEmbeddedFooterLength)
750 in
751 (let unrestricted footerBytes =
752 (nativePhysicalEmbeddedSliceOrEmpty
753 artifactBytes
754 footerOffset
755 nativePhysicalEmbeddedFooterLength)
756 in
757 (let unrestricted manifestLength =
758 nativePhysicalEmbeddedManifestLength
759 in
760 (let unrestricted manifestOffset =
761 (naturalSaturatingSubtract footerOffset manifestLength)
762 in
763 (let unrestricted manifestBytes =
764 (nativePhysicalEmbeddedSliceOrEmpty
765 artifactBytes
766 manifestOffset
767 manifestLength)
768 in
769 (let unrestricted footerValid =
770 (naturalAnd
771 (naturalLessOrEqual nativePhysicalEmbeddedFooterLength artifactLength)
772 (naturalAnd
773 (bytes-equal
774 (nativePhysicalEmbeddedSliceOrEmpty
775 footerBytes
776 zero
777 (byte-to-nat (byte 8)))
778 nativePhysicalEmbeddedFooterMagic)
779 (naturalAnd
780 (bytes-equal
781 (nativePhysicalEmbeddedSliceOrEmpty
782 footerBytes
783 (byte-to-nat (byte 8))
784 (byte-to-nat (byte 4)))
785 (nativePhysicalEmbeddedWord32Bytes manifestOffset))
786 (bytes-equal
787 (nativePhysicalEmbeddedSliceOrEmpty
788 footerBytes
789 (byte-to-nat (byte 12))
790 (byte-to-nat (byte 4)))
791 (nativePhysicalEmbeddedWord32Bytes manifestLength)))))
792 in
793 (let unrestricted manifestValid =
794 (naturalAnd
795 (naturalEqual
796 (bytes-length manifestBytes)
797 nativePhysicalEmbeddedManifestLength)
798 (naturalAnd
799 (bytes-equal
800 (nativePhysicalEmbeddedSliceOrEmpty
801 manifestBytes
802 zero
803 (byte-to-nat (byte 8)))
804 nativePhysicalEmbeddedManifestMagic)
805 (naturalEqual
806 (nativePhysicalEmbeddedWord32At
807 manifestBytes
808 (byte-to-nat (byte 8)))
809 nativePhysicalEmbeddedVersion)))
810 in
811 (let unrestricted host =
812 (nativePhysicalEmbeddedDescriptorAt
813 manifestBytes
814 (byte-to-nat (byte 12))
815 (constructor
816 NativePhysicalEmbeddedComponentKind
817 NativePhysicalEmbeddedHostELF))
818 in
819 (let unrestricted program =
820 (nativePhysicalEmbeddedDescriptorAt
821 manifestBytes
822 (byte-to-nat (byte 120))
823 (constructor
824 NativePhysicalEmbeddedComponentKind
825 NativePhysicalEmbeddedProgramTable))
826 in
827 (let unrestricted qmd =
828 (nativePhysicalEmbeddedDescriptorAt
829 manifestBytes
830 (byte-to-nat (byte 228))
831 (constructor
832 NativePhysicalEmbeddedComponentKind
833 NativePhysicalEmbeddedQMDTable))
834 in
835 (let unrestricted pushbuffer =
836 (nativePhysicalEmbeddedDescriptorAt
837 manifestBytes
838 336
839 (constructor
840 NativePhysicalEmbeddedComponentKind
841 NativePhysicalEmbeddedPushbuffer))
842 in
843 (let unrestricted gpfifo =
844 (nativePhysicalEmbeddedDescriptorAt
845 manifestBytes
846 444
847 (constructor
848 NativePhysicalEmbeddedComponentKind
849 NativePhysicalEmbeddedGPFIFO))
850 in
851 (let unrestricted tagsValid =
852 (naturalAnd
853 (naturalEqual
854 (nativePhysicalEmbeddedDescriptorTagAt
855 manifestBytes
856 (byte-to-nat (byte 12)))
857 (succ zero))
858 (naturalAnd
859 (naturalEqual
860 (nativePhysicalEmbeddedDescriptorTagAt
861 manifestBytes
862 (byte-to-nat (byte 120)))
863 (byte-to-nat (byte 2)))
864 (naturalAnd
865 (naturalEqual
866 (nativePhysicalEmbeddedDescriptorTagAt
867 manifestBytes
868 (byte-to-nat (byte 228)))
869 (byte-to-nat (byte 3)))
870 (naturalAnd
871 (naturalEqual
872 (nativePhysicalEmbeddedDescriptorTagAt
873 manifestBytes
874 336)
875 (byte-to-nat (byte 4)))
876 (naturalEqual
877 (nativePhysicalEmbeddedDescriptorTagAt
878 manifestBytes
879 444)
880 (byte-to-nat (byte 5)))))))
881 in
882 (let unrestricted layoutValid =
883 (nativePhysicalEmbeddedLayoutValid
884 host
885 program
886 qmd
887 pushbuffer
888 gpfifo
889 manifestOffset)
890 in
891 (let unrestricted hashesValid =
892 (nativePhysicalEmbeddedHashesValid
893 host
894 program
895 qmd
896 pushbuffer
897 gpfifo
898 observed)
899 in
900 (let unrestricted allValid =
901 (naturalAnd
902 footerValid
903 (naturalAnd
904 manifestValid
905 (naturalAnd tagsValid (naturalAnd layoutValid hashesValid))))
906 in
907 (nat-eliminate
908 (lambda unrestricted current : Nat .
909 (family NativePhysicalEmbeddedLoadResult))
910 (constructor
911 NativePhysicalEmbeddedLoadResult
912 NativePhysicalEmbeddedLoadFailed
913 (constructor
914 NativePhysicalEmbeddedErrorCode
915 NativePhysicalEmbeddedManifestInvalid))
916 (lambda unrestricted validPredecessor : Nat .
917 (lambda unrestricted validInduction :
918 (family NativePhysicalEmbeddedLoadResult) .
919 (let unrestricted hostBytes =
920 (nativePhysicalEmbeddedSliceOrEmpty
921 artifactBytes
922 (nativePhysicalEmbeddedDescriptorOffsetValue host)
923 (nativePhysicalEmbeddedDescriptorLengthValue host))
924 in
925 (let unrestricted programBytes =
926 (nativePhysicalEmbeddedSliceOrEmpty
927 artifactBytes
928 (nativePhysicalEmbeddedDescriptorOffsetValue program)
929 (nativePhysicalEmbeddedDescriptorLengthValue program))
930 in
931 (let unrestricted qmdBytes =
932 (nativePhysicalEmbeddedSliceOrEmpty
933 artifactBytes
934 (nativePhysicalEmbeddedDescriptorOffsetValue qmd)
935 (nativePhysicalEmbeddedDescriptorLengthValue qmd))
936 in
937 (let unrestricted pushbufferBytes =
938 (nativePhysicalEmbeddedSliceOrEmpty
939 artifactBytes
940 (nativePhysicalEmbeddedDescriptorOffsetValue pushbuffer)
941 (nativePhysicalEmbeddedDescriptorLengthValue pushbuffer))
942 in
943 (let unrestricted gpfifoBytes =
944 (nativePhysicalEmbeddedSliceOrEmpty
945 artifactBytes
946 (nativePhysicalEmbeddedDescriptorOffsetValue gpfifo)
947 (nativePhysicalEmbeddedDescriptorLengthValue gpfifo))
948 in
949 (let unrestricted manifest =
950 (constructor
951 NativePhysicalEmbeddedManifest
952 NativePhysicalEmbeddedManifestValue
953 nativePhysicalEmbeddedVersion
954 host
955 program
956 qmd
957 pushbuffer
958 gpfifo
959 manifestBytes
960 manifestOffset
961 artifactLength)
962 in
963 (constructor
964 NativePhysicalEmbeddedLoadResult
965 NativePhysicalEmbeddedLoadSucceeded
966 (constructor
967 NativePhysicalEmbeddedArtifact
968 NativePhysicalEmbeddedArtifactValue
969 artifactBytes
970 manifest)
971 hostBytes
972 programBytes
973 qmdBytes
974 pushbufferBytes
975 gpfifoBytes)))))))))
976 allValid))))))))))))))))))))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.