module Runtime.NativeCombine

import Runtime.OrderedCombine
import Compiler.Planning.OrderedCombine
import Runtime.Protocol
import Compiler.Planning.Protocol
import Runtime.NativeProtocol
import Runtime.RegionTransfer
import Runtime.RegionFrame
import Compiler.Planning.RegionFrame
import Runtime.NativeRegionFrame
import Runtime.NativePeerEndpoint
import Runtime.NativeMemoryPlan
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativePhysicalProgram
import Runtime.ArenaCertificate
import Representation.ParticipantTree
import Learning.Numerics
import Data.Bytes
import Std.Foundation
import Std.List
import Std.Natural

-- The native realization of an ordered combine and replication
-- (Runtime.OrderedCombine, Compiler.Planning.OrderedCombine) for one role.
--
-- The caller supplies the numerical tree, its anchor, the payload extent of
-- one value, where in the arena the combine lives, the leaf value's address,
-- the arithmetic that combines two values (`apply out left right`) and the
-- descriptor of each peer's connection. This owner supplies everything that
-- follows from the tree: the reduce and replicate global protocol and this
-- role's projection, one frame per payload identity the role exchanges, the
-- address of every logical reference the role holds, and the local and
-- transfer commands. After the projected protocol runs, the role's leaf
-- reference holds the replicated root value.
--
-- Placement: `base` begins the frames (one stride per payload identity, in
-- the projection's payload order), then the role's local value slots in
-- combineLocalSlots order. A reference the role does not hold maps to the
-- end of that region, outside every admitted resident, so admission refuses
-- it. Sharing: the global protocol, its projection and the payload list are
-- computed once per context and reused for every frame lookup, because
-- rebuilding them per address repeats hashing and traversal.
family NativeCombineContext : Type 0
constructor NativeCombineContextOf
field unrestricted nativeCombineRoleValue : Nat
field unrestricted nativeCombineTreeValue : (family OrderedCombineTree)
field unrestricted nativeCombineDigestValue : Bytes
field unrestricted nativeCombineAnchorValue : (family RegionTransferIdentity)
field unrestricted nativeCombineGlobalValue : (family GlobalProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision))
field unrestricted nativeCombineProjectedValue : (family ParticipantProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision))
field unrestricted nativeCombinePayloadsValue : (family StdList (family RegionTransferIdentity))

end-family

family NativeCombinePlacement : Type 0
constructor NativeCombinePlacementOf
field unrestricted nativeCombineContextValue : (family NativeCombineContext)
field unrestricted nativeCombineBaseValue : Nat
field unrestricted nativeCombineValueBytes : Nat

end-family

def nativeCombineRole =
  (lambda unrestricted context : (family NativeCombineContext) .
    (eliminate
      NativeCombineContext
      (lambda unrestricted current : (family NativeCombineContext) . Nat)
      context
      (branch NativeCombineContextOf role tree digest anchor global projected payloads . role)))

def nativeCombineTree =
  (lambda unrestricted context : (family NativeCombineContext) .
    (eliminate
      NativeCombineContext
      (lambda unrestricted current : (family NativeCombineContext) . (family OrderedCombineTree))
      context
      (branch NativeCombineContextOf role tree digest anchor global projected payloads . tree)))

def nativeCombineDigest =
  (lambda unrestricted context : (family NativeCombineContext) .
    (eliminate
      NativeCombineContext
      (lambda unrestricted current : (family NativeCombineContext) . Bytes)
      context
      (branch NativeCombineContextOf role tree digest anchor global projected payloads . digest)))

def nativeCombineAnchor =
  (lambda unrestricted context : (family NativeCombineContext) .
    (eliminate
      NativeCombineContext
      (lambda unrestricted current : (family NativeCombineContext) .
        (family RegionTransferIdentity))
      context
      (branch NativeCombineContextOf role tree digest anchor global projected payloads . anchor)))

def nativeCombineGlobal =
  (lambda unrestricted context : (family NativeCombineContext) .
    (eliminate
      NativeCombineContext
      (lambda unrestricted current : (family NativeCombineContext) .
        (family
          GlobalProtocol
          (family OrderedCombineOperation (family RegionTransferIdentity))
          (family RegionTransferIdentity)
          (family ProtocolNoDecision)))
      context
      (branch NativeCombineContextOf role tree digest anchor global projected payloads . global)))

def nativeCombineProjected =
  (lambda unrestricted context : (family NativeCombineContext) .
    (eliminate
      NativeCombineContext
      (lambda unrestricted current : (family NativeCombineContext) .
        (family
          ParticipantProtocol
          (family OrderedCombineOperation (family RegionTransferIdentity))
          (family RegionTransferIdentity)
          (family ProtocolNoDecision)))
      context
      (branch NativeCombineContextOf role tree digest anchor global projected payloads . projected)))

def nativeCombinePayloads =
  (lambda unrestricted context : (family NativeCombineContext) .
    (eliminate
      NativeCombineContext
      (lambda unrestricted current : (family NativeCombineContext) .
        (family StdList (family RegionTransferIdentity)))
      context
      (branch NativeCombineContextOf role tree digest anchor global projected payloads . payloads)))

def nativeCombinePlacementContext =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (eliminate
      NativeCombinePlacement
      (lambda unrestricted current : (family NativeCombinePlacement) .
        (family NativeCombineContext))
      placement
      (branch NativeCombinePlacementOf context base bytes . context)))

def nativeCombineBase =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (eliminate
      NativeCombinePlacement
      (lambda unrestricted current : (family NativeCombinePlacement) . Nat)
      placement
      (branch NativeCombinePlacementOf context base bytes . base)))

def nativeCombineBytes =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (eliminate
      NativeCombinePlacement
      (lambda unrestricted current : (family NativeCombinePlacement) . Nat)
      placement
      (branch NativeCombinePlacementOf context base bytes . bytes)))

-- A transfer's payload is its canonical identity; the frame is found by it.
def nativeCombineBinding =
  (lambda unrestricted stage : (family CombineStage) .
    (lambda unrestricted source : (family CombineReference) .
      (lambda unrestricted destination : (family CombineReference) .
        (lambda unrestricted identity : (family RegionTransferIdentity) . identity))))

def nativeCombineEnd =
  (constructor
    GlobalProtocol
    GlobalProtocolEnd
    (family OrderedCombineOperation (family RegionTransferIdentity))
    (family RegionTransferIdentity)
    (family ProtocolNoDecision))

-- Reduce the tree, then deliver the root value (to every leaf owner, or
-- along the path to one), projected for `role`.
def nativeCombineDeliveringContextFor =
  (lambda unrestricted anchor : (family RegionTransferIdentity) .
    (lambda unrestricted delivery : (family CombineDelivery) .
      (lambda unrestricted role : Nat .
        (lambda unrestricted tree : (family OrderedCombineTree) .
          (let unrestricted digest =
            (combineTreeDigest tree)
            in
            (let unrestricted global =
              (compileOrderedCombine
                (family RegionTransferIdentity)
                anchor
                digest
                nativeCombineBinding
                tree
                0
                (compileTreeDelivery
                  (family RegionTransferIdentity)
                  anchor
                  digest
                  nativeCombineBinding
                  delivery
                  tree
                  0
                  nativeCombineEnd))
              in
              (let unrestricted projected =
                (projectGlobalProtocol
                  (family OrderedCombineOperation (family RegionTransferIdentity))
                  (family RegionTransferIdentity)
                  (family ProtocolNoDecision)
                  role
                  global)
                in
                (constructor
                  NativeCombineContext
                  NativeCombineContextOf
                  role
                  tree
                  digest
                  anchor
                  global
                  projected
                  (participantProtocolPayloads
                    (family OrderedCombineOperation (family RegionTransferIdentity))
                    (family RegionTransferIdentity)
                    (family ProtocolNoDecision)
                    projected)))))))))

-- Reduce then replicate the tree, projected for `role`.
def nativeCombineContextFor =
  (lambda unrestricted anchor : (family RegionTransferIdentity) .
    (nativeCombineDeliveringContextFor anchor (constructor CombineDelivery CombineReplicateAll)))

-- The same tree and global protocol, projected for another role (admission
-- checks both ends of every transfer).
def nativeCombineForRole =
  (lambda unrestricted context : (family NativeCombineContext) .
    (lambda unrestricted role : Nat .
      (nat-eliminate
        (lambda unrestricted flag : Nat . (family NativeCombineContext))
        (let unrestricted projected =
          (projectGlobalProtocol
            (family OrderedCombineOperation (family RegionTransferIdentity))
            (family RegionTransferIdentity)
            (family ProtocolNoDecision)
            role
            (nativeCombineGlobal context))
          in
          (constructor
            NativeCombineContext
            NativeCombineContextOf
            role
            (nativeCombineTree context)
            (nativeCombineDigest context)
            (nativeCombineAnchor context)
            (nativeCombineGlobal context)
            projected
            (participantProtocolPayloads
              (family OrderedCombineOperation (family RegionTransferIdentity))
              (family RegionTransferIdentity)
              (family ProtocolNoDecision)
              projected)))
        (lambda unrestricted prior : Nat .
          (lambda unrestricted ignored : (family NativeCombineContext) . context))
        (naturalEqual role (nativeCombineRole context)))))

def nativeCombineForPlacementRole =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted role : Nat .
      (constructor
        NativeCombinePlacement
        NativeCombinePlacementOf
        (nativeCombineForRole (nativeCombinePlacementContext placement) role)
        (nativeCombineBase placement)
        (nativeCombineBytes placement))))

-- One frame per payload identity, laid out at a common stride: identities of
-- one tree have the same canonical shape, so one prototype sizes them all.
def nativeCombinePrototype =
  (lambda unrestricted context : (family NativeCombineContext) .
    (combineTransferIdentity
      (nativeCombineAnchor context)
      (nativeCombineDigest context)
      (constructor CombineStage CombineReduce)
      (combineReference 0 0 0)
      (combineReference 1 2 1)))

def nativeCombineLayoutAt =
  (lambda unrestricted bytes : Nat .
    (lambda unrestricted identity : (family RegionTransferIdentity) .
      (lambda unrestricted base : Nat .
        (stdResultValueOr
          (family RegionFrameLayoutFailure)
          (family RegionFrameLayout)
          (constructor RegionFrameLayout RegionFrameLayoutOf b"" 0 0 b"")
          (planRegionFrameLayout identity bytes 512 base 1073741824)))))

def nativeCombineStride =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (frameAlign
      (frameEnd
        (nativeCombineLayoutAt
          (nativeCombineBytes placement)
          (nativeCombinePrototype (nativeCombinePlacementContext placement))
          0))))

def nativeCombineFrameCount =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (stdListLength
      (family RegionTransferIdentity)
      (nativeCombinePayloads (nativeCombinePlacementContext placement))))

def nativeCombineFrameIndex =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted identity : (family RegionTransferIdentity) .
      (app
        (eliminate
          StdList
          (lambda unrestricted current : (family StdList (family RegionTransferIdentity)) .
            (pi unrestricted index : Nat . Nat))
          (nativeCombinePayloads (nativeCombinePlacementContext placement))
          (branch StdListEmpty . (lambda unrestricted index : Nat . index))
          (branch
            StdListCons
            head
            rest
            induction
            .
            (lambda unrestricted index : Nat .
              (nat-eliminate
                (lambda unrestricted flag : Nat . Nat)
                (induction (naturalAdd index 1))
                (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . index))
                (regionTransferIdentityEqual identity head)))))
        0)))

def nativeCombineFrame =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted identity : (family RegionTransferIdentity) .
      (nativeCombineLayoutAt
        (nativeCombineBytes placement)
        identity
        (naturalAdd
          (nativeCombineBase placement)
          (naturalMultiply
            (nativeCombineStride placement)
            (nativeCombineFrameIndex placement identity))))))

def nativeCombineValuesAt =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (naturalAdd
      (nativeCombineBase placement)
      (naturalMultiply (nativeCombineStride placement) (nativeCombineFrameCount placement))))

def nativeCombineRegionEnd =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (naturalAdd
      (nativeCombineValuesAt placement)
      (naturalMultiply
        (nativeCombineBytes placement)
        (stdListLength
          Nat
          (combineLocalSlots
            (nativeCombineRole (nativeCombinePlacementContext placement))
            (nativeCombineTree (nativeCombinePlacementContext placement)))))))

def nativeCombineAddress =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted reference : (family CombineReference) .
      (eliminate
        StdOption
        (lambda unrestricted current : (family StdOption Nat) . Nat)
        (combineReferenceIndex
          (nativeCombineRole (nativeCombinePlacementContext placement))
          (nativeCombineTree (nativeCombinePlacementContext placement))
          reference)
        (branch StdNone . (nativeCombineRegionEnd placement))
        (branch
          StdSome
          index
          .
          (naturalAdd
            (nativeCombineValuesAt placement)
            (naturalMultiply (nativeCombineBytes placement) index))))))

def nativeCombineReferenceValid =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted reference : (family CombineReference) .
      (naturalLess (nativeCombineAddress placement reference) (nativeCombineRegionEnd placement))))

-- The reference holding `role`'s own leaf value: after replication it holds
-- the root value.
def nativeCombineLeafReferenceFrom =
  (lambda unrestricted role : Nat .
    (lambda unrestricted tree : (family OrderedCombineTree) .
      (eliminate
        OrderedCombineTree
        (lambda unrestricted current : (family OrderedCombineTree) .
          (pi unrestricted base : Nat . (family CombineReference)))
        tree
        (branch
          OrderedCombineLeaf
          owner
          .
          (lambda unrestricted base : Nat . (combineReference owner base 0)))
        (branch
          OrderedCombineBranch
          owner
          left
          right
          leftResult
          rightResult
          .
          (lambda unrestricted base : Nat .
            (nat-eliminate
              (lambda unrestricted flag : Nat . (family CombineReference))
              (rightResult (naturalAdd base (combineNodeCount left)))
              (lambda unrestricted prior : Nat .
                (lambda unrestricted ignored : (family CombineReference) . (leftResult base)))
              (combineContains role (combineLeaves left))))))))

def nativeCombineResultAt =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (nativeCombineAddress
      placement
      (nativeCombineLeafReferenceFrom
        (nativeCombineRole (nativeCombinePlacementContext placement))
        (nativeCombineTree (nativeCombinePlacementContext placement))
        0)))

def nativeCombineCopy =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted source : Nat .
      (lambda unrestricted destination : Nat .
        (nativeMemoryCopyOperands
          (nativeMemoryState destination)
          (nativeMemoryState source)
          (nativeCombineBytes placement)
          0
          b"combine-copy"))))

-- Local work: the leaf reads `leafAt`; branches apply the caller's arithmetic.
def nativeCombineLocal =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted leafAt : Nat .
      (lambda unrestricted apply : (pi unrestricted out : Nat . (pi unrestricted left : Nat . (pi unrestricted right : Nat . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) .
        (lambda unrestricted operation : (family OrderedCombineOperation (family RegionTransferIdentity)) .
          (eliminate
            OrderedCombineOperation
            (lambda unrestricted current : (family OrderedCombineOperation (family RegionTransferIdentity)) .
              (pi unrestricted tail : (family NativePhysicalCommands) .
                (family NativePhysicalCommands)))
            operation
            (branch
              CombineReadLeaf
              destination
              .
              (nativeCombineCopy placement leafAt (nativeCombineAddress placement destination)))
            (branch
              CombineCopy
              source
              destination
              .
              (nativeCombineCopy
                placement
                (nativeCombineAddress placement source)
                (nativeCombineAddress placement destination)))
            (branch
              CombineApply
              left
              right
              destination
              .
              (apply
                (nativeCombineAddress placement destination)
                (nativeCombineAddress placement left)
                (nativeCombineAddress placement right)))
            (branch
              CombinePrepare
              source
              identity
              .
              (nativeCombineCopy
                placement
                (nativeCombineAddress placement source)
                (framePayloadAt (nativeCombineFrame placement identity))))
            (branch
              CombineConsume
              identity
              destination
              .
              (lambda unrestricted tail : (family NativePhysicalCommands) .
                (let unrestricted frame =
                  (nativeCombineFrame placement identity)
                  in
                  (nativeFrameConsume
                    frame
                    (nativeCombineCopy
                      placement
                      (framePayloadAt frame)
                      (nativeCombineAddress placement destination)
                      (nativeFrameAdvance
                        frame
                        (constructor NativeFrameTerminal NativeFrameConsumeComplete)
                        0
                        tail)))))))))))

def nativeCombineTransfer =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted descriptor : (pi unrestricted peer : Nat . (family NativePhysicalOperand)) .
      (lambda unrestricted direction : (family ProtocolDirection) .
        (lambda unrestricted identity : (family RegionTransferIdentity) .
          (lambda unrestricted value : (family RegionTransferIdentity) .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (let unrestricted frame =
                (nativeCombineFrame placement value)
                in
                (eliminate
                  ProtocolDirection
                  (lambda unrestricted current : (family ProtocolDirection) .
                    (family NativePhysicalCommands))
                  direction
                  (branch
                    ProtocolSend
                    .
                    (nativePeerIO
                      (descriptor (regionTransferReceiver identity))
                      1
                      frame
                      (nativeFrameAdvance
                        frame
                        (constructor NativeFrameTerminal NativeFrameSendComplete)
                        0
                        tail)))
                  (branch
                    ProtocolReceive
                    .
                    (nativePeerIO (descriptor (regionTransferSender identity)) 0 frame tail))))))))))

def nativeCombineDecisions =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (constructor
      NativeProtocolDecisionBinding
      NativeProtocolDecisionBindingOf
      (family ProtocolNoDecision)
      (family RegionTransferIdentity)
      (lambda unrestricted selector : (family ProtocolNoDecision) .
        (eliminate
          ProtocolNoDecision
          (lambda unrestricted current : (family ProtocolNoDecision) .
            (family NativePhysicalOperand))
          selector))
      (lambda unrestricted selector : (family ProtocolNoDecision) .
        (eliminate
          ProtocolNoDecision
          (lambda unrestricted current : (family ProtocolNoDecision) . Nat)
          selector))
      0
      (nativeCombineFrame placement)))

def nativeCombineInitialize =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted program : (family ParticipantProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision)) .
      (nativeProtocolFrames
        (family OrderedCombineOperation (family RegionTransferIdentity))
        (family RegionTransferIdentity)
        (family ProtocolNoDecision)
        (lambda unrestricted direction : (family ProtocolDirection) .
          (lambda unrestricted identity : (family RegionTransferIdentity) .
            (lambda unrestricted value : (family RegionTransferIdentity) .
              (nativeFrameInitialize (nativeCombineFrame placement value)))))
        program)))

-- ---- admission ----
def nativeCombineLocalAdmitted =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted role : Nat .
      (let unrestricted placement =
        (nativeCombineForPlacementRole placement role)
        in
        (lambda unrestricted operation : (family OrderedCombineOperation (family RegionTransferIdentity)) .
          (eliminate
            OrderedCombineOperation
            (lambda unrestricted current : (family OrderedCombineOperation (family RegionTransferIdentity)) .
              Nat)
            operation
            (branch
              CombineReadLeaf
              destination
              .
              (nativeCombineReferenceValid placement destination))
            (branch
              CombineCopy
              source
              destination
              .
              (naturalAnd
                (nativeCombineReferenceValid placement source)
                (nativeCombineReferenceValid placement destination)))
            (branch
              CombineApply
              left
              right
              destination
              .
              (naturalAnd
                (nativeCombineReferenceValid placement left)
                (naturalAnd
                  (nativeCombineReferenceValid placement right)
                  (nativeCombineReferenceValid placement destination))))
            (branch
              CombinePrepare
              source
              identity
              .
              (naturalAnd
                (nativeCombineReferenceValid placement source)
                (naturalLess
                  (nativeCombineFrameIndex placement identity)
                  (nativeCombineFrameCount placement))))
            (branch
              CombineConsume
              identity
              destination
              .
              (naturalAnd
                (nativeCombineReferenceValid placement destination)
                (naturalLess
                  (nativeCombineFrameIndex placement identity)
                  (nativeCombineFrameCount placement)))))))))

def nativeCombineTransferAdmitted =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted identity : (family RegionTransferIdentity) .
      (lambda unrestricted value : (family RegionTransferIdentity) .
        (let unrestricted sender =
          (nativeCombineForPlacementRole placement (regionTransferSender identity))
          in
          (let unrestricted receiver =
            (nativeCombineForPlacementRole placement (regionTransferReceiver identity))
            in
            (naturalAnd
              (regionTransferIdentityEqual identity value)
              (naturalAnd
                (naturalLess
                  (nativeCombineFrameIndex sender identity)
                  (nativeCombineFrameCount sender))
                (naturalAnd
                  (naturalLess
                    (nativeCombineFrameIndex receiver identity)
                    (nativeCombineFrameCount receiver))
                  (naturalAnd
                    (nativeProtocolFrameAdmitted identity (nativeCombineFrame sender identity))
                    (nativeProtocolFrameAdmitted identity (nativeCombineFrame receiver identity)))))))))))

-- Every frame and the local value slots of this role; `tail` continues the
-- caller's residents.
def nativeCombineResidents =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted tail : (family ArenaResidents) .
      (stdListFold
        (family RegionTransferIdentity)
        (family ArenaResidents)
        (lambda unrestricted identity : (family RegionTransferIdentity) .
          (lambda unrestricted rest : (family ArenaResidents) .
            (let unrestricted frame =
              (nativeCombineFrame placement identity)
              in
              (constructor
                ArenaResidents
                ArenaResidentsNext
                (constructor
                  ArenaResident
                  ArenaResidentValue
                  b"combine-frame"
                  (frameBase frame)
                  (naturalSaturatingSubtract (frameEnd frame) (frameBase frame))
                  8)
                rest))))
        (constructor
          ArenaResidents
          ArenaResidentsNext
          (constructor
            ArenaResident
            ArenaResidentValue
            b"combine-local-values"
            (nativeCombineValuesAt placement)
            (naturalSaturatingSubtract
              (nativeCombineRegionEnd placement)
              (nativeCombineValuesAt placement))
            8)
          tail)
        (nativeCombinePayloads (nativeCombinePlacementContext placement)))))

-- The left-deep ordered sum of leaves 0..count-1 combined at `owner`:
-- (((l0 + l1) + l2) + ...). Every transfer is between `owner` and a leaf,
-- so it runs over a star whose centre is `owner`.
def nativeCombineChain =
  (lambda unrestricted owner : Nat .
    (lambda unrestricted count : Nat .
      (stdListFold
        Nat
        (pi unrestricted acc : (family OrderedCombineTree) . (family OrderedCombineTree))
        (lambda unrestricted leaf : Nat .
          (lambda unrestricted next : (pi unrestricted acc : (family OrderedCombineTree) . (family OrderedCombineTree)) .
            (lambda unrestricted acc : (family OrderedCombineTree) .
              (next
                (constructor
                  OrderedCombineTree
                  OrderedCombineBranch
                  owner
                  acc
                  (constructor OrderedCombineTree OrderedCombineLeaf (succ leaf)))))))
        (lambda unrestricted acc : (family OrderedCombineTree) . acc)
        (stdListNaturalsBelow (naturalPredecessor count))
        (constructor OrderedCombineTree OrderedCombineLeaf 0))))

-- The ordered sum over a bounded-fan-out hierarchy
-- (Representation.ParticipantTree): a node's value is its own leaf followed
-- by each child's subtree value in role order, combined left-deep at the node:
--   S(p) = ((l_p + S(c1)) + S(c2)) + ...
-- Every transfer is between a node and one of its children, so reduction and
-- replication run over the hierarchy's edges and no participant combines
-- more than fanout + 1 values. With fan-out count - 1 it is the chain at 0.
def nativeCombineHierarchy =
  (lambda unrestricted fanout : Nat .
    (lambda unrestricted count : Nat .
      (let unrestricted subtree =
        (nat-eliminate
          (lambda unrestricted fuel : Nat .
            (pi unrestricted node : (family ParticipantTreeNode) . (family OrderedCombineTree)))
          (lambda unrestricted node : (family ParticipantTreeNode) .
            (constructor OrderedCombineTree OrderedCombineLeaf (participantTreeRoleOf node)))
          (lambda unrestricted fuel : Nat .
            (lambda unrestricted below : (pi unrestricted node : (family ParticipantTreeNode) . (family OrderedCombineTree)) .
              (lambda unrestricted node : (family ParticipantTreeNode) .
                (let unrestricted role =
                  (participantTreeRoleOf node)
                  in
                  (stdListFold
                    (family ParticipantTreeNode)
                    (pi unrestricted acc : (family OrderedCombineTree) .
                      (family OrderedCombineTree))
                    (lambda unrestricted child : (family ParticipantTreeNode) .
                      (lambda unrestricted next : (pi unrestricted acc : (family OrderedCombineTree) . (family OrderedCombineTree)) .
                        (lambda unrestricted acc : (family OrderedCombineTree) .
                          (next
                            (constructor
                              OrderedCombineTree
                              OrderedCombineBranch
                              role
                              acc
                              (below child))))))
                    (lambda unrestricted acc : (family OrderedCombineTree) . acc)
                    (participantTreeChildren fanout node)
                    (constructor OrderedCombineTree OrderedCombineLeaf role))))))
          (participantTreeFuel fanout count))
        in
        (subtree (participantTreeRoot count)))))

-- The reduce-and-deliver global protocol under an admitted numerical
-- contract, for a caller composing it into a larger round; the delivery
-- must be the placement context's.
def planNativeCombineGlobalDelivering =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted delivery : (family CombineDelivery) .
      (lambda unrestricted required : (family NumericalContract) .
        (lambda unrestricted participants : Nat .
          (lambda unrestricted members : (family CombineCoverage) .
            (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
              (planNumericalCombineAndDeliver
                (family RegionTransferIdentity)
                required
                required
                participants
                members
                baseAnchor
                nativeCombineBinding
                (nativeCombineLocalAdmitted placement)
                (nativeCombineTransferAdmitted placement)
                delivery
                (nativeCombineTree (nativeCombinePlacementContext placement))
                nativeCombineEnd)))))))

-- The reduce-and-replicate global protocol under an admitted numerical
-- contract, for a caller composing it into a larger round.
def planNativeCombineGlobal =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (planNativeCombineGlobalDelivering placement (constructor CombineDelivery CombineReplicateAll)))

-- Plan, check and project the reduce-and-replicate protocol for `rounds`
-- repetitions under an admitted numerical contract; the caller emits it with
-- nativeProtocolCommands and the callbacks above.
def planNativeCombineRounds =
  (lambda unrestricted placement : (family NativeCombinePlacement) .
    (lambda unrestricted required : (family NumericalContract) .
      (lambda unrestricted participants : Nat .
        (lambda unrestricted members : (family CombineCoverage) .
          (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
            (lambda unrestricted rounds : Nat .
              (stdResultBind
                (family OrderedCombineFailure)
                (family
                  GlobalProtocol
                  (family OrderedCombineOperation (family RegionTransferIdentity))
                  (family RegionTransferIdentity)
                  (family ProtocolNoDecision))
                (family
                  ParticipantProtocol
                  (family OrderedCombineOperation (family RegionTransferIdentity))
                  (family RegionTransferIdentity)
                  (family ProtocolNoDecision))
                (planNumericalCombineAndReplicate
                  (family RegionTransferIdentity)
                  required
                  required
                  participants
                  members
                  baseAnchor
                  nativeCombineBinding
                  (nativeCombineLocalAdmitted placement)
                  (nativeCombineTransferAdmitted placement)
                  (nativeCombineTree (nativeCombinePlacementContext placement))
                  nativeCombineEnd)
                (lambda unrestricted global : (family GlobalProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision)) .
                  (eliminate
                    StdResult
                    (lambda unrestricted result : (family StdResult (family ProtocolFailure) (family ParticipantProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision))) .
                      (family
                        StdResult
                        (family OrderedCombineFailure)
                        (family
                          ParticipantProtocol
                          (family OrderedCombineOperation (family RegionTransferIdentity))
                          (family RegionTransferIdentity)
                          (family ProtocolNoDecision))))
                    (planParticipantProtocol
                      (family OrderedCombineOperation (family RegionTransferIdentity))
                      (family RegionTransferIdentity)
                      (family ProtocolNoDecision)
                      participants
                      (nativeCombineRole (nativeCombinePlacementContext placement))
                      (nativeCombineLocalAdmitted placement)
                      (nativeCombineTransferAdmitted placement)
                      (protocolNoDecision (family RegionTransferIdentity))
                      (protocolRepeat
                        (family OrderedCombineOperation (family RegionTransferIdentity))
                        (family RegionTransferIdentity)
                        (family ProtocolNoDecision)
                        rounds
                        global
                        nativeCombineEnd))
                    (branch
                      StdFailure
                      failure
                      .
                      (constructor
                        StdResult
                        StdFailure
                        (family OrderedCombineFailure)
                        (family
                          ParticipantProtocol
                          (family OrderedCombineOperation (family RegionTransferIdentity))
                          (family RegionTransferIdentity)
                          (family ProtocolNoDecision))
                        (constructor OrderedCombineFailure CombineProtocolRefused failure)))
                    (branch
                      StdSuccess
                      projected
                      .
                      (constructor
                        StdResult
                        StdSuccess
                        (family OrderedCombineFailure)
                        (family
                          ParticipantProtocol
                          (family OrderedCombineOperation (family RegionTransferIdentity))
                          (family RegionTransferIdentity)
                          (family ProtocolNoDecision))
                        projected)))))))))))