---- layout ----
Below the root, the root's replicated shards' layouts after this role's
tree checkpoint; none at the root or when nothing is replicated.
429def dpotPlanRootShards =
430 (lambda unrestricted c : Nat .
431 (lambda unrestricted u : Nat .
432 (lambda unrestricted system : (family DataParallelSystem c u) .
433 (lambda unrestricted identity : Bytes .
434 (lambda unrestricted q : Nat .
435 (lambda unrestricted p : Nat .
436 (lambda unrestricted fanout : Nat .
437 (lambda unrestricted role : Nat .
438 (lambda unrestricted checkpoint : (family NativeTreeCheckpoint) .
439 (lambda unrestricted available : Nat .
440 (let unrestricted base =
441 (nativeCheckpointAlign (nativeTreeEnd checkpoint))
442 in
443 (nat-eliminate
444 (lambda unrestricted current : Nat .
445 (family
446 StdResult
447 (family NativeCheckpointFailure)
448 (family NativeRegionCheckpoint)))
449 (constructor
450 StdResult
451 StdSuccess
452 (family NativeCheckpointFailure)
453 (family NativeRegionCheckpoint)
454 (constructor
455 NativeRegionCheckpoint
456 NativeRegionCheckpointOf
457 (nativeTreeGroup checkpoint)
458 (constructor StdList StdListEmpty (family NativeRegionShard))
459 (nativeTreeEpoch checkpoint)
460 base))
461 (lambda unrestricted previous : Nat .
462 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
463 (planNativeTreeRootShards
464 (dpoContext c u system q p (dpotTopology fanout) identity)
465 (dpoRegions c u system q)
466 (lambda unrestricted owner : Nat .
467 (dpotReplicatedOf c u system q p))
468 checkpoint
469 base
470 available)))
471 (naturalAnd
472 (naturalNonzero role)
473 (naturalNonzero
474 (stdListLength
475 (family CheckpointRegionPartition)
476 (dpotReplicatedOf c u system q p))))))))))))))))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.