1module Checkpoint.NativeTreePublication
2
3import Checkpoint.Envelope
4import Checkpoint.NativeEnvelope
5import Checkpoint.NativeRegions
6import Checkpoint.NativePeerPublication
7import Checkpoint.RegionManifest
8import Compiler.Planning.RegionFrame
9import Representation.ParticipantTree
10import Representation.Partition
11import Runtime.NativePhysicalProgram
12import Runtime.NativeLaunchRecipeLoad
13import Runtime.NativeMemoryPlan
14import Runtime.NativePeerEndpoint
15import Runtime.NativeRegionFrame
16import Runtime.ArenaCertificate
17import Model.Word64
18import Data.Bytes
19import Std.Foundation
20import Std.List
21import Std.Natural
22
23-- Durable publication over a bounded-fan-out hierarchy
24-- (Representation.ParticipantTree) in which no participant ever holds
25-- another participant's tensor bytes.
26--
27-- Every participant writes its own shards durably to the admitted store,
28-- then a *group manifest*: the capture prefix, a record (descriptor, digest)
29-- for each own shard, and one record per child naming the child's role, its
30-- subtree size and the digest of the child's group manifest. It sends its
31-- parent only a commitment -- capture prefix plus that one record -- so the
32-- parent's work and memory are bounded by the fan-out. The root's group
33-- manifest is the published root: it identifies one complete state through a
34-- chain of digests, each level checked by the participant above it.
35--
36-- Coverage is structural. Roles are numbered in preorder, so a child's
37-- subtree is the role range [child, child + size); a parent checks that each
38-- received commitment names exactly the child and subtree size the hierarchy
39-- prescribes, which by induction establishes complete coverage at the root.
40-- A missing subtree cannot commit (its parent waits, then aborts), and a
41-- commitment with a different (version, cursor, epoch) prefix is refused.
42-- Completion is released down the tree only after the root is durable, so no
43-- participant reports success for a generation that was never published.
44--
45-- Fixed membership, one durable publisher (the root): this is the shape the
46-- fleet profile scales, not its failure-tolerant authority (S12) or its
47-- failure-domain storage placement (S14). The store is the POSIX filesystem
48-- named by the paths; it must be the admitted shared store for the
49-- generation (Runtime.NativeFilePlan's caller obligations).
50family NativeTreeCheckpoint : Type 0
51constructor NativeTreeCheckpointOf
52-- this role's group manifest (the root's is the published root)
53field unrestricted nativeTreeGroupValue : (family NativeCheckpointLayout)
54-- this role's own shards
55field unrestricted nativeTreeShardsValue : (family StdList (family NativeRegionShard))
56-- the group manifests of the ancestors, root first, read only on restore
57field unrestricted nativeTreeAncestorsValue : (family StdList (family NativeCheckpointLayout))
58field unrestricted nativeTreeEpochValue : Nat
59field unrestricted nativeTreeEndValue : Nat
60
61end-family
62
63-- argv positions. A role reads the previous generation's group manifests of
64-- itself and its ancestors (the root's is the previous root manifest) and its
65-- own previous shards; it writes its own shards and group manifest.
66family NativeTreePaths : Type 0
67constructor NativeTreePathsOf
68field unrestricted nativeTreePreviousGroupPath : (pi unrestricted role : Nat . Nat)
69field unrestricted nativeTreePreviousShardPath : (pi unrestricted index : Nat . Nat)
70field unrestricted nativeTreeGroupCandidatePath : Nat
71field unrestricted nativeTreeGroupCommittedPath : Nat
72field unrestricted nativeTreeShardCandidatePath : (pi unrestricted index : Nat . Nat)
73field unrestricted nativeTreeShardCommittedPath : (pi unrestricted index : Nat . Nat)
74field unrestricted nativeTreeDirectoryPath : Nat
75
76end-family
77
78def nativeTreeGroup =
79 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
80 (eliminate
81 NativeTreeCheckpoint
82 (lambda unrestricted current : (family NativeTreeCheckpoint) .
83 (family NativeCheckpointLayout))
84 plan
85 (branch NativeTreeCheckpointOf group shards ancestors epoch end . group)))
86
87def nativeTreeShards =
88 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
89 (eliminate
90 NativeTreeCheckpoint
91 (lambda unrestricted current : (family NativeTreeCheckpoint) .
92 (family StdList (family NativeRegionShard)))
93 plan
94 (branch NativeTreeCheckpointOf group shards ancestors epoch end . shards)))
95
96def nativeTreeAncestors =
97 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
98 (eliminate
99 NativeTreeCheckpoint
100 (lambda unrestricted current : (family NativeTreeCheckpoint) .
101 (family StdList (family NativeCheckpointLayout)))
102 plan
103 (branch NativeTreeCheckpointOf group shards ancestors epoch end . ancestors)))
104
105def nativeTreeEpoch =
106 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
107 (eliminate
108 NativeTreeCheckpoint
109 (lambda unrestricted current : (family NativeTreeCheckpoint) . Nat)
110 plan
111 (branch NativeTreeCheckpointOf group shards ancestors epoch end . epoch)))
112
113def nativeTreeEnd =
114 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
115 (eliminate
116 NativeTreeCheckpoint
117 (lambda unrestricted current : (family NativeTreeCheckpoint) . Nat)
118 plan
119 (branch NativeTreeCheckpointOf group shards ancestors epoch end . end)))
120
121def nativeTreePreviousGroup =
122 (lambda unrestricted paths : (family NativeTreePaths) .
123 (eliminate
124 NativeTreePaths
125 (lambda unrestricted current : (family NativeTreePaths) . (pi unrestricted role : Nat . Nat))
126 paths
127 (branch
128 NativeTreePathsOf
129 group
130 shard
131 candidate
132 committed
133 shardCandidate
134 shardCommitted
135 directory
136 .
137 group)))
138
139def nativeTreePreviousShard =
140 (lambda unrestricted paths : (family NativeTreePaths) .
141 (eliminate
142 NativeTreePaths
143 (lambda unrestricted current : (family NativeTreePaths) . (pi unrestricted index : Nat . Nat))
144 paths
145 (branch
146 NativeTreePathsOf
147 group
148 shard
149 candidate
150 committed
151 shardCandidate
152 shardCommitted
153 directory
154 .
155 shard)))
156
157def nativeTreeGroupCandidate =
158 (lambda unrestricted paths : (family NativeTreePaths) .
159 (eliminate
160 NativeTreePaths
161 (lambda unrestricted current : (family NativeTreePaths) . Nat)
162 paths
163 (branch
164 NativeTreePathsOf
165 group
166 shard
167 candidate
168 committed
169 shardCandidate
170 shardCommitted
171 directory
172 .
173 candidate)))
174
175def nativeTreeGroupCommitted =
176 (lambda unrestricted paths : (family NativeTreePaths) .
177 (eliminate
178 NativeTreePaths
179 (lambda unrestricted current : (family NativeTreePaths) . Nat)
180 paths
181 (branch
182 NativeTreePathsOf
183 group
184 shard
185 candidate
186 committed
187 shardCandidate
188 shardCommitted
189 directory
190 .
191 committed)))
192
193def nativeTreeShardCandidate =
194 (lambda unrestricted paths : (family NativeTreePaths) .
195 (eliminate
196 NativeTreePaths
197 (lambda unrestricted current : (family NativeTreePaths) . (pi unrestricted index : Nat . Nat))
198 paths
199 (branch
200 NativeTreePathsOf
201 group
202 shard
203 candidate
204 committed
205 shardCandidate
206 shardCommitted
207 directory
208 .
209 shardCandidate)))
210
211def nativeTreeShardCommitted =
212 (lambda unrestricted paths : (family NativeTreePaths) .
213 (eliminate
214 NativeTreePaths
215 (lambda unrestricted current : (family NativeTreePaths) . (pi unrestricted index : Nat . Nat))
216 paths
217 (branch
218 NativeTreePathsOf
219 group
220 shard
221 candidate
222 committed
223 shardCandidate
224 shardCommitted
225 directory
226 .
227 shardCommitted)))
228
229def nativeTreeDirectory =
230 (lambda unrestricted paths : (family NativeTreePaths) .
231 (eliminate
232 NativeTreePaths
233 (lambda unrestricted current : (family NativeTreePaths) . Nat)
234 paths
235 (branch
236 NativeTreePathsOf
237 group
238 shard
239 candidate
240 committed
241 shardCandidate
242 shardCommitted
243 directory
244 .
245 directory)))
246
247-- The same planned layouts published under a later membership epoch: a
248-- resumed generation publishes at the restored epoch + 1.
249def nativeTreeCheckpointAdvanced =
250 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
251 (lambda unrestricted resume : Nat .
252 (constructor
253 NativeTreeCheckpoint
254 NativeTreeCheckpointOf
255 (nativeTreeGroup plan)
256 (nativeTreeShards plan)
257 (nativeTreeAncestors plan)
258 (naturalAdd (nativeTreeEpoch plan) resume)
259 (nativeTreeEnd plan))))
260
261-- ---- records ----
262-- A record is a 24-byte descriptor followed by a 32-byte digest, the shape
263-- of Checkpoint.NativeRegions' manifest records. An own-shard descriptor is
264-- (ordinal, begin, end); a child descriptor is (child role, subtree size,
265-- nativeTreeGroupTag). Records sit after the capture prefix: own shards
266-- first, then children in role order, so a record's meaning is positional
267-- and fixed by the plan.
268def nativeTreeGroupTag : Nat =
269 0x50554f52472d4c41
270
271def nativeTreeChildDescriptor =
272 (lambda unrestricted role : Nat .
273 (lambda unrestricted size : Nat .
274 (bytes-append
275 (checkpointEnvelopeWord role)
276 (bytes-append (checkpointEnvelopeWord size) (checkpointEnvelopeWord nativeTreeGroupTag)))))
277
278def nativeTreeRecordAt =
279 (lambda unrestricted layout : (family NativeCheckpointLayout) .
280 (lambda unrestricted index : Nat .
281 (naturalAdd
282 (nativeCheckpointPayloadAt layout)
283 (naturalAdd nativeRegionCaptureBytes (naturalMultiply index nativeRegionRecordBytes)))))
284
285def nativeTreeRecordDigestAt =
286 (lambda unrestricted layout : (family NativeCheckpointLayout) .
287 (lambda unrestricted index : Nat .
288 (naturalAdd (nativeTreeRecordAt layout index) nativeRegionDescriptorBytes)))
289
290-- The payload digest the envelope stores for a single-chunk file.
291def nativeTreeLayoutDigestAt =
292 (lambda unrestricted layout : (family NativeCheckpointLayout) .
293 (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeDigestsAt))
294
295-- A commitment: the agreed leading state bytes (at least the capture
296-- prefix; a replicated learner's whole replicated state) followed by one
297-- child record.
298def nativeTreeCommitmentBytesOf =
299 (lambda unrestricted agreed : Nat . (naturalAdd agreed nativeRegionRecordBytes))
300
301def nativeTreeCommitmentBytes =
302 (nativeTreeCommitmentBytesOf nativeRegionCaptureBytes)
303
304-- ---- the manifest contract of one node ----
305def nativeTreeGroupSchema =
306 (lambda unrestricted logical : Bytes .
307 (lambda unrestricted fanout : Nat .
308 (lambda unrestricted count : Nat .
309 (lambda unrestricted node : (family ParticipantTreeNode) .
310 (lambda unrestricted own : (family StdList (family CheckpointRegionPartition)) .
311 (bytes-append
312 b"ALPHA-REGION-GROUP-1\x00"
313 (bytes-append
314 logical
315 (bytes-append
316 (checkpointEnvelopeWord fanout)
317 (bytes-append
318 (checkpointEnvelopeWord count)
319 (bytes-append
320 (checkpointEnvelopeWord (participantTreeRoleOf node))
321 (bytes-append
322 (checkpointEnvelopeWord (participantTreeSizeOf node))
323 (nativeRegionPartitionBytes own))))))))))))
324
325def nativeTreeRecordCount =
326 (lambda unrestricted fanout : Nat .
327 (lambda unrestricted node : (family ParticipantTreeNode) .
328 (lambda unrestricted own : (family StdList (family CheckpointRegionPartition)) .
329 (naturalAdd
330 (nativeRegionShardCount own)
331 (participantTreeChildCount fanout (participantTreeSizeOf node))))))
332
333def planNativeTreeGroup =
334 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
335 (lambda unrestricted logical : Bytes .
336 (lambda unrestricted fanout : Nat .
337 (lambda unrestricted count : Nat .
338 (lambda unrestricted node : (family ParticipantTreeNode) .
339 (lambda unrestricted own : (family StdList (family CheckpointRegionPartition)) .
340 (lambda unrestricted base : Nat .
341 (lambda unrestricted available : Nat .
342 (planNativeCheckpoint
343 (nativeRegionContract
344 context
345 (nativeTreeGroupSchema logical fanout count node own)
346 (naturalAdd
347 nativeRegionCaptureBytes
348 (naturalMultiply
349 (nativeTreeRecordCount fanout node own)
350 nativeRegionRecordBytes)))
351 base
352 0
353 nativeCheckpointWordBytes
354 available)))))))))
355
356-- Plan this role's group manifest, its own shards and its ancestors' group
357-- manifests, in that order from `base`. `ownOf role` gives a role's own
358-- partition (the regions and intervals it holds); every participant derives
359-- every ancestor's contract from it and the hierarchy, never from a peer.
360-- Memory is the role's own shards plus at most height + 1 manifests of at
361-- most fan-out + own records each: independent of the participant count.
362def planNativeTreeAncestors =
363 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
364 (lambda unrestricted logical : Bytes .
365 (lambda unrestricted fanout : Nat .
366 (lambda unrestricted count : Nat .
367 (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) .
368 (lambda unrestricted available : Nat .
369 (lambda unrestricted ancestors : (family StdList (family ParticipantTreeNode)) .
370 (lambda unrestricted finish : (pi unrestricted at : Nat . (pi unrestricted planned : (family StdList (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)))) .
371 (stdListFold
372 (family ParticipantTreeNode)
373 (pi unrestricted at : Nat .
374 (pi unrestricted planned : (family StdList (family NativeCheckpointLayout)) .
375 (family
376 StdResult
377 (family NativeCheckpointFailure)
378 (family NativeTreeCheckpoint))))
379 (lambda unrestricted ancestor : (family ParticipantTreeNode) .
380 (lambda unrestricted next : (pi unrestricted at : Nat . (pi unrestricted planned : (family StdList (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)))) .
381 (lambda unrestricted at : Nat .
382 (lambda unrestricted planned : (family StdList (family NativeCheckpointLayout)) .
383 (eliminate
384 StdResult
385 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
386 (family
387 StdResult
388 (family NativeCheckpointFailure)
389 (family NativeTreeCheckpoint)))
390 (planNativeTreeGroup
391 context
392 logical
393 fanout
394 count
395 ancestor
396 (ownOf (participantTreeRoleOf ancestor))
397 at
398 available)
399 (branch
400 StdFailure
401 error
402 .
403 (constructor
404 StdResult
405 StdFailure
406 (family NativeCheckpointFailure)
407 (family NativeTreeCheckpoint)
408 error))
409 (branch
410 StdSuccess
411 layout
412 .
413 (next
414 (nativeCheckpointAlign (nativeCheckpointEnd layout))
415 (stdListAppend
416 (family NativeCheckpointLayout)
417 planned
418 (constructor
419 StdList
420 StdListCons
421 (family NativeCheckpointLayout)
422 layout
423 (constructor
424 StdList
425 StdListEmpty
426 (family NativeCheckpointLayout)))))))))))
427 finish
428 ancestors)))))))))
429
430def planNativeTreeCheckpoint =
431 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
432 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
433 (lambda unrestricted fanout : Nat .
434 (lambda unrestricted count : Nat .
435 (lambda unrestricted role : Nat .
436 (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) .
437 (lambda unrestricted epoch : Nat .
438 (lambda unrestricted base : Nat .
439 (lambda unrestricted available : Nat .
440 (let unrestricted logical =
441 (checkpointLogicalSchemaBytes regions)
442 in
443 (eliminate
444 StdResult
445 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
446 (family
447 StdResult
448 (family NativeCheckpointFailure)
449 (family NativeTreeCheckpoint)))
450 (planNativeTreeGroup
451 context
452 logical
453 fanout
454 count
455 (participantTreeNode fanout count role)
456 (ownOf role)
457 base
458 available)
459 (branch
460 StdFailure
461 error
462 .
463 (constructor
464 StdResult
465 StdFailure
466 (family NativeCheckpointFailure)
467 (family NativeTreeCheckpoint)
468 error))
469 (branch
470 StdSuccess
471 group
472 .
473 (eliminate
474 StdResult
475 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
476 (family
477 StdResult
478 (family NativeCheckpointFailure)
479 (family NativeTreeCheckpoint)))
480 (nativeRegionAppendParts
481 context
482 logical
483 available
484 (ownOf role)
485 (constructor
486 StdResult
487 StdSuccess
488 (family NativeCheckpointFailure)
489 (family NativeRegionCheckpoint)
490 (constructor
491 NativeRegionCheckpoint
492 NativeRegionCheckpointOf
493 group
494 (constructor StdList StdListEmpty (family NativeRegionShard))
495 epoch
496 (nativeCheckpointEnd group))))
497 (branch
498 StdFailure
499 error
500 .
501 (constructor
502 StdResult
503 StdFailure
504 (family NativeCheckpointFailure)
505 (family NativeTreeCheckpoint)
506 error))
507 (branch
508 StdSuccess
509 shards
510 .
511 (planNativeTreeAncestors
512 context
513 logical
514 fanout
515 count
516 ownOf
517 available
518 (participantTreeAncestors fanout count role)
519 (lambda unrestricted at : Nat .
520 (lambda unrestricted planned : (family StdList (family NativeCheckpointLayout)) .
521 (constructor
522 StdResult
523 StdSuccess
524 (family NativeCheckpointFailure)
525 (family NativeTreeCheckpoint)
526 (constructor
527 NativeTreeCheckpoint
528 NativeTreeCheckpointOf
529 group
530 (stdListReverse
531 (family NativeRegionShard)
532 (nativeRegionShards shards))
533 planned
534 epoch
535 at))))
536 (nativeCheckpointAlign (nativeRegionEnd shards))
537 (constructor StdList StdListEmpty (family NativeCheckpointLayout)))))))))))))))))
538
539-- ---- publication ----
540def nativeTreeArgument =
541 nativeRegionPathArgument
542
543-- Prepare this role's own shards from its state and record each one's
544-- descriptor and payload digest in its group manifest.
545def nativeTreePrepareOwn =
546 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
547 (lambda unrestricted stateAt : Nat .
548 (lambda unrestricted offsetOf : (pi unrestricted shard : (family NativeRegionShard) . Nat) .
549 (lambda unrestricted paths : (family NativeTreePaths) .
550 (lambda unrestricted tail : (family NativePhysicalCommands) .
551 (stdListFold
552 (family NativeRegionShard)
553 (pi unrestricted index : Nat . (family NativePhysicalCommands))
554 (lambda unrestricted shard : (family NativeRegionShard) .
555 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
556 (lambda unrestricted index : Nat .
557 (nativeRegionPrepareShard
558 shard
559 (nativeMemoryState stateAt)
560 (nativeMemoryState (naturalAdd stateAt (offsetOf shard)))
561 (nativeTreeArgument (nativeTreeShardCandidate paths index))
562 (nativeTreeArgument (nativeTreeShardCommitted paths index))
563 (nativeTreeArgument (nativeTreeDirectory paths))
564 nativePeerListenerSlot
565 nativePeerScratchSlot
566 (nativeMemoryCopyPayload
567 (nativeTreeRecordAt (nativeTreeGroup plan) index)
568 (nativeRegionDescriptor
569 (nativeRegionOrdinal shard)
570 (nativeRegionInterval shard))
571 (nativeMemoryCopyOperands
572 (nativeMemoryState
573 (nativeTreeRecordDigestAt (nativeTreeGroup plan) index))
574 (nativeMemoryState (nativeTreeLayoutDigestAt (nativeRegionLayout shard)))
575 checkpointEnvelopeDigestBytes
576 nativePeerScratchSlot
577 b"tree-shard-record"
578 (next (succ index))))))))
579 (lambda unrestricted index : Nat . tail)
580 (nativeTreeShards plan)
581 0))))))
582
583-- Receive each child's commitment over its edge and record it after checking
584-- the capture prefix and that it covers exactly the prescribed subtree.
585def nativeTreeReceiveChildren =
586 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
587 (lambda unrestricted fanout : Nat .
588 (lambda unrestricted node : (family ParticipantTreeNode) .
589 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
590 (lambda unrestricted commitment : (pi unrestricted child : Nat . (family RegionFrameLayout)) .
591 (lambda unrestricted stateAt : Nat .
592 (lambda unrestricted agreed : Nat .
593 (lambda unrestricted epoch : (family NativePhysicalOperand) .
594 (lambda unrestricted version : (family NativePhysicalOperand) .
595 (lambda unrestricted tail : (family NativePhysicalCommands) .
596 (let unrestricted own =
597 (stdListLength (family NativeRegionShard) (nativeTreeShards plan))
598 in
599 (stdListFold
600 (family ParticipantTreeNode)
601 (pi unrestricted index : Nat . (family NativePhysicalCommands))
602 (lambda unrestricted child : (family ParticipantTreeNode) .
603 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
604 (lambda unrestricted index : Nat .
605 (let unrestricted role =
606 (participantTreeRoleOf child)
607 in
608 (let unrestricted frame =
609 (commitment role)
610 in
611 (let unrestricted record =
612 (naturalAdd own index)
613 in
614 (nativeFrameInitializeRound
615 frame
616 epoch
617 version
618 (nativePeerPublicationIO
619 (nativeLaunchRecipeSlotValue
620 (nativePeerEdgeConnectionTo edges role))
621 0
622 frame
623 (nativeFrameConsume
624 frame
625 (nativeMemoryCompareRegions
626 stateAt
627 (framePayloadAt frame)
628 agreed
629 nativePeerScratchSlot
630 b"tree-child-position"
631 (nativeMemoryCopyPayload
632 (nativeTreeRecordAt (nativeTreeGroup plan) record)
633 (nativeTreeChildDescriptor
634 role
635 (participantTreeSizeOf child))
636 (nativeMemoryCompareRegions
637 (nativeTreeRecordAt (nativeTreeGroup plan) record)
638 (naturalAdd (framePayloadAt frame) agreed)
639 nativeRegionDescriptorBytes
640 nativePeerScratchSlot
641 b"tree-child-coverage"
642 (nativeMemoryCopyOperands
643 (nativeMemoryState
644 (nativeTreeRecordDigestAt (nativeTreeGroup plan) record))
645 (nativeMemoryState
646 (naturalAdd
647 (framePayloadAt frame)
648 (naturalAdd agreed nativeRegionDescriptorBytes)))
649 checkpointEnvelopeDigestBytes
650 nativePeerScratchSlot
651 b"tree-child-record"
652 (next (succ index)))))))))))))))
653 (lambda unrestricted index : Nat . tail)
654 (participantTreeChildren fanout node)
655 0))))))))))))
656
657-- Commit this role's group manifest to its parent and wait for release.
658def nativeTreeCommitUpward =
659 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
660 (lambda unrestricted node : (family ParticipantTreeNode) .
661 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
662 (lambda unrestricted commitment : (pi unrestricted child : Nat . (family RegionFrameLayout)) .
663 (lambda unrestricted release : (pi unrestricted child : Nat . (family RegionFrameLayout)) .
664 (lambda unrestricted stateAt : Nat .
665 (lambda unrestricted agreed : Nat .
666 (lambda unrestricted epoch : (family NativePhysicalOperand) .
667 (lambda unrestricted version : (family NativePhysicalOperand) .
668 (lambda unrestricted tail : (family NativePhysicalCommands) .
669 (let unrestricted role =
670 (participantTreeRoleOf node)
671 in
672 (let unrestricted frame =
673 (commitment role)
674 in
675 (let unrestricted released =
676 (release role)
677 in
678 (let unrestricted parent =
679 (nativeLaunchRecipeSlotValue
680 (nativePeerEdgeConnectionTo edges (participantTreeParentOf node)))
681 in
682 (nativeFrameInitializeRound
683 frame
684 epoch
685 version
686 (nativeFrameInitializeRound
687 released
688 epoch
689 version
690 (nativeMemoryCopyOperands
691 (nativeMemoryState (framePayloadAt frame))
692 (nativeMemoryState stateAt)
693 agreed
694 nativePeerScratchSlot
695 b"tree-commit-position"
696 (nativeMemoryCopyPayload
697 (naturalAdd (framePayloadAt frame) agreed)
698 (nativeTreeChildDescriptor role (participantTreeSizeOf node))
699 (nativeMemoryCopyOperands
700 (nativeMemoryState
701 (naturalAdd
702 (framePayloadAt frame)
703 (naturalAdd agreed nativeRegionDescriptorBytes)))
704 (nativeMemoryState
705 (nativeTreeLayoutDigestAt (nativeTreeGroup plan)))
706 checkpointEnvelopeDigestBytes
707 nativePeerScratchSlot
708 b"tree-commit-digest"
709 (nativePeerPublicationIO
710 parent
711 1
712 frame
713 (nativePeerPublicationIO
714 parent
715 0
716 released
717 (nativeFrameConsume
718 released
719 (nativeLaunchRecipeAssertEqual
720 (nativeMemoryLoad (framePayloadAt released))
721 version
722 b"tree-released-version"
723 tail)))))))))))))))))))))))
724
725-- Release each child, in role order, with the published version.
726def nativeTreeReleaseChildren =
727 (lambda unrestricted fanout : Nat .
728 (lambda unrestricted node : (family ParticipantTreeNode) .
729 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
730 (lambda unrestricted release : (pi unrestricted child : Nat . (family RegionFrameLayout)) .
731 (lambda unrestricted epoch : (family NativePhysicalOperand) .
732 (lambda unrestricted version : (family NativePhysicalOperand) .
733 (lambda unrestricted tail : (family NativePhysicalCommands) .
734 (stdListFold
735 (family ParticipantTreeNode)
736 (family NativePhysicalCommands)
737 (lambda unrestricted child : (family ParticipantTreeNode) .
738 (lambda unrestricted rest : (family NativePhysicalCommands) .
739 (let unrestricted role =
740 (participantTreeRoleOf child)
741 in
742 (let unrestricted released =
743 (release role)
744 in
745 (nativeFrameInitializeRound
746 released
747 epoch
748 version
749 (nativeMemoryStoreWord64
750 b"tree-release-version"
751 (framePayloadAt released)
752 version
753 (nativePeerPublicationIO
754 (nativeLaunchRecipeSlotValue
755 (nativePeerEdgeConnectionTo edges role))
756 1
757 released
758 rest)))))))
759 tail
760 (participantTreeChildren fanout node)))))))))
761
762-- The complete publication of one role: own shards, children's commitments,
763-- group manifest (the root's at the published-root path), commitment to the
764-- parent and its release, then the children's release. A role completes
765-- only after the root is durable. `commitment c` / `release c` are the
766-- frames of the edge between c and its parent; the caller plans them with
767-- identities naming that edge so a frame received on the wrong edge fails.
768def nativeTreePublish =
769 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
770 (lambda unrestricted fanout : Nat .
771 (lambda unrestricted count : Nat .
772 (lambda unrestricted role : Nat .
773 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
774 (lambda unrestricted commitment : (pi unrestricted child : Nat . (family RegionFrameLayout)) .
775 (lambda unrestricted release : (pi unrestricted child : Nat . (family RegionFrameLayout)) .
776 (lambda unrestricted stateAt : Nat .
777 (lambda unrestricted agreed : Nat .
778 (lambda unrestricted offsetOf : (pi unrestricted shard : (family NativeRegionShard) . Nat) .
779 (lambda unrestricted paths : (family NativeTreePaths) .
780 (lambda unrestricted success : (family NativePhysicalCommands) .
781 (let unrestricted node =
782 (participantTreeNode fanout count role)
783 in
784 (let unrestricted version =
785 (nativeMemoryLoad stateAt)
786 in
787 (let unrestricted epoch =
788 (nativeMemoryLoad
789 (naturalAdd stateAt (naturalMultiply 2 nativeCheckpointWordBytes)))
790 in
791 (nativeMemoryCopyOperands
792 (nativeMemoryState
793 (nativeCheckpointPayloadAt (nativeTreeGroup plan)))
794 (nativeMemoryState stateAt)
795 nativeRegionCaptureBytes
796 nativePeerScratchSlot
797 b"tree-capture"
798 (nativeLaunchRecipeAssertEqual
799 epoch
800 (nativeLaunchRecipeImmediate (nativeTreeEpoch plan))
801 b"tree-membership-epoch"
802 (nativeTreePrepareOwn
803 plan
804 stateAt
805 offsetOf
806 paths
807 (nativeTreeReceiveChildren
808 plan
809 fanout
810 node
811 edges
812 commitment
813 stateAt
814 agreed
815 epoch
816 version
817 (nativeCheckpointPublish
818 (nativeTreeGroup plan)
819 (nativeTreeArgument (nativeTreeGroupCandidate paths))
820 (nativeTreeArgument (nativeTreeGroupCommitted paths))
821 (nativeTreeArgument (nativeTreeDirectory paths))
822 nativePeerListenerSlot
823 nativePeerScratchSlot
824 6
825 (nat-eliminate
826 (lambda unrestricted root : Nat .
827 (family NativePhysicalCommands))
828 (nativeTreeCommitUpward
829 plan
830 node
831 edges
832 commitment
833 release
834 stateAt
835 agreed
836 epoch
837 version
838 (nativeTreeReleaseChildren
839 fanout
840 node
841 edges
842 release
843 epoch
844 version
845 success))
846 (lambda unrestricted predecessor : Nat .
847 (lambda unrestricted ignored : (family NativePhysicalCommands) .
848 (nativeTreeReleaseChildren
849 fanout
850 node
851 edges
852 release
853 epoch
854 version
855 success)))
856 (participantTreeIsRoot node))))))))))))))))))))))
857
858-- ---- restore ----
859-- Read the previous generation along one path: the root manifest, then each
860-- descendant's group manifest down to this role's own, checking each
861-- manifest's payload digest against the record its parent holds and every
862-- capture prefix against the root's; then this role's own shards, checked
863-- against its own records, into `destination shard`. Reads touch height + 1
864-- manifests and the own shards, never a sibling subtree. The root manifest's
865-- capture prefix is left in this role's group layout for the caller.
866def nativeTreeRestoreManifests =
867 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
868 (lambda unrestricted fanout : Nat .
869 (lambda unrestricted count : Nat .
870 (lambda unrestricted role : Nat .
871 (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) .
872 (lambda unrestricted paths : (family NativeTreePaths) .
873 (lambda unrestricted tail : (family NativePhysicalCommands) .
874 (let unrestricted chain =
875 (stdListAppend
876 (family NativeCheckpointLayout)
877 (nativeTreeAncestors plan)
878 (constructor
879 StdList
880 StdListCons
881 (family NativeCheckpointLayout)
882 (nativeTreeGroup plan)
883 (constructor StdList StdListEmpty (family NativeCheckpointLayout))))
884 in
885 (let unrestricted roles =
886 (stdListAppend
887 Nat
888 (stdListMap
889 (family ParticipantTreeNode)
890 Nat
891 participantTreeRoleOf
892 (participantTreeAncestors fanout count role))
893 (constructor
894 StdList
895 StdListCons
896 Nat
897 role
898 (constructor StdList StdListEmpty Nat)))
899 in
900 (let unrestricted root =
901 (stdListHeadOr (family NativeCheckpointLayout) (nativeTreeGroup plan) chain)
902 in
903 (stdListFold
904 Nat
905 (pi unrestricted index : Nat . (family NativePhysicalCommands))
906 (lambda unrestricted at : Nat .
907 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
908 (lambda unrestricted index : Nat .
909 (let unrestricted layout =
910 (stdListHeadOr
911 (family NativeCheckpointLayout)
912 (nativeTreeGroup plan)
913 (stdListDrop (family NativeCheckpointLayout) index chain))
914 in
915 (let unrestricted parentRole =
916 (stdListHeadOr
917 Nat
918 0
919 (stdListDrop Nat (naturalPredecessor index) roles))
920 in
921 (let unrestricted parent =
922 (stdListHeadOr
923 (family NativeCheckpointLayout)
924 (nativeTreeGroup plan)
925 (stdListDrop
926 (family NativeCheckpointLayout)
927 (naturalPredecessor index)
928 chain))
929 in
930 (nativeCheckpointRestore
931 layout
932 (nativeTreeArgument (nativeTreePreviousGroup paths at))
933 nativePeerListenerSlot
934 nativePeerScratchSlot
935 (nat-eliminate
936 (lambda unrestricted first : Nat .
937 (family NativePhysicalCommands))
938 (nativeMemoryCompareRegions
939 (nativeTreeLayoutDigestAt layout)
940 (nativeTreeRecordDigestAt
941 parent
942 (naturalAdd
943 (nativeRegionShardCount (ownOf parentRole))
944 (participantTreeChildHolding
945 fanout
946 (participantTreeNode fanout count parentRole)
947 at)))
948 checkpointEnvelopeDigestBytes
949 nativePeerScratchSlot
950 b"tree-restore-digest"
951 (nativeMemoryCompareRegions
952 (nativeCheckpointPayloadAt root)
953 (nativeCheckpointPayloadAt layout)
954 nativeRegionCaptureBytes
955 nativePeerScratchSlot
956 b"tree-restore-position"
957 (next (succ index))))
958 (lambda unrestricted predecessor : Nat .
959 (lambda unrestricted ignored : (family NativePhysicalCommands) .
960 (nativeLaunchRecipeAssertEqual
961 (nativeMemoryLoad
962 (naturalAdd
963 (nativeCheckpointPayloadAt root)
964 (naturalMultiply 2 nativeCheckpointWordBytes)))
965 (nativeLaunchRecipeImmediate (nativeTreeEpoch plan))
966 b"tree-membership-epoch"
967 (next (succ index)))))
968 (naturalIsZero index)))))))))
969 (lambda unrestricted index : Nat . tail)
970 roles
971 0)))))))))))
972
973-- The shards of the records from position `first` on: a role that needs only
974-- some of another manifest's shards checks each against its own record.
975-- `pathOf` and every record index are positions in that manifest.
976def nativeTreeRestoreShardsFrom =
977 (lambda unrestricted records : (family NativeCheckpointLayout) .
978 (lambda unrestricted first : Nat .
979 (lambda unrestricted shards : (family StdList (family NativeRegionShard)) .
980 (lambda unrestricted pathOf : (pi unrestricted index : Nat . Nat) .
981 (lambda unrestricted destination : (pi unrestricted shard : (family NativeRegionShard) . Nat) .
982 (lambda unrestricted tail : (family NativePhysicalCommands) .
983 (stdListFold
984 (family NativeRegionShard)
985 (pi unrestricted index : Nat . (family NativePhysicalCommands))
986 (lambda unrestricted shard : (family NativeRegionShard) .
987 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
988 (lambda unrestricted index : Nat .
989 (let unrestricted layout =
990 (nativeRegionLayout shard)
991 in
992 (nativeCheckpointRestore
993 layout
994 (nativeTreeArgument (pathOf index))
995 nativePeerListenerSlot
996 nativePeerScratchSlot
997 (nativeMemoryCompareRegions
998 (nativeTreeLayoutDigestAt layout)
999 (nativeTreeRecordDigestAt records index)
1000 checkpointEnvelopeDigestBytes
1001 nativePeerScratchSlot
1002 b"tree-restore-shard-digest"
1003 (nativeMemoryCompareRegions
1004 (nativeCheckpointPayloadAt records)
1005 (nativeCheckpointPayloadAt layout)
1006 nativeRegionCaptureBytes
1007 nativePeerScratchSlot
1008 b"tree-restore-shard-position"
1009 (nativeMemoryCopyOperands
1010 (nativeMemoryState (destination shard))
1011 (nativeMemoryState
1012 (naturalAdd
1013 (nativeCheckpointPayloadAt layout)
1014 nativeRegionCaptureBytes))
1015 (intervalExtent (nativeRegionInterval shard))
1016 nativePeerScratchSlot
1017 b"tree-restore-shard-state"
1018 (next (succ index))))))))))
1019 (lambda unrestricted index : Nat . tail)
1020 shards
1021 first)))))))
1022
1023-- The shards of `records`, in record order, from record 0.
1024def nativeTreeRestoreShards =
1025 (lambda unrestricted records : (family NativeCheckpointLayout) .
1026 (nativeTreeRestoreShardsFrom records 0))
1027
1028-- This role's own shards, checked against its own group manifest's records.
1029def nativeTreeRestoreOwn =
1030 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
1031 (lambda unrestricted paths : (family NativeTreePaths) .
1032 (lambda unrestricted destination : (pi unrestricted shard : (family NativeRegionShard) . Nat) .
1033 (lambda unrestricted tail : (family NativePhysicalCommands) .
1034 (nativeTreeRestoreShards
1035 (nativeTreeGroup plan)
1036 (nativeTreeShards plan)
1037 (lambda unrestricted index : Nat . (nativeTreePreviousShard paths index))
1038 destination
1039 tail)))))
1040
1041-- The root's group manifest as this role restored it: the first ancestor,
1042-- or the role's own when it is the root.
1043def nativeTreeRootLayout =
1044 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
1045 (stdListHeadOr
1046 (family NativeCheckpointLayout)
1047 (nativeTreeGroup plan)
1048 (nativeTreeAncestors plan)))
1049
1050-- Layouts, from `base`, for the root's own shards at any role. A replicated
1051-- region the root alone publishes is restored by every role from the root's
1052-- shards, each checked against the root manifest's records
1053-- (nativeTreeRestoreShards with nativeTreeRootLayout): one manifest path and
1054-- the region itself, never another subtree.
1055def planNativeTreeRootShards =
1056 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
1057 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
1058 (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) .
1059 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
1060 (lambda unrestricted base : Nat .
1061 (lambda unrestricted available : Nat .
1062 (stdResultBind
1063 (family NativeCheckpointFailure)
1064 (family NativeRegionCheckpoint)
1065 (family NativeRegionCheckpoint)
1066 (nativeRegionAppendParts
1067 context
1068 (checkpointLogicalSchemaBytes regions)
1069 available
1070 (ownOf 0)
1071 (constructor
1072 StdResult
1073 StdSuccess
1074 (family NativeCheckpointFailure)
1075 (family NativeRegionCheckpoint)
1076 (constructor
1077 NativeRegionCheckpoint
1078 NativeRegionCheckpointOf
1079 (nativeTreeGroup plan)
1080 (constructor StdList StdListEmpty (family NativeRegionShard))
1081 (nativeTreeEpoch plan)
1082 base)))
1083 -- appended shards accumulate last first; records are in order
1084 (lambda unrestricted planned : (family NativeRegionCheckpoint) .
1085 (constructor
1086 StdResult
1087 StdSuccess
1088 (family NativeCheckpointFailure)
1089 (family NativeRegionCheckpoint)
1090 (constructor
1091 NativeRegionCheckpoint
1092 NativeRegionCheckpointOf
1093 (nativeRegionManifest planned)
1094 (stdListReverse (family NativeRegionShard) (nativeRegionShards planned))
1095 (nativeRegionEpoch planned)
1096 (nativeRegionEnd planned)))))))))))
1097
1098def nativeTreeRestore =
1099 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
1100 (lambda unrestricted fanout : Nat .
1101 (lambda unrestricted count : Nat .
1102 (lambda unrestricted role : Nat .
1103 (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) .
1104 (lambda unrestricted paths : (family NativeTreePaths) .
1105 (lambda unrestricted destination : (pi unrestricted shard : (family NativeRegionShard) . Nat) .
1106 (lambda unrestricted tail : (family NativePhysicalCommands) .
1107 (nativeTreeRestoreManifests
1108 plan
1109 fanout
1110 count
1111 role
1112 ownOf
1113 paths
1114 (nativeTreeRestoreOwn plan paths destination tail))))))))))
1115
1116-- The prefix restored from the root manifest (version, cursor, epoch).
1117def nativeTreeRestoredCaptureAt =
1118 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
1119 (nativeCheckpointPayloadAt (nativeTreeGroup plan)))
1120
1121-- ---- admission ----
1122-- The plan's group manifest, own shards and ancestor manifests are laid out
1123-- contiguously from the group's base: one private staging resident.
1124def nativeTreeResidents =
1125 (lambda unrestricted plan : (family NativeTreeCheckpoint) .
1126 (constructor
1127 ArenaResidents
1128 ArenaResidentsNext
1129 (constructor
1130 ArenaResident
1131 ArenaResidentValue
1132 b"checkpoint-tree-private-staging"
1133 (nativeCheckpointBase (nativeTreeGroup plan))
1134 (naturalSaturatingSubtract
1135 (nativeTreeEnd plan)
1136 (nativeCheckpointBase (nativeTreeGroup plan)))
1137 1)
1138 (constructor ArenaResidents ArenaResidentsEnd)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.