module Runtime.NativePhysicalEmbeddedArtifact import Data.Bytes import Model.Config import Model.Word32 import Std.Natural -- Versioned envelope for a native ELF and the GPU artifacts it owns. -- Large materials remain runtime Bytes values and are joined through the -- runtime byte builder. No component is expanded into source-level literals. family NativePhysicalEmbeddedComponentKind : Type 0 constructor NativePhysicalEmbeddedHostELF constructor NativePhysicalEmbeddedProgramTable constructor NativePhysicalEmbeddedQMDTable constructor NativePhysicalEmbeddedPushbuffer constructor NativePhysicalEmbeddedGPFIFO end-family family NativePhysicalEmbeddedPayload : Type 0 constructor NativePhysicalEmbeddedPayloadValue field unrestricted nativePhysicalEmbeddedPayloadBytes : Bytes field unrestricted nativePhysicalEmbeddedPayloadIdentity : Bytes field unrestricted nativePhysicalEmbeddedPayloadSHA256 : Bytes end-family family NativePhysicalEmbeddedDescriptor : Type 0 constructor NativePhysicalEmbeddedDescriptorValue field unrestricted nativePhysicalEmbeddedDescriptorKind : (family NativePhysicalEmbeddedComponentKind) field unrestricted nativePhysicalEmbeddedDescriptorOffset : Nat field unrestricted nativePhysicalEmbeddedDescriptorLength : Nat field unrestricted nativePhysicalEmbeddedDescriptorIdentity : Bytes field unrestricted nativePhysicalEmbeddedDescriptorSHA256 : Bytes end-family family NativePhysicalEmbeddedManifest : Type 0 constructor NativePhysicalEmbeddedManifestValue field unrestricted nativePhysicalEmbeddedManifestVersion : Nat field unrestricted nativePhysicalEmbeddedManifestHost : (family NativePhysicalEmbeddedDescriptor) field unrestricted nativePhysicalEmbeddedManifestProgram : (family NativePhysicalEmbeddedDescriptor) field unrestricted nativePhysicalEmbeddedManifestQMD : (family NativePhysicalEmbeddedDescriptor) field unrestricted nativePhysicalEmbeddedManifestPushbuffer : (family NativePhysicalEmbeddedDescriptor) field unrestricted nativePhysicalEmbeddedManifestGPFIFO : (family NativePhysicalEmbeddedDescriptor) field unrestricted nativePhysicalEmbeddedManifestBytes : Bytes field unrestricted nativePhysicalEmbeddedManifestOffset : Nat field unrestricted nativePhysicalEmbeddedManifestArtifactLength : Nat end-family family NativePhysicalEmbeddedArtifact : Type 0 constructor NativePhysicalEmbeddedArtifactValue field unrestricted nativePhysicalEmbeddedArtifactBytes : Bytes field unrestricted nativePhysicalEmbeddedArtifactManifest : (family NativePhysicalEmbeddedManifest) end-family -- Digests are observed independently by the native runtime hasher. The -- manifest parser never treats its own embedded claims as observations. family NativePhysicalEmbeddedObservedDigests : Type 0 constructor NativePhysicalEmbeddedObservedDigestsValue field unrestricted nativePhysicalEmbeddedObservedHostSHA256 : Bytes field unrestricted nativePhysicalEmbeddedObservedProgramSHA256 : Bytes field unrestricted nativePhysicalEmbeddedObservedQMDSHA256 : Bytes field unrestricted nativePhysicalEmbeddedObservedPushbufferSHA256 : Bytes field unrestricted nativePhysicalEmbeddedObservedGPFIFOSHA256 : Bytes end-family family NativePhysicalEmbeddedErrorCode : Type 0 constructor NativePhysicalEmbeddedBuildInputsInvalid constructor NativePhysicalEmbeddedLengthOverflow constructor NativePhysicalEmbeddedFooterInvalid constructor NativePhysicalEmbeddedManifestInvalid constructor NativePhysicalEmbeddedBoundsInvalid constructor NativePhysicalEmbeddedComponentHashMismatch end-family family NativePhysicalEmbeddedBuildResult : Type 0 constructor NativePhysicalEmbeddedBuildSucceeded field unrestricted nativePhysicalEmbeddedBuiltArtifact : (family NativePhysicalEmbeddedArtifact) constructor NativePhysicalEmbeddedBuildFailed field unrestricted nativePhysicalEmbeddedBuildError : (family NativePhysicalEmbeddedErrorCode) end-family family NativePhysicalEmbeddedLoadResult : Type 0 constructor NativePhysicalEmbeddedLoadSucceeded field unrestricted nativePhysicalEmbeddedLoadedArtifact : (family NativePhysicalEmbeddedArtifact) field unrestricted nativePhysicalEmbeddedLoadedHostELF : Bytes field unrestricted nativePhysicalEmbeddedLoadedProgramTable : Bytes field unrestricted nativePhysicalEmbeddedLoadedQMDTable : Bytes field unrestricted nativePhysicalEmbeddedLoadedPushbuffer : Bytes field unrestricted nativePhysicalEmbeddedLoadedGPFIFO : Bytes constructor NativePhysicalEmbeddedLoadFailed field unrestricted nativePhysicalEmbeddedLoadError : (family NativePhysicalEmbeddedErrorCode) end-family -- Eight-byte manifest magic: "ALPHAEMB". def nativePhysicalEmbeddedManifestMagic : Bytes = b"ALPHAEMB" -- Eight-byte EOF footer magic: "ALPHAFTR". def nativePhysicalEmbeddedFooterMagic : Bytes = b"ALPHAFTR" -- Canonical envelope version. def nativePhysicalEmbeddedVersion : Nat = (succ zero) -- Owner identities remain the established 64-byte identity representation. def nativePhysicalEmbeddedIdentityLength : Nat = (byte-to-nat (byte 64)) -- SHA-256 is stored as its raw 32-byte digest. def nativePhysicalEmbeddedDigestLength : Nat = (byte-to-nat (byte 32)) -- Component digests are optional runtime evidence. Whole-program builds use -- this explicit sentinel rather than spending evaluator time hashing payloads -- that the Haskell artifact writer and receipt hash again after linking. def nativePhysicalEmbeddedDigestOmitted : Bytes = 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" -- In-memory payload constructor for direct whole-program linking. The stable -- identity is kept typed and the material never becomes a path or temporary -- file. def nativePhysicalEmbeddedPayloadInMemory = (lambda unrestricted identity : Bytes . (lambda unrestricted material : Bytes . (constructor NativePhysicalEmbeddedPayload NativePhysicalEmbeddedPayloadValue material identity nativePhysicalEmbeddedDigestOmitted))) -- tag:u32 + offset:u32 + length:u32 + identity[64] + sha256[32]. def nativePhysicalEmbeddedDescriptorLength : Nat = (byte-to-nat (byte 108)) -- magic[8] + version:u32 + five 108-byte component descriptors. def nativePhysicalEmbeddedManifestLength : Nat = 552 -- magic[8] + manifest-offset:u32 + manifest-length:u32. def nativePhysicalEmbeddedFooterLength : Nat = (byte-to-nat (byte 16)) -- Version 1 uses canonical unsigned 32-bit offsets and lengths. def nativePhysicalEmbeddedMaximumLength : Nat = 4294967295 -- Stable descriptor tags, in physical layout order. def nativePhysicalEmbeddedComponentTag = (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . (eliminate NativePhysicalEmbeddedComponentKind (lambda unrestricted current : (family NativePhysicalEmbeddedComponentKind) . Nat) kind (branch NativePhysicalEmbeddedHostELF . (succ zero)) (branch NativePhysicalEmbeddedProgramTable . (byte-to-nat (byte 2))) (branch NativePhysicalEmbeddedQMDTable . (byte-to-nat (byte 3))) (branch NativePhysicalEmbeddedPushbuffer . (byte-to-nat (byte 4))) (branch NativePhysicalEmbeddedGPFIFO . (byte-to-nat (byte 5))))) -- Canonical little-endian u32 encoder for bounded manifest fields. def nativePhysicalEmbeddedWord32Bytes = (lambda unrestricted value : Nat . (dataBytesWord32LE (modelWord32FromNaturalTruncated value))) -- Efficiently joins two immutable byte values without source expansion. def nativePhysicalEmbeddedJoin = (lambda unrestricted left : Bytes . (lambda unrestricted right : Bytes . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk left) (bytes-builder-chunk right))))) -- Returns the material bytes of a payload. def nativePhysicalEmbeddedPayloadMaterial = (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) . (eliminate NativePhysicalEmbeddedPayload (lambda unrestricted current : (family NativePhysicalEmbeddedPayload) . Bytes) payload (branch NativePhysicalEmbeddedPayloadValue material identity digest . material))) -- Returns the stable owner identity of a payload. def nativePhysicalEmbeddedPayloadIdentityValue = (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) . (eliminate NativePhysicalEmbeddedPayload (lambda unrestricted current : (family NativePhysicalEmbeddedPayload) . Bytes) payload (branch NativePhysicalEmbeddedPayloadValue material identity digest . identity))) -- Returns the independently established raw SHA-256 of a payload. def nativePhysicalEmbeddedPayloadDigestValue = (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) . (eliminate NativePhysicalEmbeddedPayload (lambda unrestricted current : (family NativePhysicalEmbeddedPayload) . Bytes) payload (branch NativePhysicalEmbeddedPayloadValue material identity digest . digest))) -- Payload admission is non-empty and fixes identity/hash widths. def nativePhysicalEmbeddedPayloadValid = (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) . (naturalAnd (naturalNonzero (bytes-length (nativePhysicalEmbeddedPayloadMaterial payload))) (naturalAnd (naturalEqual (bytes-length (nativePhysicalEmbeddedPayloadIdentityValue payload)) nativePhysicalEmbeddedIdentityLength) (naturalEqual (bytes-length (nativePhysicalEmbeddedPayloadDigestValue payload)) nativePhysicalEmbeddedDigestLength)))) -- Constructs a typed descriptor from an admitted payload and physical offset. def nativePhysicalEmbeddedMakeDescriptor = (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . (lambda unrestricted offset : Nat . (lambda unrestricted payload : (family NativePhysicalEmbeddedPayload) . (constructor NativePhysicalEmbeddedDescriptor NativePhysicalEmbeddedDescriptorValue kind offset (bytes-length (nativePhysicalEmbeddedPayloadMaterial payload)) (nativePhysicalEmbeddedPayloadIdentityValue payload) (nativePhysicalEmbeddedPayloadDigestValue payload))))) -- Canonical fixed-width descriptor encoding. def nativePhysicalEmbeddedDescriptorBytes = (lambda unrestricted descriptor : (family NativePhysicalEmbeddedDescriptor) . (eliminate NativePhysicalEmbeddedDescriptor (lambda unrestricted current : (family NativePhysicalEmbeddedDescriptor) . Bytes) descriptor (branch NativePhysicalEmbeddedDescriptorValue kind offset length identity digest . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedWord32Bytes (nativePhysicalEmbeddedComponentTag kind))) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedWord32Bytes offset)) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedWord32Bytes length)) (bytes-builder-append (bytes-builder-chunk identity) (bytes-builder-chunk digest))))))))) -- Fixed-width descriptor encoding for large-artifact packagers. Callers that -- already proved their u32 bounds can supply the canonical words directly and -- avoid reducing million-sized offsets through unary Nat arithmetic. def nativePhysicalEmbeddedDescriptorFixedWidthBytes = (lambda unrestricted tag : (family ModelWord32) . (lambda unrestricted offset : (family ModelWord32) . (lambda unrestricted length : (family ModelWord32) . (lambda unrestricted identity : Bytes . (lambda unrestricted digest : Bytes . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk (dataBytesWord32LE tag)) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32LE offset)) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32LE length)) (bytes-builder-append (bytes-builder-chunk identity) (bytes-builder-chunk digest))))))))))) -- Fixed-width canonical manifest assembly. Each input is one canonical -- 108-byte descriptor produced by the function above. def nativePhysicalEmbeddedManifestFixedWidthBytes = (lambda unrestricted host : Bytes . (lambda unrestricted program : Bytes . (lambda unrestricted qmd : Bytes . (lambda unrestricted pushbuffer : Bytes . (lambda unrestricted gpfifo : Bytes . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk nativePhysicalEmbeddedManifestMagic) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32LE modelWord32One)) (bytes-builder-append (bytes-builder-chunk host) (bytes-builder-append (bytes-builder-chunk program) (bytes-builder-append (bytes-builder-chunk qmd) (bytes-builder-append (bytes-builder-chunk pushbuffer) (bytes-builder-chunk gpfifo))))))))))))) -- Canonical version-1 manifest encoding. def nativePhysicalEmbeddedManifestCanonicalBytes = (lambda unrestricted host : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted program : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted qmd : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedDescriptor) . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk nativePhysicalEmbeddedManifestMagic) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedWord32Bytes nativePhysicalEmbeddedVersion)) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedDescriptorBytes host)) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedDescriptorBytes program)) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedDescriptorBytes qmd)) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedDescriptorBytes pushbuffer)) (bytes-builder-chunk (nativePhysicalEmbeddedDescriptorBytes gpfifo)))))))))))))) -- Canonical EOF locator encoding. def nativePhysicalEmbeddedFooterBytes = (lambda unrestricted manifestOffset : Nat . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk nativePhysicalEmbeddedFooterMagic) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedWord32Bytes manifestOffset)) (bytes-builder-chunk (nativePhysicalEmbeddedWord32Bytes nativePhysicalEmbeddedManifestLength)))))) -- Fixed-width EOF locator matching nativePhysicalEmbeddedFooterBytes without -- a large Nat-to-Word32 reduction in the packager evaluator. def nativePhysicalEmbeddedFooterFixedWidthBytes = (lambda unrestricted manifestOffset : (family ModelWord32) . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk nativePhysicalEmbeddedFooterMagic) (bytes-builder-append (bytes-builder-chunk (dataBytesWord32LE manifestOffset)) (bytes-builder-chunk (dataBytesWord32LE (constructor ModelWord32 ModelWord32Value (byte 40) (byte 2) (byte 0) (byte 0)))))))) -- Assembles already-admitted payloads without re-copying them through source -- syntax. The runtime builder performs one final materialization. def nativePhysicalEmbeddedAssemble = (lambda unrestricted host : (family NativePhysicalEmbeddedPayload) . (lambda unrestricted program : (family NativePhysicalEmbeddedPayload) . (lambda unrestricted qmd : (family NativePhysicalEmbeddedPayload) . (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedPayload) . (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedPayload) . (let unrestricted hostLength = (bytes-length (nativePhysicalEmbeddedPayloadMaterial host)) in (let unrestricted programOffset = hostLength in (let unrestricted qmdOffset = (naturalAdd programOffset (bytes-length (nativePhysicalEmbeddedPayloadMaterial program))) in (let unrestricted pushbufferOffset = (naturalAdd qmdOffset (bytes-length (nativePhysicalEmbeddedPayloadMaterial qmd))) in (let unrestricted gpfifoOffset = (naturalAdd pushbufferOffset (bytes-length (nativePhysicalEmbeddedPayloadMaterial pushbuffer))) in (let unrestricted manifestOffset = (naturalAdd gpfifoOffset (bytes-length (nativePhysicalEmbeddedPayloadMaterial gpfifo))) in (let unrestricted artifactLength = (naturalAdd manifestOffset (naturalAdd nativePhysicalEmbeddedManifestLength nativePhysicalEmbeddedFooterLength)) in (let unrestricted hostDescriptor = (nativePhysicalEmbeddedMakeDescriptor (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedHostELF) zero host) in (let unrestricted programDescriptor = (nativePhysicalEmbeddedMakeDescriptor (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedProgramTable) programOffset program) in (let unrestricted qmdDescriptor = (nativePhysicalEmbeddedMakeDescriptor (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedQMDTable) qmdOffset qmd) in (let unrestricted pushbufferDescriptor = (nativePhysicalEmbeddedMakeDescriptor (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedPushbuffer) pushbufferOffset pushbuffer) in (let unrestricted gpfifoDescriptor = (nativePhysicalEmbeddedMakeDescriptor (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedGPFIFO) gpfifoOffset gpfifo) in (let unrestricted manifestBytes = (nativePhysicalEmbeddedManifestCanonicalBytes hostDescriptor programDescriptor qmdDescriptor pushbufferDescriptor gpfifoDescriptor) in (let unrestricted footerBytes = (nativePhysicalEmbeddedFooterBytes manifestOffset) in (let unrestricted artifactBytes = (bytes-builder-build (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedPayloadMaterial host)) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedPayloadMaterial program)) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedPayloadMaterial qmd)) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedPayloadMaterial pushbuffer)) (bytes-builder-append (bytes-builder-chunk (nativePhysicalEmbeddedPayloadMaterial gpfifo)) (bytes-builder-append (bytes-builder-chunk manifestBytes) (bytes-builder-chunk footerBytes)))))))) in (let unrestricted manifest = (constructor NativePhysicalEmbeddedManifest NativePhysicalEmbeddedManifestValue nativePhysicalEmbeddedVersion hostDescriptor programDescriptor qmdDescriptor pushbufferDescriptor gpfifoDescriptor manifestBytes manifestOffset artifactLength) in (constructor NativePhysicalEmbeddedBuildResult NativePhysicalEmbeddedBuildSucceeded (constructor NativePhysicalEmbeddedArtifact NativePhysicalEmbeddedArtifactValue artifactBytes manifest))))))))))))))))))))))) -- Validates every fixed-width input before assembling the artifact. def nativePhysicalEmbeddedBuild = (lambda unrestricted host : (family NativePhysicalEmbeddedPayload) . (lambda unrestricted program : (family NativePhysicalEmbeddedPayload) . (lambda unrestricted qmd : (family NativePhysicalEmbeddedPayload) . (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedPayload) . (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedPayload) . (let unrestricted totalLength = (naturalAdd (bytes-length (nativePhysicalEmbeddedPayloadMaterial host)) (naturalAdd (bytes-length (nativePhysicalEmbeddedPayloadMaterial program)) (naturalAdd (bytes-length (nativePhysicalEmbeddedPayloadMaterial qmd)) (naturalAdd (bytes-length (nativePhysicalEmbeddedPayloadMaterial pushbuffer)) (naturalAdd (bytes-length (nativePhysicalEmbeddedPayloadMaterial gpfifo)) (naturalAdd nativePhysicalEmbeddedManifestLength nativePhysicalEmbeddedFooterLength)))))) in (let unrestricted inputsValid = (naturalAnd (nativePhysicalEmbeddedPayloadValid host) (naturalAnd (nativePhysicalEmbeddedPayloadValid program) (naturalAnd (nativePhysicalEmbeddedPayloadValid qmd) (naturalAnd (nativePhysicalEmbeddedPayloadValid pushbuffer) (nativePhysicalEmbeddedPayloadValid gpfifo))))) in (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalEmbeddedBuildResult)) (constructor NativePhysicalEmbeddedBuildResult NativePhysicalEmbeddedBuildFailed (constructor NativePhysicalEmbeddedErrorCode NativePhysicalEmbeddedBuildInputsInvalid)) (lambda unrestricted inputsPredecessor : Nat . (lambda unrestricted inputsInduction : (family NativePhysicalEmbeddedBuildResult) . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalEmbeddedBuildResult)) (constructor NativePhysicalEmbeddedBuildResult NativePhysicalEmbeddedBuildFailed (constructor NativePhysicalEmbeddedErrorCode NativePhysicalEmbeddedLengthOverflow)) (lambda unrestricted lengthPredecessor : Nat . (lambda unrestricted lengthInduction : (family NativePhysicalEmbeddedBuildResult) . (nativePhysicalEmbeddedAssemble host program qmd pushbuffer gpfifo))) (naturalLessOrEqual totalLength nativePhysicalEmbeddedMaximumLength)))) inputsValid)))))))) -- Direct artifact projection. An invalid component set becomes empty bytes, -- which the compiler's ELF writer rejects without running an intermediate -- packager executable. def nativePhysicalEmbeddedBuildResultBytes = (lambda unrestricted result : (family NativePhysicalEmbeddedBuildResult) . (eliminate NativePhysicalEmbeddedBuildResult (lambda unrestricted current : (family NativePhysicalEmbeddedBuildResult) . Bytes) result (branch NativePhysicalEmbeddedBuildSucceeded artifact . (eliminate NativePhysicalEmbeddedArtifact (lambda unrestricted current : (family NativePhysicalEmbeddedArtifact) . Bytes) artifact (branch NativePhysicalEmbeddedArtifactValue bytes manifest . bytes))) (branch NativePhysicalEmbeddedBuildFailed error . b""))) -- Bounded exact slice used by the manifest decoder. Empty means failure; -- admitted components are non-empty, so the sentinel is unambiguous. def nativePhysicalEmbeddedSliceOrEmpty = (lambda unrestricted input : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted length : Nat . (eliminate DataBytesSliceResult (lambda unrestricted current : (family DataBytesSliceResult) . Bytes) (dataBytesSlice input offset length) (branch DataBytesSliceSucceeded slice telemetry . (eliminate DataBytesResult (lambda unrestricted current : (family DataBytesResult) . Bytes) (dataBytesSliceToBytes slice) (branch DataBytesSucceeded value materialTelemetry . value) (branch DataBytesFailed code materialTelemetry . b""))) (branch DataBytesSliceFailed code telemetry . b""))))) -- Bounded little-endian u32 reader; zero is a fail-closed sentinel. def nativePhysicalEmbeddedWord32At = (lambda unrestricted input : Bytes . (lambda unrestricted offset : Nat . (eliminate DataBytesWord32ExactDecodeResult (lambda unrestricted current : (family DataBytesWord32ExactDecodeResult) . Nat) (dataBytesDecodeWord32LEExact (nativePhysicalEmbeddedSliceOrEmpty input offset (byte-to-nat (byte 4)))) (branch DataBytesWord32ExactlyDecoded value telemetry . (modelWord32ToNatural value)) (branch DataBytesWord32ExactDecodeFailed code telemetry . zero)))) -- Decodes one descriptor at its fixed manifest offset. def nativePhysicalEmbeddedDescriptorAt = (lambda unrestricted manifestBytes : Bytes . (lambda unrestricted descriptorOffset : Nat . (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . (constructor NativePhysicalEmbeddedDescriptor NativePhysicalEmbeddedDescriptorValue kind (nativePhysicalEmbeddedWord32At manifestBytes (naturalAdd descriptorOffset (byte-to-nat (byte 4)))) (nativePhysicalEmbeddedWord32At manifestBytes (naturalAdd descriptorOffset (byte-to-nat (byte 8)))) (nativePhysicalEmbeddedSliceOrEmpty manifestBytes (naturalAdd descriptorOffset (byte-to-nat (byte 12))) nativePhysicalEmbeddedIdentityLength) (nativePhysicalEmbeddedSliceOrEmpty manifestBytes (naturalAdd descriptorOffset (byte-to-nat (byte 76))) nativePhysicalEmbeddedDigestLength))))) -- Descriptor field projections used by bounds and hash validation. def nativePhysicalEmbeddedDescriptorOffsetValue = (lambda unrestricted descriptor : (family NativePhysicalEmbeddedDescriptor) . (eliminate NativePhysicalEmbeddedDescriptor (lambda unrestricted current : (family NativePhysicalEmbeddedDescriptor) . Nat) descriptor (branch NativePhysicalEmbeddedDescriptorValue kind offset length identity digest . offset))) def nativePhysicalEmbeddedDescriptorLengthValue = (lambda unrestricted descriptor : (family NativePhysicalEmbeddedDescriptor) . (eliminate NativePhysicalEmbeddedDescriptor (lambda unrestricted current : (family NativePhysicalEmbeddedDescriptor) . Nat) descriptor (branch NativePhysicalEmbeddedDescriptorValue kind offset length identity digest . length))) def nativePhysicalEmbeddedDescriptorDigestValue = (lambda unrestricted descriptor : (family NativePhysicalEmbeddedDescriptor) . (eliminate NativePhysicalEmbeddedDescriptor (lambda unrestricted current : (family NativePhysicalEmbeddedDescriptor) . Bytes) descriptor (branch NativePhysicalEmbeddedDescriptorValue kind offset length identity digest . digest))) def nativePhysicalEmbeddedDescriptorTagAt = (lambda unrestricted manifestBytes : Bytes . (lambda unrestricted descriptorOffset : Nat . (nativePhysicalEmbeddedWord32At manifestBytes descriptorOffset))) -- Version-1 descriptors must be contiguous and end exactly at the manifest. def nativePhysicalEmbeddedLayoutValid = (lambda unrestricted host : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted program : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted qmd : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted manifestOffset : Nat . (naturalAnd (naturalNonzero (nativePhysicalEmbeddedDescriptorLengthValue host)) (naturalAnd (naturalEqual (nativePhysicalEmbeddedDescriptorOffsetValue host) zero) (naturalAnd (naturalEqual (nativePhysicalEmbeddedDescriptorOffsetValue program) (nativePhysicalEmbeddedDescriptorLengthValue host)) (naturalAnd (naturalEqual (nativePhysicalEmbeddedDescriptorOffsetValue qmd) (naturalAdd (nativePhysicalEmbeddedDescriptorOffsetValue program) (nativePhysicalEmbeddedDescriptorLengthValue program))) (naturalAnd (naturalEqual (nativePhysicalEmbeddedDescriptorOffsetValue pushbuffer) (naturalAdd (nativePhysicalEmbeddedDescriptorOffsetValue qmd) (nativePhysicalEmbeddedDescriptorLengthValue qmd))) (naturalAnd (naturalEqual (nativePhysicalEmbeddedDescriptorOffsetValue gpfifo) (naturalAdd (nativePhysicalEmbeddedDescriptorOffsetValue pushbuffer) (nativePhysicalEmbeddedDescriptorLengthValue pushbuffer))) (naturalEqual manifestOffset (naturalAdd (nativePhysicalEmbeddedDescriptorOffsetValue gpfifo) (nativePhysicalEmbeddedDescriptorLengthValue gpfifo))))))))))))))) -- Compares manifest claims only with independently observed raw digests. def nativePhysicalEmbeddedHashesValid = (lambda unrestricted host : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted program : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted qmd : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted pushbuffer : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted gpfifo : (family NativePhysicalEmbeddedDescriptor) . (lambda unrestricted observed : (family NativePhysicalEmbeddedObservedDigests) . (eliminate NativePhysicalEmbeddedObservedDigests (lambda unrestricted current : (family NativePhysicalEmbeddedObservedDigests) . Nat) observed (branch NativePhysicalEmbeddedObservedDigestsValue hostDigest programDigest qmdDigest pushbufferDigest gpfifoDigest . (naturalAnd (naturalEqual (bytes-length hostDigest) nativePhysicalEmbeddedDigestLength) (naturalAnd (bytes-equal (nativePhysicalEmbeddedDescriptorDigestValue host) hostDigest) (naturalAnd (bytes-equal (nativePhysicalEmbeddedDescriptorDigestValue program) programDigest) (naturalAnd (bytes-equal (nativePhysicalEmbeddedDescriptorDigestValue qmd) qmdDigest) (naturalAnd (bytes-equal (nativePhysicalEmbeddedDescriptorDigestValue pushbuffer) pushbufferDigest) (bytes-equal (nativePhysicalEmbeddedDescriptorDigestValue gpfifo) gpfifoDigest)))))))))))))) -- Decodes and validates an artifact after the native hasher has supplied all -- five observations. No bytes reach GPU submission through a failed result. def nativePhysicalEmbeddedLoad = (lambda unrestricted artifactBytes : Bytes . (lambda unrestricted observed : (family NativePhysicalEmbeddedObservedDigests) . (let unrestricted artifactLength = (bytes-length artifactBytes) in (let unrestricted footerOffset = (naturalSaturatingSubtract artifactLength nativePhysicalEmbeddedFooterLength) in (let unrestricted footerBytes = (nativePhysicalEmbeddedSliceOrEmpty artifactBytes footerOffset nativePhysicalEmbeddedFooterLength) in (let unrestricted manifestLength = nativePhysicalEmbeddedManifestLength in (let unrestricted manifestOffset = (naturalSaturatingSubtract footerOffset manifestLength) in (let unrestricted manifestBytes = (nativePhysicalEmbeddedSliceOrEmpty artifactBytes manifestOffset manifestLength) in (let unrestricted footerValid = (naturalAnd (naturalLessOrEqual nativePhysicalEmbeddedFooterLength artifactLength) (naturalAnd (bytes-equal (nativePhysicalEmbeddedSliceOrEmpty footerBytes zero (byte-to-nat (byte 8))) nativePhysicalEmbeddedFooterMagic) (naturalAnd (bytes-equal (nativePhysicalEmbeddedSliceOrEmpty footerBytes (byte-to-nat (byte 8)) (byte-to-nat (byte 4))) (nativePhysicalEmbeddedWord32Bytes manifestOffset)) (bytes-equal (nativePhysicalEmbeddedSliceOrEmpty footerBytes (byte-to-nat (byte 12)) (byte-to-nat (byte 4))) (nativePhysicalEmbeddedWord32Bytes manifestLength))))) in (let unrestricted manifestValid = (naturalAnd (naturalEqual (bytes-length manifestBytes) nativePhysicalEmbeddedManifestLength) (naturalAnd (bytes-equal (nativePhysicalEmbeddedSliceOrEmpty manifestBytes zero (byte-to-nat (byte 8))) nativePhysicalEmbeddedManifestMagic) (naturalEqual (nativePhysicalEmbeddedWord32At manifestBytes (byte-to-nat (byte 8))) nativePhysicalEmbeddedVersion))) in (let unrestricted host = (nativePhysicalEmbeddedDescriptorAt manifestBytes (byte-to-nat (byte 12)) (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedHostELF)) in (let unrestricted program = (nativePhysicalEmbeddedDescriptorAt manifestBytes (byte-to-nat (byte 120)) (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedProgramTable)) in (let unrestricted qmd = (nativePhysicalEmbeddedDescriptorAt manifestBytes (byte-to-nat (byte 228)) (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedQMDTable)) in (let unrestricted pushbuffer = (nativePhysicalEmbeddedDescriptorAt manifestBytes 336 (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedPushbuffer)) in (let unrestricted gpfifo = (nativePhysicalEmbeddedDescriptorAt manifestBytes 444 (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedGPFIFO)) in (let unrestricted tagsValid = (naturalAnd (naturalEqual (nativePhysicalEmbeddedDescriptorTagAt manifestBytes (byte-to-nat (byte 12))) (succ zero)) (naturalAnd (naturalEqual (nativePhysicalEmbeddedDescriptorTagAt manifestBytes (byte-to-nat (byte 120))) (byte-to-nat (byte 2))) (naturalAnd (naturalEqual (nativePhysicalEmbeddedDescriptorTagAt manifestBytes (byte-to-nat (byte 228))) (byte-to-nat (byte 3))) (naturalAnd (naturalEqual (nativePhysicalEmbeddedDescriptorTagAt manifestBytes 336) (byte-to-nat (byte 4))) (naturalEqual (nativePhysicalEmbeddedDescriptorTagAt manifestBytes 444) (byte-to-nat (byte 5))))))) in (let unrestricted layoutValid = (nativePhysicalEmbeddedLayoutValid host program qmd pushbuffer gpfifo manifestOffset) in (let unrestricted hashesValid = (nativePhysicalEmbeddedHashesValid host program qmd pushbuffer gpfifo observed) in (let unrestricted allValid = (naturalAnd footerValid (naturalAnd manifestValid (naturalAnd tagsValid (naturalAnd layoutValid hashesValid)))) in (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalEmbeddedLoadResult)) (constructor NativePhysicalEmbeddedLoadResult NativePhysicalEmbeddedLoadFailed (constructor NativePhysicalEmbeddedErrorCode NativePhysicalEmbeddedManifestInvalid)) (lambda unrestricted validPredecessor : Nat . (lambda unrestricted validInduction : (family NativePhysicalEmbeddedLoadResult) . (let unrestricted hostBytes = (nativePhysicalEmbeddedSliceOrEmpty artifactBytes (nativePhysicalEmbeddedDescriptorOffsetValue host) (nativePhysicalEmbeddedDescriptorLengthValue host)) in (let unrestricted programBytes = (nativePhysicalEmbeddedSliceOrEmpty artifactBytes (nativePhysicalEmbeddedDescriptorOffsetValue program) (nativePhysicalEmbeddedDescriptorLengthValue program)) in (let unrestricted qmdBytes = (nativePhysicalEmbeddedSliceOrEmpty artifactBytes (nativePhysicalEmbeddedDescriptorOffsetValue qmd) (nativePhysicalEmbeddedDescriptorLengthValue qmd)) in (let unrestricted pushbufferBytes = (nativePhysicalEmbeddedSliceOrEmpty artifactBytes (nativePhysicalEmbeddedDescriptorOffsetValue pushbuffer) (nativePhysicalEmbeddedDescriptorLengthValue pushbuffer)) in (let unrestricted gpfifoBytes = (nativePhysicalEmbeddedSliceOrEmpty artifactBytes (nativePhysicalEmbeddedDescriptorOffsetValue gpfifo) (nativePhysicalEmbeddedDescriptorLengthValue gpfifo)) in (let unrestricted manifest = (constructor NativePhysicalEmbeddedManifest NativePhysicalEmbeddedManifestValue nativePhysicalEmbeddedVersion host program qmd pushbuffer gpfifo manifestBytes manifestOffset artifactLength) in (constructor NativePhysicalEmbeddedLoadResult NativePhysicalEmbeddedLoadSucceeded (constructor NativePhysicalEmbeddedArtifact NativePhysicalEmbeddedArtifactValue artifactBytes manifest) hostBytes programBytes qmdBytes pushbufferBytes gpfifoBytes))))))))) allValid))))))))))))))))))))