module Checkpoint.NativeTreePublication import Checkpoint.Envelope import Checkpoint.NativeEnvelope import Checkpoint.NativeRegions import Checkpoint.NativePeerPublication import Checkpoint.RegionManifest import Compiler.Planning.RegionFrame import Representation.ParticipantTree import Representation.Partition import Runtime.NativePhysicalProgram import Runtime.NativeLaunchRecipeLoad import Runtime.NativeMemoryPlan import Runtime.NativePeerEndpoint import Runtime.NativeRegionFrame import Runtime.ArenaCertificate import Model.Word64 import Data.Bytes import Std.Foundation import Std.List import Std.Natural -- Durable publication over a bounded-fan-out hierarchy -- (Representation.ParticipantTree) in which no participant ever holds -- another participant's tensor bytes. -- -- Every participant writes its own shards durably to the admitted store, -- then a *group manifest*: the capture prefix, a record (descriptor, digest) -- for each own shard, and one record per child naming the child's role, its -- subtree size and the digest of the child's group manifest. It sends its -- parent only a commitment -- capture prefix plus that one record -- so the -- parent's work and memory are bounded by the fan-out. The root's group -- manifest is the published root: it identifies one complete state through a -- chain of digests, each level checked by the participant above it. -- -- Coverage is structural. Roles are numbered in preorder, so a child's -- subtree is the role range [child, child + size); a parent checks that each -- received commitment names exactly the child and subtree size the hierarchy -- prescribes, which by induction establishes complete coverage at the root. -- A missing subtree cannot commit (its parent waits, then aborts), and a -- commitment with a different (version, cursor, epoch) prefix is refused. -- Completion is released down the tree only after the root is durable, so no -- participant reports success for a generation that was never published. -- -- Fixed membership, one durable publisher (the root): this is the shape the -- fleet profile scales, not its failure-tolerant authority (S12) or its -- failure-domain storage placement (S14). The store is the POSIX filesystem -- named by the paths; it must be the admitted shared store for the -- generation (Runtime.NativeFilePlan's caller obligations). family NativeTreeCheckpoint : Type 0 constructor NativeTreeCheckpointOf -- this role's group manifest (the root's is the published root) field unrestricted nativeTreeGroupValue : (family NativeCheckpointLayout) -- this role's own shards field unrestricted nativeTreeShardsValue : (family StdList (family NativeRegionShard)) -- the group manifests of the ancestors, root first, read only on restore field unrestricted nativeTreeAncestorsValue : (family StdList (family NativeCheckpointLayout)) field unrestricted nativeTreeEpochValue : Nat field unrestricted nativeTreeEndValue : Nat end-family -- argv positions. A role reads the previous generation's group manifests of -- itself and its ancestors (the root's is the previous root manifest) and its -- own previous shards; it writes its own shards and group manifest. family NativeTreePaths : Type 0 constructor NativeTreePathsOf field unrestricted nativeTreePreviousGroupPath : (pi unrestricted role : Nat . Nat) field unrestricted nativeTreePreviousShardPath : (pi unrestricted index : Nat . Nat) field unrestricted nativeTreeGroupCandidatePath : Nat field unrestricted nativeTreeGroupCommittedPath : Nat field unrestricted nativeTreeShardCandidatePath : (pi unrestricted index : Nat . Nat) field unrestricted nativeTreeShardCommittedPath : (pi unrestricted index : Nat . Nat) field unrestricted nativeTreeDirectoryPath : Nat end-family def nativeTreeGroup = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (eliminate NativeTreeCheckpoint (lambda unrestricted current : (family NativeTreeCheckpoint) . (family NativeCheckpointLayout)) plan (branch NativeTreeCheckpointOf group shards ancestors epoch end . group))) def nativeTreeShards = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (eliminate NativeTreeCheckpoint (lambda unrestricted current : (family NativeTreeCheckpoint) . (family StdList (family NativeRegionShard))) plan (branch NativeTreeCheckpointOf group shards ancestors epoch end . shards))) def nativeTreeAncestors = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (eliminate NativeTreeCheckpoint (lambda unrestricted current : (family NativeTreeCheckpoint) . (family StdList (family NativeCheckpointLayout))) plan (branch NativeTreeCheckpointOf group shards ancestors epoch end . ancestors))) def nativeTreeEpoch = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (eliminate NativeTreeCheckpoint (lambda unrestricted current : (family NativeTreeCheckpoint) . Nat) plan (branch NativeTreeCheckpointOf group shards ancestors epoch end . epoch))) def nativeTreeEnd = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (eliminate NativeTreeCheckpoint (lambda unrestricted current : (family NativeTreeCheckpoint) . Nat) plan (branch NativeTreeCheckpointOf group shards ancestors epoch end . end))) def nativeTreePreviousGroup = (lambda unrestricted paths : (family NativeTreePaths) . (eliminate NativeTreePaths (lambda unrestricted current : (family NativeTreePaths) . (pi unrestricted role : Nat . Nat)) paths (branch NativeTreePathsOf group shard candidate committed shardCandidate shardCommitted directory . group))) def nativeTreePreviousShard = (lambda unrestricted paths : (family NativeTreePaths) . (eliminate NativeTreePaths (lambda unrestricted current : (family NativeTreePaths) . (pi unrestricted index : Nat . Nat)) paths (branch NativeTreePathsOf group shard candidate committed shardCandidate shardCommitted directory . shard))) def nativeTreeGroupCandidate = (lambda unrestricted paths : (family NativeTreePaths) . (eliminate NativeTreePaths (lambda unrestricted current : (family NativeTreePaths) . Nat) paths (branch NativeTreePathsOf group shard candidate committed shardCandidate shardCommitted directory . candidate))) def nativeTreeGroupCommitted = (lambda unrestricted paths : (family NativeTreePaths) . (eliminate NativeTreePaths (lambda unrestricted current : (family NativeTreePaths) . Nat) paths (branch NativeTreePathsOf group shard candidate committed shardCandidate shardCommitted directory . committed))) def nativeTreeShardCandidate = (lambda unrestricted paths : (family NativeTreePaths) . (eliminate NativeTreePaths (lambda unrestricted current : (family NativeTreePaths) . (pi unrestricted index : Nat . Nat)) paths (branch NativeTreePathsOf group shard candidate committed shardCandidate shardCommitted directory . shardCandidate))) def nativeTreeShardCommitted = (lambda unrestricted paths : (family NativeTreePaths) . (eliminate NativeTreePaths (lambda unrestricted current : (family NativeTreePaths) . (pi unrestricted index : Nat . Nat)) paths (branch NativeTreePathsOf group shard candidate committed shardCandidate shardCommitted directory . shardCommitted))) def nativeTreeDirectory = (lambda unrestricted paths : (family NativeTreePaths) . (eliminate NativeTreePaths (lambda unrestricted current : (family NativeTreePaths) . Nat) paths (branch NativeTreePathsOf group shard candidate committed shardCandidate shardCommitted directory . directory))) -- The same planned layouts published under a later membership epoch: a -- resumed generation publishes at the restored epoch + 1. def nativeTreeCheckpointAdvanced = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (lambda unrestricted resume : Nat . (constructor NativeTreeCheckpoint NativeTreeCheckpointOf (nativeTreeGroup plan) (nativeTreeShards plan) (nativeTreeAncestors plan) (naturalAdd (nativeTreeEpoch plan) resume) (nativeTreeEnd plan)))) -- ---- records ---- -- A record is a 24-byte descriptor followed by a 32-byte digest, the shape -- of Checkpoint.NativeRegions' manifest records. An own-shard descriptor is -- (ordinal, begin, end); a child descriptor is (child role, subtree size, -- nativeTreeGroupTag). Records sit after the capture prefix: own shards -- first, then children in role order, so a record's meaning is positional -- and fixed by the plan. def nativeTreeGroupTag : Nat = 0x50554f52472d4c41 def nativeTreeChildDescriptor = (lambda unrestricted role : Nat . (lambda unrestricted size : Nat . (bytes-append (checkpointEnvelopeWord role) (bytes-append (checkpointEnvelopeWord size) (checkpointEnvelopeWord nativeTreeGroupTag))))) def nativeTreeRecordAt = (lambda unrestricted layout : (family NativeCheckpointLayout) . (lambda unrestricted index : Nat . (naturalAdd (nativeCheckpointPayloadAt layout) (naturalAdd nativeRegionCaptureBytes (naturalMultiply index nativeRegionRecordBytes))))) def nativeTreeRecordDigestAt = (lambda unrestricted layout : (family NativeCheckpointLayout) . (lambda unrestricted index : Nat . (naturalAdd (nativeTreeRecordAt layout index) nativeRegionDescriptorBytes))) -- The payload digest the envelope stores for a single-chunk file. def nativeTreeLayoutDigestAt = (lambda unrestricted layout : (family NativeCheckpointLayout) . (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeDigestsAt)) -- A commitment: the agreed leading state bytes (at least the capture -- prefix; a replicated learner's whole replicated state) followed by one -- child record. def nativeTreeCommitmentBytesOf = (lambda unrestricted agreed : Nat . (naturalAdd agreed nativeRegionRecordBytes)) def nativeTreeCommitmentBytes = (nativeTreeCommitmentBytesOf nativeRegionCaptureBytes) -- ---- the manifest contract of one node ---- def nativeTreeGroupSchema = (lambda unrestricted logical : Bytes . (lambda unrestricted fanout : Nat . (lambda unrestricted count : Nat . (lambda unrestricted node : (family ParticipantTreeNode) . (lambda unrestricted own : (family StdList (family CheckpointRegionPartition)) . (bytes-append b"ALPHA-REGION-GROUP-1\x00" (bytes-append logical (bytes-append (checkpointEnvelopeWord fanout) (bytes-append (checkpointEnvelopeWord count) (bytes-append (checkpointEnvelopeWord (participantTreeRoleOf node)) (bytes-append (checkpointEnvelopeWord (participantTreeSizeOf node)) (nativeRegionPartitionBytes own)))))))))))) def nativeTreeRecordCount = (lambda unrestricted fanout : Nat . (lambda unrestricted node : (family ParticipantTreeNode) . (lambda unrestricted own : (family StdList (family CheckpointRegionPartition)) . (naturalAdd (nativeRegionShardCount own) (participantTreeChildCount fanout (participantTreeSizeOf node)))))) def planNativeTreeGroup = (lambda unrestricted context : (family CheckpointEnvelopeContract) . (lambda unrestricted logical : Bytes . (lambda unrestricted fanout : Nat . (lambda unrestricted count : Nat . (lambda unrestricted node : (family ParticipantTreeNode) . (lambda unrestricted own : (family StdList (family CheckpointRegionPartition)) . (lambda unrestricted base : Nat . (lambda unrestricted available : Nat . (planNativeCheckpoint (nativeRegionContract context (nativeTreeGroupSchema logical fanout count node own) (naturalAdd nativeRegionCaptureBytes (naturalMultiply (nativeTreeRecordCount fanout node own) nativeRegionRecordBytes))) base 0 nativeCheckpointWordBytes available))))))))) -- Plan this role's group manifest, its own shards and its ancestors' group -- manifests, in that order from `base`. `ownOf role` gives a role's own -- partition (the regions and intervals it holds); every participant derives -- every ancestor's contract from it and the hierarchy, never from a peer. -- Memory is the role's own shards plus at most height + 1 manifests of at -- most fan-out + own records each: independent of the participant count. def planNativeTreeAncestors = (lambda unrestricted context : (family CheckpointEnvelopeContract) . (lambda unrestricted logical : Bytes . (lambda unrestricted fanout : Nat . (lambda unrestricted count : Nat . (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) . (lambda unrestricted available : Nat . (lambda unrestricted ancestors : (family StdList (family ParticipantTreeNode)) . (lambda unrestricted finish : (pi unrestricted at : Nat . (pi unrestricted planned : (family StdList (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)))) . (stdListFold (family ParticipantTreeNode) (pi unrestricted at : Nat . (pi unrestricted planned : (family StdList (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)))) (lambda unrestricted ancestor : (family ParticipantTreeNode) . (lambda unrestricted next : (pi unrestricted at : Nat . (pi unrestricted planned : (family StdList (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)))) . (lambda unrestricted at : Nat . (lambda unrestricted planned : (family StdList (family NativeCheckpointLayout)) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint))) (planNativeTreeGroup context logical fanout count ancestor (ownOf (participantTreeRoleOf ancestor)) at available) (branch StdFailure error . (constructor StdResult StdFailure (family NativeCheckpointFailure) (family NativeTreeCheckpoint) error)) (branch StdSuccess layout . (next (nativeCheckpointAlign (nativeCheckpointEnd layout)) (stdListAppend (family NativeCheckpointLayout) planned (constructor StdList StdListCons (family NativeCheckpointLayout) layout (constructor StdList StdListEmpty (family NativeCheckpointLayout))))))))))) finish ancestors))))))))) def planNativeTreeCheckpoint = (lambda unrestricted context : (family CheckpointEnvelopeContract) . (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) . (lambda unrestricted fanout : Nat . (lambda unrestricted count : Nat . (lambda unrestricted role : Nat . (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) . (lambda unrestricted epoch : Nat . (lambda unrestricted base : Nat . (lambda unrestricted available : Nat . (let unrestricted logical = (checkpointLogicalSchemaBytes regions) in (eliminate StdResult (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint))) (planNativeTreeGroup context logical fanout count (participantTreeNode fanout count role) (ownOf role) base available) (branch StdFailure error . (constructor StdResult StdFailure (family NativeCheckpointFailure) (family NativeTreeCheckpoint) error)) (branch StdSuccess group . (eliminate StdResult (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint))) (nativeRegionAppendParts context logical available (ownOf role) (constructor StdResult StdSuccess (family NativeCheckpointFailure) (family NativeRegionCheckpoint) (constructor NativeRegionCheckpoint NativeRegionCheckpointOf group (constructor StdList StdListEmpty (family NativeRegionShard)) epoch (nativeCheckpointEnd group)))) (branch StdFailure error . (constructor StdResult StdFailure (family NativeCheckpointFailure) (family NativeTreeCheckpoint) error)) (branch StdSuccess shards . (planNativeTreeAncestors context logical fanout count ownOf available (participantTreeAncestors fanout count role) (lambda unrestricted at : Nat . (lambda unrestricted planned : (family StdList (family NativeCheckpointLayout)) . (constructor StdResult StdSuccess (family NativeCheckpointFailure) (family NativeTreeCheckpoint) (constructor NativeTreeCheckpoint NativeTreeCheckpointOf group (stdListReverse (family NativeRegionShard) (nativeRegionShards shards)) planned epoch at)))) (nativeCheckpointAlign (nativeRegionEnd shards)) (constructor StdList StdListEmpty (family NativeCheckpointLayout))))))))))))))))) -- ---- publication ---- def nativeTreeArgument = nativeRegionPathArgument -- Prepare this role's own shards from its state and record each one's -- descriptor and payload digest in its group manifest. def nativeTreePrepareOwn = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (lambda unrestricted stateAt : Nat . (lambda unrestricted offsetOf : (pi unrestricted shard : (family NativeRegionShard) . Nat) . (lambda unrestricted paths : (family NativeTreePaths) . (lambda unrestricted tail : (family NativePhysicalCommands) . (stdListFold (family NativeRegionShard) (pi unrestricted index : Nat . (family NativePhysicalCommands)) (lambda unrestricted shard : (family NativeRegionShard) . (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) . (lambda unrestricted index : Nat . (nativeRegionPrepareShard shard (nativeMemoryState stateAt) (nativeMemoryState (naturalAdd stateAt (offsetOf shard))) (nativeTreeArgument (nativeTreeShardCandidate paths index)) (nativeTreeArgument (nativeTreeShardCommitted paths index)) (nativeTreeArgument (nativeTreeDirectory paths)) nativePeerListenerSlot nativePeerScratchSlot (nativeMemoryCopyPayload (nativeTreeRecordAt (nativeTreeGroup plan) index) (nativeRegionDescriptor (nativeRegionOrdinal shard) (nativeRegionInterval shard)) (nativeMemoryCopyOperands (nativeMemoryState (nativeTreeRecordDigestAt (nativeTreeGroup plan) index)) (nativeMemoryState (nativeTreeLayoutDigestAt (nativeRegionLayout shard))) checkpointEnvelopeDigestBytes nativePeerScratchSlot b"tree-shard-record" (next (succ index)))))))) (lambda unrestricted index : Nat . tail) (nativeTreeShards plan) 0)))))) -- Receive each child's commitment over its edge and record it after checking -- the capture prefix and that it covers exactly the prescribed subtree. def nativeTreeReceiveChildren = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (lambda unrestricted fanout : Nat . (lambda unrestricted node : (family ParticipantTreeNode) . (lambda unrestricted edges : (family StdList (family NativePeerEdge)) . (lambda unrestricted commitment : (pi unrestricted child : Nat . (family RegionFrameLayout)) . (lambda unrestricted stateAt : Nat . (lambda unrestricted agreed : Nat . (lambda unrestricted epoch : (family NativePhysicalOperand) . (lambda unrestricted version : (family NativePhysicalOperand) . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted own = (stdListLength (family NativeRegionShard) (nativeTreeShards plan)) in (stdListFold (family ParticipantTreeNode) (pi unrestricted index : Nat . (family NativePhysicalCommands)) (lambda unrestricted child : (family ParticipantTreeNode) . (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) . (lambda unrestricted index : Nat . (let unrestricted role = (participantTreeRoleOf child) in (let unrestricted frame = (commitment role) in (let unrestricted record = (naturalAdd own index) in (nativeFrameInitializeRound frame epoch version (nativePeerPublicationIO (nativeLaunchRecipeSlotValue (nativePeerEdgeConnectionTo edges role)) 0 frame (nativeFrameConsume frame (nativeMemoryCompareRegions stateAt (framePayloadAt frame) agreed nativePeerScratchSlot b"tree-child-position" (nativeMemoryCopyPayload (nativeTreeRecordAt (nativeTreeGroup plan) record) (nativeTreeChildDescriptor role (participantTreeSizeOf child)) (nativeMemoryCompareRegions (nativeTreeRecordAt (nativeTreeGroup plan) record) (naturalAdd (framePayloadAt frame) agreed) nativeRegionDescriptorBytes nativePeerScratchSlot b"tree-child-coverage" (nativeMemoryCopyOperands (nativeMemoryState (nativeTreeRecordDigestAt (nativeTreeGroup plan) record)) (nativeMemoryState (naturalAdd (framePayloadAt frame) (naturalAdd agreed nativeRegionDescriptorBytes))) checkpointEnvelopeDigestBytes nativePeerScratchSlot b"tree-child-record" (next (succ index))))))))))))))) (lambda unrestricted index : Nat . tail) (participantTreeChildren fanout node) 0)))))))))))) -- Commit this role's group manifest to its parent and wait for release. def nativeTreeCommitUpward = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (lambda unrestricted node : (family ParticipantTreeNode) . (lambda unrestricted edges : (family StdList (family NativePeerEdge)) . (lambda unrestricted commitment : (pi unrestricted child : Nat . (family RegionFrameLayout)) . (lambda unrestricted release : (pi unrestricted child : Nat . (family RegionFrameLayout)) . (lambda unrestricted stateAt : Nat . (lambda unrestricted agreed : Nat . (lambda unrestricted epoch : (family NativePhysicalOperand) . (lambda unrestricted version : (family NativePhysicalOperand) . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted role = (participantTreeRoleOf node) in (let unrestricted frame = (commitment role) in (let unrestricted released = (release role) in (let unrestricted parent = (nativeLaunchRecipeSlotValue (nativePeerEdgeConnectionTo edges (participantTreeParentOf node))) in (nativeFrameInitializeRound frame epoch version (nativeFrameInitializeRound released epoch version (nativeMemoryCopyOperands (nativeMemoryState (framePayloadAt frame)) (nativeMemoryState stateAt) agreed nativePeerScratchSlot b"tree-commit-position" (nativeMemoryCopyPayload (naturalAdd (framePayloadAt frame) agreed) (nativeTreeChildDescriptor role (participantTreeSizeOf node)) (nativeMemoryCopyOperands (nativeMemoryState (naturalAdd (framePayloadAt frame) (naturalAdd agreed nativeRegionDescriptorBytes))) (nativeMemoryState (nativeTreeLayoutDigestAt (nativeTreeGroup plan))) checkpointEnvelopeDigestBytes nativePeerScratchSlot b"tree-commit-digest" (nativePeerPublicationIO parent 1 frame (nativePeerPublicationIO parent 0 released (nativeFrameConsume released (nativeLaunchRecipeAssertEqual (nativeMemoryLoad (framePayloadAt released)) version b"tree-released-version" tail))))))))))))))))))))))) -- Release each child, in role order, with the published version. def nativeTreeReleaseChildren = (lambda unrestricted fanout : Nat . (lambda unrestricted node : (family ParticipantTreeNode) . (lambda unrestricted edges : (family StdList (family NativePeerEdge)) . (lambda unrestricted release : (pi unrestricted child : Nat . (family RegionFrameLayout)) . (lambda unrestricted epoch : (family NativePhysicalOperand) . (lambda unrestricted version : (family NativePhysicalOperand) . (lambda unrestricted tail : (family NativePhysicalCommands) . (stdListFold (family ParticipantTreeNode) (family NativePhysicalCommands) (lambda unrestricted child : (family ParticipantTreeNode) . (lambda unrestricted rest : (family NativePhysicalCommands) . (let unrestricted role = (participantTreeRoleOf child) in (let unrestricted released = (release role) in (nativeFrameInitializeRound released epoch version (nativeMemoryStoreWord64 b"tree-release-version" (framePayloadAt released) version (nativePeerPublicationIO (nativeLaunchRecipeSlotValue (nativePeerEdgeConnectionTo edges role)) 1 released rest))))))) tail (participantTreeChildren fanout node))))))))) -- The complete publication of one role: own shards, children's commitments, -- group manifest (the root's at the published-root path), commitment to the -- parent and its release, then the children's release. A role completes -- only after the root is durable. `commitment c` / `release c` are the -- frames of the edge between c and its parent; the caller plans them with -- identities naming that edge so a frame received on the wrong edge fails. def nativeTreePublish = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (lambda unrestricted fanout : Nat . (lambda unrestricted count : Nat . (lambda unrestricted role : Nat . (lambda unrestricted edges : (family StdList (family NativePeerEdge)) . (lambda unrestricted commitment : (pi unrestricted child : Nat . (family RegionFrameLayout)) . (lambda unrestricted release : (pi unrestricted child : Nat . (family RegionFrameLayout)) . (lambda unrestricted stateAt : Nat . (lambda unrestricted agreed : Nat . (lambda unrestricted offsetOf : (pi unrestricted shard : (family NativeRegionShard) . Nat) . (lambda unrestricted paths : (family NativeTreePaths) . (lambda unrestricted success : (family NativePhysicalCommands) . (let unrestricted node = (participantTreeNode fanout count role) in (let unrestricted version = (nativeMemoryLoad stateAt) in (let unrestricted epoch = (nativeMemoryLoad (naturalAdd stateAt (naturalMultiply 2 nativeCheckpointWordBytes))) in (nativeMemoryCopyOperands (nativeMemoryState (nativeCheckpointPayloadAt (nativeTreeGroup plan))) (nativeMemoryState stateAt) nativeRegionCaptureBytes nativePeerScratchSlot b"tree-capture" (nativeLaunchRecipeAssertEqual epoch (nativeLaunchRecipeImmediate (nativeTreeEpoch plan)) b"tree-membership-epoch" (nativeTreePrepareOwn plan stateAt offsetOf paths (nativeTreeReceiveChildren plan fanout node edges commitment stateAt agreed epoch version (nativeCheckpointPublish (nativeTreeGroup plan) (nativeTreeArgument (nativeTreeGroupCandidate paths)) (nativeTreeArgument (nativeTreeGroupCommitted paths)) (nativeTreeArgument (nativeTreeDirectory paths)) nativePeerListenerSlot nativePeerScratchSlot 6 (nat-eliminate (lambda unrestricted root : Nat . (family NativePhysicalCommands)) (nativeTreeCommitUpward plan node edges commitment release stateAt agreed epoch version (nativeTreeReleaseChildren fanout node edges release epoch version success)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (nativeTreeReleaseChildren fanout node edges release epoch version success))) (participantTreeIsRoot node)))))))))))))))))))))) -- ---- restore ---- -- Read the previous generation along one path: the root manifest, then each -- descendant's group manifest down to this role's own, checking each -- manifest's payload digest against the record its parent holds and every -- capture prefix against the root's; then this role's own shards, checked -- against its own records, into `destination shard`. Reads touch height + 1 -- manifests and the own shards, never a sibling subtree. The root manifest's -- capture prefix is left in this role's group layout for the caller. def nativeTreeRestoreManifests = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (lambda unrestricted fanout : Nat . (lambda unrestricted count : Nat . (lambda unrestricted role : Nat . (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) . (lambda unrestricted paths : (family NativeTreePaths) . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted chain = (stdListAppend (family NativeCheckpointLayout) (nativeTreeAncestors plan) (constructor StdList StdListCons (family NativeCheckpointLayout) (nativeTreeGroup plan) (constructor StdList StdListEmpty (family NativeCheckpointLayout)))) in (let unrestricted roles = (stdListAppend Nat (stdListMap (family ParticipantTreeNode) Nat participantTreeRoleOf (participantTreeAncestors fanout count role)) (constructor StdList StdListCons Nat role (constructor StdList StdListEmpty Nat))) in (let unrestricted root = (stdListHeadOr (family NativeCheckpointLayout) (nativeTreeGroup plan) chain) in (stdListFold Nat (pi unrestricted index : Nat . (family NativePhysicalCommands)) (lambda unrestricted at : Nat . (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) . (lambda unrestricted index : Nat . (let unrestricted layout = (stdListHeadOr (family NativeCheckpointLayout) (nativeTreeGroup plan) (stdListDrop (family NativeCheckpointLayout) index chain)) in (let unrestricted parentRole = (stdListHeadOr Nat 0 (stdListDrop Nat (naturalPredecessor index) roles)) in (let unrestricted parent = (stdListHeadOr (family NativeCheckpointLayout) (nativeTreeGroup plan) (stdListDrop (family NativeCheckpointLayout) (naturalPredecessor index) chain)) in (nativeCheckpointRestore layout (nativeTreeArgument (nativeTreePreviousGroup paths at)) nativePeerListenerSlot nativePeerScratchSlot (nat-eliminate (lambda unrestricted first : Nat . (family NativePhysicalCommands)) (nativeMemoryCompareRegions (nativeTreeLayoutDigestAt layout) (nativeTreeRecordDigestAt parent (naturalAdd (nativeRegionShardCount (ownOf parentRole)) (participantTreeChildHolding fanout (participantTreeNode fanout count parentRole) at))) checkpointEnvelopeDigestBytes nativePeerScratchSlot b"tree-restore-digest" (nativeMemoryCompareRegions (nativeCheckpointPayloadAt root) (nativeCheckpointPayloadAt layout) nativeRegionCaptureBytes nativePeerScratchSlot b"tree-restore-position" (next (succ index)))) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (nativeLaunchRecipeAssertEqual (nativeMemoryLoad (naturalAdd (nativeCheckpointPayloadAt root) (naturalMultiply 2 nativeCheckpointWordBytes))) (nativeLaunchRecipeImmediate (nativeTreeEpoch plan)) b"tree-membership-epoch" (next (succ index))))) (naturalIsZero index))))))))) (lambda unrestricted index : Nat . tail) roles 0))))))))))) -- The shards of the records from position `first` on: a role that needs only -- some of another manifest's shards checks each against its own record. -- `pathOf` and every record index are positions in that manifest. def nativeTreeRestoreShardsFrom = (lambda unrestricted records : (family NativeCheckpointLayout) . (lambda unrestricted first : Nat . (lambda unrestricted shards : (family StdList (family NativeRegionShard)) . (lambda unrestricted pathOf : (pi unrestricted index : Nat . Nat) . (lambda unrestricted destination : (pi unrestricted shard : (family NativeRegionShard) . Nat) . (lambda unrestricted tail : (family NativePhysicalCommands) . (stdListFold (family NativeRegionShard) (pi unrestricted index : Nat . (family NativePhysicalCommands)) (lambda unrestricted shard : (family NativeRegionShard) . (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) . (lambda unrestricted index : Nat . (let unrestricted layout = (nativeRegionLayout shard) in (nativeCheckpointRestore layout (nativeTreeArgument (pathOf index)) nativePeerListenerSlot nativePeerScratchSlot (nativeMemoryCompareRegions (nativeTreeLayoutDigestAt layout) (nativeTreeRecordDigestAt records index) checkpointEnvelopeDigestBytes nativePeerScratchSlot b"tree-restore-shard-digest" (nativeMemoryCompareRegions (nativeCheckpointPayloadAt records) (nativeCheckpointPayloadAt layout) nativeRegionCaptureBytes nativePeerScratchSlot b"tree-restore-shard-position" (nativeMemoryCopyOperands (nativeMemoryState (destination shard)) (nativeMemoryState (naturalAdd (nativeCheckpointPayloadAt layout) nativeRegionCaptureBytes)) (intervalExtent (nativeRegionInterval shard)) nativePeerScratchSlot b"tree-restore-shard-state" (next (succ index)))))))))) (lambda unrestricted index : Nat . tail) shards first))))))) -- The shards of `records`, in record order, from record 0. def nativeTreeRestoreShards = (lambda unrestricted records : (family NativeCheckpointLayout) . (nativeTreeRestoreShardsFrom records 0)) -- This role's own shards, checked against its own group manifest's records. def nativeTreeRestoreOwn = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (lambda unrestricted paths : (family NativeTreePaths) . (lambda unrestricted destination : (pi unrestricted shard : (family NativeRegionShard) . Nat) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeTreeRestoreShards (nativeTreeGroup plan) (nativeTreeShards plan) (lambda unrestricted index : Nat . (nativeTreePreviousShard paths index)) destination tail))))) -- The root's group manifest as this role restored it: the first ancestor, -- or the role's own when it is the root. def nativeTreeRootLayout = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (stdListHeadOr (family NativeCheckpointLayout) (nativeTreeGroup plan) (nativeTreeAncestors plan))) -- Layouts, from `base`, for the root's own shards at any role. A replicated -- region the root alone publishes is restored by every role from the root's -- shards, each checked against the root manifest's records -- (nativeTreeRestoreShards with nativeTreeRootLayout): one manifest path and -- the region itself, never another subtree. def planNativeTreeRootShards = (lambda unrestricted context : (family CheckpointEnvelopeContract) . (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) . (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) . (lambda unrestricted plan : (family NativeTreeCheckpoint) . (lambda unrestricted base : Nat . (lambda unrestricted available : Nat . (stdResultBind (family NativeCheckpointFailure) (family NativeRegionCheckpoint) (family NativeRegionCheckpoint) (nativeRegionAppendParts context (checkpointLogicalSchemaBytes regions) available (ownOf 0) (constructor StdResult StdSuccess (family NativeCheckpointFailure) (family NativeRegionCheckpoint) (constructor NativeRegionCheckpoint NativeRegionCheckpointOf (nativeTreeGroup plan) (constructor StdList StdListEmpty (family NativeRegionShard)) (nativeTreeEpoch plan) base))) -- appended shards accumulate last first; records are in order (lambda unrestricted planned : (family NativeRegionCheckpoint) . (constructor StdResult StdSuccess (family NativeCheckpointFailure) (family NativeRegionCheckpoint) (constructor NativeRegionCheckpoint NativeRegionCheckpointOf (nativeRegionManifest planned) (stdListReverse (family NativeRegionShard) (nativeRegionShards planned)) (nativeRegionEpoch planned) (nativeRegionEnd planned))))))))))) def nativeTreeRestore = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (lambda unrestricted fanout : Nat . (lambda unrestricted count : Nat . (lambda unrestricted role : Nat . (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) . (lambda unrestricted paths : (family NativeTreePaths) . (lambda unrestricted destination : (pi unrestricted shard : (family NativeRegionShard) . Nat) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeTreeRestoreManifests plan fanout count role ownOf paths (nativeTreeRestoreOwn plan paths destination tail)))))))))) -- The prefix restored from the root manifest (version, cursor, epoch). def nativeTreeRestoredCaptureAt = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (nativeCheckpointPayloadAt (nativeTreeGroup plan))) -- ---- admission ---- -- The plan's group manifest, own shards and ancestor manifests are laid out -- contiguously from the group's base: one private staging resident. def nativeTreeResidents = (lambda unrestricted plan : (family NativeTreeCheckpoint) . (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"checkpoint-tree-private-staging" (nativeCheckpointBase (nativeTreeGroup plan)) (naturalSaturatingSubtract (nativeTreeEnd plan) (nativeCheckpointBase (nativeTreeGroup plan))) 1) (constructor ArenaResidents ArenaResidentsEnd)))