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