module Runtime.NativePhysicalProgramComposer import Model.Word64 import Runtime.NativePhysicalProgram import Std.Natural import Model.Parameter family NativePhysicalProgramComposeAddressClass : Type 0 constructor NativePhysicalProgramComposeStateAddress constructor NativePhysicalProgramComposeResultSlot constructor NativePhysicalProgramComposePayloadAddress constructor NativePhysicalProgramComposeStateExtent constructor NativePhysicalProgramComposeResultExtent end-family family NativePhysicalProgramComposeErrorCode : Type 0 constructor NativePhysicalProgramComposeIdentityInvalid constructor NativePhysicalProgramComposeTrainingRejected field unrestricted nativePhysicalProgramComposeTrainingError : (family NativePhysicalErrorCode) constructor NativePhysicalProgramComposeInferenceRejected field unrestricted nativePhysicalProgramComposeInferenceError : (family NativePhysicalErrorCode) constructor NativePhysicalProgramComposeArithmeticFailed field unrestricted nativePhysicalProgramComposeAddressClass : (family NativePhysicalProgramComposeAddressClass) field unrestricted nativePhysicalProgramComposeArithmeticError : (family ModelWord64ArithmeticErrorCode) constructor NativePhysicalProgramComposeTrainingHaltMissing constructor NativePhysicalProgramComposeTrainingHaltNotFinal constructor NativePhysicalProgramComposeCombinedRejected field unrestricted nativePhysicalProgramComposeCombinedError : (family NativePhysicalErrorCode) end-family family NativePhysicalProgramComposeTelemetry : Type 0 constructor NativePhysicalProgramComposeTelemetryValue field unrestricted nativePhysicalProgramComposeTrainingCommands : Nat field unrestricted nativePhysicalProgramComposeInferenceCommands : Nat field unrestricted nativePhysicalProgramComposeCombinedCommands : Nat field unrestricted nativePhysicalProgramComposeCommandsRelocated : Nat field unrestricted nativePhysicalProgramComposeOperationsRelocated : Nat field unrestricted nativePhysicalProgramComposeOperandsRelocated : Nat field unrestricted nativePhysicalProgramComposeArithmeticChecks : Nat field unrestricted nativePhysicalProgramComposeTrainingHaltsRemoved : Nat field unrestricted nativePhysicalProgramComposeProgramValidations : Nat field unrestricted nativePhysicalProgramComposeFailures : Nat field unrestricted nativePhysicalProgramComposeHostFallbacks : Nat field unrestricted nativePhysicalProgramComposeTrainingIdentity : Bytes field unrestricted nativePhysicalProgramComposeInferenceIdentity : Bytes field unrestricted nativePhysicalProgramComposeCombinedIdentity : Bytes field unrestricted nativePhysicalProgramComposeLastError : Bytes end-family family NativePhysicalProgramComposeOperandResult : Type 0 constructor NativePhysicalProgramComposeOperandRelocated field unrestricted nativePhysicalProgramComposeRelocatedOperand : (family NativePhysicalOperand) field unrestricted nativePhysicalProgramComposeOperandRelocations : Nat field unrestricted nativePhysicalProgramComposeOperandArithmeticChecks : Nat constructor NativePhysicalProgramComposeOperandRejected field unrestricted nativePhysicalProgramComposeOperandError : (family NativePhysicalProgramComposeErrorCode) field unrestricted nativePhysicalProgramComposeRejectedOperandRelocations : Nat field unrestricted nativePhysicalProgramComposeRejectedOperandArithmeticChecks : Nat end-family family NativePhysicalProgramComposeArgumentsResult : Type 0 constructor NativePhysicalProgramComposeArgumentsRelocated field unrestricted nativePhysicalProgramComposeRelocatedArguments : (family NativePhysicalArguments) field unrestricted nativePhysicalProgramComposeArgumentsRelocations : Nat field unrestricted nativePhysicalProgramComposeArgumentsArithmeticChecks : Nat constructor NativePhysicalProgramComposeArgumentsRejected field unrestricted nativePhysicalProgramComposeArgumentsError : (family NativePhysicalProgramComposeErrorCode) field unrestricted nativePhysicalProgramComposeRejectedArgumentsRelocations : Nat field unrestricted nativePhysicalProgramComposeRejectedArgumentsArithmeticChecks : Nat end-family family NativePhysicalProgramComposeBindingResult : Type 0 constructor NativePhysicalProgramComposeBindingRelocated field unrestricted nativePhysicalProgramComposeRelocatedBinding : (family NativePhysicalResultBinding) field unrestricted nativePhysicalProgramComposeBindingRelocations : Nat field unrestricted nativePhysicalProgramComposeBindingArithmeticChecks : Nat constructor NativePhysicalProgramComposeBindingRejected field unrestricted nativePhysicalProgramComposeBindingError : (family NativePhysicalProgramComposeErrorCode) end-family family NativePhysicalProgramComposeOperationResult : Type 0 constructor NativePhysicalProgramComposeOperationRelocated field unrestricted nativePhysicalProgramComposeRelocatedOperation : (family NativePhysicalOperation) field unrestricted nativePhysicalProgramComposeOperationOperandRelocations : Nat field unrestricted nativePhysicalProgramComposeOperationArithmeticChecks : Nat constructor NativePhysicalProgramComposeOperationRejected field unrestricted nativePhysicalProgramComposeOperationError : (family NativePhysicalProgramComposeErrorCode) field unrestricted nativePhysicalProgramComposeRejectedOperationRelocations : Nat field unrestricted nativePhysicalProgramComposeRejectedOperationArithmeticChecks : Nat end-family family NativePhysicalProgramComposeCommandsResult : Type 0 constructor NativePhysicalProgramComposeCommandsRelocated field unrestricted nativePhysicalProgramComposeRelocatedCommands : (family NativePhysicalCommands) field unrestricted nativePhysicalProgramComposeRelocatedCommandCount : Nat field unrestricted nativePhysicalProgramComposeRelocatedOperationCount : Nat field unrestricted nativePhysicalProgramComposeRelocatedOperandCount : Nat field unrestricted nativePhysicalProgramComposeCommandsArithmeticChecks : Nat constructor NativePhysicalProgramComposeCommandsRejected field unrestricted nativePhysicalProgramComposeCommandsError : (family NativePhysicalProgramComposeErrorCode) field unrestricted nativePhysicalProgramComposeRejectedCommandCount : Nat field unrestricted nativePhysicalProgramComposeRejectedOperationCount : Nat field unrestricted nativePhysicalProgramComposeRejectedOperandCount : Nat field unrestricted nativePhysicalProgramComposeRejectedArithmeticChecks : Nat end-family family NativePhysicalProgramComposeStripResult : Type 0 constructor NativePhysicalProgramComposeStripEmpty constructor NativePhysicalProgramComposeStripSucceeded field unrestricted nativePhysicalProgramComposeStrippedCommands : (family NativePhysicalCommands) field unrestricted nativePhysicalProgramComposeStrippedCount : Nat constructor NativePhysicalProgramComposeStripRejected field unrestricted nativePhysicalProgramComposeStripError : (family NativePhysicalProgramComposeErrorCode) field unrestricted nativePhysicalProgramComposeStripVisited : Nat end-family family NativePhysicalProgramComposeResult : Type 0 constructor NativePhysicalProgramComposed field unrestricted nativePhysicalProgramComposeProgram : (family NativePhysicalProgram) field unrestricted nativePhysicalProgramComposeValidation : (family NativePhysicalProgramValidation) field unrestricted nativePhysicalProgramComposeSuccessTelemetry : (family NativePhysicalProgramComposeTelemetry) constructor NativePhysicalProgramCompositionRejected field unrestricted nativePhysicalProgramCompositionError : (family NativePhysicalProgramComposeErrorCode) field unrestricted nativePhysicalProgramComposeFailureTelemetry : (family NativePhysicalProgramComposeTelemetry) end-family def nativePhysicalProgramComposeErrorCodeBytes = (lambda unrestricted code : (family NativePhysicalProgramComposeErrorCode) . (eliminate NativePhysicalProgramComposeErrorCode (lambda unrestricted current : (family NativePhysicalProgramComposeErrorCode) . Bytes) code (branch NativePhysicalProgramComposeIdentityInvalid . b"ALPHA-PCOMP-001") (branch NativePhysicalProgramComposeTrainingRejected error . (bytes-append b"ALPHA-PCOMP-002-" (app nativePhysicalErrorCodeBytes error))) (branch NativePhysicalProgramComposeInferenceRejected error . (bytes-append b"ALPHA-PCOMP-003-" (app nativePhysicalErrorCodeBytes error))) (branch NativePhysicalProgramComposeArithmeticFailed addressClass error . (bytes-append b"ALPHA-PCOMP-004-" (app modelWord64ArithmeticErrorCodeBytes error))) (branch NativePhysicalProgramComposeTrainingHaltMissing . b"ALPHA-PCOMP-005") (branch NativePhysicalProgramComposeTrainingHaltNotFinal . b"ALPHA-PCOMP-006") (branch NativePhysicalProgramComposeCombinedRejected error . (bytes-append b"ALPHA-PCOMP-007-" (app nativePhysicalErrorCodeBytes error))))) def nativePhysicalProgramComposeTelemetry = (lambda unrestricted trainingCommands : Nat . (lambda unrestricted inferenceCommands : Nat . (lambda unrestricted combinedCommands : Nat . (lambda unrestricted relocatedCommands : Nat . (lambda unrestricted relocatedOperations : Nat . (lambda unrestricted relocatedOperands : Nat . (lambda unrestricted arithmeticChecks : Nat . (lambda unrestricted haltsRemoved : Nat . (lambda unrestricted validations : Nat . (lambda unrestricted failures : Nat . (lambda unrestricted trainingIdentity : Bytes . (lambda unrestricted inferenceIdentity : Bytes . (lambda unrestricted combinedIdentity : Bytes . (lambda unrestricted lastError : Bytes . (constructor NativePhysicalProgramComposeTelemetry NativePhysicalProgramComposeTelemetryValue trainingCommands inferenceCommands combinedCommands relocatedCommands relocatedOperations relocatedOperands arithmeticChecks haltsRemoved validations failures zero trainingIdentity inferenceIdentity combinedIdentity lastError))))))))))))))) def nativePhysicalProgramComposeCommandsCount = (lambda unrestricted commands : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . Nat) commands (branch NativePhysicalCommandsEnd . zero) (branch NativePhysicalCommandsNext head tail induction . (succ induction)))) def nativePhysicalProgramComposeCommandsAppend = (lambda unrestricted left : (family NativePhysicalCommands) . (lambda unrestricted right : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (family NativePhysicalCommands)) left (branch NativePhysicalCommandsEnd . right) (branch NativePhysicalCommandsNext head tail induction . (constructor NativePhysicalCommands NativePhysicalCommandsNext head induction))))) def nativePhysicalProgramComposeProgramIdentity = (lambda unrestricted program : (family NativePhysicalProgram) . (eliminate NativePhysicalProgram (lambda unrestricted current : (family NativePhysicalProgram) . Bytes) program (branch NativePhysicalProgramValue stateExtent resultSlots commands expected identity fallbacks . identity))) def nativePhysicalProgramComposeProgramCommands = (lambda unrestricted program : (family NativePhysicalProgram) . (eliminate NativePhysicalProgram (lambda unrestricted current : (family NativePhysicalProgram) . (family NativePhysicalCommands)) program (branch NativePhysicalProgramValue stateExtent resultSlots commands expected identity fallbacks . commands))) def nativePhysicalProgramComposeProgramPayloadBytes = (lambda unrestricted program : (family NativePhysicalProgram) . (eliminate NativePhysicalProgram (lambda unrestricted current : (family NativePhysicalProgram) . Nat) program (branch NativePhysicalProgramValue stateExtent resultSlots commands expected identity fallbacks . (eliminate NativePhysicalCounts (lambda unrestricted current : (family NativePhysicalCounts) . Nat) (app nativePhysicalCommandsCounts commands) (branch NativePhysicalCountsValue commandCount systemCalls copies routines polls telemetry assertions halts payloadBytes . payloadBytes))))) def nativePhysicalProgramComposeWord64FromNatural = (lambda unrestricted value : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family ModelWord64CheckedResult)) (constructor ModelWord64CheckedResult ModelWord64CheckedSucceeded modelWord64Zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family ModelWord64CheckedResult) . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family ModelWord64CheckedResult)) induction (branch ModelWord64CheckedSucceeded prior . (app (app modelWord64AddChecked prior) modelWord64One)) (branch ModelWord64CheckedFailed error . induction)))) value)) def nativePhysicalProgramComposeShiftOperandValue = (lambda unrestricted addressClass : (family NativePhysicalProgramComposeAddressClass) . (lambda unrestricted base : (family ModelWord64) . (lambda unrestricted value : (family ModelWord64) . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeOperandResult)) (app (app modelWord64AddChecked base) value) (branch ModelWord64CheckedSucceeded shifted . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated (constructor NativePhysicalOperand NativePhysicalImmediate shifted) (succ zero) (succ zero))) (branch ModelWord64CheckedFailed error . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed addressClass error) zero (succ zero))))))) def nativePhysicalProgramComposeRelocateOperand = (lambda unrestricted operand : (family NativePhysicalOperand) . (lambda unrestricted stateBase : (family ModelWord64) . (lambda unrestricted resultBase : (family ModelWord64) . (lambda unrestricted payloadBase : (family ModelWord64) . (eliminate NativePhysicalOperand (lambda unrestricted current : (family NativePhysicalOperand) . (family NativePhysicalProgramComposeOperandResult)) operand (branch NativePhysicalImmediate value . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated operand zero zero)) (branch NativePhysicalResultValue slot . (eliminate NativePhysicalSlot (lambda unrestricted current : (family NativePhysicalSlot) . (family NativePhysicalProgramComposeOperandResult)) slot (branch NativePhysicalSlotValue index . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeOperandResult)) (app (app modelWord64AddChecked resultBase) index) (branch ModelWord64CheckedSucceeded shifted . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated (constructor NativePhysicalOperand NativePhysicalResultValue (constructor NativePhysicalSlot NativePhysicalSlotValue shifted)) (succ zero) (succ zero))) (branch ModelWord64CheckedFailed error . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposeResultSlot) error) zero (succ zero))))))) (branch NativePhysicalResultAddress slot offset . (eliminate NativePhysicalSlot (lambda unrestricted current : (family NativePhysicalSlot) . (family NativePhysicalProgramComposeOperandResult)) slot (branch NativePhysicalSlotValue index . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeOperandResult)) (app (app modelWord64AddChecked resultBase) index) (branch ModelWord64CheckedSucceeded shifted . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated (constructor NativePhysicalOperand NativePhysicalResultAddress (constructor NativePhysicalSlot NativePhysicalSlotValue shifted) offset) (succ zero) (succ zero))) (branch ModelWord64CheckedFailed error . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposeResultSlot) error) zero (succ zero))))))) (branch NativePhysicalStateAddress offset . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeOperandResult)) (app (app modelWord64AddChecked stateBase) offset) (branch ModelWord64CheckedSucceeded shifted . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated (constructor NativePhysicalOperand NativePhysicalStateAddress shifted) (succ zero) (succ zero))) (branch ModelWord64CheckedFailed error . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposeStateAddress) error) zero (succ zero))))) (branch NativePhysicalStateLoad64 offset . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeOperandResult)) (app (app modelWord64AddChecked stateBase) offset) (branch ModelWord64CheckedSucceeded shifted . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated (constructor NativePhysicalOperand NativePhysicalStateLoad64 shifted) (succ zero) (succ zero))) (branch ModelWord64CheckedFailed error . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposeStateAddress) error) zero (succ zero))))) (branch NativePhysicalPayloadAddress offset . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeOperandResult)) (app (app modelWord64AddChecked payloadBase) offset) (branch ModelWord64CheckedSucceeded shifted . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated (constructor NativePhysicalOperand NativePhysicalPayloadAddress shifted) (succ zero) (succ zero))) (branch ModelWord64CheckedFailed error . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposePayloadAddress) error) zero (succ zero))))) (branch NativePhysicalPayloadLoad64 offset . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeOperandResult)) (app (app modelWord64AddChecked payloadBase) offset) (branch ModelWord64CheckedSucceeded shifted . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated (constructor NativePhysicalOperand NativePhysicalPayloadLoad64 shifted) (succ zero) (succ zero))) (branch ModelWord64CheckedFailed error . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposePayloadAddress) error) zero (succ zero))))) (branch NativePhysicalProcessArgument index . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated operand zero zero)) (branch NativePhysicalLoopAffine base stride . (constructor NativePhysicalProgramComposeOperandResult NativePhysicalProgramComposeOperandRelocated operand zero zero))))))) def nativePhysicalProgramComposeRelocateArguments = (lambda unrestricted arguments : (family NativePhysicalArguments) . (lambda unrestricted stateBase : (family ModelWord64) . (lambda unrestricted resultBase : (family ModelWord64) . (lambda unrestricted payloadBase : (family ModelWord64) . (eliminate NativePhysicalArguments (lambda unrestricted current : (family NativePhysicalArguments) . (family NativePhysicalProgramComposeArgumentsResult)) arguments (branch NativePhysicalArgumentsValue a0 a1 a2 a3 a4 a5 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeArgumentsResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand a0) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated r0 n0 c0 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeArgumentsResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand a1) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated r1 n1 c1 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeArgumentsResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand a2) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated r2 n2 c2 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeArgumentsResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand a3) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated r3 n3 c3 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeArgumentsResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand a4) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated r4 n4 c4 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeArgumentsResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand a5) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated r5 n5 c5 . (constructor NativePhysicalProgramComposeArgumentsResult NativePhysicalProgramComposeArgumentsRelocated (constructor NativePhysicalArguments NativePhysicalArgumentsValue r0 r1 r2 r3 r4 r5) (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)) n3)) n4)) n5) (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)) c3)) c4)) c5))) (branch NativePhysicalProgramComposeOperandRejected error n5 c5 . (constructor NativePhysicalProgramComposeArgumentsResult NativePhysicalProgramComposeArgumentsRejected error (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)) n3)) n4)) n5) (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)) c3)) c4)) c5))))) (branch NativePhysicalProgramComposeOperandRejected error n4 c4 . (constructor NativePhysicalProgramComposeArgumentsResult NativePhysicalProgramComposeArgumentsRejected error (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)) n3)) n4) (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)) c3)) c4))))) (branch NativePhysicalProgramComposeOperandRejected error n3 c3 . (constructor NativePhysicalProgramComposeArgumentsResult NativePhysicalProgramComposeArgumentsRejected error (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)) n3) (app (app naturalAdd (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)) c3))))) (branch NativePhysicalProgramComposeOperandRejected error n2 c2 . (constructor NativePhysicalProgramComposeArgumentsResult NativePhysicalProgramComposeArgumentsRejected error (app (app naturalAdd (app (app naturalAdd n0) n1)) n2) (app (app naturalAdd (app (app naturalAdd c0) c1)) c2))))) (branch NativePhysicalProgramComposeOperandRejected error n1 c1 . (constructor NativePhysicalProgramComposeArgumentsResult NativePhysicalProgramComposeArgumentsRejected error (app (app naturalAdd n0) n1) (app (app naturalAdd c0) c1))))) (branch NativePhysicalProgramComposeOperandRejected error relocations checks . (constructor NativePhysicalProgramComposeArgumentsResult NativePhysicalProgramComposeArgumentsRejected error relocations checks))))))))) def nativePhysicalProgramComposeRelocateBinding = (lambda unrestricted binding : (family NativePhysicalResultBinding) . (lambda unrestricted resultBase : (family ModelWord64) . (eliminate NativePhysicalResultBinding (lambda unrestricted current : (family NativePhysicalResultBinding) . (family NativePhysicalProgramComposeBindingResult)) binding (branch NativePhysicalDiscardResult . (constructor NativePhysicalProgramComposeBindingResult NativePhysicalProgramComposeBindingRelocated binding zero zero)) (branch NativePhysicalStoreResult slot . (eliminate NativePhysicalSlot (lambda unrestricted current : (family NativePhysicalSlot) . (family NativePhysicalProgramComposeBindingResult)) slot (branch NativePhysicalSlotValue index . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeBindingResult)) (app (app modelWord64AddChecked resultBase) index) (branch ModelWord64CheckedSucceeded shifted . (constructor NativePhysicalProgramComposeBindingResult NativePhysicalProgramComposeBindingRelocated (constructor NativePhysicalResultBinding NativePhysicalStoreResult (constructor NativePhysicalSlot NativePhysicalSlotValue shifted)) (succ zero) (succ zero))) (branch ModelWord64CheckedFailed error . (constructor NativePhysicalProgramComposeBindingResult NativePhysicalProgramComposeBindingRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposeResultSlot) error)))))))))) def nativePhysicalProgramComposeRelocateOperation = (lambda unrestricted operation : (family NativePhysicalOperation) . (lambda unrestricted stateBase : (family ModelWord64) . (lambda unrestricted resultBase : (family ModelWord64) . (lambda unrestricted payloadBase : (family ModelWord64) . (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . (family NativePhysicalProgramComposeOperationResult)) operation (branch NativePhysicalSystemCall number arguments payload binding . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand number) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedNumber n0 c0 . (eliminate NativePhysicalProgramComposeArgumentsResult (lambda unrestricted current : (family NativePhysicalProgramComposeArgumentsResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateArguments arguments) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeArgumentsRelocated relocatedArguments n1 c1 . (eliminate NativePhysicalProgramComposeBindingResult (lambda unrestricted current : (family NativePhysicalProgramComposeBindingResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app nativePhysicalProgramComposeRelocateBinding binding) resultBase) (branch NativePhysicalProgramComposeBindingRelocated relocatedBinding n2 c2 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated (constructor NativePhysicalOperation NativePhysicalSystemCall relocatedNumber relocatedArguments payload relocatedBinding) (app (app naturalAdd (app (app naturalAdd n0) n1)) n2) (app (app naturalAdd (app (app naturalAdd c0) c1)) c2))) (branch NativePhysicalProgramComposeBindingRejected error . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error (app (app naturalAdd n0) n1) (app (app naturalAdd c0) c1))))) (branch NativePhysicalProgramComposeArgumentsRejected error n1 c1 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error (app (app naturalAdd n0) n1) (app (app naturalAdd c0) c1))))) (branch NativePhysicalProgramComposeOperandRejected error n c . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error n c)) )) (branch NativePhysicalCopyPayloadToState destination extent payload . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app modelWord64AddChecked stateBase) destination) (branch ModelWord64CheckedSucceeded shifted . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated (constructor NativePhysicalOperation NativePhysicalCopyPayloadToState shifted extent payload) (succ zero) (succ zero))) (branch ModelWord64CheckedFailed error . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposeStateAddress) error) zero (succ zero))))) (branch NativePhysicalMachineRoutine machineCode arguments binding . (eliminate NativePhysicalProgramComposeArgumentsResult (lambda unrestricted current : (family NativePhysicalProgramComposeArgumentsResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateArguments arguments) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeArgumentsRelocated relocatedArguments n1 c1 . (eliminate NativePhysicalProgramComposeBindingResult (lambda unrestricted current : (family NativePhysicalProgramComposeBindingResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app nativePhysicalProgramComposeRelocateBinding binding) resultBase) (branch NativePhysicalProgramComposeBindingRelocated relocatedBinding n2 c2 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated (constructor NativePhysicalOperation NativePhysicalMachineRoutine machineCode relocatedArguments relocatedBinding) (app (app naturalAdd n1) n2) (app (app naturalAdd c1) c2))) (branch NativePhysicalProgramComposeBindingRejected error . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error n1 c1)))) (branch NativePhysicalProgramComposeArgumentsRejected error n c . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error n c)) )) (branch NativePhysicalFencePoll address expected maximumPolls . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand address) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedAddress n0 c0 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand expected) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedExpected n1 c1 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated (constructor NativePhysicalOperation NativePhysicalFencePoll relocatedAddress relocatedExpected maximumPolls) (app (app naturalAdd n0) n1) (app (app naturalAdd c0) c1))) (branch NativePhysicalProgramComposeOperandRejected error n1 c1 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error (app (app naturalAdd n0) n1) (app (app naturalAdd c0) c1))))) (branch NativePhysicalProgramComposeOperandRejected error n c . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error n c)) )) (branch NativePhysicalTelemetryAppend path record . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero)) (branch NativePhysicalAssertEqual left right errorCode . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand left) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedLeft n0 c0 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand right) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedRight n1 c1 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated (constructor NativePhysicalOperation NativePhysicalAssertEqual relocatedLeft relocatedRight errorCode) (app (app naturalAdd n0) n1) (app (app naturalAdd c0) c1))) (branch NativePhysicalProgramComposeOperandRejected error n1 c1 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error (app (app naturalAdd n0) n1) (app (app naturalAdd c0) c1))))) (branch NativePhysicalProgramComposeOperandRejected error n c . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error n c)) )) (branch NativePhysicalAssertOneOf observed first second errorCode . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand observed) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedObserved n0 c0 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand first) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedFirst n1 c1 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperand second) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedSecond n2 c2 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated (constructor NativePhysicalOperation NativePhysicalAssertOneOf relocatedObserved relocatedFirst relocatedSecond errorCode) (app (app naturalAdd n0) (app (app naturalAdd n1) n2)) (app (app naturalAdd c0) (app (app naturalAdd c1) c2)))) (branch NativePhysicalProgramComposeOperandRejected error n2 c2 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error (app (app naturalAdd n0) (app (app naturalAdd n1) n2)) (app (app naturalAdd c0) (app (app naturalAdd c1) c2)))))) (branch NativePhysicalProgramComposeOperandRejected error n1 c1 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error (app (app naturalAdd n0) n1) (app (app naturalAdd c0) c1))))) (branch NativePhysicalProgramComposeOperandRejected error n c . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error n c)) )) (branch NativePhysicalHaltSuccess . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero)) (branch NativePhysicalRepeatBegin count . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero)) (branch NativePhysicalSkipUnlessEqual left right count . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (nativePhysicalProgramComposeRelocateOperand left stateBase resultBase payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedLeft n0 c0 . (eliminate NativePhysicalProgramComposeOperandResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) . (family NativePhysicalProgramComposeOperationResult)) (nativePhysicalProgramComposeRelocateOperand right stateBase resultBase payloadBase) (branch NativePhysicalProgramComposeOperandRelocated relocatedRight n1 c1 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated (constructor NativePhysicalOperation NativePhysicalSkipUnlessEqual relocatedLeft relocatedRight count) (naturalAdd n0 n1) (naturalAdd c0 c1))) (branch NativePhysicalProgramComposeOperandRejected error n1 c1 . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error (naturalAdd n0 n1) (naturalAdd c0 c1))))) (branch NativePhysicalProgramComposeOperandRejected error n c . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRejected error n c)))) (branch NativePhysicalRepeatEnd . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero)) (branch NativePhysicalRepeatEndWhen observed expected . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero)) (branch NativePhysicalStoreWord64 destination value . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero)) (branch NativePhysicalFenceWait address expected polls interval . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero)) (branch NativePhysicalRepeatBeginCounted count . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero)) (branch NativePhysicalAddWord64 destination left right . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero)) (branch NativePhysicalFloat64 kind destination left right . (constructor NativePhysicalProgramComposeOperationResult NativePhysicalProgramComposeOperationRelocated operation zero zero))))))) def nativePhysicalProgramComposeRelocateCommands = (lambda unrestricted commands : (family NativePhysicalCommands) . (lambda unrestricted stateBase : (family ModelWord64) . (lambda unrestricted resultBase : (family ModelWord64) . (lambda unrestricted payloadBase : (family ModelWord64) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (family NativePhysicalProgramComposeCommandsResult)) commands (branch NativePhysicalCommandsEnd . (constructor NativePhysicalProgramComposeCommandsResult NativePhysicalProgramComposeCommandsRelocated (constructor NativePhysicalCommands NativePhysicalCommandsEnd) zero zero zero zero)) (branch NativePhysicalCommandsNext head tail induction . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . (family NativePhysicalProgramComposeCommandsResult)) head (branch NativePhysicalCommandValue operation errorIdentity . (eliminate NativePhysicalProgramComposeOperationResult (lambda unrestricted current : (family NativePhysicalProgramComposeOperationResult) . (family NativePhysicalProgramComposeCommandsResult)) (app (app (app (app nativePhysicalProgramComposeRelocateOperation operation) stateBase) resultBase) payloadBase) (branch NativePhysicalProgramComposeOperationRelocated relocatedOperation n0 c0 . (eliminate NativePhysicalProgramComposeCommandsResult (lambda unrestricted current : (family NativePhysicalProgramComposeCommandsResult) . (family NativePhysicalProgramComposeCommandsResult)) induction (branch NativePhysicalProgramComposeCommandsRelocated relocatedTail commandsDone operationsDone operandsDone checksDone . (constructor NativePhysicalProgramComposeCommandsResult NativePhysicalProgramComposeCommandsRelocated (constructor NativePhysicalCommands NativePhysicalCommandsNext (constructor NativePhysicalCommand NativePhysicalCommandValue relocatedOperation errorIdentity) relocatedTail) (succ commandsDone) (succ operationsDone) (app (app naturalAdd n0) operandsDone) (app (app naturalAdd c0) checksDone))) (branch NativePhysicalProgramComposeCommandsRejected error commandsDone operationsDone operandsDone checksDone . (constructor NativePhysicalProgramComposeCommandsResult NativePhysicalProgramComposeCommandsRejected error (succ commandsDone) (succ operationsDone) (app (app naturalAdd n0) operandsDone) (app (app naturalAdd c0) checksDone))))) (branch NativePhysicalProgramComposeOperationRejected error n c . (constructor NativePhysicalProgramComposeCommandsResult NativePhysicalProgramComposeCommandsRejected error zero zero n c))))))))))) def nativePhysicalProgramComposeOperationIsHalt = (lambda unrestricted operation : (family NativePhysicalOperation) . (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . Nat) operation (branch NativePhysicalSystemCall number arguments payload binding . zero) (branch NativePhysicalCopyPayloadToState destination extent payload . zero) (branch NativePhysicalMachineRoutine code arguments binding . zero) (branch NativePhysicalFencePoll address expected polls . zero) (branch NativePhysicalTelemetryAppend path record . zero) (branch NativePhysicalAssertEqual left right error . zero) (branch NativePhysicalAssertOneOf observed first second error . zero) (branch NativePhysicalHaltSuccess . (succ zero)) (branch NativePhysicalRepeatBegin count . zero) (branch NativePhysicalSkipUnlessEqual left right count . zero) (branch NativePhysicalRepeatEnd . zero) (branch NativePhysicalRepeatEndWhen observed expected . 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 operation destination left right . zero))) def nativePhysicalProgramComposeCommandIsHalt = (lambda unrestricted command : (family NativePhysicalCommand) . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . Nat) command (branch NativePhysicalCommandValue operation errorIdentity . (app nativePhysicalProgramComposeOperationIsHalt operation)))) -- Sequential composition removes the training program's final halt. A -- forward branch targeting the old end must now target the first inference -- command, not skip that command. Other relative record distances are stable. -- originalRestCount comes from the strip fold, avoiding a scan per command. def nativePhysicalProgramComposeRemoveFinalHaltJump = (lambda unrestricted originalRestCount : Nat . (lambda unrestricted command : (family NativePhysicalCommand) . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . (family NativePhysicalCommand)) command (branch NativePhysicalCommandValue original identity . (constructor NativePhysicalCommand NativePhysicalCommandValue (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . (family NativePhysicalOperation)) original (branch NativePhysicalSystemCall number arguments payload binding . original) (branch NativePhysicalCopyPayloadToState destination extent payload . original) (branch NativePhysicalMachineRoutine code arguments binding . original) (branch NativePhysicalFencePoll address expected polls . original) (branch NativePhysicalTelemetryAppend path record . original) (branch NativePhysicalAssertEqual left right error . original) (branch NativePhysicalAssertOneOf observed first second error . original) (branch NativePhysicalHaltSuccess . original) (branch NativePhysicalRepeatBegin count . original) (branch NativePhysicalSkipUnlessEqual left right count . (constructor NativePhysicalOperation NativePhysicalSkipUnlessEqual left right (modelWord64FromNaturalTruncated (naturalSaturatingSubtract (modelWord64Natural count) (naturalEqual (modelWord64Natural count) originalRestCount))))) (branch NativePhysicalRepeatEnd . original) (branch NativePhysicalRepeatEndWhen observed expected . original) (branch NativePhysicalStoreWord64 destination value . original) (branch NativePhysicalFenceWait address expected polls interval . original) (branch NativePhysicalRepeatBeginCounted count . original) (branch NativePhysicalAddWord64 destination left right . original) (branch NativePhysicalFloat64 operation destination left right . original)) identity))))) def nativePhysicalProgramComposeStripTrainingHalt = (lambda unrestricted commands : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (family NativePhysicalProgramComposeStripResult)) commands (branch NativePhysicalCommandsEnd . (constructor NativePhysicalProgramComposeStripResult NativePhysicalProgramComposeStripEmpty)) (branch NativePhysicalCommandsNext head tail induction . (eliminate NativePhysicalProgramComposeStripResult (lambda unrestricted current : (family NativePhysicalProgramComposeStripResult) . (family NativePhysicalProgramComposeStripResult)) induction (branch NativePhysicalProgramComposeStripEmpty . (nat-eliminate (lambda unrestricted isHalt : Nat . (family NativePhysicalProgramComposeStripResult)) (constructor NativePhysicalProgramComposeStripResult NativePhysicalProgramComposeStripRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeTrainingHaltMissing) (succ zero)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalProgramComposeStripResult) . (constructor NativePhysicalProgramComposeStripResult NativePhysicalProgramComposeStripSucceeded (constructor NativePhysicalCommands NativePhysicalCommandsEnd) zero))) (app nativePhysicalProgramComposeCommandIsHalt head))) (branch NativePhysicalProgramComposeStripSucceeded stripped count . (nat-eliminate (lambda unrestricted isHalt : Nat . (family NativePhysicalProgramComposeStripResult)) (constructor NativePhysicalProgramComposeStripResult NativePhysicalProgramComposeStripSucceeded (constructor NativePhysicalCommands NativePhysicalCommandsNext (nativePhysicalProgramComposeRemoveFinalHaltJump (succ count) head) stripped) (succ count)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalProgramComposeStripResult) . (constructor NativePhysicalProgramComposeStripResult NativePhysicalProgramComposeStripRejected (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeTrainingHaltNotFinal) (succ count)))) (app nativePhysicalProgramComposeCommandIsHalt head))) (branch NativePhysicalProgramComposeStripRejected error visited . induction))))) def nativePhysicalProgramComposeFailure = (lambda unrestricted error : (family NativePhysicalProgramComposeErrorCode) . (lambda unrestricted trainingCommands : Nat . (lambda unrestricted inferenceCommands : Nat . (lambda unrestricted combinedCommands : Nat . (lambda unrestricted relocatedCommands : Nat . (lambda unrestricted relocatedOperations : Nat . (lambda unrestricted relocatedOperands : Nat . (lambda unrestricted arithmeticChecks : Nat . (lambda unrestricted haltsRemoved : Nat . (lambda unrestricted validations : Nat . (lambda unrestricted trainingIdentity : Bytes . (lambda unrestricted inferenceIdentity : Bytes . (lambda unrestricted combinedIdentity : Bytes . (constructor NativePhysicalProgramComposeResult NativePhysicalProgramCompositionRejected error (app (app (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeTelemetry trainingCommands) inferenceCommands) combinedCommands) relocatedCommands) relocatedOperations) relocatedOperands) arithmeticChecks) haltsRemoved) validations) (succ zero)) trainingIdentity) inferenceIdentity) combinedIdentity) (app nativePhysicalProgramComposeErrorCodeBytes error)))))))))))))))) def nativePhysicalComposePrograms = (lambda unrestricted training : (family NativePhysicalProgram) . (lambda unrestricted inference : (family NativePhysicalProgram) . (lambda unrestricted combinedIdentity : Bytes . (app (lambda unrestricted trainingIdentity : Bytes . (app (lambda unrestricted inferenceIdentity : Bytes . (app (lambda unrestricted trainingCommands : (family NativePhysicalCommands) . (app (lambda unrestricted inferenceCommands : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted identityValid : Nat . (family NativePhysicalProgramComposeResult)) (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeIdentityInvalid)) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) zero) zero) zero) zero) zero) zero) zero) trainingIdentity) inferenceIdentity combinedIdentity) (lambda unrestricted identityPredecessor : Nat . (lambda unrestricted identityInduction : (family NativePhysicalProgramComposeResult) . (eliminate NativePhysicalProgramValidation (lambda unrestricted current : (family NativePhysicalProgramValidation) . (family NativePhysicalProgramComposeResult)) (app nativePhysicalValidateProgram training) (branch NativePhysicalProgramValidated validatedTraining trainingTelemetry . (eliminate NativePhysicalProgramValidation (lambda unrestricted current : (family NativePhysicalProgramValidation) . (family NativePhysicalProgramComposeResult)) (app nativePhysicalValidateProgram inference) (branch NativePhysicalProgramValidated validatedInference inferenceTelemetry . (eliminate NativePhysicalProgram (lambda unrestricted current : (family NativePhysicalProgram) . (family NativePhysicalProgramComposeResult)) training (branch NativePhysicalProgramValue trainingState trainingResults ignoredTrainingCommands trainingExpected ignoredTrainingIdentity trainingFallbacks . (eliminate NativePhysicalProgram (lambda unrestricted current : (family NativePhysicalProgram) . (family NativePhysicalProgramComposeResult)) inference (branch NativePhysicalProgramValue inferenceState inferenceResults ignoredInferenceCommands inferenceExpected ignoredInferenceIdentity inferenceFallbacks . (eliminate NativePhysicalProgramComposeStripResult (lambda unrestricted current : (family NativePhysicalProgramComposeStripResult) . (family NativePhysicalProgramComposeResult)) (app nativePhysicalProgramComposeStripTrainingHalt trainingCommands) (branch NativePhysicalProgramComposeStripEmpty . (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeTrainingHaltMissing)) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) zero) zero) zero) zero) zero) zero) (byte-to-nat (byte 2))) trainingIdentity) inferenceIdentity combinedIdentity)) (branch NativePhysicalProgramComposeStripSucceeded trainingPrefix trainingPrefixCount . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeResult)) (app nativePhysicalProgramComposeWord64FromNatural (app nativePhysicalProgramComposeProgramPayloadBytes training)) (branch ModelWord64CheckedSucceeded payloadBase . (eliminate NativePhysicalProgramComposeCommandsResult (lambda unrestricted current : (family NativePhysicalProgramComposeCommandsResult) . (family NativePhysicalProgramComposeResult)) (app (app (app (app nativePhysicalProgramComposeRelocateCommands inferenceCommands) trainingState) trainingResults) payloadBase) (branch NativePhysicalProgramComposeCommandsRelocated relocatedInference commandCount operationCount operandCount checks . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeResult)) (app (app modelWord64AddChecked trainingState) inferenceState) (branch ModelWord64CheckedSucceeded combinedState . (eliminate ModelWord64CheckedResult (lambda unrestricted current : (family ModelWord64CheckedResult) . (family NativePhysicalProgramComposeResult)) (app (app modelWord64AddChecked trainingResults) inferenceResults) (branch ModelWord64CheckedSucceeded combinedResults . (app (lambda unrestricted combinedCommands : (family NativePhysicalCommands) . (app (lambda unrestricted combinedProgram : (family NativePhysicalProgram) . (eliminate NativePhysicalProgramValidation (lambda unrestricted current : (family NativePhysicalProgramValidation) . (family NativePhysicalProgramComposeResult)) (app nativePhysicalValidateProgram combinedProgram) (branch NativePhysicalProgramValidated validated telemetry . (constructor NativePhysicalProgramComposeResult NativePhysicalProgramComposed combinedProgram (constructor NativePhysicalProgramValidation NativePhysicalProgramValidated validated telemetry) (app (app (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeTelemetry (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) (app nativePhysicalProgramComposeCommandsCount combinedCommands)) commandCount) operationCount) operandCount) (app (app naturalAdd checks) (succ (succ zero)))) (succ zero)) (byte-to-nat (byte 3))) zero) trainingIdentity) inferenceIdentity) combinedIdentity) b""))) (branch NativePhysicalProgramRejected error telemetry . (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeCombinedRejected error)) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) (app nativePhysicalProgramComposeCommandsCount combinedCommands)) commandCount) operationCount) operandCount) (app (app naturalAdd checks) (succ (succ zero)))) (succ zero)) (byte-to-nat (byte 3))) trainingIdentity) inferenceIdentity combinedIdentity)))) (constructor NativePhysicalProgram NativePhysicalProgramValue combinedState combinedResults combinedCommands (app nativePhysicalProgramComposeCommandsCount combinedCommands) combinedIdentity (app (app naturalAdd trainingFallbacks) inferenceFallbacks)))) (app (app nativePhysicalProgramComposeCommandsAppend trainingPrefix) relocatedInference))) (branch ModelWord64CheckedFailed error . (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposeResultExtent) error)) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) zero) commandCount) operationCount) operandCount) (app (app naturalAdd checks) (succ (succ zero)))) (succ zero)) (byte-to-nat (byte 2))) trainingIdentity) inferenceIdentity combinedIdentity)))) (branch ModelWord64CheckedFailed error . (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposeStateExtent) error)) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) zero) commandCount) operationCount) operandCount) (succ checks)) (succ zero)) (byte-to-nat (byte 2))) trainingIdentity) inferenceIdentity combinedIdentity)))) (branch NativePhysicalProgramComposeCommandsRejected error commandCount operationCount operandCount checks . (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure error) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) zero) commandCount) operationCount) operandCount) checks) (succ zero)) (byte-to-nat (byte 2))) trainingIdentity) inferenceIdentity combinedIdentity)))) (branch ModelWord64CheckedFailed error . (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeArithmeticFailed (constructor NativePhysicalProgramComposeAddressClass NativePhysicalProgramComposePayloadAddress) error)) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) zero) zero) zero) zero) zero) (succ zero)) (byte-to-nat (byte 2))) trainingIdentity) inferenceIdentity combinedIdentity)))) (branch NativePhysicalProgramComposeStripRejected error visited . (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure error) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) zero) zero) zero) zero) zero) zero) (byte-to-nat (byte 2))) trainingIdentity) inferenceIdentity combinedIdentity)))))))) (branch NativePhysicalProgramRejected error telemetry . (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeInferenceRejected error)) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) zero) zero) zero) zero) zero) zero) (byte-to-nat (byte 2))) trainingIdentity) inferenceIdentity combinedIdentity)))) (branch NativePhysicalProgramRejected error telemetry . (app (app (app (app (app (app (app (app (app (app (app (app nativePhysicalProgramComposeFailure (constructor NativePhysicalProgramComposeErrorCode NativePhysicalProgramComposeTrainingRejected error)) (app nativePhysicalProgramComposeCommandsCount trainingCommands)) (app nativePhysicalProgramComposeCommandsCount inferenceCommands)) zero) zero) zero) zero) zero) zero) (succ zero)) trainingIdentity) inferenceIdentity combinedIdentity))))) (app naturalAnd (app (app naturalAnd (app (app naturalEqual (bytes-length trainingIdentity)) (byte-to-nat (byte 64)))) (app (app naturalEqual (bytes-length inferenceIdentity)) (byte-to-nat (byte 64)))) (app (app naturalEqual (bytes-length combinedIdentity)) (byte-to-nat (byte 64)))))) (app nativePhysicalProgramComposeProgramCommands inference))) (app nativePhysicalProgramComposeProgramCommands training))) (app nativePhysicalProgramComposeProgramIdentity inference))) (app nativePhysicalProgramComposeProgramIdentity training))))) def nativePhysicalProgramComposerHostFallbacks : Nat = zero