module Runtime.NativeDataParallelOwnedTree

import Learning.DataParallel
import Learning.Transition
import Learning.Numerics
import Runtime.NativeDataParallel
import Runtime.NativeDataParallelOwned
import Runtime.NativeCombine
import Runtime.NativeIndependentState
import Runtime.NativePeerEndpoint
import Runtime.NativePeerTree
import Runtime.NativeHostTarget
import Runtime.NativeResourcePlan
import Runtime.NativePhysicalProgram
import Runtime.NativeMemoryPlan
import Runtime.RegionTransfer
import Runtime.RegionFrame
import Compiler.Planning.RegionFrame
import Runtime.NativeRegionFrame
import Runtime.ArenaCertificate
import Checkpoint.Envelope
import Checkpoint.NativeEnvelope
import Checkpoint.NativeRegions
import Checkpoint.NativePeerPublication
import Checkpoint.NativeTreePublication
import Checkpoint.RegionManifest
import Representation.ParticipantTree
import Representation.Partition
import Data.Bytes
import Std.Foundation
import Std.List
import Std.Natural

-- Per-coordinate ownership (Runtime.NativeDataParallelOwned: optimizer state
-- and, with p = 1, parameters) over a bounded-fan-out hierarchy
-- (Representation.ParticipantTree) instead of a star:
--   combine: the sum and the assembly run on the hierarchy's tree
--     (Runtime.NativeCombine), so a participant exchanges with at most
--     fanout + 1 peers per combine;
--   publication: Checkpoint.NativeTreePublication. Every owner writes the
--     shards of its own words (its coordinates' optimizer state and, when
--     partitioned, parameters); the root also writes the replicated words
--     (replicated parameters, shared state). Each commitment carries the
--     child's capture prefix and replicated words, which the parent compares
--     with its own, so diverged replicas publish no root, and no owner ever
--     holds another owner's words;
--   restore: every owner reads its manifest path, its own shards and, below
--     the root, only the root's replicated shards.
-- The checkpoint's identity is the star's for replicated parameters with the
-- hierarchy's combine order, and for partitioned parameters the learner's
-- placement-independent identity tagged with the hierarchy's manifest tree.
family NativeDataParallelOwnedTreeLayout : Type 0
constructor NativeDataParallelOwnedTreeLayoutOf
-- template frames, planned for the edge of role 1; every edge's frames share
-- this storage
field unrestricted dataParallelOwnedTreeCommitment : (family RegionFrameLayout)
field unrestricted dataParallelOwnedTreeRelease : (family RegionFrameLayout)
field unrestricted dataParallelOwnedTreeCheckpoint : (family NativeTreeCheckpoint)
-- below the root, the root's replicated shards as this owner restores them
-- (none at the root, whose replicated words are its own shards)
field unrestricted dataParallelOwnedTreeRootShards : (family NativeRegionCheckpoint)

end-family

def dpotCommitment =
  (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
    (eliminate
      NativeDataParallelOwnedTreeLayout
      (lambda unrestricted current : (family NativeDataParallelOwnedTreeLayout) .
        (family RegionFrameLayout))
      tree
      (branch NativeDataParallelOwnedTreeLayoutOf commitment release checkpoint root . commitment)))

def dpotRelease =
  (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
    (eliminate
      NativeDataParallelOwnedTreeLayout
      (lambda unrestricted current : (family NativeDataParallelOwnedTreeLayout) .
        (family RegionFrameLayout))
      tree
      (branch NativeDataParallelOwnedTreeLayoutOf commitment release checkpoint root . release)))

def dpotCheckpoint =
  (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
    (eliminate
      NativeDataParallelOwnedTreeLayout
      (lambda unrestricted current : (family NativeDataParallelOwnedTreeLayout) .
        (family NativeTreeCheckpoint))
      tree
      (branch NativeDataParallelOwnedTreeLayoutOf commitment release checkpoint root . checkpoint)))

def dpotRootShards =
  (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
    (eliminate
      NativeDataParallelOwnedTreeLayout
      (lambda unrestricted current : (family NativeDataParallelOwnedTreeLayout) .
        (family NativeRegionCheckpoint))
      tree
      (branch NativeDataParallelOwnedTreeLayoutOf commitment release checkpoint root . root)))

def dpotTopology =
  (lambda unrestricted fanout : Nat .
    (constructor DataParallelTopology DataParallelHierarchy fanout))

-- ---- who holds which words ----
-- The one-word intervals of the indices below `count` whose coordinate
-- (index mod k) this role owns.
def dpotOwnedWords =
  (lambda unrestricted k : Nat .
    (lambda unrestricted owners : Nat .
      (lambda unrestricted role : Nat .
        (lambda unrestricted count : Nat .
          (stdListFold
            Nat
            (family StdList (family LogicalInterval))
            (lambda unrestricted index : Nat .
              (lambda unrestricted rest : (family StdList (family LogicalInterval)) .
                (nat-eliminate
                  (lambda unrestricted held : Nat . (family StdList (family LogicalInterval)))
                  rest
                  (lambda unrestricted previous : Nat .
                    (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
                      (constructor
                        StdList
                        StdListCons
                        (family LogicalInterval)
                        (dpoInterval (naturalMultiply dpWord index) dpWord)
                        rest)))
                  (dpoOwns owners role (naturalModuloUnchecked index k)))))
            (constructor StdList StdListEmpty (family LogicalInterval))
            (stdListNaturalsBelow count))))))

-- A partition of `ordinal` when it holds any interval.
def dpotPart =
  (lambda unrestricted ordinal : Nat .
    (lambda unrestricted intervals : (family StdList (family LogicalInterval)) .
      (lambda unrestricted rest : (family StdList (family CheckpointRegionPartition)) .
        (nat-eliminate
          (lambda unrestricted empty : Nat . (family StdList (family CheckpointRegionPartition)))
          (constructor
            StdList
            StdListCons
            (family CheckpointRegionPartition)
            (constructor CheckpointRegionPartition CheckpointRegionPartitionOf ordinal intervals)
            rest)
          (lambda unrestricted previous : Nat .
            (lambda unrestricted ignored : (family StdList (family CheckpointRegionPartition)) .
              rest))
          (naturalIsZero (stdListLength (family LogicalInterval) intervals))))))

def dpotWhole =
  (lambda unrestricted held : Nat .
    (lambda unrestricted bytes : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family StdList (family LogicalInterval)))
        (constructor StdList StdListEmpty (family LogicalInterval))
        (lambda unrestricted previous : Nat .
          (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
            (constructor
              StdList
              StdListCons
              (family LogicalInterval)
              (dpoInterval 0 bytes)
              (constructor StdList StdListEmpty (family LogicalInterval)))))
        held)))

-- The replicated words the root alone publishes: the parameters when they
-- are replicated, then the shared state.
def dpotReplicatedOf =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (let unrestricted shared =
              (dpoShared c u system q)
              in
              (dpotPart
                0
                (dpotWhole (naturalIsZero p) (dpParameterBytes c u system))
                (dpotPart
                  dpoSharedOrdinal
                  (dpotWhole (naturalNonzero shared) (naturalMultiply dpWord shared))
                  (constructor StdList StdListEmpty (family CheckpointRegionPartition))))))))))

-- A role's own partitions, in region order: its parameter words (all of them
-- at the root when replicated), the shared state at the root, its
-- coordinates' optimizer-state words.
def dpotOwnOf =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (lambda unrestricted role : Nat .
              (let unrestricted k =
                (dpK c u system)
                in
                (let unrestricted owners =
                  (dpOwners c u system)
                  in
                  (let unrestricted shared =
                    (dpoShared c u system q)
                    in
                    (let unrestricted root =
                      (naturalIsZero role)
                      in
                      (dpotPart
                        0
                        (nat-eliminate
                          (lambda unrestricted current : Nat .
                            (family StdList (family LogicalInterval)))
                          (dpotWhole root (dpParameterBytes c u system))
                          (lambda unrestricted previous : Nat .
                            (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
                              (dpotOwnedWords k owners role k)))
                          p)
                        (dpotPart
                          dpoSharedOrdinal
                          (dpotWhole
                            (naturalAnd root (naturalNonzero shared))
                            (naturalMultiply dpWord shared))
                          (dpotPart
                            (dpoCoordinateOrdinal shared)
                            (dpotOwnedWords k owners role (naturalMultiply q k))
                            (constructor StdList StdListEmpty (family CheckpointRegionPartition)))))))))))))))

-- The global shard number of a word (dpoPartitions' order: parameters, one
-- per word when partitioned; shared state; coordinate words), which names
-- its file.
def dpotGlobalOf =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (lambda unrestricted ordinal : Nat .
              (lambda unrestricted begin : Nat .
                (let unrestricted shared =
                  (dpoShared c u system q)
                  in
                  (let unrestricted word =
                    (naturalDivideUnchecked begin dpWord)
                    in
                    (let unrestricted parameters =
                      (naturalSelect p (dpK c u system) 1)
                      in
                      (naturalSelect
                        (naturalIsZero ordinal)
                        (naturalSelect p word 0)
                        (naturalSelect
                          (naturalEqual ordinal (dpoCoordinateOrdinal shared))
                          (naturalAdd (naturalAdd parameters (naturalNonzero shared)) word)
                          parameters))))))))))))

-- The global shard numbers of a role's own shards, in its record order.
def dpotOwnGlobals =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (lambda unrestricted role : Nat .
              (stdListFold
                (family CheckpointRegionPartition)
                (family StdList Nat)
                (lambda unrestricted part : (family CheckpointRegionPartition) .
                  (lambda unrestricted rest : (family StdList Nat) .
                    (stdListAppend
                      Nat
                      (stdListMap
                        (family LogicalInterval)
                        Nat
                        (lambda unrestricted interval : (family LogicalInterval) .
                          (dpotGlobalOf
                            c
                            u
                            system
                            q
                            p
                            (checkpointPartitionOrdinal part)
                            (intervalBegin interval)))
                        (checkpointPartitionIntervals part))
                      rest)))
                (constructor StdList StdListEmpty Nat)
                (dpotOwnOf c u system q p role))))))))

def dpotNth =
  (lambda unrestricted values : (family StdList Nat) .
    (lambda unrestricted index : Nat . (stdListHeadOr Nat 0 (stdListDrop Nat index values))))

-- argv for n owners and h global shards, positions after the program name:
-- 1 the previous root manifest; 1 + r the previous group manifest of role
-- r >= 1; n + 1 + g the previous shard g; n + 1 + h + 2r and n + 2 + h + 2r
-- the candidate and committed group manifest of role r (role 0's is the
-- published root); 3n + 1 + h + 2g and 3n + 2 + h + 2g the candidate and
-- committed shard g; 3n + 1 + 3h the generation directory. Every owner
-- receives the same argv; a role's own shard j is the global shard its
-- record names.
def dpotPaths =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (lambda unrestricted role : Nat .
              (let unrestricted owners =
                (dpOwners c u system)
                in
                (let unrestricted shards =
                  (dpoShardCount c u system q p)
                  in
                  (let unrestricted groups =
                    (naturalAdd (succ owners) shards)
                    in
                    (let unrestricted outputs =
                      (naturalAdd (succ (naturalMultiply 3 owners)) shards)
                      in
                      (let unrestricted globals =
                        (dpotOwnGlobals c u system q p role)
                        in
                        (constructor
                          NativeTreePaths
                          NativeTreePathsOf
                          (lambda unrestricted at : Nat . (succ at))
                          (lambda unrestricted index : Nat .
                            (succ (naturalAdd owners (dpotNth globals index))))
                          (naturalAdd groups (naturalMultiply 2 role))
                          (succ (naturalAdd groups (naturalMultiply 2 role)))
                          (lambda unrestricted index : Nat .
                            (naturalAdd outputs (naturalMultiply 2 (dpotNth globals index))))
                          (lambda unrestricted index : Nat .
                            (succ (naturalAdd outputs (naturalMultiply 2 (dpotNth globals index)))))
                          (naturalAdd (succ (naturalMultiply 3 owners)) (naturalMultiply 3 shards))))))))))))))

-- ---- publication frames ----
def dpotIdentity =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted digest : Bytes .
          (lambda unrestricted q : Nat .
            (lambda unrestricted p : Nat .
              (lambda unrestricted operation : Nat .
                (lambda unrestricted sender : Nat .
                  (lambda unrestricted receiver : Nat .
                    (constructor
                      RegionTransferIdentity
                      RegionTransferIdentityOf
                      digest
                      b"data-parallel-owned-tree-publication-v1"
                      b"replicated-words"
                      b"finite-f64-rne-separate"
                      (constructor LearningRound LearningRoundOf 1 0)
                      operation
                      sender
                      receiver
                      (constructor
                        LogicalInterval
                        LogicalIntervalOf
                        0
                        (dpoAgreedBytes c u system q p))))))))))))

def dpotParent =
  (lambda unrestricted fanout : Nat .
    (lambda unrestricted count : Nat .
      (lambda unrestricted role : Nat .
        (participantTreeParentOf (participantTreeNode fanout count role)))))

def dpotCommitmentBytes =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (nativeTreeCommitmentBytesOf (dpoAgreedBytes c u system q p)))))))

def dpotCommitmentFor =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted digest : Bytes .
          (lambda unrestricted q : Nat .
            (lambda unrestricted p : Nat .
              (lambda unrestricted fanout : Nat .
                (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
                  (lambda unrestricted child : Nat .
                    (niFrameAt
                      (dpotIdentity
                        c
                        u
                        system
                        digest
                        q
                        p
                        2
                        child
                        (dpotParent fanout (dpOwners c u system) child))
                      (dpotCommitmentBytes c u system q p)
                      (dpotCommitment tree)))))))))))

def dpotReleaseFor =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted digest : Bytes .
          (lambda unrestricted q : Nat .
            (lambda unrestricted p : Nat .
              (lambda unrestricted fanout : Nat .
                (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
                  (lambda unrestricted child : Nat .
                    (niFrameAt
                      (dpotIdentity
                        c
                        u
                        system
                        digest
                        q
                        p
                        3
                        (dpotParent fanout (dpOwners c u system) child)
                        child)
                      dpWord
                      (dpotRelease tree)))))))))))

-- ---- 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.
def dpotPlanRootShards =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted identity : Bytes .
          (lambda unrestricted q : Nat .
            (lambda unrestricted p : Nat .
              (lambda unrestricted fanout : Nat .
                (lambda unrestricted role : Nat .
                  (lambda unrestricted checkpoint : (family NativeTreeCheckpoint) .
                    (lambda unrestricted available : Nat .
                      (let unrestricted base =
                        (nativeCheckpointAlign (nativeTreeEnd checkpoint))
                        in
                        (nat-eliminate
                          (lambda unrestricted current : Nat .
                            (family
                              StdResult
                              (family NativeCheckpointFailure)
                              (family NativeRegionCheckpoint)))
                          (constructor
                            StdResult
                            StdSuccess
                            (family NativeCheckpointFailure)
                            (family NativeRegionCheckpoint)
                            (constructor
                              NativeRegionCheckpoint
                              NativeRegionCheckpointOf
                              (nativeTreeGroup checkpoint)
                              (constructor StdList StdListEmpty (family NativeRegionShard))
                              (nativeTreeEpoch checkpoint)
                              base))
                          (lambda unrestricted previous : Nat .
                            (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
                              (planNativeTreeRootShards
                                (dpoContext c u system q p (dpotTopology fanout) identity)
                                (dpoRegions c u system q)
                                (lambda unrestricted owner : Nat .
                                  (dpotReplicatedOf c u system q p))
                                checkpoint
                                base
                                available)))
                          (naturalAnd
                            (naturalNonzero role)
                            (naturalNonzero
                              (stdListLength
                                (family CheckpointRegionPartition)
                                (dpotReplicatedOf c u system q p))))))))))))))))

-- The root's record number of its first replicated shard: they follow its
-- own parameter words when parameters are partitioned.
def dpotReplicatedFirst =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted p : Nat .
          (naturalMultiply
            p
            (stdListLength
              (family LogicalInterval)
              (dpotOwnedWords (dpK c u system) (dpOwners c u system) 0 (dpK c u system))))))))

-- Combine storage (the sum, the assembly, this owner's offer and read
-- replica), then the edge frames, the tree checkpoint and the root's
-- replicated shard layouts, then the owner state.
def dpotWithLayout =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (lambda unrestricted g : Nat .
              (lambda unrestricted fanout : Nat .
                (lambda unrestricted role : Nat .
                  (lambda unrestricted epoch : Nat .
                    (lambda unrestricted available : Nat .
                      (lambda unrestricted emit : (pi unrestricted layout : (family NativeDataParallelOwnedLayout) . (pi unrestricted tree : (family NativeDataParallelOwnedTreeLayout) . Bytes)) .
                        (let unrestricted digest =
                          (dpIdentityDigest c u system)
                          in
                          (let unrestricted contextDigest =
                            (dpoContextDigest c u system p digest)
                            in
                            (let unrestricted sum =
                              (dpPlacementFor c u system digest (dpotTopology fanout) role)
                              in
                              (let unrestricted assemble =
                                (dpoAssemblePlacementFor
                                  c
                                  u
                                  system
                                  digest
                                  (dpotTopology fanout)
                                  role
                                  sum)
                                in
                                (let unrestricted gradients =
                                  (dpoGradientsFor
                                    c
                                    u
                                    system
                                    g
                                    digest
                                    (dpotTopology fanout)
                                    role
                                    (dpoPublicationStart c u system p assemble))
                                  in
                                  (eliminate
                                    StdResult
                                    (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
                                      Bytes)
                                    (planRegionFrameLayout
                                      (dpotIdentity c u system digest q p 2 1 0)
                                      (dpotCommitmentBytes c u system q p)
                                      512
                                      (dpoGradientsEnd
                                        c
                                        u
                                        system
                                        gradients
                                        (dpoPublicationStart c u system p assemble))
                                      available)
                                    (branch StdFailure error . b"")
                                    (branch
                                      StdSuccess
                                      commitment
                                      .
                                      (eliminate
                                        StdResult
                                        (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
                                        Bytes)
                                        (planRegionFrameLayout
                                        (dpotIdentity c u system digest q p 3 0 1)
                                        dpWord
                                        512
                                        (frameAlign (frameEnd commitment))
                                        available)
                                        (branch StdFailure error . b"")
                                        (branch
                                        StdSuccess
                                        release
                                        .
                                        (eliminate
                                        StdResult
                                        (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)) .
                                        Bytes)
                                        (planNativeTreeCheckpoint
                                        (dpoContext
                                        c
                                        u
                                        system
                                        q
                                        p
                                        (dpotTopology fanout)
                                        contextDigest)
                                        (dpoRegions c u system q)
                                        fanout
                                        (dpOwners c u system)
                                        role
                                        (dpotOwnOf c u system q p)
                                        epoch
                                        (frameAlign (frameEnd release))
                                        available)
                                        (branch StdFailure error . b"")
                                        (branch
                                        StdSuccess
                                        checkpoint
                                        .
                                        (eliminate
                                        StdResult
                                        (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
                                        Bytes)
                                        (dpotPlanRootShards
                                        c
                                        u
                                        system
                                        contextDigest
                                        q
                                        p
                                        fanout
                                        role
                                        checkpoint
                                        available)
                                        (branch StdFailure error . b"")
                                        (branch
                                        StdSuccess
                                        root
                                        .
                                        (emit
                                        (constructor
                                        NativeDataParallelOwnedLayout
                                        NativeDataParallelOwnedLayoutOf
                                        sum
                                        assemble
                                        (nativeCheckpointAlign (nativeRegionEnd root))
                                        (nativeTreeEpoch checkpoint)
                                        digest
                                        gradients)
                                        (constructor
                                        NativeDataParallelOwnedTreeLayout
                                        NativeDataParallelOwnedTreeLayoutOf
                                        commitment
                                        release
                                        checkpoint
                                        root))))))))))))))))))))))))))

-- ---- start, publication ----
-- Fresh: the declared words. Resume: the verified manifest path, this
-- owner's own shards and, below the root, the root's replicated shards, then
-- the restored prefix and a new membership epoch.
def dpotStart =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
              (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
                (lambda unrestricted fanout : Nat .
                  (lambda unrestricted role : Nat .
                    (lambda unrestricted resume : Nat .
                      (lambda unrestricted tail : (family NativePhysicalCommands) .
                        (let unrestricted checkpoint =
                          (dpotCheckpoint tree)
                          in
                          (let unrestricted owners =
                            (dpOwners c u system)
                            in
                            (let unrestricted destination =
                              (lambda unrestricted shard : (family NativeRegionShard) .
                                (naturalAdd
                                  (dpoStateAt layout)
                                  (dpoShardOffset c u system q p shard)))
                              in
                              (let unrestricted rootGlobals =
                                (dpotOwnGlobals c u system q p 0)
                                in
                                (constructor
                                  StdResult
                                  StdSuccess
                                  (family NativeCheckpointFailure)
                                  (family NativePhysicalCommands)
                                  (nat-eliminate
                                    (lambda unrestricted mode : Nat .
                                      (family NativePhysicalCommands))
                                    (dpoFresh c u system q p layout role tail)
                                    (lambda unrestricted previous : Nat .
                                      (lambda unrestricted ignored : (family NativePhysicalCommands) .
                                        (nativeTreeRestoreManifests
                                        checkpoint
                                        fanout
                                        owners
                                        role
                                        (dpotOwnOf c u system q p)
                                        (dpotPaths c u system q p role)
                                        (nativeTreeRestoreOwn
                                        checkpoint
                                        (dpotPaths c u system q p role)
                                        destination
                                        (nativeTreeRestoreShardsFrom
                                        (nativeTreeRootLayout checkpoint)
                                        (dpotReplicatedFirst c u system p)
                                        (nativeRegionShards (dpotRootShards tree))
                                        (lambda unrestricted index : Nat .
                                        (succ (naturalAdd owners (dpotNth rootGlobals index))))
                                        destination
                                        (dpResumed
                                        (dpoGeneric layout)
                                        (nativeTreeRestoredCaptureAt checkpoint)
                                        tail))))))
                                    resume)))))))))))))))))

-- Every edge's frames share the template's storage exactly.
def dpotFramesAdmitted =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted digest : Bytes .
          (lambda unrestricted q : Nat .
            (lambda unrestricted p : Nat .
              (lambda unrestricted fanout : Nat .
                (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
                  (stdListFold
                    Nat
                    Nat
                    (lambda unrestricted index : Nat .
                      (lambda unrestricted rest : Nat .
                        (naturalAnd
                          rest
                          (naturalAnd
                            (naturalEqual
                              (frameEnd
                                (dpotCommitmentFor c u system digest q p fanout tree (succ index)))
                              (frameEnd (dpotCommitment tree)))
                            (naturalEqual
                              (frameEnd
                                (dpotReleaseFor c u system digest q p fanout tree (succ index)))
                              (frameEnd (dpotRelease tree)))))))
                    1
                    (stdListNaturalsBelow (naturalPredecessor (dpOwners c u system))))))))))))

-- 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.
def dpotPublish =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
              (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
                (lambda unrestricted fanout : Nat .
                  (lambda unrestricted role : Nat .
                    (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
                      (lambda unrestricted resume : Nat .
                        (lambda unrestricted success : (family NativePhysicalCommands) .
                          (nat-eliminate
                            (lambda unrestricted valid : Nat .
                              (family
                                StdResult
                                (family NativeCheckpointFailure)
                                (family NativePhysicalCommands)))
                            (constructor
                              StdResult
                              StdFailure
                              (family NativeCheckpointFailure)
                              (family NativePhysicalCommands)
                              (constructor NativeCheckpointFailure NativeCheckpointBounds))
                            (lambda unrestricted previous : Nat .
                              (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
                                (constructor
                                  StdResult
                                  StdSuccess
                                  (family NativeCheckpointFailure)
                                  (family NativePhysicalCommands)
                                  (nativeTreePublish
                                    (nativeTreeCheckpointAdvanced (dpotCheckpoint tree) resume)
                                    fanout
                                    (dpOwners c u system)
                                    role
                                    edges
                                    (dpotCommitmentFor
                                      c
                                      u
                                      system
                                      (dpoDigest layout)
                                      q
                                      p
                                      fanout
                                      tree)
                                    (dpotReleaseFor c u system (dpoDigest layout) q p fanout tree)
                                    (dpoStateAt layout)
                                    (dpoAgreedBytes c u system q p)
                                    (dpoShardOffset c u system q p)
                                    (dpotPaths c u system q p role)
                                    success))))
                            (dpotFramesAdmitted c u system (dpoDigest layout) q p fanout tree))))))))))))))

-- The publication's arena: both frame templates, the tree checkpoint's
-- staging and, below the root, the root's replicated shard layouts.
def dpotResidents =
  (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
    (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
      (let unrestricted staged =
        (nativeTreeResidents (dpotCheckpoint tree))
        in
        (let unrestricted rootBase =
          (nativeCheckpointAlign (nativeTreeEnd (dpotCheckpoint tree)))
          in
          (let unrestricted rootBytes =
            (naturalSaturatingSubtract (nativeRegionEnd (dpotRootShards tree)) rootBase)
            in
            (constructor
              ArenaResidents
              ArenaResidentsNext
              (constructor
                ArenaResident
                ArenaResidentValue
                b"tree-commitment-frame"
                (frameBase (dpotCommitment tree))
                (naturalSaturatingSubtract
                  (frameEnd (dpotCommitment tree))
                  (frameBase (dpotCommitment tree)))
                1)
              (constructor
                ArenaResidents
                ArenaResidentsNext
                (constructor
                  ArenaResident
                  ArenaResidentValue
                  b"tree-release-frame"
                  (frameBase (dpotRelease tree))
                  (naturalSaturatingSubtract
                    (frameEnd (dpotRelease tree))
                    (frameBase (dpotRelease tree)))
                  1)
                (nat-eliminate
                  (lambda unrestricted current : Nat . (family ArenaResidents))
                  staged
                  (lambda unrestricted previous : Nat .
                    (lambda unrestricted ignored : (family ArenaResidents) .
                      (constructor
                        ArenaResidents
                        ArenaResidentsNext
                        (constructor
                          ArenaResident
                          ArenaResidentValue
                          b"tree-root-shards"
                          rootBase
                          rootBytes
                          nativeCheckpointWordBytes)
                        staged)))
                  (naturalNonzero rootBytes)))))))))

def dpotRunAdmitted =
  (lambda unrestricted c : Nat .
    (lambda unrestricted u : Nat .
      (lambda unrestricted system : (family DataParallelSystem c u) .
        (lambda unrestricted q : Nat .
          (lambda unrestricted p : Nat .
            (lambda unrestricted g : Nat .
              (lambda unrestricted fanout : Nat .
                (lambda unrestricted role : Nat .
                  (lambda unrestricted addresses : (family StdList Bytes) .
                    (lambda unrestricted resume : Nat .
                      (lambda unrestricted epoch : Nat .
                        (lambda unrestricted steps : Nat .
                          (naturalAnd
                            (dataParallelAdmitted c u system)
                            (naturalAnd
                              (nativePeerTreeListedAdmitted
                                fanout
                                (dpOwners c u system)
                                role
                                addresses)
                              (naturalAnd
                                (naturalLessOrEqual resume 1)
                                (naturalAnd
                                  (naturalNonzero epoch)
                                  (naturalAnd
                                    (naturalBelowTwoPower 64 (naturalAdd epoch resume))
                                    (naturalAnd
                                      (naturalNonzero steps)
                                      (naturalAnd
                                        (naturalBelowTwoPower 64 steps)
                                        (naturalAnd
                                        (naturalAnd
                                        (naturalLessOrEqual p 1)
                                        (naturalLessOrEqual g 1))
                                        (dataParallelSeparable c u system q)))))))))))))))))))))

-- One owner of the hierarchy, for `target`.
def nativeDataParallelOwnedTreeArtifact =
  (lambda unrestricted target : (family NativeHostTarget) .
    (lambda unrestricted resources : (family NativeResourceContext) .
      (lambda unrestricted c : Nat .
        (lambda unrestricted u : Nat .
          (lambda unrestricted system : (family DataParallelSystem c u) .
            (lambda unrestricted q : Nat .
              (lambda unrestricted p : Nat .
                (lambda unrestricted g : Nat .
                  (lambda unrestricted fanout : Nat .
                    (lambda unrestricted role : Nat .
                      (lambda unrestricted addresses : (family StdList Bytes) .
                        (lambda unrestricted resume : Nat .
                          (lambda unrestricted epoch : Nat .
                            (lambda unrestricted steps : Nat .
                              (lambda unrestricted available : Nat .
                                (let unrestricted edges =
                                  (nativePeerTreeEdgesListed
                                    fanout
                                    (dpOwners c u system)
                                    role
                                    addresses)
                                  in
                                  (nat-eliminate
                                    (lambda unrestricted valid : Nat . Bytes)
                                    b""
                                    (lambda unrestricted previous : Nat .
                                      (lambda unrestricted ignored : Bytes .
                                        (dpotWithLayout
                                        c
                                        u
                                        system
                                        q
                                        p
                                        g
                                        fanout
                                        role
                                        epoch
                                        available
                                        (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
                                        (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
                                        (dpoEmitWith
                                        target
                                        resources
                                        c
                                        u
                                        system
                                        q
                                        p
                                        (dpotTopology fanout)
                                        layout
                                        role
                                        edges
                                        steps
                                        available
                                        (lambda unrestricted extent : Nat .
                                        (lambda unrestricted tail : (family NativePhysicalCommands) .
                                        (dpotStart
                                        c
                                        u
                                        system
                                        q
                                        p
                                        layout
                                        tree
                                        fanout
                                        role
                                        resume
                                        tail)))
                                        (lambda unrestricted extent : Nat .
                                        (lambda unrestricted success : (family NativePhysicalCommands) .
                                        (dpotPublish
                                        c
                                        u
                                        system
                                        q
                                        p
                                        layout
                                        tree
                                        fanout
                                        role
                                        edges
                                        resume
                                        success)))
                                        (dpotResidents layout tree)))))))
                                    (dpotRunAdmitted
                                      c
                                      u
                                      system
                                      q
                                      p
                                      g
                                      fanout
                                      role
                                      addresses
                                      resume
                                      epoch
                                      steps))))))))))))))))))