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