Layouts, from `base`, for the root's own shards at any role. A replicated
region the root alone publishes is restored by every role from the root's
shards, each checked against the root manifest's records
(nativeTreeRestoreShards with nativeTreeRootLayout): one manifest path and
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)))))))))))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.