module PartitionedRegression.CoordinateHost import PartitionedRegression.Coordinates import Checkpoint.Envelope import Checkpoint.NativeEnvelope import Checkpoint.NativeRegions import Checkpoint.NativePeerPublication import Checkpoint.RegionManifest import Compiler.Planning.Protocol import Compiler.Planning.OrderedCombine import Runtime.OrderedCombine import Learning.Numerics import Std.Numeric.Profile import Runtime.Protocol import Runtime.NativeProtocol import Compiler.Planning.RegionFrame import Runtime.ArenaCertificate import Runtime.NativeFloatPlan import Runtime.NativePeerEndpoint import Runtime.NativeFilePlan import Runtime.NativeMemoryPlan import Runtime.NativeWordArithmetic import Runtime.NativeRegionFrame import Runtime.NativePhysicalProgram import Runtime.NativePhysicalNativeELF import Runtime.NativeResourcePlan import Runtime.NativeLaunchRecipeLoad import Runtime.NativeSocketPlan import Runtime.RegionFrame import Runtime.RegionTransfer import Runtime.SocketAddress import Learning.Transition import Representation.ParticipantGroup import Representation.Partition import Model.Parameter import Model.Word64 import Data.Bytes import Data.SHA256 import Data.SHA256Padding import Std.Byte import Std.Foundation import Std.List import Std.Natural import Runtime.NativeHostTarget -- A synchronous coordinate-owned learner. Only predictions, one residual and -- acknowledgments cross the edge during an update. Parameters/accumulators are -- local live state; final capture transfers immutable bytes to the designated -- durable publisher. Both participant successes wait for manifest publication. family CoordinateHostLayout : Type 0 constructor CoordinateHostLayoutOf field unrestricted chPredictionValue : (family RegionFrameLayout) field unrestricted chResidualValue : (family RegionFrameLayout) field unrestricted chAcknowledgmentValue : (family RegionFrameLayout) field unrestricted chCaptureValue : (family RegionFrameLayout) field unrestricted chCommittedValue : (family RegionFrameLayout) field unrestricted chCheckpointValue : (family NativeRegionCheckpoint) field unrestricted chNumericsValue : Bytes end-family -- Typed local work in one dependency round. Transfers are declared separately -- and projected, so no local operation hides a network send or receive. family CoordinateRoundOperation : Type 0 constructor CoordinateCombine field unrestricted coordinateCombineOperation : (family OrderedCombineOperation (family RegionFrameLayout)) constructor CoordinateInstallCombined constructor CoordinateBackwardUpdate constructor CoordinatePrepareAcknowledgment constructor CoordinateAcceptAcknowledgment end-family -- Prediction has a separate arena: no training frames or endpoint slots are -- retained. The common checkpoint plan still validates every learner shard. family CoordinatePredictionLayout : Type 0 constructor CoordinatePredictionLayoutOf field unrestricted cpCheckpointValue : (family NativeRegionCheckpoint) end-family def chPrediction = (lambda unrestricted layout : (family CoordinateHostLayout) . (eliminate CoordinateHostLayout (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout)) layout (branch CoordinateHostLayoutOf chPrediction chResidual chAcknowledgment chCapture chCommitted chCheckpoint numerics . chPrediction))) def chResidual = (lambda unrestricted layout : (family CoordinateHostLayout) . (eliminate CoordinateHostLayout (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout)) layout (branch CoordinateHostLayoutOf chPrediction chResidual chAcknowledgment chCapture chCommitted chCheckpoint numerics . chResidual))) def chAcknowledgment = (lambda unrestricted layout : (family CoordinateHostLayout) . (eliminate CoordinateHostLayout (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout)) layout (branch CoordinateHostLayoutOf chPrediction chResidual chAcknowledgment chCapture chCommitted chCheckpoint numerics . chAcknowledgment))) def chCapture = (lambda unrestricted layout : (family CoordinateHostLayout) . (eliminate CoordinateHostLayout (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout)) layout (branch CoordinateHostLayoutOf chPrediction chResidual chAcknowledgment chCapture chCommitted chCheckpoint numerics . chCapture))) def chCommitted = (lambda unrestricted layout : (family CoordinateHostLayout) . (eliminate CoordinateHostLayout (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout)) layout (branch CoordinateHostLayoutOf chPrediction chResidual chAcknowledgment chCapture chCommitted chCheckpoint numerics . chCommitted))) def chCheckpoint = (lambda unrestricted layout : (family CoordinateHostLayout) . (eliminate CoordinateHostLayout (lambda unrestricted current : (family CoordinateHostLayout) . (family NativeRegionCheckpoint)) layout (branch CoordinateHostLayoutOf chPrediction chResidual chAcknowledgment chCapture chCommitted chCheckpoint numerics . chCheckpoint))) def chNumerics = (lambda unrestricted layout : (family CoordinateHostLayout) . (eliminate CoordinateHostLayout (lambda unrestricted current : (family CoordinateHostLayout) . Bytes) layout (branch CoordinateHostLayoutOf prediction residual acknowledgment capture committed checkpoint numerics . numerics))) def chFloat = (nativeFloat64 b"coordinate-arithmetic") def chNatural = (nativeFloat64Natural b"coordinate-arithmetic") def chBinary = (nativeFloat64Binary b"coordinate-arithmetic") def chStore = (nativeMemoryStoreWord64 b"coordinate-state") def chAdd = (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Add) def chSubtract = (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Subtract) def chMultiply = (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Multiply) def chDivide = (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Divide) def chEnd = (constructor NativePhysicalCommands NativePhysicalCommandsEnd) def chHalt = (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalHaltSuccess) b"coordinate-done" chEnd) def chConnection = (nativeLaunchRecipeSlotValue nativePeerConnectionSlot) def chStateBytes = (naturalAdd nativeRegionCaptureBytes (naturalMultiply 2 coordinateWordBytes)) def chArgument = nativeRegionPathArgument -- All consumers, including GPU endpoint arguments, use the shared path layout. def chSavedShardCount = (nativeRegionShardCount coordinatePartitions) def chManifestInputIndex : Nat = 1 def chPaths = (constructor NativeRegionPaths NativeRegionPathsOf chManifestInputIndex chSavedShardCount) def chInputShardBase = (nativeRegionInputShardBase chPaths) def chOutputShardBase = (nativeRegionOutputShardBase chPaths) def chManifestCandidateIndex = (nativeRegionManifestCandidateIndex chPaths) def chManifestCommittedIndex = (nativeRegionManifestCommittedIndex chPaths) def chDirectoryIndex = (nativeRegionDirectoryIndex chPaths) def chStateAt = (lambda unrestricted layout : (family CoordinateHostLayout) . (nativeRegionEnd (chCheckpoint layout))) def chVersion = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 0 coordinateWordBytes))) def chCursor = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 1 coordinateWordBytes))) def chEpoch = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 2 coordinateWordBytes))) def chWeight = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 3 coordinateWordBytes))) def chAccumulator = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 4 coordinateWordBytes))) def chFeature = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 5 coordinateWordBytes))) def chPartial = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 6 coordinateWordBytes))) def chError = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 7 coordinateWordBytes))) def chGradient = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 8 coordinateWordBytes))) def chDecay = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 9 coordinateWordBytes))) def chRate = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 10 coordinateWordBytes))) def chScratch = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chStateAt layout) (naturalMultiply 11 coordinateWordBytes))) def chEndpoint = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAdd (chScratch layout) coordinateWordBytes)) def chExtent = (lambda unrestricted layout : (family CoordinateHostLayout) . (nativePeerEndpointEnd (chEndpoint layout))) -- Only the combined prediction uses this profile. Device-local products -- retain their explicit policy; their results enter a host binary64 combine. def chCombineArithmetic = (constructor NumericalContract NumericalContractOf nativeFiniteFloat64Profile (constructor StdList StdListCons (family StdNumericOperation) stdOpAdd (constructor StdList StdListEmpty (family StdNumericOperation))) (constructor NumericalRelation NumericalExactOrder b"coordinate-prediction-add-v1")) def chCombineArithmeticDigest = (numericalExactContractDigest chCombineArithmetic) -- Membership is independent of numerical tree order and device placement. -- Changing its epoch or relation changes both frames and checkpoint context. def chMemberGroup = (constructor ParticipantGroup ParticipantGroupOf coordinateCount 0 b"coordinate-owner-members-v1" (constructor ParticipantSelection ParticipantStride 0 1 coordinateCount)) def chMemberCoverage = (constructor CombineCoverage CombineParticipantGroup chMemberGroup 1 1) def chContext = (lambda unrestricted numerics : Bytes . (constructor CheckpointEnvelopeContract CheckpointEnvelopeContractValue (bytes-append b"coordinate-regression-v1;" (bytes-append numerics (bytes-append chCombineArithmeticDigest (participantGroupDigest chMemberGroup)))) b"scaled-accumulation:decay=1/2;subtract-update:rate=1/8" b"repeated-input:[1,2];target=0;one-batch-per-update" b"weights:[3,1];accumulators:[0,0];no-randomness" 1 1 1)) def chIdentity = (lambda unrestricted numerics : Bytes . (lambda unrestricted operation : Nat . (lambda unrestricted sender : Nat . (lambda unrestricted receiver : Nat . (lambda unrestricted region : Bytes . (constructor RegionTransferIdentity RegionTransferIdentityOf b"coordinate-squared-error" b"coordinate-learning-v1" region numerics (constructor LearningRound LearningRoundOf 1 0) operation sender receiver (constructor LogicalInterval LogicalIntervalOf 0 coordinateCount))))))) def chPublicationPlan = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted resume : Nat . (constructor NativeRegionCheckpoint NativeRegionCheckpointOf (nativeRegionManifest (chCheckpoint layout)) (nativeRegionShards (chCheckpoint layout)) (naturalAdd (nativeRegionEpoch (chCheckpoint layout)) resume) (nativeRegionEnd (chCheckpoint layout))))) -- Two coordinate owners: owner 0 publishes, owner 1 is its one peer over -- the pair's single edge. A shard's owner is the coordinate its interval -- holds; parameter and accumulator follow the capture prefix in that -- owner's state, in ordinal order. def chPublication = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted resume : Nat . (constructor NativePeerRegionPublication NativePeerRegionPublicationOf (chPublicationPlan layout resume) 1 (lambda unrestricted owner : Nat . (chCapture layout)) (lambda unrestricted owner : Nat . (chCommitted layout)) (lambda unrestricted peer : Nat . nativePeerConnectionSlot) (chStateAt layout) chStateBytes nativeRegionCaptureBytes (lambda unrestricted shard : (family NativeRegionShard) . (naturalDivideUnchecked (intervalBegin (nativeRegionInterval shard)) coordinateWordBytes)) (lambda unrestricted shard : (family NativeRegionShard) . (naturalAdd nativeRegionCaptureBytes (naturalMultiply (nativeRegionOrdinal shard) coordinateWordBytes))) chPaths))) def chDestinations = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (constructor StdList StdListCons (family NativeRegionDestination) (constructor NativeRegionDestination NativeRegionDestinationOf 0 (coordinateInterval worker) (chWeight layout)) (constructor StdList StdListCons (family NativeRegionDestination) (constructor NativeRegionDestination NativeRegionDestinationOf 1 (coordinateInterval worker) (chAccumulator layout)) (constructor StdList StdListEmpty (family NativeRegionDestination)))))) -- These are source-layout admission checks, before artifact emission. An -- unavailable placement never becomes an empty successful restore program. def chRestoreAdmitted = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (stdBoolToNatural (stdResultIsSuccess (family NativeCheckpointFailure) (family NativePhysicalCommands) (planNativeRegionRestore (chCheckpoint layout) (chArgument chManifestInputIndex) chArgument nativePeerListenerSlot nativePeerScratchSlot (chExtent layout) (chDestinations layout worker) chEnd))))) -- Aggregate every independently admitted frame/checkpoint arena and the -- local state/endpoint block. The whole host must fit with no live aliases. def chResidents = (lambda unrestricted layout : (family CoordinateHostLayout) . (stdListFold (family RegionFrameLayout) (family ArenaResidents) (lambda unrestricted frame : (family RegionFrameLayout) . (lambda unrestricted rest : (family ArenaResidents) . (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"coordinate-frame" (frameBase frame) (naturalSaturatingSubtract (frameEnd frame) (frameBase frame)) 1) rest))) (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"coordinate-owned-state" (chStateAt layout) (naturalSaturatingSubtract (chExtent layout) (chStateAt layout)) coordinateWordBytes) (nativeRegionResidents (chCheckpoint layout))) (constructor StdList StdListCons (family RegionFrameLayout) (chPrediction layout) (constructor StdList StdListCons (family RegionFrameLayout) (chResidual layout) (constructor StdList StdListCons (family RegionFrameLayout) (chAcknowledgment layout) (constructor StdList StdListCons (family RegionFrameLayout) (chCapture layout) (constructor StdList StdListCons (family RegionFrameLayout) (chCommitted layout) (constructor StdList StdListEmpty (family RegionFrameLayout))))))))) -- The whole round has one communication order. Projection removes unrelated -- local work and selects send/receive from the exact frame identity. Each local -- callback owns arithmetic or payload preparation/consumption, not transport. -- The coordinate prediction is one declared numerical tree. Its reduction -- and replication transfers, references and identity derive from this tree. def chCombineLeft = (constructor OrderedCombineTree OrderedCombineLeaf 0) def chCombineRight = (constructor OrderedCombineTree OrderedCombineLeaf 1) def chCombineTree = (constructor OrderedCombineTree OrderedCombineBranch 0 chCombineLeft chCombineRight) def chCombineDigest = (combineTreeDigest chCombineTree) def chCombineNode = (naturalAdd (combineNodeCount chCombineLeft) (combineNodeCount chCombineRight)) def chCombineLeftReference = (combineTreeReference chCombineLeft 0) def chCombineRightReference = (combineTreeReference chCombineRight (combineNodeCount chCombineLeft)) def chCombineResult = (combineReference 0 chCombineNode 0) def chCombineLeftInput = (combineReference 0 chCombineNode 1) def chCombineRightInput = (combineReference 0 chCombineNode 2) def chCombineBaseAnchor = (lambda unrestricted numerics : Bytes . (chIdentity numerics 0 0 0 b"coordinate-prediction")) def chCombineAnchor = (lambda unrestricted numerics : Bytes . (combineCoverageAnchor chMemberCoverage (combineNumericalAnchor chCombineArithmetic (chCombineBaseAnchor numerics)))) def chCombinePredictionIdentity = (lambda unrestricted numerics : Bytes . (combineTransferIdentity (chCombineAnchor numerics) chCombineDigest (constructor CombineStage CombineReduce) chCombineRightReference chCombineRightInput)) def chCombineResidualIdentity = (lambda unrestricted numerics : Bytes . (combineTransferIdentity (chCombineAnchor numerics) chCombineDigest (constructor CombineStage CombineReplicate) chCombineResult chCombineRightReference)) def chCombineBinding = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted stage : (family CombineStage) . (lambda unrestricted source : (family CombineReference) . (lambda unrestricted destination : (family CombineReference) . (lambda unrestricted identity : (family RegionTransferIdentity) . (eliminate CombineStage (lambda unrestricted current : (family CombineStage) . (family RegionFrameLayout)) stage (branch CombineReduce . (chPrediction layout)) (branch CombineReplicate . (chResidual layout)))))))) -- These are locations already owned by the coordinate host layout. The -- planner admits each logical reference against this exact tree before use. -- An unknown reference maps outside the arena and is rejected by admission. def chCombineAddress = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted reference : (family CombineReference) . (nat-eliminate (lambda unrestricted flag : Nat . Nat) (nat-eliminate (lambda unrestricted flag : Nat . Nat) (nat-eliminate (lambda unrestricted flag : Nat . Nat) (nat-eliminate (lambda unrestricted flag : Nat . Nat) (nat-eliminate (lambda unrestricted flag : Nat . Nat) (chExtent layout) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . (framePayloadAt (chPrediction layout)))) (naturalEqual (combineReferenceSlot reference) (combineReferenceSlot chCombineRightInput))) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . (chScratch layout))) (naturalEqual (combineReferenceSlot reference) (combineReferenceSlot chCombineLeftInput))) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . (chError layout))) (naturalEqual (combineReferenceSlot reference) (combineReferenceSlot chCombineResult))) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . (chPartial layout))) (naturalEqual (combineReferenceSlot reference) (combineReferenceSlot chCombineRightReference))) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . (chPartial layout))) (naturalEqual (combineReferenceSlot reference) (combineReferenceSlot chCombineLeftReference))))) def chCombineReferenceAdmitted = (lambda unrestricted role : Nat . (lambda unrestricted reference : (family CombineReference) . (eliminate StdOption (lambda unrestricted current : (family StdOption Nat) . Nat) (combineReferenceIndex role chCombineTree reference) (branch StdNone . 0) (branch StdSome index . 1)))) def chCombineOperationAdmitted = (lambda unrestricted role : Nat . (lambda unrestricted operation : (family OrderedCombineOperation (family RegionFrameLayout)) . (eliminate OrderedCombineOperation (lambda unrestricted current : (family OrderedCombineOperation (family RegionFrameLayout)) . Nat) operation (branch CombineReadLeaf destination . (chCombineReferenceAdmitted role destination)) (branch CombineCopy source destination . (naturalAnd (chCombineReferenceAdmitted role source) (naturalAnd (chCombineReferenceAdmitted role destination) 1))) (branch CombineApply left right destination . (naturalAnd (chCombineReferenceAdmitted role left) (naturalAnd (chCombineReferenceAdmitted role right) (naturalAnd (chCombineReferenceAdmitted role destination) 1)))) (branch CombinePrepare source frame . (chCombineReferenceAdmitted role source)) (branch CombineConsume frame destination . (chCombineReferenceAdmitted role destination))))) def chCombineEnd = (constructor GlobalProtocol GlobalProtocolEnd (family OrderedCombineOperation (family RegionFrameLayout)) (family RegionFrameLayout) (family ProtocolNoDecision)) def chCombinePlan = (lambda unrestricted layout : (family CoordinateHostLayout) . (planNumericalCombineAndReplicate (family RegionFrameLayout) chCombineArithmetic chCombineArithmetic coordinateCount chMemberCoverage (chCombineBaseAnchor (chNumerics layout)) (chCombineBinding layout) chCombineOperationAdmitted nativeProtocolFrameAdmitted chCombineTree chCombineEnd)) def chGlobalRound = (lambda unrestricted layout : (family CoordinateHostLayout) . (appendGlobalProtocol (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) (mapGlobalProtocolOperations (family OrderedCombineOperation (family RegionFrameLayout)) (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) (lambda unrestricted operation : (family OrderedCombineOperation (family RegionFrameLayout)) . (constructor CoordinateRoundOperation CoordinateCombine operation)) (stdResultValueOr (family OrderedCombineFailure) (family GlobalProtocol (family OrderedCombineOperation (family RegionFrameLayout)) (family RegionFrameLayout) (family ProtocolNoDecision)) chCombineEnd (chCombinePlan layout))) (protocolLocal (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) 0 (constructor CoordinateRoundOperation CoordinateInstallCombined) (protocolLocal (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) 1 (constructor CoordinateRoundOperation CoordinateInstallCombined) (protocolLocal (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) 0 (constructor CoordinateRoundOperation CoordinateBackwardUpdate) (protocolLocal (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) 1 (constructor CoordinateRoundOperation CoordinateBackwardUpdate) (protocolLocal (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) 1 (constructor CoordinateRoundOperation CoordinatePrepareAcknowledgment) (protocolTransfer (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) (chIdentity (chNumerics layout) 2 1 0 b"updated-coordinate") (chAcknowledgment layout) (protocolLocal (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) 0 (constructor CoordinateRoundOperation CoordinateAcceptAcknowledgment) (constructor GlobalProtocol GlobalProtocolEnd (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision))))))))))) def chOperationAdmitted = (lambda unrestricted role : Nat . (lambda unrestricted operation : (family CoordinateRoundOperation) . (eliminate CoordinateRoundOperation (lambda unrestricted current : (family CoordinateRoundOperation) . Nat) operation (branch CoordinateCombine value . (chCombineOperationAdmitted role value)) (branch CoordinateInstallCombined . (naturalLess role coordinateCount)) (branch CoordinateBackwardUpdate . (naturalLess role coordinateCount)) (branch CoordinatePrepareAcknowledgment . (naturalEqual role 1)) (branch CoordinateAcceptAcknowledgment . (naturalEqual role 0))))) def chProtocolAdmitted = (lambda unrestricted layout : (family CoordinateHostLayout) . (naturalAnd (stdBoolToNatural (stdResultIsSuccess (family OrderedCombineFailure) (family GlobalProtocol (family OrderedCombineOperation (family RegionFrameLayout)) (family RegionFrameLayout) (family ProtocolNoDecision)) (chCombinePlan layout))) (naturalAnd (stdBoolToNatural (stdResultIsSuccess (family ProtocolFailure) Nat (checkGlobalProtocol (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) coordinateCount chOperationAdmitted nativeProtocolFrameAdmitted (protocolNoDecision (family RegionFrameLayout)) (chGlobalRound layout)))) 1))) -- Declared metadata ceiling; RegionFrame derives actual storage from the -- canonical identity. The collective scope includes its tree and references. def chFrameMaximumHeader : Nat = 512 def chWithLayout = (lambda unrestricted numerics : Bytes . (lambda unrestricted epoch : Nat . (lambda unrestricted base : Nat . (lambda unrestricted emit : (pi unrestricted layout : (family CoordinateHostLayout) . Bytes) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) . Bytes) (planRegionFrameLayout (chCombinePredictionIdentity numerics) coordinateWordBytes chFrameMaximumHeader base 1048576) (branch StdFailure error . b"") (branch StdSuccess prediction . (eliminate StdResult (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) . Bytes) (planRegionFrameLayout (chCombineResidualIdentity numerics) coordinateWordBytes chFrameMaximumHeader (frameAlign (frameEnd prediction)) 1048576) (branch StdFailure error . b"") (branch StdSuccess residual . (eliminate StdResult (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) . Bytes) (planRegionFrameLayout (chIdentity numerics 2 1 0 b"updated-coordinate") coordinateWordBytes chFrameMaximumHeader (frameAlign (frameEnd residual)) 1048576) (branch StdFailure error . b"") (branch StdSuccess acknowledgment . (eliminate StdResult (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) . Bytes) (planRegionFrameLayout (chIdentity numerics 3 1 0 b"prepared-owned-state") chStateBytes chFrameMaximumHeader (frameAlign (frameEnd acknowledgment)) 1048576) (branch StdFailure error . b"") (branch StdSuccess capture . (eliminate StdResult (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) . Bytes) (planRegionFrameLayout (chIdentity numerics 4 0 1 b"manifest-published") coordinateWordBytes chFrameMaximumHeader (frameAlign (frameEnd capture)) 1048576) (branch StdFailure error . b"") (branch StdSuccess committed . (eliminate StdResult (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . Bytes) (planNativeRegionCheckpoint (chContext numerics) coordinateRegions coordinatePartitions epoch (frameAlign (frameEnd committed)) 1048576 (naturalMultiply coordinateCount (stdListLength (family CheckpointLogicalRegion) coordinateRegions))) (branch StdFailure error . b"") (branch StdSuccess checkpoint . (let unrestricted layout = (constructor CoordinateHostLayout CoordinateHostLayoutOf prediction residual acknowledgment capture committed checkpoint numerics) in (nat-eliminate (lambda unrestricted admitted : Nat . Bytes) b"" (lambda unrestricted previous : Nat . (lambda unrestricted ignored : Bytes . (emit layout))) (naturalAnd (naturalAnd (arenaCertificate (chExtent layout) (chResidents layout)) (naturalAnd (chProtocolAdmitted layout) (nativePeerPublicationAdmitted (chPublication layout 0) (chExtent layout) 0))) (naturalAnd (chRestoreAdmitted layout 0) (chRestoreAdmitted layout 1))))))))))))))))))))) def chStart = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (lambda unrestricted resume : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted mode : Nat . (family NativePhysicalCommands)) (chStore (chVersion layout) (nativeLaunchRecipeImmediate 0) (chStore (chCursor layout) (nativeLaunchRecipeImmediate 0) (chStore (chEpoch layout) (nativeLaunchRecipeImmediate (nativeRegionEpoch (chCheckpoint layout))) (chNatural (chWeight layout) (naturalSelect worker 1 3) (chNatural (chAccumulator layout) 0 tail))))) (lambda unrestricted previous : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) . (family NativePhysicalCommands)) (planNativeRegionRestore (chCheckpoint layout) (chArgument chManifestInputIndex) (lambda unrestricted index : Nat . (chArgument (naturalAdd chInputShardBase index))) nativePeerListenerSlot nativePeerScratchSlot (chExtent layout) (chDestinations layout worker) (nativeMemoryCopyOperands (nativeMemoryState (chStateAt layout)) (nativeMemoryState (nativeRegionCaptureAt (chCheckpoint layout))) nativeRegionCaptureBytes nativePeerScratchSlot b"coordinate-restore-capture" (nativeLaunchRecipeAssertEqual (nativeMemoryLoad (chVersion layout)) (nativeMemoryLoad (chCursor layout)) b"coordinate-input-position" (nativeCheckedWordAdd (nativeMemoryState (chEpoch layout)) (nativeMemoryLoad (chEpoch layout)) (nativeLaunchRecipeImmediate 1) nativePeerScratchSlot b"coordinate-epoch-overflow" tail)))) (branch StdFailure error . (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 1) b"coordinate-restore-admission" chEnd)) (branch StdSuccess commands . commands)))) resume))))) def chConstants = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (chNatural (chFeature layout) (succ worker) (chNatural (chScratch layout) 1 (chNatural (chDecay layout) 2 (chBinary chDivide (chDecay layout) (chScratch layout) (chDecay layout) (chNatural (chRate layout) 8 (chBinary chDivide (chRate layout) (chScratch layout) (chRate layout) tail))))))))) def chHostForward = (lambda unrestricted layout : (family CoordinateHostLayout) . (chBinary chMultiply (chPartial layout) (chWeight layout) (chFeature layout))) def chHostBackward = (lambda unrestricted layout : (family CoordinateHostLayout) . (chBinary chMultiply (chGradient layout) (chError layout) (chFeature layout))) def chUpdate = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted tail : (family NativePhysicalCommands) . (chBinary chMultiply (chAccumulator layout) (chDecay layout) (chAccumulator layout) (chBinary chAdd (chAccumulator layout) (chAccumulator layout) (chGradient layout) (chBinary chMultiply (chScratch layout) (chRate layout) (chAccumulator layout) (chBinary chSubtract (chWeight layout) (chWeight layout) (chScratch layout) tail)))))) -- Progress advances after the selected target transition and finite checks. def chAdvance = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeCheckedWordAdd (nativeMemoryState (chVersion layout)) (nativeMemoryLoad (chVersion layout)) (nativeLaunchRecipeImmediate 1) nativePeerScratchSlot b"coordinate-update-overflow" (nativeCheckedWordAdd (nativeMemoryState (chCursor layout)) (nativeMemoryLoad (chCursor layout)) (nativeLaunchRecipeImmediate 1) nativePeerScratchSlot b"coordinate-cursor-overflow" tail)))) -- Arithmetic is shared by both projections; the next acknowledgment is a -- separate global transfer after local state and progress have advanced. def chBackwardUpdate = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeFloat64RequireFinite (nativeMemoryLoad (chError layout)) nativePeerScratchSlot b"coordinate-residual-nonfinite" (backward (nativeFloat64RequireFinite (nativeMemoryLoad (chGradient layout)) nativePeerScratchSlot b"coordinate-gradient-nonfinite" (update (nativeFloat64RequireFinite (nativeMemoryLoad (chWeight layout)) nativePeerScratchSlot b"coordinate-parameter-nonfinite" (nativeFloat64RequireFinite (nativeMemoryLoad (chAccumulator layout)) nativePeerScratchSlot b"coordinate-accumulator-nonfinite" (chAdvance layout tail))))))))))) def chCombineLocal = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted operation : (family OrderedCombineOperation (family RegionFrameLayout)) . (eliminate OrderedCombineOperation (lambda unrestricted current : (family OrderedCombineOperation (family RegionFrameLayout)) . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) operation (branch CombineReadLeaf destination . (lambda unrestricted tail : (family NativePhysicalCommands) . (forward (nativeFloat64RequireFinite (nativeMemoryLoad (chPartial layout)) nativePeerScratchSlot b"coordinate-partial-nonfinite" tail)))) (branch CombineCopy source destination . (chStore (chCombineAddress layout destination) (nativeMemoryLoad (chCombineAddress layout source)))) (branch CombineApply left right destination . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted a = (chCombineAddress layout left) in (let unrestricted z = (chCombineAddress layout right) in (let unrestricted out = (chCombineAddress layout destination) in (nativeFloat64RequireFinite (nativeMemoryLoad a) nativePeerScratchSlot b"coordinate-partial-nonfinite" (nativeFloat64RequireFinite (nativeMemoryLoad z) nativePeerScratchSlot b"coordinate-partial-nonfinite" (chBinary chAdd out a z (nativeFloat64RequireFinite (nativeMemoryLoad out) nativePeerScratchSlot b"coordinate-partial-nonfinite" tail))))))))) (branch CombinePrepare source frame . (chStore (framePayloadAt frame) (nativeMemoryLoad (chCombineAddress layout source)))) (branch CombineConsume frame destination . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeFrameConsume frame (nativeFloat64RequireFinite (nativeMemoryLoad (framePayloadAt frame)) nativePeerScratchSlot b"coordinate-partial-nonfinite" (chStore (chCombineAddress layout destination) (nativeMemoryLoad (framePayloadAt frame)) tail))))))))) def chLocalRound = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted operation : (family CoordinateRoundOperation) . (eliminate CoordinateRoundOperation (lambda unrestricted current : (family CoordinateRoundOperation) . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) operation (branch CoordinateCombine value . (chCombineLocal layout forward value)) (branch CoordinateInstallCombined . (chStore (chError layout) (nativeMemoryLoad (chPartial layout)))) (branch CoordinateBackwardUpdate . (chBackwardUpdate layout backward update)) (branch CoordinatePrepareAcknowledgment . (chStore (framePayloadAt (chAcknowledgment layout)) (nativeMemoryLoad (chVersion layout)))) (branch CoordinateAcceptAcknowledgment . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeFrameConsume (chAcknowledgment layout) (nativeLaunchRecipeAssertEqual (nativeMemoryLoad (framePayloadAt (chAcknowledgment layout))) (nativeMemoryLoad (chVersion layout)) b"coordinate-acknowledged-version" tail)))))))))) def chProjectedRound = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (projectGlobalProtocol (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) worker (chGlobalRound layout)))) def chTransferRound = (lambda unrestricted direction : (family ProtocolDirection) . (lambda unrestricted identity : (family RegionTransferIdentity) . (lambda unrestricted layout : (family RegionFrameLayout) . (nativePeerIO chConnection (eliminate ProtocolDirection (lambda unrestricted current : (family ProtocolDirection) . Nat) direction (branch ProtocolSend . 1) (branch ProtocolReceive . 0)) layout)))) -- chWithLayout checks the complete global program and every frame binding -- before either role's artifact is emitted. These lowerings use that admitted -- projection; they cannot independently select a peer or reorder messages. def chRound = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (nativeProtocolCommands (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) (chLocalRound layout forward backward update) chTransferRound nativeProtocolNoFrameDecisions b"coordinate-protocol" (chProjectedRound layout worker))))))) -- Reuse phases come from the same projection as the actual transfers. This -- removes a second manually maintained sender/consumer table for each role. def chAdvanceRound = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (nativeProtocolCommands (family CoordinateRoundOperation) (family RegionFrameLayout) (family ProtocolNoDecision) (lambda unrestricted operation : (family CoordinateRoundOperation) . (lambda unrestricted tail : (family NativePhysicalCommands) . tail)) (lambda unrestricted direction : (family ProtocolDirection) . (lambda unrestricted identity : (family RegionTransferIdentity) . (lambda unrestricted frame : (family RegionFrameLayout) . (nativeFrameAdvance frame (eliminate ProtocolDirection (lambda unrestricted current : (family ProtocolDirection) . (family NativeFrameTerminal)) direction (branch ProtocolSend . (constructor NativeFrameTerminal NativeFrameSendComplete)) (branch ProtocolReceive . (constructor NativeFrameTerminal NativeFrameConsumeComplete))) nativePeerScratchSlot)))) nativeProtocolNoFrameDecisions b"coordinate-rearm" (chProjectedRound layout worker)))) def chRounds = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted finish : (family NativePhysicalCommands) . (nativeCheckedWordAdd (nativeMemoryState (chScratch layout)) (nativeMemoryLoad (chVersion layout)) (nativeLaunchRecipeImmediate steps) nativePeerScratchSlot b"coordinate-version-range" (nativeCheckedWordAdd (nativeMemoryState (chScratch layout)) (nativeMemoryLoad (chCursor layout)) (nativeLaunchRecipeImmediate steps) nativePeerScratchSlot b"coordinate-cursor-range" (nat-eliminate (lambda unrestricted count : Nat . (family NativePhysicalCommands)) finish (lambda unrestricted previous : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (nativeCheckedWordAdd (nativeMemoryState (chScratch layout)) (nativeMemoryLoad (chVersion layout)) (nativeLaunchRecipeImmediate 1) nativePeerScratchSlot b"coordinate-first-version" (nativeFrameInitializeRound (chPrediction layout) (nativeMemoryLoad (chEpoch layout)) (nativeMemoryLoad (chVersion layout)) (nativeFrameInitializeRound (chResidual layout) (nativeMemoryLoad (chEpoch layout)) (nativeMemoryLoad (chVersion layout)) (nativeFrameInitializeRound (chAcknowledgment layout) (nativeMemoryLoad (chEpoch layout)) (nativeMemoryLoad (chScratch layout)) (chRound layout worker forward backward update (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeImmediate previous)) b"coordinate-repeat" (chAdvanceRound layout worker (chRound layout worker forward backward update (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) b"coordinate-repeat-end" finish))))))))))) steps)))))))))) def chOutput = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeFileCall 1 (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 1) (nativeMemoryState (chStateAt layout)) (nativeLaunchRecipeImmediate chStateBytes) (nativeLaunchRecipeImmediate 0)) nativePeerScratchSlot chStateBytes b"coordinate-result" tail))) -- The shared publisher handles capture agreement and durability. This system -- supplies only its region-to-state placement and final result protocol. def chFinish = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (lambda unrestricted resume : Nat . (eliminate StdResult (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) . (family NativePhysicalCommands)) (planNativePeerRegionPublish (chPublication layout resume) (chExtent layout) worker (nativeSocketCloseChecked chConnection nativePeerScratchSlot (chOutput layout chHalt))) (branch StdFailure error . (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 1) b"coordinate-publication-admission" chEnd)) (branch StdSuccess commands . commands))))) def chCommandsWithSession = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (lambda unrestricted address : Bytes . (lambda unrestricted resume : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted prepare : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted finish : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (chStart layout worker resume (nativeFloat64RequireFinite (nativeMemoryLoad (chWeight layout)) nativePeerScratchSlot b"coordinate-parameter-nonfinite" (nativeFloat64RequireFinite (nativeMemoryLoad (chAccumulator layout)) nativePeerScratchSlot b"coordinate-accumulator-nonfinite" (chConstants layout worker (prepare (nativePeerSetup worker address (chEndpoint layout) (chStore (chScratch layout) (nativeLaunchRecipeImmediate 1) (nativeSocketRequireZero (nativeSocketNoDelay chConnection (nativeMemoryState (chScratch layout)) (nativeLaunchRecipeStore nativePeerScratchSlot)) nativePeerScratchSlot b"coordinate-tcp-nodelay" (chRounds layout worker steps forward backward update (finish (chFinish layout worker resume))))))))))))))))))))) -- Host reference chooses no device lifecycle. GPU callers supply their -- admitted, relocated setup and readback/release fragments explicitly. def chCommands = (lambda unrestricted layout : (family CoordinateHostLayout) . (lambda unrestricted worker : Nat . (lambda unrestricted address : Bytes . (lambda unrestricted resume : Nat . (lambda unrestricted steps : Nat . (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (chCommandsWithSession layout worker address resume steps forward backward (chUpdate layout) (lambda unrestricted tail : (family NativePhysicalCommands) . tail) (lambda unrestricted tail : (family NativePhysicalCommands) . tail))))))))) def chProgramFor = (lambda unrestricted slots : Nat . (lambda unrestricted extent : Nat . (nativePhysicalProgramFromCommands (bytes-append b"coordinate-owned-learning-v1" (dataBytesRepeatByte (byte 0) (naturalSaturatingSubtract 64 (bytes-length b"coordinate-owned-learning-v1")))) extent slots))) def chProgram = (lambda unrestricted layout : (family CoordinateHostLayout) . (chProgramFor nativePeerEndpointSlots (chExtent layout))) -- The host target selects this participant's instruction set and ABI -- (Runtime.NativeHostTarget). Both coordinate owners derive the same program, -- frames and checkpoint encoding on every target, so they may run on -- different host architectures within one session. def coordinateHostTargetArtifact = (lambda unrestricted target : (family NativeHostTarget) . (lambda unrestricted resources : (family NativeResourceContext) . (lambda unrestricted worker : Nat . (lambda unrestricted port : Nat . (lambda unrestricted resume : Nat . (lambda unrestricted epoch : Nat . (lambda unrestricted steps : Nat . (nat-eliminate (lambda unrestricted valid : Nat . Bytes) b"" (lambda unrestricted previous : Nat . (lambda unrestricted ignored : Bytes . (chWithLayout b"f64-local-and-update" epoch 0 (lambda unrestricted layout : (family CoordinateHostLayout) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family SocketAddressFailure) Bytes) . Bytes) (linuxIPv4SocketAddress ipv4Loopback port) (branch StdFailure error . b"") (branch StdSuccess address . (nativeHostTargetResourceArtifact target resources (chProgram layout (chCommands layout worker address resume steps (chHostForward layout) (chHostBackward layout)))))))))) (naturalAnd (naturalLessOrEqual worker 1) (naturalAnd (naturalLessOrEqual resume 1) (naturalAnd (naturalNonzero epoch) (naturalAnd (naturalLessOrEqual (naturalAdd epoch resume) regionFrameWordLimit) (naturalAnd (naturalNonzero steps) (naturalLessOrEqual steps regionFrameWordLimit)))))))))))))) -- The Linux x86-64 pairing. def coordinateHostArtifact = (coordinateHostTargetArtifact nativeHostTargetX86_64Linux) def cpCheckpoint = (lambda unrestricted layout : (family CoordinatePredictionLayout) . (eliminate CoordinatePredictionLayout (lambda unrestricted current : (family CoordinatePredictionLayout) . (family NativeRegionCheckpoint)) layout (branch CoordinatePredictionLayoutOf checkpoint . checkpoint))) def cpLeft = (lambda unrestricted layout : (family CoordinatePredictionLayout) . (nativeRegionEnd (cpCheckpoint layout))) def cpRight = (lambda unrestricted layout : (family CoordinatePredictionLayout) . (naturalAdd (cpLeft layout) coordinateWordBytes)) def cpFeature = (lambda unrestricted layout : (family CoordinatePredictionLayout) . (naturalAdd (cpRight layout) coordinateWordBytes)) def cpPrediction = (lambda unrestricted layout : (family CoordinatePredictionLayout) . (naturalAdd (cpFeature layout) coordinateWordBytes)) def cpExtent = (lambda unrestricted layout : (family CoordinatePredictionLayout) . (naturalAdd (cpPrediction layout) coordinateWordBytes)) def cpSlots = (succ nativePeerListenerSlot) def cpWithLayout = (lambda unrestricted numerics : Bytes . (lambda unrestricted epoch : Nat . (lambda unrestricted base : Nat . (lambda unrestricted emit : (pi unrestricted layout : (family CoordinatePredictionLayout) . Bytes) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . Bytes) (planNativeRegionCheckpoint (chContext numerics) coordinateRegions coordinatePartitions epoch base 1048576 chSavedShardCount) (branch StdFailure error . b"") (branch StdSuccess checkpoint . (emit (constructor CoordinatePredictionLayout CoordinatePredictionLayoutOf checkpoint)))))))) -- Compile only an admitted full-vector restore. The realization chooses the -- computation after validation; both host and device predictions use exactly -- this saved-state interpretation and finite-input check. def cpWithRestore = (lambda unrestricted layout : (family CoordinatePredictionLayout) . (lambda unrestricted tail : (family NativePhysicalCommands) . (lambda unrestricted emit : (pi unrestricted commands : (family NativePhysicalCommands) . Bytes) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) . Bytes) (planNativeRegionRestore (cpCheckpoint layout) (chArgument chManifestInputIndex) (lambda unrestricted index : Nat . (chArgument (naturalAdd chInputShardBase index))) nativePeerListenerSlot nativePeerScratchSlot (cpExtent layout) (constructor StdList StdListCons (family NativeRegionDestination) (constructor NativeRegionDestination NativeRegionDestinationOf 0 (constructor LogicalInterval LogicalIntervalOf 0 coordinateVectorBytes) (cpLeft layout)) (constructor StdList StdListEmpty (family NativeRegionDestination))) (nativeFloat64RequireFinite (nativeMemoryLoad (cpLeft layout)) nativePeerScratchSlot b"prediction-parameter-nonfinite" (nativeFloat64RequireFinite (nativeMemoryLoad (cpRight layout)) nativePeerScratchSlot b"prediction-parameter-nonfinite" tail))) (branch StdFailure error . b"") (branch StdSuccess commands . (emit commands)))))) def cpOutput = (lambda unrestricted layout : (family CoordinatePredictionLayout) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeFloat64RequireFinite (nativeMemoryLoad (cpPrediction layout)) nativePeerScratchSlot b"prediction-result-nonfinite" (nativeFileCall 1 (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 1) (nativeMemoryState (cpPrediction layout)) (nativeLaunchRecipeImmediate coordinateWordBytes) (nativeLaunchRecipeImmediate 0)) nativePeerScratchSlot coordinateWordBytes b"coordinate-prediction" tail)))) -- Prediction validates the full committed checkpoint but materializes only the -- parameter region. Its state extent contains no communication-frame arenas. def coordinateHostTargetPredictionArtifact = (lambda unrestricted target : (family NativeHostTarget) . (lambda unrestricted resources : (family NativeResourceContext) . (lambda unrestricted epoch : Nat . (cpWithLayout b"f64-local-and-update" epoch 0 (lambda unrestricted layout : (family CoordinatePredictionLayout) . (cpWithRestore layout (chNatural (cpFeature layout) 2 (chBinary chMultiply (cpPrediction layout) (cpRight layout) (cpFeature layout) (chBinary chAdd (cpPrediction layout) (cpLeft layout) (cpPrediction layout) (cpOutput layout chHalt)))) (lambda unrestricted commands : (family NativePhysicalCommands) . (nativeHostTargetResourceArtifact target resources (chProgramFor cpSlots (cpExtent layout) commands))))))))) def coordinateHostPredictionArtifact = (coordinateHostTargetPredictionArtifact nativeHostTargetX86_64Linux)