module Runtime.NativePhysicalNativeELF import Compiler.ELF import Compiler.MachineX86NativeAssembly import Data.SHA256Digest import Runtime.NativePhysicalImage import Runtime.NativePhysicalNative import Runtime.NativePhysicalProgram family NativePhysicalNativeELFErrorCode : Type 0 constructor NativePhysicalNativeELFImageGenerationFailed field unrestricted nativePhysicalNativeELFImageError : (family NativePhysicalImageErrorCode) constructor NativePhysicalNativeELFDuplicateLabel field unrestricted nativePhysicalNativeELFDuplicateLabelName : Bytes constructor NativePhysicalNativeELFAssemblyOffsetOverflow constructor NativePhysicalNativeELFMissingLabel field unrestricted nativePhysicalNativeELFMissingLabelName : Bytes constructor NativePhysicalNativeELFDisplacementOutOfRange field unrestricted nativePhysicalNativeELFDistantLabelName : Bytes end-family family NativePhysicalNativeELFTelemetry : Type 0 constructor NativePhysicalNativeELFTelemetryValue field unrestricted nativePhysicalNativeELFTelemetryCodeBytes : Nat field unrestricted nativePhysicalNativeELFTelemetryImageBytes : Nat field unrestricted nativePhysicalNativeELFTelemetryMachineBytes : Nat field unrestricted nativePhysicalNativeELFTelemetryELFBytes : Nat field unrestricted nativePhysicalNativeELFTelemetryFailures : Nat field unrestricted nativePhysicalNativeELFTelemetryFallbacks : Nat field unrestricted nativePhysicalNativeELFTelemetryProgramIdentity : Bytes field unrestricted nativePhysicalNativeELFTelemetryCodeSHA256 : Bytes field unrestricted nativePhysicalNativeELFTelemetryImageSHA256 : Bytes field unrestricted nativePhysicalNativeELFTelemetryMachineSHA256 : Bytes field unrestricted nativePhysicalNativeELFTelemetryELFSHA256 : Bytes end-family family NativePhysicalNativeELFFailureTelemetry : Type 0 constructor NativePhysicalNativeELFFailureTelemetryValue field unrestricted nativePhysicalNativeELFFailurePhase : Bytes field unrestricted nativePhysicalNativeELFFailureCode : Bytes field unrestricted nativePhysicalNativeELFFailureImageTelemetry : Bytes field unrestricted nativePhysicalNativeELFFailureAssemblySubject : Bytes field unrestricted nativePhysicalNativeELFFailureCount : Nat field unrestricted nativePhysicalNativeELFFailureFallbacks : Nat end-family family NativePhysicalNativeELFArtifact : Type 0 constructor NativePhysicalNativeELFArtifactValue field unrestricted nativePhysicalNativeELFBytes : Bytes field unrestricted nativePhysicalNativeCodeBytes : Bytes field unrestricted nativePhysicalNativeImageBytes : Bytes field unrestricted nativePhysicalNativeMachineBytes : Bytes field unrestricted nativePhysicalNativeProgramIdentity : Bytes field unrestricted nativePhysicalNativeCodeSHA256 : Bytes field unrestricted nativePhysicalNativeImageSHA256 : Bytes field unrestricted nativePhysicalNativeMachineSHA256 : Bytes field unrestricted nativePhysicalNativeELFSHA256 : Bytes field unrestricted nativePhysicalNativeCommandCount : Nat field unrestricted nativePhysicalNativeELFTelemetry : (family NativePhysicalNativeELFTelemetry) end-family family NativePhysicalNativeELFResult : Type 0 constructor NativePhysicalNativeELFGenerated field unrestricted nativePhysicalNativeELFArtifact : (family NativePhysicalNativeELFArtifact) field unrestricted nativePhysicalNativeELFSuccessTelemetry : (family NativePhysicalNativeELFTelemetry) constructor NativePhysicalNativeELFGenerationFailed field unrestricted nativePhysicalNativeELFGenerationError : (family NativePhysicalNativeELFErrorCode) field unrestricted nativePhysicalNativeELFFailureTelemetry : (family NativePhysicalNativeELFFailureTelemetry) end-family def nativePhysicalNativeELFErrorCodeBytes = (lambda unrestricted code : (family NativePhysicalNativeELFErrorCode) . (eliminate NativePhysicalNativeELFErrorCode (lambda unrestricted current : (family NativePhysicalNativeELFErrorCode) . Bytes) code (branch NativePhysicalNativeELFImageGenerationFailed imageError . (bytes-append b"ALPHA-NELF-001-" (nativePhysicalImageErrorCodeBytes imageError))) (branch NativePhysicalNativeELFDuplicateLabel labelName . (bytes-append b"ALPHA-NELF-002-" labelName)) (branch NativePhysicalNativeELFAssemblyOffsetOverflow . b"ALPHA-NELF-003") (branch NativePhysicalNativeELFMissingLabel labelName . (bytes-append b"ALPHA-NELF-004-" labelName)) (branch NativePhysicalNativeELFDisplacementOutOfRange labelName . (bytes-append b"ALPHA-NELF-005-" labelName)))) def nativePhysicalNativeELFImageFailurePhase : Bytes = b"image-generation" def nativePhysicalNativeELFAssemblyFailurePhase : Bytes = b"x86-assembly" def nativePhysicalNativeELFEncodeValidationTelemetry = (lambda unrestricted telemetry : (family NativePhysicalValidationTelemetry) . (eliminate NativePhysicalValidationTelemetry (lambda unrestricted current : (family NativePhysicalValidationTelemetry) . Bytes) telemetry (branch NativePhysicalValidationTelemetryValue counts expected stateExtent resultSlots fallbacks identity failures ordinal code . (bytes-append identity (bytes-append (bytes 0) (bytes-append code (bytes-append (bytes 0) (bytes (nat-to-byte expected) (nat-to-byte fallbacks) (nat-to-byte failures) (nat-to-byte ordinal))))))))) def nativePhysicalNativeELFEncodeImageFailureTelemetry = (lambda unrestricted telemetry : (family NativePhysicalImageFailureTelemetry) . (eliminate NativePhysicalImageFailureTelemetry (lambda unrestricted current : (family NativePhysicalImageFailureTelemetry) . Bytes) telemetry (branch NativePhysicalImageFailureTelemetryValue validation encoded bodyBytes code . (bytes-append (nativePhysicalNativeELFEncodeValidationTelemetry validation) (bytes-append (bytes 0) code))))) def nativePhysicalNativeELFFailureTelemetryFor = (lambda unrestricted phase : Bytes . (lambda unrestricted code : (family NativePhysicalNativeELFErrorCode) . (lambda unrestricted imageTelemetry : Bytes . (lambda unrestricted subject : Bytes . (constructor NativePhysicalNativeELFFailureTelemetry NativePhysicalNativeELFFailureTelemetryValue phase (nativePhysicalNativeELFErrorCodeBytes code) imageTelemetry subject (succ zero) zero))))) def nativePhysicalNativeELFFail = (lambda unrestricted phase : Bytes . (lambda unrestricted code : (family NativePhysicalNativeELFErrorCode) . (lambda unrestricted imageTelemetry : Bytes . (lambda unrestricted subject : Bytes . (constructor NativePhysicalNativeELFResult NativePhysicalNativeELFGenerationFailed code (nativePhysicalNativeELFFailureTelemetryFor phase code imageTelemetry subject)))))) def nativePhysicalNativeELFTelemetryFor = (lambda unrestricted code : Bytes . (lambda unrestricted image : Bytes . (lambda unrestricted machine : Bytes . (lambda unrestricted elf : Bytes . (lambda unrestricted identity : Bytes . (lambda unrestricted codeDigest : Bytes . (lambda unrestricted imageDigest : Bytes . (lambda unrestricted machineDigest : Bytes . (lambda unrestricted elfDigest : Bytes . (constructor NativePhysicalNativeELFTelemetry NativePhysicalNativeELFTelemetryValue (bytes-length code) (bytes-length image) (bytes-length machine) (bytes-length elf) zero zero identity codeDigest imageDigest machineDigest elfDigest)))))))))) def nativePhysicalGenerateNativeELF = (lambda unrestricted program : (family NativePhysicalProgram) . (eliminate NativePhysicalImageResult (lambda unrestricted current : (family NativePhysicalImageResult) . (family NativePhysicalNativeELFResult)) (nativePhysicalGenerateImage program) (branch NativePhysicalImageGenerated image imageTelemetry . (eliminate NativePhysicalImage (lambda unrestricted current : (family NativePhysicalImage) . (family NativePhysicalNativeELFResult)) image (branch NativePhysicalImageValue imageBytes bodyDigest identity commandCount stateExtent resultSlots telemetry . (eliminate X86NativeAssemblyResult (lambda unrestricted current : (family X86NativeAssemblyResult) . (family NativePhysicalNativeELFResult)) (x86NativeAssemble nativePhysicalNativeAssembly) (branch X86NativeAssemblyEncoded codeBytes . (app (lambda unrestricted machineBytes : Bytes . (app (lambda unrestricted elfBytes : Bytes . (app (lambda unrestricted codeSHA256 : Bytes . (app (lambda unrestricted imageSHA256 : Bytes . (app (lambda unrestricted machineSHA256 : Bytes . (app (lambda unrestricted elfSHA256 : Bytes . (app (lambda unrestricted artifactTelemetry : (family NativePhysicalNativeELFTelemetry) . (constructor NativePhysicalNativeELFResult NativePhysicalNativeELFGenerated (constructor NativePhysicalNativeELFArtifact NativePhysicalNativeELFArtifactValue elfBytes codeBytes imageBytes machineBytes identity codeSHA256 imageSHA256 machineSHA256 elfSHA256 commandCount artifactTelemetry) artifactTelemetry)) (nativePhysicalNativeELFTelemetryFor codeBytes imageBytes machineBytes elfBytes identity codeSHA256 imageSHA256 machineSHA256 elfSHA256))) (sha256HexBytesOrEmpty (sha256Hex elfBytes)))) (sha256HexBytesOrEmpty (sha256Hex machineBytes)))) (sha256HexBytesOrEmpty (sha256Hex imageBytes)))) (sha256HexBytesOrEmpty (sha256Hex codeBytes)))) (wrapMachineCodeSparseLarge machineBytes))) (bytes-append codeBytes imageBytes))) (branch X86NativeAssemblyEncodeDuplicateLabel duplicateName . (nativePhysicalNativeELFFail nativePhysicalNativeELFAssemblyFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFDuplicateLabel duplicateName) b"" duplicateName)) (branch X86NativeAssemblyEncodeOffsetOverflow . (nativePhysicalNativeELFFail nativePhysicalNativeELFAssemblyFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFAssemblyOffsetOverflow) b"" b"")) (branch X86NativeAssemblyMissingLabel missingName . (nativePhysicalNativeELFFail nativePhysicalNativeELFAssemblyFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFMissingLabel missingName) b"" missingName)) (branch X86NativeAssemblyDisplacementOutOfRange distantName . (nativePhysicalNativeELFFail nativePhysicalNativeELFAssemblyFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFDisplacementOutOfRange distantName) b"" distantName)))))) (branch NativePhysicalImageGenerationFailed imageError failureTelemetry . (nativePhysicalNativeELFFail nativePhysicalNativeELFImageFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFImageGenerationFailed imageError) (nativePhysicalNativeELFEncodeImageFailureTelemetry failureTelemetry) b"")))) -- FAST EMIT (GPU bring-up): runnable ELF, all SHA-256 digests stubbed so the -- emit is seconds instead of tens of minutes. The four receipt digests are -- separate telemetry fields (never in the elfBytes). The image BODY digest IS -- embedded in the elfBytes, but it sits in the inert header region [112,176) -- that the native loader skips (it jumps to the body at offset 176), so -- stubbing it (via nativePhysicalGenerateImageFast) leaves a byte-for-byte -- identical executable code+body -- only that inert 64-byte digest field is -- zeroed. sha256Hex over the body was the whole remaining cost (~54s per -- 512-bit block); everything else in the emit is already first-order (<3s). def nativePhysicalGenerateNativeELFFast = (lambda unrestricted program : (family NativePhysicalProgram) . (eliminate NativePhysicalImageResult (lambda unrestricted current : (family NativePhysicalImageResult) . (family NativePhysicalNativeELFResult)) (nativePhysicalGenerateImageFast program) (branch NativePhysicalImageGenerated image imageTelemetry . (eliminate NativePhysicalImage (lambda unrestricted current : (family NativePhysicalImage) . (family NativePhysicalNativeELFResult)) image (branch NativePhysicalImageValue imageBytes bodyDigest identity commandCount stateExtent resultSlots telemetry . (eliminate X86NativeAssemblyResult (lambda unrestricted current : (family X86NativeAssemblyResult) . (family NativePhysicalNativeELFResult)) (x86NativeAssemble nativePhysicalNativeAssembly) (branch X86NativeAssemblyEncoded codeBytes . (app (lambda unrestricted machineBytes : Bytes . (app (lambda unrestricted elfBytes : Bytes . (app (lambda unrestricted codeSHA256 : Bytes . (app (lambda unrestricted imageSHA256 : Bytes . (app (lambda unrestricted machineSHA256 : Bytes . (app (lambda unrestricted elfSHA256 : Bytes . (app (lambda unrestricted artifactTelemetry : (family NativePhysicalNativeELFTelemetry) . (constructor NativePhysicalNativeELFResult NativePhysicalNativeELFGenerated (constructor NativePhysicalNativeELFArtifact NativePhysicalNativeELFArtifactValue elfBytes codeBytes imageBytes machineBytes identity codeSHA256 imageSHA256 machineSHA256 elfSHA256 commandCount artifactTelemetry) artifactTelemetry)) (nativePhysicalNativeELFTelemetryFor codeBytes imageBytes machineBytes elfBytes identity codeSHA256 imageSHA256 machineSHA256 elfSHA256))) b"")) b"")) b"")) b"")) (wrapMachineCodeSparseLarge machineBytes))) (bytes-append codeBytes imageBytes))) (branch X86NativeAssemblyEncodeDuplicateLabel duplicateName . (nativePhysicalNativeELFFail nativePhysicalNativeELFAssemblyFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFDuplicateLabel duplicateName) b"" duplicateName)) (branch X86NativeAssemblyEncodeOffsetOverflow . (nativePhysicalNativeELFFail nativePhysicalNativeELFAssemblyFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFAssemblyOffsetOverflow) b"" b"")) (branch X86NativeAssemblyMissingLabel missingName . (nativePhysicalNativeELFFail nativePhysicalNativeELFAssemblyFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFMissingLabel missingName) b"" missingName)) (branch X86NativeAssemblyDisplacementOutOfRange distantName . (nativePhysicalNativeELFFail nativePhysicalNativeELFAssemblyFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFDisplacementOutOfRange distantName) b"" distantName)))))) (branch NativePhysicalImageGenerationFailed imageError failureTelemetry . (nativePhysicalNativeELFFail nativePhysicalNativeELFImageFailurePhase (constructor NativePhysicalNativeELFErrorCode NativePhysicalNativeELFImageGenerationFailed imageError) (nativePhysicalNativeELFEncodeImageFailureTelemetry failureTelemetry) b"")))) -- Whole-program publication path. The NativePhysicalProgram remains a -- checked Alpha value, while the compiler lowers its constructor tree to the -- ALPXPHY2 records in one backend operation. This is semantically the fast -- image encoder above (including the inert 64-byte zero digest), but avoids -- interpreting thousands of byte-building eliminators during compilation. def nativePhysicalGenerateNativeELFBytesDirect = (lambda unrestricted program : (family NativePhysicalProgram) . (wrapMachineCodeSparseLarge (bytes-append (compiler-native-encode (family X86NativeAssembly) nativePhysicalNativeAssembly) (compiler-native-encode (family NativePhysicalProgram) program)))) -- Final projection used by whole-program artifact roots. Failure stays -- fail-closed: the compiler's direct artifact writer rejects the empty value -- as a non-ELF instead of executing a generated emitter to discover it later. def nativePhysicalNativeELFResultBytes = (lambda unrestricted result : (family NativePhysicalNativeELFResult) . (eliminate NativePhysicalNativeELFResult (lambda unrestricted current : (family NativePhysicalNativeELFResult) . Bytes) result (branch NativePhysicalNativeELFGenerated artifact successTelemetry . (eliminate NativePhysicalNativeELFArtifact (lambda unrestricted current : (family NativePhysicalNativeELFArtifact) . Bytes) artifact (branch NativePhysicalNativeELFArtifactValue elfBytes codeBytes imageBytes machineBytes identity codeSHA imageSHA machineSHA elfSHA commandCount telemetry . elfBytes))) (branch NativePhysicalNativeELFGenerationFailed error telemetry . b"")))