After the last update: the tree publication of this generation, under the
new membership epoch after a resume. Every owner's shards are read from its
own state; commitments carry the capture prefix and replicated words.
733def dpotPublish =
734 (lambda unrestricted c : Nat .
735 (lambda unrestricted u : Nat .
736 (lambda unrestricted system : (family DataParallelSystem c u) .
737 (lambda unrestricted q : Nat .
738 (lambda unrestricted p : Nat .
739 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
740 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
741 (lambda unrestricted fanout : Nat .
742 (lambda unrestricted role : Nat .
743 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
744 (lambda unrestricted resume : Nat .
745 (lambda unrestricted success : (family NativePhysicalCommands) .
746 (nat-eliminate
747 (lambda unrestricted valid : Nat .
748 (family
749 StdResult
750 (family NativeCheckpointFailure)
751 (family NativePhysicalCommands)))
752 (constructor
753 StdResult
754 StdFailure
755 (family NativeCheckpointFailure)
756 (family NativePhysicalCommands)
757 (constructor NativeCheckpointFailure NativeCheckpointBounds))
758 (lambda unrestricted previous : Nat .
759 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
760 (constructor
761 StdResult
762 StdSuccess
763 (family NativeCheckpointFailure)
764 (family NativePhysicalCommands)
765 (nativeTreePublish
766 (nativeTreeCheckpointAdvanced (dpotCheckpoint tree) resume)
767 fanout
768 (dpOwners c u system)
769 role
770 edges
771 (dpotCommitmentFor
772 c
773 u
774 system
775 (dpoDigest layout)
776 q
777 p
778 fanout
779 tree)
780 (dpotReleaseFor c u system (dpoDigest layout) q p fanout tree)
781 (dpoStateAt layout)
782 (dpoAgreedBytes c u system q p)
783 (dpoShardOffset c u system q p)
784 (dpotPaths c u system q p role)
785 success))))
786 (dpotFramesAdmitted c u system (dpoDigest layout) q p fanout tree))))))))))))))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.