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.
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))))))))))))))))))))))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.