module PartitionedRegression.NativeHost import Checkpoint.Envelope import Checkpoint.NativeEnvelope import Runtime.NativeFloatPlan import Runtime.NativePeerEndpoint import Runtime.NativeFilePlan import Runtime.NativeMemoryPlan import Compiler.Planning.RegionFrame import Runtime.RegionTransfer import Runtime.RegionFrame import Runtime.NativeWordArithmetic import Runtime.NativeRegionFrame import Runtime.NativeSocketPlan import Runtime.SocketAddress import Runtime.NativePhysicalProgram import Runtime.NativePhysicalNativeELF import Runtime.NativeLaunchRecipeLoad import Runtime.WordDigest import Learning.Transition import Representation.Partition import Model.Word64 import Data.Bytes import Std.Foundation import Std.Natural -- Partitioned scalar squared-error learner. Transport, weighted combination, -- version consumption and recovery are shared by explicitly selected local -- realizations. The binary64 realization is a host reference, never a fallback -- for an unavailable device target. def peerWordBytes = nativePeerWordBytes def peerIdentityFor = (lambda unrestricted run : Bytes . (lambda unrestricted schema : Bytes . (lambda unrestricted version : Nat . (lambda unrestricted operation : Nat . (lambda unrestricted sender : Nat . (lambda unrestricted receiver : Nat . (lambda unrestricted region : Bytes . (constructor RegionTransferIdentity RegionTransferIdentityOf b"squared-error-scalar" run region schema (constructor LearningRound LearningRoundOf 1 version) operation sender receiver (constructor LogicalInterval LogicalIntervalOf 0 1))))))))) def peerIdentity = (peerIdentityFor b"native-two-peer-test" b"f64-le-with-u64-mass") def peerInitialIdentity = (peerIdentity 0 0 0 1 b"parameter") def peerContributionIdentity = (peerIdentity 0 1 1 0 b"gradient-numerator-and-mass") def peerUpdatedIdentity = (peerIdentity 1 2 0 1 b"parameter") def peerAcknowledgedIdentity = (peerIdentity 1 3 1 0 b"consumed-version") def peerPlan = (lambda unrestricted identity : (family RegionTransferIdentity) . (lambda unrestricted bytes : Nat . (lambda unrestricted base : Nat . (planRegionFrameLayout identity bytes 256 base 1048576)))) def peerEnd = (constructor NativePhysicalCommands NativePhysicalCommandsEnd) def peerHalt = (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalHaltSuccess) b"peer-done" peerEnd) def peerIO = nativePeerIO def peerFloat = (nativeFloat64 b"peer-arithmetic") def peerNatural = (nativeFloat64Natural b"peer-arithmetic") def peerBinary = (nativeFloat64Binary b"peer-arithmetic") def peerStore = (nativeMemoryStoreWord64 b"peer-state") def peerOutput = (lambda unrestricted descriptor : (family NativePhysicalOperand) . (lambda unrestricted offset : Nat . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalSystemCall (nativeLaunchRecipeImmediate 1) (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 1) (frameNativeState offset) (nativeLaunchRecipeImmediate peerWordBytes) (nativeLaunchRecipeImmediate 0)) b"" (nativeLaunchRecipeStore 0)) b"peer-result" (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue 0) (nativeLaunchRecipeImmediate peerWordBytes) b"peer-result-count" (nativeSocketCloseChecked descriptor 0 peerHalt))))) def peerAdd = (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Add) def peerMultiply = (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Multiply) def peerDivide = (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Divide) def peerSubtract = (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Subtract) -- The combiner has sample x=1, y=0, gradient w. The worker has x=1 and x=2, -- hence numerator w*1*1 + w*2*2. Its mass is carried as an integer, not a mean. -- Divide by the total sample mass, then apply w - (1/4)*g. No gradient or -- learning-rate byte pattern is pasted into the program. def peerHostContribution = (lambda unrestricted worker : Nat . (lambda unrestricted weight : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted work : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted role : Nat . (family NativePhysicalCommands)) (peerStore numerator (frameNativeLoad weight) tail) (lambda unrestricted previous : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (peerNatural work 2 (peerBinary peerMultiply work work work (peerBinary peerMultiply numerator weight work (peerBinary peerAdd numerator numerator weight tail)))))) worker)))))) def peerCoordinatorWith = (lambda unrestricted local : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted descriptor : (family NativePhysicalOperand) . (lambda unrestricted wrongMean : Nat . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted weight = (framePayloadAt initial) in (let unrestricted numerator = (framePayloadAt contribution) in (let unrestricted mass = (naturalAdd numerator peerWordBytes) in (let unrestricted rate = (naturalAdd work peerWordBytes) in (let unrestricted total = (naturalAdd rate peerWordBytes) in (peerIO descriptor 1 initial (peerIO descriptor 0 contribution (nativeFrameConsume contribution (nativeLaunchRecipeAssertEqual (frameNativeLoad mass) (nativeLaunchRecipeImmediate 2) b"peer-sample-coverage" (local (peerNatural work 1 (peerNatural rate 4 (peerBinary peerDivide rate work rate (nat-eliminate (lambda unrestricted n : Nat . (family NativePhysicalCommands)) (peerNatural total 3 (peerBinary peerAdd numerator (framePayloadAt updated) numerator (peerBinary peerDivide numerator numerator total (peerBinary peerMultiply numerator rate numerator (peerBinary peerSubtract (framePayloadAt updated) weight numerator (peerIO descriptor 1 updated tail)))))) (lambda unrestricted n : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (peerNatural total 2 (peerBinary peerDivide numerator numerator total (peerBinary peerAdd numerator (framePayloadAt updated) numerator (peerBinary peerDivide numerator numerator total (peerBinary peerMultiply numerator rate numerator (peerBinary peerSubtract (framePayloadAt updated) weight numerator (peerIO descriptor 1 updated tail))))))))) wrongMean)))))))))))))))))))))) def peerWorkerWith = (lambda unrestricted local : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted descriptor : (family NativePhysicalOperand) . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted weight = (framePayloadAt initial) in (let unrestricted numerator = (framePayloadAt contribution) in (let unrestricted mass = (naturalAdd numerator peerWordBytes) in (peerIO descriptor 0 initial (nativeFrameConsume initial (local (peerStore mass (nativeLaunchRecipeImmediate 2) (peerIO descriptor 1 contribution (peerIO descriptor 0 updated (nativeFrameConsume updated tail))))))))))))))))) def peerProgram = (lambda unrestricted slots : Nat . (lambda unrestricted extent : Nat . (nativePhysicalProgramFromCommands (bytes-append b"native-framed-learning-v1" (dataBytesRepeatByte (byte 0) (naturalSaturatingSubtract 64 (bytes-length b"native-framed-learning-v1")))) extent slots))) -- The transport owns endpoint slots; the arithmetic keeps only its scratch. def peerScratchSlot = nativePeerScratchSlot def peerListenerSlot = nativePeerListenerSlot def peerConnectionSlot = nativePeerConnectionSlot def peerEndpointSlots = nativePeerEndpointSlots def peerWorkEnd = (lambda unrestricted work : Nat . (naturalAdd work (naturalMultiply 3 peerWordBytes))) def peerEndpointLengthAt = nativePeerEndpointLengthAt def peerEndpointEnd = nativePeerEndpointEnd def peerPortWrite = nativePeerPortWrite def peerNativeSetup = nativePeerSetup def peerByRole = nativePeerByRole def peerRoundWith = (lambda unrestricted local : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted descriptor : (family NativePhysicalOperand) . (lambda unrestricted worker : Nat . (lambda unrestricted wrongMean : Nat . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted after = (peerStore (framePayloadAt initial) (frameNativeLoad (framePayloadAt updated)) tail) in (let unrestricted acknowledge = (peerByRole worker (peerIO descriptor 0 acknowledged (nativeFrameConsume acknowledged (nativeLaunchRecipeAssertEqual (frameNativeLoad (framePayloadAt acknowledged)) (frameNativeLoad (frameExpectedVersionAt updated)) b"peer-acknowledged-version" after))) (peerStore (framePayloadAt acknowledged) (frameNativeLoad (frameExpectedVersionAt updated)) (peerIO descriptor 1 acknowledged after))) in (peerByRole worker (peerCoordinatorWith local descriptor wrongMean initial contribution updated work acknowledge) (peerWorkerWith local descriptor initial contribution updated work acknowledge)))))))))))))) def peerAdvance = (lambda unrestricted worker : Nat . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted sent = (constructor NativeFrameTerminal NativeFrameSendComplete) in (let unrestricted consumed = (constructor NativeFrameTerminal NativeFrameConsumeComplete) in (peerByRole worker (nativeFrameAdvance initial sent 0 (nativeFrameAdvance contribution consumed 0 (nativeFrameAdvance updated sent 0 (nativeFrameAdvance acknowledged consumed 0 tail)))) (nativeFrameAdvance initial consumed 0 (nativeFrameAdvance contribution sent 0 (nativeFrameAdvance updated consumed 0 (nativeFrameAdvance acknowledged sent 0 tail))))))))))))) -- First round uses the initialized version. Only later rounds rearm completed -- slots, so finishing at u64 max does not require an impossible next version. -- The up-front checked sum rejects an unrepresentable run before any transfer. def peerUpdatesWith = (lambda unrestricted local : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted descriptor : (family NativePhysicalOperand) . (lambda unrestricted worker : Nat . (lambda unrestricted wrongMean : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted epoch : (family NativePhysicalOperand) . (lambda unrestricted version : (family NativePhysicalOperand) . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (lambda unrestricted finish : (family NativePhysicalCommands) . (nativeCheckedWordAdd (frameNativeState work) version (nativeLaunchRecipeImmediate steps) 0 b"peer-run-version-overflow" (nat-eliminate (lambda unrestricted count : Nat . (family NativePhysicalCommands)) finish (lambda unrestricted previous : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (nativeCheckedWordAdd (frameNativeState work) version (nativeLaunchRecipeImmediate 1) 0 b"peer-initial-version-overflow" (nativeFrameInitializeRound initial epoch version (nativeFrameInitializeRound contribution epoch version (nativeFrameInitializeRound updated epoch (frameNativeLoad work) (nativeFrameInitializeRound acknowledged epoch (frameNativeLoad work) (peerRoundWith local descriptor worker wrongMean initial contribution updated acknowledged work (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeImmediate previous)) b"peer-repeat" (peerAdvance worker initial contribution updated acknowledged (peerRoundWith local descriptor worker wrongMean initial contribution updated acknowledged work (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) b"peer-repeat-end" finish)))))))))))) steps))))))))))))))) def peerUpdates = (lambda unrestricted descriptor : (family NativePhysicalOperand) . (lambda unrestricted worker : Nat . (lambda unrestricted wrongMean : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted epoch : (family NativePhysicalOperand) . (lambda unrestricted version : (family NativePhysicalOperand) . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (peerUpdatesWith (peerHostContribution worker (framePayloadAt initial) (naturalSelect worker (framePayloadAt contribution) (framePayloadAt updated)) work) descriptor worker wrongMean steps epoch version initial contribution updated acknowledged work)))))))))))) def peerCommands = (lambda unrestricted descriptor : (family NativePhysicalOperand) . (lambda unrestricted worker : Nat . (lambda unrestricted initialWeight : Nat . (lambda unrestricted wrongMean : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted epoch : Nat . (lambda unrestricted version : Nat . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (peerNatural (framePayloadAt initial) initialWeight (peerUpdates descriptor worker wrongMean steps (nativeLaunchRecipeImmediate epoch) (nativeLaunchRecipeImmediate version) initial contribution updated acknowledged work (peerOutput descriptor (framePayloadAt initial)))))))))))))))) -- This deployment exchanges small synchronous messages. Select per-socket -- immediate transmission after endpoint establishment, before any frame. The -- work word is dead here and is overwritten by run preflight and arithmetic. def peerImmediateTransmission = (lambda unrestricted work : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (peerStore work (nativeLaunchRecipeImmediate 1) (nativeSocketRequireZero (nativeSocketNoDelay (nativeLaunchRecipeSlotValue peerConnectionSlot) (frameNativeState work) (nativeLaunchRecipeStore peerScratchSlot)) peerScratchSlot b"socket-tcp-nodelay" tail)))) def peerWithTransport = (lambda unrestricted endpoint : Nat . (lambda unrestricted worker : Nat . (lambda unrestricted initialWeight : Nat . (lambda unrestricted wrongMean : Nat . (lambda unrestricted port : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted epoch : Nat . (lambda unrestricted version : Nat . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (let unrestricted commands = (lambda unrestricted descriptor : (family NativePhysicalOperand) . (peerCommands descriptor worker initialWeight wrongMean steps epoch version initial contribution updated acknowledged work)) in (nat-eliminate (lambda unrestricted choice : Nat . Bytes) (nativePhysicalGenerateNativeELFBytesDirect (peerProgram (naturalAdd peerScratchSlot 1) (peerWorkEnd work) (commands (nativeLaunchRecipeImmediate 0)))) (lambda unrestricted previous : Nat . (lambda unrestricted ignored : Bytes . (eliminate StdResult (lambda unrestricted r : (family StdResult (family SocketAddressFailure) Bytes) . Bytes) (linuxIPv4SocketAddress ipv4Loopback port) (branch StdFailure error . b"") (branch StdSuccess address . (nativePhysicalGenerateNativeELFBytesDirect (peerProgram peerEndpointSlots (peerEndpointEnd (peerWorkEnd work)) (peerNativeSetup worker address (peerWorkEnd work) (peerImmediateTransmission work (commands (nativeLaunchRecipeSlotValue peerConnectionSlot)))))))))) endpoint))))))))))))))) def peerLayoutsFor = (lambda unrestricted run : Bytes . (lambda unrestricted schema : Bytes . (lambda unrestricted base : Nat . (lambda unrestricted emit : (pi unrestricted initial : (family RegionFrameLayout) . (pi unrestricted contribution : (family RegionFrameLayout) . (pi unrestricted updated : (family RegionFrameLayout) . (pi unrestricted acknowledged : (family RegionFrameLayout) . (pi unrestricted work : Nat . Bytes))))) . (eliminate StdResult (lambda unrestricted r : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) . Bytes) (peerPlan (peerIdentityFor run schema 0 0 0 1 b"parameter") peerWordBytes base) (branch StdFailure error . b"") (branch StdSuccess initial . (eliminate StdResult (lambda unrestricted r : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) . Bytes) (peerPlan (peerIdentityFor run schema 0 1 1 0 b"gradient-numerator-and-mass") (naturalMultiply 2 peerWordBytes) (frameAlign (frameEnd initial))) (branch StdFailure error . b"") (branch StdSuccess contribution . (eliminate StdResult (lambda unrestricted r : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) . Bytes) (peerPlan (peerIdentityFor run schema 1 2 0 1 b"parameter") peerWordBytes (frameAlign (frameEnd contribution))) (branch StdFailure error . b"") (branch StdSuccess updated . (eliminate StdResult (lambda unrestricted r : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) . Bytes) (peerPlan (peerIdentityFor run schema 1 3 1 0 b"consumed-version") peerWordBytes (frameAlign (frameEnd updated))) (branch StdFailure error . b"") (branch StdSuccess acknowledged . (emit initial contribution updated acknowledged (frameEnd acknowledged)))))))))))))) def peerLayoutsAt = (peerLayoutsFor b"native-two-peer-test" b"f64-le-with-u64-mass") def peerLayouts = (peerLayoutsAt 0) def repeatedArtifactAdmitted = (lambda unrestricted endpoint : Nat . (lambda unrestricted port : Nat . (lambda unrestricted worker : Nat . (lambda unrestricted initialWeight : Nat . (lambda unrestricted wrongMean : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted epoch : Nat . (lambda unrestricted version : Nat . (peerLayouts (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (peerWithTransport endpoint worker initialWeight wrongMean port steps epoch version initial contribution updated acknowledged work))))))))))))))) -- Counts and epochs enter word-valued runtime state only after admission. -- The natural-to-binary64 conversion additionally needs the signed domain. def repeatedArtifactFor = (lambda unrestricted endpoint : Nat . (lambda unrestricted port : Nat . (lambda unrestricted worker : Nat . (lambda unrestricted weight : Nat . (lambda unrestricted wrongMean : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted epoch : Nat . (lambda unrestricted version : Nat . (nat-eliminate (lambda unrestricted admitted : Nat . Bytes) b"" (lambda unrestricted previous : Nat . (lambda unrestricted ignored : Bytes . (repeatedArtifactAdmitted endpoint port worker weight wrongMean steps epoch version))) (naturalAnd (naturalLessOrEqual steps regionFrameWordLimit) (naturalAnd (naturalLessOrEqual epoch regionFrameWordLimit) (naturalAnd (naturalLessOrEqual version regionFrameWordLimit) (naturalLessOrEqual weight 9223372036854775807))))))))))))) def peerArtifactFor = (lambda unrestricted endpoint : Nat . (lambda unrestricted port : Nat . (lambda unrestricted worker : Nat . (lambda unrestricted weight : Nat . (lambda unrestricted wrongMean : Nat . (repeatedArtifactFor endpoint port worker weight wrongMean 1 1 0)))))) def peerArtifact = (peerArtifactFor 0 0) def endpointServerArtifact = (lambda unrestricted weight : Nat . (peerArtifactFor 1 0 0 weight 0)) def endpointWorkerArtifact = (lambda unrestricted port : Nat . (peerArtifactFor 1 port 1 0 0)) def coordinatorArtifact = (lambda unrestricted weight : Nat . (peerArtifact 0 weight 0)) def workerArtifact = (peerArtifact 1 0 0) def wrongMeanArtifact = (peerArtifact 0 1 1) def repeatedServerArtifact = (lambda unrestricted weight : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted epoch : Nat . (lambda unrestricted version : Nat . (repeatedArtifactFor 1 0 0 weight 0 steps epoch version))))) def repeatedWorkerArtifact = (lambda unrestricted port : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted epoch : Nat . (lambda unrestricted version : Nat . (repeatedArtifactFor 1 port 1 0 0 steps epoch version))))) -- Complete replicated logical state for this deterministic scalar learner: -- parameter, completed updates, consumed batches, prior membership epoch. -- No optimizer accumulator or RNG state exists in this example. Their absence -- here is not permission for another learner to omit its continuation state. def peerCheckpointContract = (constructor CheckpointEnvelopeContract CheckpointEnvelopeContractValue b"scalar-parameter-updates-batches-epoch/v1" b"sample-mass-squared-error;rate=1/4;binary64" b"fixed-repeated-batch:x=1,1,2;y=0" b"initial-natural-weight=3" (naturalMultiply 4 peerWordBytes) (naturalMultiply 3 peerWordBytes) 1) def peerCheckpointEpochAt = (lambda unrestricted checkpoint : (family NativeCheckpointLayout) . (naturalAdd (nativeCheckpointPayloadAt checkpoint) (naturalMultiply 3 peerWordBytes))) def peerArgument = (lambda unrestricted index : Nat . (constructor NativePhysicalOperand NativePhysicalProcessArgument (modelWord64FromNaturalTruncated index))) def peerCheckpointStart = (lambda unrestricted checkpoint : (family NativeCheckpointLayout) . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted resume : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted mode : Nat . (family NativePhysicalCommands)) (peerNatural (framePayloadAt initial) 3 (peerStore (nativeCheckpointUpdatesAt checkpoint) (nativeLaunchRecipeImmediate 0) (peerStore (nativeCheckpointInvocationsAt checkpoint) (nativeLaunchRecipeImmediate 0) (peerStore (peerCheckpointEpochAt checkpoint) (nativeLaunchRecipeImmediate 1) tail)))) (lambda unrestricted previous : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (nativeCheckpointRestore checkpoint (peerArgument 1) peerListenerSlot peerScratchSlot (nativeLaunchRecipeAssertEqual (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint)) (frameNativeLoad (nativeCheckpointInvocationsAt checkpoint)) b"peer-batch-position" (peerStore (framePayloadAt initial) (frameNativeLoad (nativeCheckpointPayloadAt checkpoint)) (nativeCheckedWordAdd (frameNativeState (peerCheckpointEpochAt checkpoint)) (frameNativeLoad (peerCheckpointEpochAt checkpoint)) (nativeLaunchRecipeImmediate 1) peerScratchSlot b"peer-recovery-epoch-overflow" tail)))))) resume))))) def peerCheckpointFinish = (lambda unrestricted checkpoint : (family NativeCheckpointLayout) . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted worker : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted descriptor : (family NativePhysicalOperand) . (peerStore (nativeCheckpointPayloadAt checkpoint) (frameNativeLoad (framePayloadAt initial)) (nativeCheckedWordAdd (frameNativeState (nativeCheckpointUpdatesAt checkpoint)) (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint)) (nativeLaunchRecipeImmediate steps) peerScratchSlot b"peer-update-counter-overflow" (nativeCheckedWordAdd (frameNativeState (nativeCheckpointInvocationsAt checkpoint)) (frameNativeLoad (nativeCheckpointInvocationsAt checkpoint)) (nativeLaunchRecipeImmediate steps) peerScratchSlot b"peer-batch-counter-overflow" (peerByRole worker (nativeCheckpointPublish checkpoint (peerArgument 2) (peerArgument 3) (peerArgument 4) peerListenerSlot peerScratchSlot 6 (peerOutput descriptor (framePayloadAt initial))) (peerOutput descriptor (framePayloadAt initial))))))))))) def peerCheckpointWithLayouts = (lambda unrestricted worker : Nat . (lambda unrestricted port : Nat . (lambda unrestricted resume : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (eliminate StdResult (lambda unrestricted r : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) . Bytes) (planNativeCheckpoint peerCheckpointContract (frameAlign (peerEndpointEnd (peerWorkEnd work))) peerWordBytes (naturalMultiply 2 peerWordBytes) 1048576) (branch StdFailure error . b"") (branch StdSuccess checkpoint . (eliminate StdResult (lambda unrestricted addressResult : (family StdResult (family SocketAddressFailure) Bytes) . Bytes) (linuxIPv4SocketAddress ipv4Loopback port) (branch StdFailure error . b"") (branch StdSuccess address . (nativePhysicalGenerateNativeELFBytesDirect (peerProgram peerEndpointSlots (nativeCheckpointEnd checkpoint) (peerCheckpointStart checkpoint initial resume (peerNativeSetup worker address (peerWorkEnd work) (peerImmediateTransmission work (peerUpdates (nativeLaunchRecipeSlotValue peerConnectionSlot) worker 0 steps (frameNativeLoad (peerCheckpointEpochAt checkpoint)) (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint)) initial contribution updated acknowledged work (peerCheckpointFinish checkpoint initial worker steps (nativeLaunchRecipeSlotValue peerConnectionSlot))))))))))))))))))))) def checkpointPeerArtifact = (lambda unrestricted worker : Nat . (lambda unrestricted port : Nat . (lambda unrestricted resume : Nat . (lambda unrestricted steps : Nat . (nat-eliminate (lambda unrestricted fits : Nat . Bytes) b"" (lambda unrestricted previous : Nat . (lambda unrestricted ignored : Bytes . (peerLayouts (lambda unrestricted initial : (family RegionFrameLayout) . (lambda unrestricted contribution : (family RegionFrameLayout) . (lambda unrestricted updated : (family RegionFrameLayout) . (lambda unrestricted acknowledged : (family RegionFrameLayout) . (lambda unrestricted work : Nat . (peerCheckpointWithLayouts worker port resume steps initial contribution updated acknowledged work))))))))) (naturalLessOrEqual steps regionFrameWordLimit)))))) def checkpointPredictionArtifactFor = (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (eliminate StdResult (lambda unrestricted r : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) . Bytes) (planNativeCheckpoint contract 0 peerWordBytes (naturalMultiply 2 peerWordBytes) 1048576) (branch StdFailure error . b"") (branch StdSuccess checkpoint . (nativePhysicalGenerateNativeELFBytesDirect (peerProgram peerEndpointSlots (nativeCheckpointEnd checkpoint) (nativeCheckpointRestore checkpoint (peerArgument 1) peerListenerSlot peerScratchSlot (nativeLaunchRecipeAssertEqual (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint)) (frameNativeLoad (nativeCheckpointInvocationsAt checkpoint)) b"peer-batch-position" (peerNatural (nativeCheckpointSourcePointerAt checkpoint) 2 (peerBinary peerMultiply (nativeCheckpointPayloadAt checkpoint) (nativeCheckpointPayloadAt checkpoint) (nativeCheckpointSourcePointerAt checkpoint) (nativeFileCall 1 (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 1) (nativeMemoryState (nativeCheckpointPayloadAt checkpoint)) (nativeLaunchRecipeImmediate peerWordBytes) (nativeLaunchRecipeImmediate 0)) peerScratchSlot peerWordBytes b"peer-prediction" peerHalt)))))))))) def checkpointPredictionArtifact = (checkpointPredictionArtifactFor peerCheckpointContract)