module Runtime.NativePhysicalImage import Data.SHA256Digest import Model.Config import Model.Parameter import Runtime.NativePhysicalProgram import Runtime.NativePhysicalImagePlan import Runtime.NativeTelemetry import Std.Natural family NativePhysicalImageErrorCode : Type 0 constructor NativePhysicalImageProgramRejected field unrestricted nativePhysicalImageRejectedProgramError : (family NativePhysicalErrorCode) constructor NativePhysicalImageExtentOverflow constructor NativePhysicalImageCommandErrorIdentityEmpty constructor NativePhysicalImageCommandCountMismatch end-family family NativePhysicalImageResultDescriptor : Type 0 constructor NativePhysicalImageResultDescriptorValue field unrestricted nativePhysicalImageResultKind : (family ModelWord64) field unrestricted nativePhysicalImageResultSlot : (family ModelWord64) end-family family NativePhysicalEncodedCommand : Type 0 constructor NativePhysicalEncodedCommandValue field unrestricted nativePhysicalEncodedCommandBytes : Bytes field unrestricted nativePhysicalEncodedCommandPayloadBytes : Nat field unrestricted nativePhysicalEncodedCommandAuxiliaryBytes : Nat field unrestricted nativePhysicalEncodedCommandErrorBytes : Nat end-family family NativePhysicalEncodedCommandResult : Type 0 constructor NativePhysicalCommandEncoded field unrestricted nativePhysicalEncodedCommand : (family NativePhysicalEncodedCommand) constructor NativePhysicalCommandEncodingFailed field unrestricted nativePhysicalCommandEncodingError : (family NativePhysicalImageErrorCode) end-family family NativePhysicalEncodedCommands : Type 0 constructor NativePhysicalEncodedCommandsValue field unrestricted nativePhysicalEncodedCommandsBytes : Bytes field unrestricted nativePhysicalEncodedCommandsCount : Nat field unrestricted nativePhysicalEncodedCommandsPayloadBytes : Nat field unrestricted nativePhysicalEncodedCommandsAuxiliaryBytes : Nat field unrestricted nativePhysicalEncodedCommandsErrorBytes : Nat end-family family NativePhysicalEncodedCommandsResult : Type 0 constructor NativePhysicalCommandsEncoded field unrestricted nativePhysicalEncodedCommands : (family NativePhysicalEncodedCommands) constructor NativePhysicalCommandsEncodingFailed field unrestricted nativePhysicalCommandsEncodingError : (family NativePhysicalImageErrorCode) field unrestricted nativePhysicalCommandsEncodingOrdinal : Nat end-family family NativePhysicalImageTelemetry : Type 0 constructor NativePhysicalImageTelemetryValue field unrestricted nativePhysicalImageTelemetryCounts : (family NativePhysicalCounts) field unrestricted nativePhysicalImageTelemetryPayloadBytes : Nat field unrestricted nativePhysicalImageTelemetryAuxiliaryBytes : Nat field unrestricted nativePhysicalImageTelemetryErrorIdentityBytes : Nat field unrestricted nativePhysicalImageTelemetryBodyBytes : Nat field unrestricted nativePhysicalImageTelemetryOutputBytes : Nat field unrestricted nativePhysicalImageTelemetryFailures : Nat field unrestricted nativePhysicalImageTelemetryFallbacks : Nat field unrestricted nativePhysicalImageTelemetryIdentity : Bytes field unrestricted nativePhysicalImageTelemetryBodySHA256 : Bytes end-family family NativePhysicalImageFailureTelemetry : Type 0 constructor NativePhysicalImageFailureTelemetryValue field unrestricted nativePhysicalImageFailureValidation : (family NativePhysicalValidationTelemetry) field unrestricted nativePhysicalImageFailureEncodedCommands : Nat field unrestricted nativePhysicalImageFailureBodyBytes : Nat field unrestricted nativePhysicalImageFailureCode : Bytes end-family family NativePhysicalImage : Type 0 constructor NativePhysicalImageValue field unrestricted nativePhysicalImageBytes : Bytes field unrestricted nativePhysicalImageBodySHA256 : Bytes field unrestricted nativePhysicalImageProgramIdentity : Bytes field unrestricted nativePhysicalImageCommandCount : Nat field unrestricted nativePhysicalImageStateExtent : (family ModelWord64) field unrestricted nativePhysicalImageResultSlots : (family ModelWord64) field unrestricted nativePhysicalImageTelemetry : (family NativePhysicalImageTelemetry) end-family family NativePhysicalImageResult : Type 0 constructor NativePhysicalImageGenerated field unrestricted nativePhysicalGeneratedImage : (family NativePhysicalImage) field unrestricted nativePhysicalImageSuccessTelemetry : (family NativePhysicalImageTelemetry) constructor NativePhysicalImageGenerationFailed field unrestricted nativePhysicalImageGenerationError : (family NativePhysicalImageErrorCode) field unrestricted nativePhysicalImageGenerationFailureTelemetry : (family NativePhysicalImageFailureTelemetry) end-family def nativePhysicalImageErrorCodeBytes = (lambda unrestricted code : (family NativePhysicalImageErrorCode) . (eliminate NativePhysicalImageErrorCode (lambda unrestricted current : (family NativePhysicalImageErrorCode) . Bytes) code (branch NativePhysicalImageProgramRejected programError . (bytes-append b"ALPHA-PHYIMG-001-" (nativePhysicalErrorCodeBytes programError))) (branch NativePhysicalImageExtentOverflow . b"ALPHA-PHYIMG-002") (branch NativePhysicalImageCommandErrorIdentityEmpty . b"ALPHA-PHYIMG-003") (branch NativePhysicalImageCommandCountMismatch . b"ALPHA-PHYIMG-004"))) def nativePhysicalImageMagic : Bytes = b"ALPXPHY2" def nativePhysicalImageVersion : (family ModelWord64) = 2 def nativePhysicalImageZeroWord64 : (family ModelWord64) = 0 def nativePhysicalImageWord64 = (lambda unrestricted byte0 : Byte . (constructor ModelWord64 ModelWord64Value byte0 (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0))) def nativePhysicalImageWord64Bytes = (lambda unrestricted value : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . Bytes) value (branch ModelWord64Value byte0 byte1 byte2 byte3 byte4 byte5 byte6 byte7 . (bytes-cons byte0 (bytes-cons byte1 (bytes-cons byte2 (bytes-cons byte3 (bytes-cons byte4 (bytes-cons byte5 (bytes-cons byte6 (bytes-cons byte7 b""))))))))))) def nativePhysicalImageSlotWord = (lambda unrestricted slot : (family NativePhysicalSlot) . (eliminate NativePhysicalSlot (lambda unrestricted current : (family NativePhysicalSlot) . (family ModelWord64)) slot (branch NativePhysicalSlotValue index . index))) def nativePhysicalImageResultDescriptor = (lambda unrestricted binding : (family NativePhysicalResultBinding) . (eliminate NativePhysicalResultBinding (lambda unrestricted current : (family NativePhysicalResultBinding) . (family NativePhysicalImageResultDescriptor)) binding (branch NativePhysicalDiscardResult . (constructor NativePhysicalImageResultDescriptor NativePhysicalImageResultDescriptorValue nativePhysicalImageZeroWord64 nativePhysicalImageZeroWord64)) (branch NativePhysicalStoreResult slot . (constructor NativePhysicalImageResultDescriptor NativePhysicalImageResultDescriptorValue (nativePhysicalImageWord64 (byte 1)) (nativePhysicalImageSlotWord slot))))) def nativePhysicalImageOperandDescriptor = (lambda unrestricted operand : (family NativePhysicalOperand) . (eliminate NativePhysicalOperand (lambda unrestricted current : (family NativePhysicalOperand) . Bytes) operand (branch NativePhysicalImmediate value . (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 0))) (bytes-append (nativePhysicalImageWord64Bytes value) (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64)))) (branch NativePhysicalResultValue slot . (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 1))) (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageSlotWord slot)) (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64)))) (branch NativePhysicalResultAddress slot offset . (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 2))) (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageSlotWord slot)) (nativePhysicalImageWord64Bytes offset)))) (branch NativePhysicalStateAddress offset . (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 3))) (bytes-append (nativePhysicalImageWord64Bytes offset) (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64)))) (branch NativePhysicalStateLoad64 offset . (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 4))) (bytes-append (nativePhysicalImageWord64Bytes offset) (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64)))) (branch NativePhysicalPayloadAddress offset . (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 5))) (bytes-append (nativePhysicalImageWord64Bytes offset) (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64)))) (branch NativePhysicalPayloadLoad64 offset . (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 6))) (bytes-append (nativePhysicalImageWord64Bytes offset) (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64)))) (branch NativePhysicalProcessArgument index . (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 7))) (bytes-append (nativePhysicalImageWord64Bytes index) (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64)))) (branch NativePhysicalLoopAffine base stride . (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 (byte 8))) (bytes-append (nativePhysicalImageWord64Bytes base) (nativePhysicalImageWord64Bytes stride)))))) def nativePhysicalImageZeroOperand : (family NativePhysicalOperand) = (constructor NativePhysicalOperand NativePhysicalImmediate nativePhysicalImageZeroWord64) def nativePhysicalImageSevenOperandBytes = (lambda unrestricted operand0 : (family NativePhysicalOperand) . (lambda unrestricted operand1 : (family NativePhysicalOperand) . (lambda unrestricted operand2 : (family NativePhysicalOperand) . (lambda unrestricted operand3 : (family NativePhysicalOperand) . (lambda unrestricted operand4 : (family NativePhysicalOperand) . (lambda unrestricted operand5 : (family NativePhysicalOperand) . (lambda unrestricted operand6 : (family NativePhysicalOperand) . (bytes-append (nativePhysicalImageOperandDescriptor operand0) (bytes-append (nativePhysicalImageOperandDescriptor operand1) (bytes-append (nativePhysicalImageOperandDescriptor operand2) (bytes-append (nativePhysicalImageOperandDescriptor operand3) (bytes-append (nativePhysicalImageOperandDescriptor operand4) (bytes-append (nativePhysicalImageOperandDescriptor operand5) (nativePhysicalImageOperandDescriptor operand6)))))))))))))) def nativePhysicalImageSystemCallOperandBytes = (lambda unrestricted number : (family NativePhysicalOperand) . (lambda unrestricted arguments : (family NativePhysicalArguments) . (eliminate NativePhysicalArguments (lambda unrestricted current : (family NativePhysicalArguments) . Bytes) arguments (branch NativePhysicalArgumentsValue arg0 arg1 arg2 arg3 arg4 arg5 . (nativePhysicalImageSevenOperandBytes number arg0 arg1 arg2 arg3 arg4 arg5))))) def nativePhysicalImageRoutineOperandBytes = (lambda unrestricted arguments : (family NativePhysicalArguments) . (eliminate NativePhysicalArguments (lambda unrestricted current : (family NativePhysicalArguments) . Bytes) arguments (branch NativePhysicalArgumentsValue arg0 arg1 arg2 arg3 arg4 arg5 . (nativePhysicalImageSevenOperandBytes arg0 arg1 arg2 arg3 arg4 arg5 nativePhysicalImageZeroOperand)))) def nativePhysicalImageCommandFixedBytes : Nat = (byte-to-nat (byte 232)) def nativePhysicalImageRecordAlignment : Nat = (byte-to-nat (byte 4)) -- Legacy V2 padded syscall payloads, but this does not align every record. -- Preserve its bytes for existing x86 artifacts. V3 separately pads the complete -- record without altering any content extent; Runtime.NativePhysicalImagePlan -- owns that wire contract and the AArch64 runtime requires it. def nativePhysicalImageSystemCallPayloadPadding = (lambda unrestricted payloadLength : Nat . (naturalModuloUnchecked (naturalSaturatingSubtract nativePhysicalImageRecordAlignment (naturalModuloUnchecked payloadLength nativePhysicalImageRecordAlignment)) nativePhysicalImageRecordAlignment)) def nativePhysicalImageZeroPad = (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted current : Nat . Bytes) b"" (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction))) count)) def nativePhysicalImageAlignedSystemCallPayload = (lambda unrestricted payload : Bytes . (bytes-append payload (nativePhysicalImageZeroPad (nativePhysicalImageSystemCallPayloadPadding (bytes-length payload))))) def nativePhysicalImageMagicFor = (lambda unrestricted format : (family NativePhysicalImageFormat) . (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . Bytes) format (branch NativePhysicalImagePackedV2 . nativePhysicalImageMagic) (branch NativePhysicalImageAlignedV3 . b"ALPXPHY3"))) def nativePhysicalImageVersionFor = (lambda unrestricted format : (family NativePhysicalImageFormat) . (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . (family ModelWord64)) format (branch NativePhysicalImagePackedV2 . nativePhysicalImageVersion) (branch NativePhysicalImageAlignedV3 . (nativePhysicalImageWord64 (byte 3))))) def nativePhysicalImageRecordExtentFor = (lambda unrestricted format : (family NativePhysicalImageFormat) . (lambda unrestricted extent : Nat . (eliminate NativePhysicalImageFormat (lambda unrestricted current : (family NativePhysicalImageFormat) . Nat) format (branch NativePhysicalImagePackedV2 . extent) (branch NativePhysicalImageAlignedV3 . (nativePhysicalImageAlignedExtent extent))))) def nativePhysicalImageRecordPaddingFor = (lambda unrestricted format : (family NativePhysicalImageFormat) . (lambda unrestricted extent : Nat . (naturalSaturatingSubtract (nativePhysicalImageRecordExtentFor format extent) extent))) def nativePhysicalImageCommandRecordForFormat = (lambda unrestricted format : (family NativePhysicalImageFormat) . (lambda unrestricted tag : Byte . (lambda unrestricted binding : (family NativePhysicalResultBinding) . (lambda unrestricted operands : Bytes . (lambda unrestricted payload : Bytes . (lambda unrestricted auxiliary : Bytes . (lambda unrestricted errorIdentity : Bytes . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalEncodedCommandResult)) (constructor NativePhysicalEncodedCommandResult NativePhysicalCommandEncodingFailed (constructor NativePhysicalImageErrorCode NativePhysicalImageCommandErrorIdentityEmpty)) (lambda unrestricted errorPredecessor : Nat . (lambda unrestricted ignoredError : (family NativePhysicalEncodedCommandResult) . (eliminate NativeTelemetryCounterResult (lambda unrestricted current : (family NativeTelemetryCounterResult) . (family NativePhysicalEncodedCommandResult)) (nativeTelemetryCounterFromNatural (bytes-length payload)) (branch NativeTelemetryCounterSucceeded payloadExtent . (eliminate NativeTelemetryCounterResult (lambda unrestricted current : (family NativeTelemetryCounterResult) . (family NativePhysicalEncodedCommandResult)) (nativeTelemetryCounterFromNatural (bytes-length auxiliary)) (branch NativeTelemetryCounterSucceeded auxiliaryExtent . (eliminate NativeTelemetryCounterResult (lambda unrestricted current : (family NativeTelemetryCounterResult) . (family NativePhysicalEncodedCommandResult)) (nativeTelemetryCounterFromNatural (bytes-length errorIdentity)) (branch NativeTelemetryCounterSucceeded errorExtent . (eliminate NativeTelemetryCounterResult (lambda unrestricted current : (family NativeTelemetryCounterResult) . (family NativePhysicalEncodedCommandResult)) (nativeTelemetryCounterFromNatural (nativePhysicalImageRecordExtentFor format (naturalAdd nativePhysicalImageCommandFixedBytes (naturalAdd (bytes-length payload) (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity)))))) (branch NativeTelemetryCounterSucceeded recordExtent . (eliminate NativePhysicalImageResultDescriptor (lambda unrestricted current : (family NativePhysicalImageResultDescriptor) . (family NativePhysicalEncodedCommandResult)) (nativePhysicalImageResultDescriptor binding) (branch NativePhysicalImageResultDescriptorValue resultKind resultSlot . (constructor NativePhysicalEncodedCommandResult NativePhysicalCommandEncoded (constructor NativePhysicalEncodedCommand NativePhysicalEncodedCommandValue (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageWord64 tag)) (bytes-append (nativePhysicalImageWord64Bytes recordExtent) (bytes-append (nativePhysicalImageWord64Bytes resultKind) (bytes-append (nativePhysicalImageWord64Bytes resultSlot) (bytes-append (nativePhysicalImageWord64Bytes payloadExtent) (bytes-append (nativePhysicalImageWord64Bytes auxiliaryExtent) (bytes-append (nativePhysicalImageWord64Bytes errorExtent) (bytes-append (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64) (bytes-append operands (bytes-append payload (bytes-append auxiliary (bytes-append errorIdentity (nativePhysicalImageZeroPad (nativePhysicalImageRecordPaddingFor format (naturalAdd nativePhysicalImageCommandFixedBytes (naturalAdd (bytes-length payload) (naturalAdd (bytes-length auxiliary) (bytes-length errorIdentity)))))))))))))))))) (bytes-length payload) (bytes-length auxiliary) (bytes-length errorIdentity)))))) (branch NativeTelemetryCounterFailed counterError naturalValue . (constructor NativePhysicalEncodedCommandResult NativePhysicalCommandEncodingFailed (constructor NativePhysicalImageErrorCode NativePhysicalImageExtentOverflow))))) (branch NativeTelemetryCounterFailed counterError naturalValue . (constructor NativePhysicalEncodedCommandResult NativePhysicalCommandEncodingFailed (constructor NativePhysicalImageErrorCode NativePhysicalImageExtentOverflow))))) (branch NativeTelemetryCounterFailed counterError naturalValue . (constructor NativePhysicalEncodedCommandResult NativePhysicalCommandEncodingFailed (constructor NativePhysicalImageErrorCode NativePhysicalImageExtentOverflow))))) (branch NativeTelemetryCounterFailed counterError naturalValue . (constructor NativePhysicalEncodedCommandResult NativePhysicalCommandEncodingFailed (constructor NativePhysicalImageErrorCode NativePhysicalImageExtentOverflow)))))) (bytes-length errorIdentity))))))))) def nativePhysicalImageCommandRecord = (nativePhysicalImageCommandRecordForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2)) def nativePhysicalImageDiscardResult : (family NativePhysicalResultBinding) = (constructor NativePhysicalResultBinding NativePhysicalDiscardResult) -- the binary64 operations' record tags: 14 .. 21, in the family's order def nativePhysicalImageFloat64Tag = (lambda unrestricted kind : (family NativePhysicalFloat64Operation) . (eliminate NativePhysicalFloat64Operation (lambda unrestricted current : (family NativePhysicalFloat64Operation) . Byte) kind (branch NativePhysicalFloat64Add . (byte 14)) (branch NativePhysicalFloat64Subtract . (byte 15)) (branch NativePhysicalFloat64Multiply . (byte 16)) (branch NativePhysicalFloat64Divide . (byte 17)) (branch NativePhysicalFloat64SquareRoot . (byte 18)) (branch NativePhysicalFloat64FromNatural . (byte 19)) (branch NativePhysicalFloat64ToBinary32 . (byte 20)) (branch NativePhysicalFloat64FromBinary32 . (byte 21)))) def nativePhysicalImageEncodeOperationForFormat = (lambda unrestricted format : (family NativePhysicalImageFormat) . (lambda unrestricted operation : (family NativePhysicalOperation) . (lambda unrestricted errorIdentity : Bytes . (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . (family NativePhysicalEncodedCommandResult)) operation (branch NativePhysicalSystemCall number arguments payload result . (nativePhysicalImageCommandRecordForFormat format (byte 1) result (nativePhysicalImageSystemCallOperandBytes number arguments) (nativePhysicalImageAlignedSystemCallPayload payload) b"" errorIdentity)) (branch NativePhysicalCopyPayloadToState destination extent payload . (nativePhysicalImageCommandRecordForFormat format (byte 2) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes (constructor NativePhysicalOperand NativePhysicalImmediate destination) (constructor NativePhysicalOperand NativePhysicalImmediate extent) nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) payload b"" errorIdentity)) (branch NativePhysicalMachineRoutine code arguments result . (nativePhysicalImageCommandRecordForFormat format (byte 3) result (nativePhysicalImageRoutineOperandBytes arguments) code b"" errorIdentity)) (branch NativePhysicalFencePoll address expected maximumPolls . (nativePhysicalImageCommandRecordForFormat format (byte 4) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes address expected (constructor NativePhysicalOperand NativePhysicalImmediate maximumPolls) nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" b"" errorIdentity)) (branch NativePhysicalTelemetryAppend path record . (nativePhysicalImageCommandRecordForFormat format (byte 5) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) path record errorIdentity)) (branch NativePhysicalAssertEqual left right error . (nativePhysicalImageCommandRecordForFormat format (byte 6) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes left right nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" (nativePhysicalErrorCodeBytes error) errorIdentity)) (branch NativePhysicalAssertOneOf observed first second error . (nativePhysicalImageCommandRecordForFormat format (byte 8) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes observed first second nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" (nativePhysicalErrorCodeBytes error) errorIdentity)) (branch NativePhysicalHaltSuccess . (nativePhysicalImageCommandRecordForFormat format (byte 7) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" b"" errorIdentity)) (branch NativePhysicalRepeatBegin count . (nativePhysicalImageCommandRecordForFormat format (byte 9) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes (constructor NativePhysicalOperand NativePhysicalImmediate count) nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" b"" errorIdentity)) (branch NativePhysicalRepeatEnd . (nativePhysicalImageCommandRecordForFormat format (byte 10) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" b"" errorIdentity)) (branch NativePhysicalStoreWord64 destination value . (nativePhysicalImageCommandRecordForFormat format (byte 11) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes destination value nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" b"" errorIdentity)) (branch NativePhysicalFenceWait address expected maximumPolls interval . (nativePhysicalImageCommandRecordForFormat format (byte 12) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes address expected (constructor NativePhysicalOperand NativePhysicalImmediate maximumPolls) (constructor NativePhysicalOperand NativePhysicalImmediate interval) nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" b"" errorIdentity)) (branch NativePhysicalRepeatBeginCounted count . (nativePhysicalImageCommandRecordForFormat format (byte 9) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes count nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" b"" errorIdentity)) (branch NativePhysicalAddWord64 destination left right . (nativePhysicalImageCommandRecordForFormat format (byte 13) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes destination left right nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" b"" errorIdentity)) (branch NativePhysicalFloat64 kind destination left right . (nativePhysicalImageCommandRecordForFormat format (nativePhysicalImageFloat64Tag kind) nativePhysicalImageDiscardResult (nativePhysicalImageSevenOperandBytes destination left right nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand nativePhysicalImageZeroOperand) b"" b"" errorIdentity)))))) def nativePhysicalImageEncodeOperation = (nativePhysicalImageEncodeOperationForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2)) def nativePhysicalImageEncodeCommandForFormat = (lambda unrestricted format : (family NativePhysicalImageFormat) . (lambda unrestricted command : (family NativePhysicalCommand) . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . (family NativePhysicalEncodedCommandResult)) command (branch NativePhysicalCommandValue operation errorIdentity . (nativePhysicalImageEncodeOperationForFormat format operation errorIdentity))))) def nativePhysicalImageEncodeCommand = (nativePhysicalImageEncodeCommandForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2)) def nativePhysicalImageEncodeCommandsForFormat = (lambda unrestricted format : (family NativePhysicalImageFormat) . (lambda unrestricted commands : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (family NativePhysicalEncodedCommandsResult)) commands (branch NativePhysicalCommandsEnd . (constructor NativePhysicalEncodedCommandsResult NativePhysicalCommandsEncoded (constructor NativePhysicalEncodedCommands NativePhysicalEncodedCommandsValue b"" zero zero zero zero))) (branch NativePhysicalCommandsNext head tail induction . (eliminate NativePhysicalEncodedCommandResult (lambda unrestricted current : (family NativePhysicalEncodedCommandResult) . (family NativePhysicalEncodedCommandsResult)) (nativePhysicalImageEncodeCommandForFormat format head) (branch NativePhysicalCommandEncoded encoded . (eliminate NativePhysicalEncodedCommandsResult (lambda unrestricted current : (family NativePhysicalEncodedCommandsResult) . (family NativePhysicalEncodedCommandsResult)) induction (branch NativePhysicalCommandsEncoded encodedTail . (eliminate NativePhysicalEncodedCommand (lambda unrestricted current : (family NativePhysicalEncodedCommand) . (family NativePhysicalEncodedCommandsResult)) encoded (branch NativePhysicalEncodedCommandValue bytes payloadBytes auxiliaryBytes errorBytes . (eliminate NativePhysicalEncodedCommands (lambda unrestricted current : (family NativePhysicalEncodedCommands) . (family NativePhysicalEncodedCommandsResult)) encodedTail (branch NativePhysicalEncodedCommandsValue tailBytes tailCount tailPayload tailAuxiliary tailError . (constructor NativePhysicalEncodedCommandsResult NativePhysicalCommandsEncoded (constructor NativePhysicalEncodedCommands NativePhysicalEncodedCommandsValue (bytes-append bytes tailBytes) (succ tailCount) (naturalAdd payloadBytes tailPayload) (naturalAdd auxiliaryBytes tailAuxiliary) (naturalAdd errorBytes tailError)))))))) (branch NativePhysicalCommandsEncodingFailed error ordinal . (constructor NativePhysicalEncodedCommandsResult NativePhysicalCommandsEncodingFailed error (succ ordinal))))) (branch NativePhysicalCommandEncodingFailed error . (constructor NativePhysicalEncodedCommandsResult NativePhysicalCommandsEncodingFailed error zero))))))) -- The extent of the record nativePhysicalImageEncodeCommand writes for a -- command: the fixed 232 bytes, the (aligned) payload, the auxiliary bytes and -- the error identity -- the same fields, measured instead of written. Where a -- MachineRoutine's code lands follows from these (see -- nativePhysicalImageRecordAlignment). def nativePhysicalImageCommandExtent = (lambda unrestricted command : (family NativePhysicalCommand) . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . Nat) command (branch NativePhysicalCommandValue operation errorIdentity . (naturalAdd nativePhysicalImageCommandFixedBytes (naturalAdd (bytes-length errorIdentity) (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . Nat) operation (branch NativePhysicalSystemCall number arguments payload result . (naturalAdd (bytes-length payload) (nativePhysicalImageSystemCallPayloadPadding (bytes-length payload)))) (branch NativePhysicalCopyPayloadToState destination extent payload . (bytes-length payload)) (branch NativePhysicalMachineRoutine code arguments result . (bytes-length code)) (branch NativePhysicalFencePoll address expected polls . zero) (branch NativePhysicalTelemetryAppend path record . (naturalAdd (bytes-length path) (bytes-length record))) (branch NativePhysicalAssertEqual left right error . (bytes-length (nativePhysicalErrorCodeBytes error))) (branch NativePhysicalAssertOneOf observed first second error . (bytes-length (nativePhysicalErrorCodeBytes error))) (branch NativePhysicalHaltSuccess . zero) (branch NativePhysicalRepeatBegin count . zero) (branch NativePhysicalRepeatEnd . zero) (branch NativePhysicalStoreWord64 destination value . zero) (branch NativePhysicalFenceWait address expected polls interval . zero) (branch NativePhysicalRepeatBeginCounted count . zero) (branch NativePhysicalAddWord64 destination left right . zero) (branch NativePhysicalFloat64 kind destination left right . zero))))))) def nativePhysicalImageEncodeCommands = (nativePhysicalImageEncodeCommandsForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2)) def nativePhysicalImageFailureTelemetryFor = (lambda unrestricted validation : (family NativePhysicalValidationTelemetry) . (lambda unrestricted encoded : Nat . (lambda unrestricted bodyBytes : Nat . (lambda unrestricted error : (family NativePhysicalImageErrorCode) . (constructor NativePhysicalImageFailureTelemetry NativePhysicalImageFailureTelemetryValue validation encoded bodyBytes (nativePhysicalImageErrorCodeBytes error)))))) def nativePhysicalImageFail = (lambda unrestricted validation : (family NativePhysicalValidationTelemetry) . (lambda unrestricted encoded : Nat . (lambda unrestricted bodyBytes : Nat . (lambda unrestricted error : (family NativePhysicalImageErrorCode) . (constructor NativePhysicalImageResult NativePhysicalImageGenerationFailed error (nativePhysicalImageFailureTelemetryFor validation encoded bodyBytes error)))))) def nativePhysicalImageTelemetryFor = (lambda unrestricted counts : (family NativePhysicalCounts) . (lambda unrestricted payloadBytes : Nat . (lambda unrestricted auxiliaryBytes : Nat . (lambda unrestricted errorBytes : Nat . (lambda unrestricted bodyBytes : Nat . (lambda unrestricted outputBytes : Nat . (lambda unrestricted fallbacks : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted digest : Bytes . (constructor NativePhysicalImageTelemetry NativePhysicalImageTelemetryValue counts payloadBytes auxiliaryBytes errorBytes bodyBytes outputBytes zero fallbacks identity digest)))))))))) -- Body-digest strategy is now a parameter so the FAST (GPU bring-up) ELF path -- can supply a stub instead of paying for a real SHA-256 of the image body. -- The digest lives in the image header's telemetry region [112,176); the native -- loader jumps straight to the body at offset 176 (NativePhysicalNative.alpha, -- "byte 176") and never reads or verifies it, so the choice of digest does not -- change what the emitted ELF executes def nativePhysicalGenerateImageWithBodyDigestForFormat = (lambda unrestricted format : (family NativePhysicalImageFormat) . (lambda unrestricted digestOfBody : (pi unrestricted bodyInput : Bytes . Bytes) . (lambda unrestricted inputProgram : (family NativePhysicalProgram) . (eliminate NativePhysicalProgramValidation (lambda unrestricted current : (family NativePhysicalProgramValidation) . (family NativePhysicalImageResult)) (nativePhysicalValidateProgram inputProgram) (branch NativePhysicalProgramValidated program validation . (eliminate NativePhysicalProgram (lambda unrestricted current : (family NativePhysicalProgram) . (family NativePhysicalImageResult)) program (branch NativePhysicalProgramValue stateExtent resultSlots commands expected identity fallbacks . (eliminate NativePhysicalEncodedCommandsResult (lambda unrestricted current : (family NativePhysicalEncodedCommandsResult) . (family NativePhysicalImageResult)) (nativePhysicalImageEncodeCommandsForFormat format commands) (branch NativePhysicalCommandsEncoded encoded . (eliminate NativePhysicalEncodedCommands (lambda unrestricted current : (family NativePhysicalEncodedCommands) . (family NativePhysicalImageResult)) encoded (branch NativePhysicalEncodedCommandsValue body commandCount payloadBytes auxiliaryBytes errorBytes . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalImageResult)) (nativePhysicalImageFail validation commandCount (bytes-length body) (constructor NativePhysicalImageErrorCode NativePhysicalImageCommandCountMismatch)) (lambda unrestricted countPredecessor : Nat . (lambda unrestricted ignoredCount : (family NativePhysicalImageResult) . (eliminate NativeTelemetryCounterResult (lambda unrestricted current : (family NativeTelemetryCounterResult) . (family NativePhysicalImageResult)) (nativeTelemetryCounterFromNatural commandCount) (branch NativeTelemetryCounterSucceeded commandCountWord . (eliminate NativeTelemetryCounterResult (lambda unrestricted current : (family NativeTelemetryCounterResult) . (family NativePhysicalImageResult)) (nativeTelemetryCounterFromNatural (bytes-length body)) (branch NativeTelemetryCounterSucceeded bodyExtent . (app (lambda unrestricted bodyDigest : Bytes . (app (lambda unrestricted output : Bytes . (app (lambda unrestricted telemetry : (family NativePhysicalImageTelemetry) . (constructor NativePhysicalImageResult NativePhysicalImageGenerated (constructor NativePhysicalImage NativePhysicalImageValue output bodyDigest identity commandCount stateExtent resultSlots telemetry) telemetry)) (nativePhysicalImageTelemetryFor (nativePhysicalCommandsCounts commands) payloadBytes auxiliaryBytes errorBytes (bytes-length body) (bytes-length output) fallbacks identity bodyDigest))) (bytes-append (nativePhysicalImageMagicFor format) (bytes-append (nativePhysicalImageWord64Bytes (nativePhysicalImageVersionFor format)) (bytes-append (nativePhysicalImageWord64Bytes commandCountWord) (bytes-append (nativePhysicalImageWord64Bytes stateExtent) (bytes-append (nativePhysicalImageWord64Bytes resultSlots) (bytes-append (nativePhysicalImageWord64Bytes bodyExtent) (bytes-append identity (bytes-append bodyDigest body)))))))))) (digestOfBody body))) (branch NativeTelemetryCounterFailed counterError naturalValue . (nativePhysicalImageFail validation commandCount (bytes-length body) (constructor NativePhysicalImageErrorCode NativePhysicalImageExtentOverflow))))) (branch NativeTelemetryCounterFailed counterError naturalValue . (nativePhysicalImageFail validation commandCount (bytes-length body) (constructor NativePhysicalImageErrorCode NativePhysicalImageExtentOverflow)))))) (naturalEqual commandCount expected))))) (branch NativePhysicalCommandsEncodingFailed error ordinal . (nativePhysicalImageFail validation ordinal zero error)))))) (branch NativePhysicalProgramRejected programError validation . (nativePhysicalImageFail validation zero zero (constructor NativePhysicalImageErrorCode NativePhysicalImageProgramRejected programError))))))) -- Real body digest: the SHA-256 hex of the image body (unchanged behaviour for -- every non-fast caller, e.g. Training/Inference receipt ELFs). def nativePhysicalGenerateImageWithBodyDigest = (nativePhysicalGenerateImageWithBodyDigestForFormat (constructor NativePhysicalImageFormat NativePhysicalImagePackedV2)) def nativePhysicalImageRealBodyDigest = (lambda unrestricted bodyInput : Bytes . (sha256HexBytesOrEmpty (sha256Hex bodyInput))) -- Stub body digest for the FAST path: 64 zero bytes, matching the exact width of -- the real 64-hex-char digest so the image layout (and the body offset 176 that -- the loader jumps to) is byte-identical; only the inert digest field differs. def nativePhysicalImageStubBodyDigest = (lambda unrestricted bodyInput : Bytes . (bytes 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0)) def nativePhysicalGenerateImage = (lambda unrestricted inputProgram : (family NativePhysicalProgram) . (nativePhysicalGenerateImageWithBodyDigest nativePhysicalImageRealBodyDigest inputProgram)) def nativePhysicalGenerateImageFast = (lambda unrestricted inputProgram : (family NativePhysicalProgram) . (nativePhysicalGenerateImageWithBodyDigest nativePhysicalImageStubBodyDigest inputProgram)) -- Reference encoder for native AArch64 programs (already in the target ABI). def nativePhysicalGenerateImageAlignedFast = (nativePhysicalGenerateImageWithBodyDigestForFormat (constructor NativePhysicalImageFormat NativePhysicalImageAlignedV3) nativePhysicalImageStubBodyDigest)