module Compiler.Planning.OrderedCombine

import Runtime.OrderedCombine
import Representation.ParticipantGroup
import Learning.Numerics
import Runtime.Protocol
import Runtime.RegionTransfer
import Runtime.RegionFrame
import Compiler.Planning.Protocol
import Std.Foundation
import Std.List
import Std.Natural

-- Where a reduced value goes after the ordered combine: to every leaf owner
-- (replication), or only to one target owner, moved from the root down the
-- tree path to the target's leaf (a reduction to one owner, for instance a
-- coordinate's owner). Every other owner's leaf value is left as it was.
family CombineDelivery : Type 0
constructor CombineReplicateAll
constructor CombineDeliverTo
field unrestricted combineDeliveryTarget : Nat

end-family

-- Fixed, explicit trees are admitted without enumerating unrelated fleet
-- members. Duplicate checking is quadratic in the leaf count; this is not the
-- future hierarchical fleet planner. A combine runs at one of its child owners,
-- so every execution role belongs to the declared contribution set.
def combineContains =
  (lambda unrestricted role : Nat .
    (lambda unrestricted members : (family StdList Nat) .
      (eliminate
        StdList
        (lambda unrestricted current : (family StdList Nat) . Nat)
        members
        (branch StdListEmpty . 0)
        (branch StdListCons head tail induction . (naturalOr (naturalEqual role head) induction)))))

-- Whether `subtree` receives the value under `delivery`.
def combineDeliveryReaches =
  (lambda unrestricted delivery : (family CombineDelivery) .
    (lambda unrestricted subtree : (family OrderedCombineTree) .
      (eliminate
        CombineDelivery
        (lambda unrestricted current : (family CombineDelivery) . Nat)
        delivery
        (branch CombineReplicateAll . 1)
        (branch CombineDeliverTo target . (combineContains target (combineLeaves subtree))))))

-- A delivery is admitted when its target, if any, is a leaf owner.
def combineDeliveryAdmitted =
  (lambda unrestricted delivery : (family CombineDelivery) .
    (lambda unrestricted tree : (family OrderedCombineTree) .
      (combineDeliveryReaches delivery tree)))

def combineDistinct =
  (lambda unrestricted members : (family StdList Nat) .
    (eliminate
      StdList
      (lambda unrestricted current : (family StdList Nat) . Nat)
      members
      (branch StdListEmpty . 1)
      (branch
        StdListCons
        head
        tail
        induction
        .
        (naturalAnd (naturalIsZero (combineContains head tail)) induction))))

def combineOwnersValid =
  (lambda unrestricted participants : Nat .
    (lambda unrestricted tree : (family OrderedCombineTree) .
      (eliminate
        OrderedCombineTree
        (lambda unrestricted current : (family OrderedCombineTree) . Nat)
        tree
        (branch OrderedCombineLeaf owner . (naturalLess owner participants))
        (branch
          OrderedCombineBranch
          owner
          left
          right
          leftResult
          rightResult
          .
          (naturalAnd
            leftResult
            (naturalAnd
              rightResult
              (naturalAnd
                (naturalOr
                  (naturalEqual owner (combineOwner left))
                  (naturalEqual owner (combineOwner right)))
                1)))))))

def combineTreeAdmitted =
  (lambda unrestricted participants : Nat .
    (lambda unrestricted tree : (family OrderedCombineTree) .
      (naturalAnd
        (naturalNonzero participants)
        (naturalAnd
          (naturalLessOrEqual participants regionFrameWordLimit)
          (naturalAnd
            (combineOwnersValid participants tree)
            (naturalAnd
              (combineDistinct (combineLeaves tree))
              (naturalAnd
                (naturalLessOrEqual
                  (combineNodeCount tree)
                  (naturalDivideUnchecked regionFrameWordLimit 3))
                1)))))))

def combineLocal =
  (lambda erased payload : Type 0 .
    (lambda unrestricted owner : Nat .
      (lambda unrestricted operation : (family OrderedCombineOperation payload) .
        (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
          (protocolLocal
            (family OrderedCombineOperation payload)
            payload
            (family ProtocolNoDecision)
            owner
            operation
            tail)))))

-- A local move remains an explicit copy. A remote move is prepare,
-- transfer, consume in that order, and never invokes numerical arithmetic.
-- The payload binding cannot change the derived canonical identity.
def combineMove =
  (lambda erased payload : Type 0 .
    (lambda unrestricted anchor : (family RegionTransferIdentity) .
      (lambda unrestricted digest : Bytes .
        (lambda unrestricted stage : (family CombineStage) .
          (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
            (lambda unrestricted source : (family CombineReference) .
              (lambda unrestricted destination : (family CombineReference) .
                (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                  (nat-eliminate
                    (lambda unrestricted flag : Nat .
                      (family
                        GlobalProtocol
                        (family OrderedCombineOperation payload)
                        payload
                        (family ProtocolNoDecision)))
                    (let unrestricted identity =
                      (combineTransferIdentity anchor digest stage source destination)
                      in
                      (let unrestricted value =
                        (binding stage source destination identity)
                        in
                        (combineLocal
                          payload
                          (combineReferenceOwner source)
                          (constructor OrderedCombineOperation CombinePrepare payload source value)
                          (protocolTransfer
                            (family OrderedCombineOperation payload)
                            payload
                            (family ProtocolNoDecision)
                            identity
                            value
                            (combineLocal
                              payload
                              (combineReferenceOwner destination)
                              (constructor
                                OrderedCombineOperation
                                CombineConsume
                                payload
                                value
                                destination)
                              tail)))))
                    (lambda unrestricted prior : Nat .
                      (lambda unrestricted ignored : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                        (combineLocal
                          payload
                          (combineReferenceOwner source)
                          (constructor
                            OrderedCombineOperation
                            CombineCopy
                            payload
                            source
                            destination)
                          tail)))
                    (naturalEqual
                      (combineReferenceOwner source)
                      (combineReferenceOwner destination)))))))))))

def compileOrderedCombine =
  (lambda erased payload : Type 0 .
    (lambda unrestricted anchor : (family RegionTransferIdentity) .
      (lambda unrestricted digest : Bytes .
        (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
          (lambda unrestricted tree : (family OrderedCombineTree) .
            (eliminate
              OrderedCombineTree
              (lambda unrestricted current : (family OrderedCombineTree) .
                (pi unrestricted base : Nat .
                  (pi unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                    (family
                      GlobalProtocol
                      (family OrderedCombineOperation payload)
                      payload
                      (family ProtocolNoDecision)))))
              tree
              (branch
                OrderedCombineLeaf
                owner
                .
                (lambda unrestricted base : Nat .
                  (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                    (combineLocal
                      payload
                      owner
                      (constructor
                        OrderedCombineOperation
                        CombineReadLeaf
                        payload
                        (combineReference owner base 0))
                      tail))))
              (branch
                OrderedCombineBranch
                owner
                left
                right
                leftResult
                rightResult
                .
                (lambda unrestricted base : Nat .
                  (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                    (let unrestricted rightBase =
                      (naturalAdd base (combineNodeCount left))
                      in
                      (let unrestricted node =
                        (naturalAdd rightBase (combineNodeCount right))
                        in
                        (let unrestricted leftInput =
                          (combineReference owner node 1)
                          in
                          (let unrestricted rightInput =
                            (combineReference owner node 2)
                            in
                            (leftResult
                              base
                              (rightResult
                                rightBase
                                (combineMove
                                  payload
                                  anchor
                                  digest
                                  (constructor CombineStage CombineReduce)
                                  binding
                                  (combineTreeReference left base)
                                  leftInput
                                  (combineMove
                                    payload
                                    anchor
                                    digest
                                    (constructor CombineStage CombineReduce)
                                    binding
                                    (combineTreeReference right rightBase)
                                    rightInput
                                    (combineLocal
                                      payload
                                      owner
                                      (constructor
                                        OrderedCombineOperation
                                        CombineApply
                                        payload
                                        leftInput
                                        rightInput
                                        (combineReference owner node 0))
                                      tail))))))))))))))))))

-- `moves rest` when the subtree is reached, otherwise `rest` alone.
def combineDeliverInto =
  (lambda erased payload : Type 0 .
    (lambda unrestricted reached : Nat .
      (lambda unrestricted moves : (pi unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) . (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision))) .
        (lambda unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
          (nat-eliminate
            (lambda unrestricted current : Nat .
              (family
                GlobalProtocol
                (family OrderedCombineOperation payload)
                payload
                (family ProtocolNoDecision)))
            rest
            (lambda unrestricted previous : Nat .
              (lambda unrestricted ignored : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                (moves rest)))
            reached)))))

def compileTreeDelivery =
  (lambda erased payload : Type 0 .
    (lambda unrestricted anchor : (family RegionTransferIdentity) .
      (lambda unrestricted digest : Bytes .
        (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
          (lambda unrestricted delivery : (family CombineDelivery) .
            (lambda unrestricted tree : (family OrderedCombineTree) .
              (eliminate
                OrderedCombineTree
                (lambda unrestricted current : (family OrderedCombineTree) .
                  (pi unrestricted base : Nat .
                    (pi unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                      (family
                        GlobalProtocol
                        (family OrderedCombineOperation payload)
                        payload
                        (family ProtocolNoDecision)))))
                tree
                (branch
                  OrderedCombineLeaf
                  owner
                  .
                  (lambda unrestricted base : Nat .
                    (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                      tail)))
                (branch
                  OrderedCombineBranch
                  owner
                  left
                  right
                  leftResult
                  rightResult
                  .
                  (lambda unrestricted base : Nat .
                    (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                      (let unrestricted rightBase =
                        (naturalAdd base (combineNodeCount left))
                        in
                        (let unrestricted node =
                          (naturalAdd rightBase (combineNodeCount right))
                          in
                          (let unrestricted source =
                            (combineReference owner node 0)
                            in
                            (combineDeliverInto
                              payload
                              (combineDeliveryReaches delivery left)
                              (lambda unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                                (combineMove
                                  payload
                                  anchor
                                  digest
                                  (constructor CombineStage CombineReplicate)
                                  binding
                                  source
                                  (combineTreeReference left base)
                                  (leftResult base rest)))
                              (combineDeliverInto
                                payload
                                (combineDeliveryReaches delivery right)
                                (lambda unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                                  (combineMove
                                    payload
                                    anchor
                                    digest
                                    (constructor CombineStage CombineReplicate)
                                    binding
                                    source
                                    (combineTreeReference right rightBase)
                                    (rightResult rightBase rest)))
                                tail)))))))))))))))

-- Replication to every leaf owner.
def compileTreeReplication =
  (lambda erased payload : Type 0 .
    (lambda unrestricted anchor : (family RegionTransferIdentity) .
      (lambda unrestricted digest : Bytes .
        (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
          (compileTreeDelivery
            payload
            anchor
            digest
            binding
            (constructor CombineDelivery CombineReplicateAll))))))

-- Exact round contracts still pass through checkGlobalProtocol: this
-- producer owns topology/order, not target admission or frame lifecycle.
def orderedCombineAndReplicate =
  (lambda erased payload : Type 0 .
    (lambda unrestricted anchor : (family RegionTransferIdentity) .
      (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
        (lambda unrestricted tree : (family OrderedCombineTree) .
          (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
            (let unrestricted digest =
              (combineTreeDigest tree)
              in
              (compileOrderedCombine
                payload
                anchor
                digest
                binding
                tree
                0
                (compileTreeReplication payload anchor digest binding tree 0 tail))))))))

-- Reachable logical slots only: unrelated participants consume no local arena.
def combineLocalSlotsFrom =
  (lambda unrestricted role : Nat .
    (lambda unrestricted tree : (family OrderedCombineTree) .
      (eliminate
        OrderedCombineTree
        (lambda unrestricted current : (family OrderedCombineTree) .
          (pi unrestricted base : Nat . (family StdList Nat)))
        tree
        (branch
          OrderedCombineLeaf
          owner
          .
          (lambda unrestricted base : Nat .
            (nat-eliminate
              (lambda unrestricted flag : Nat . (family StdList Nat))
              (constructor StdList StdListEmpty Nat)
              (lambda unrestricted prior : Nat .
                (lambda unrestricted ignored : (family StdList Nat) .
                  (constructor
                    StdList
                    StdListCons
                    Nat
                    (naturalMultiply 3 base)
                    (constructor StdList StdListEmpty Nat))))
              (naturalEqual owner role))))
        (branch
          OrderedCombineBranch
          owner
          left
          right
          leftResult
          rightResult
          .
          (lambda unrestricted base : Nat .
            (let unrestricted rightBase =
              (naturalAdd base (combineNodeCount left))
              in
              (let unrestricted node =
                (naturalAdd rightBase (combineNodeCount right))
                in
                (stdListAppend
                  Nat
                  (leftResult base)
                  (stdListAppend
                    Nat
                    (rightResult rightBase)
                    (nat-eliminate
                      (lambda unrestricted flag : Nat . (family StdList Nat))
                      (constructor StdList StdListEmpty Nat)
                      (lambda unrestricted prior : Nat .
                        (lambda unrestricted ignored : (family StdList Nat) .
                          (constructor
                            StdList
                            StdListCons
                            Nat
                            (naturalMultiply 3 node)
                            (constructor
                              StdList
                              StdListCons
                              Nat
                              (naturalAdd (naturalMultiply 3 node) 1)
                              (constructor
                                StdList
                                StdListCons
                                Nat
                                (naturalAdd (naturalMultiply 3 node) 2)
                                (constructor StdList StdListEmpty Nat))))))
                      (naturalEqual owner role)))))))))))

def combineLocalSlots =
  (lambda unrestricted role : Nat .
    (lambda unrestricted tree : (family OrderedCombineTree) . (combineLocalSlotsFrom role tree 0)))

def combineReferenceIndex =
  (lambda unrestricted role : Nat .
    (lambda unrestricted tree : (family OrderedCombineTree) .
      (lambda unrestricted reference : (family CombineReference) .
        (nat-eliminate
          (lambda unrestricted flag : Nat . (family StdOption Nat))
          (constructor StdOption StdNone Nat)
          (lambda unrestricted prior : Nat .
            (lambda unrestricted ignored : (family StdOption Nat) .
              (app
                (eliminate
                  StdList
                  (lambda unrestricted current : (family StdList Nat) .
                    (pi unrestricted index : Nat . (family StdOption Nat)))
                  (combineLocalSlots role tree)
                  (branch
                    StdListEmpty
                    .
                    (lambda unrestricted index : Nat . (constructor StdOption StdNone Nat)))
                  (branch
                    StdListCons
                    head
                    tail
                    induction
                    .
                    (lambda unrestricted index : Nat .
                      (nat-eliminate
                        (lambda unrestricted flag : Nat . (family StdOption Nat))
                        (induction (naturalAdd index 1))
                        (lambda unrestricted prior : Nat .
                          (lambda unrestricted ignored : (family StdOption Nat) .
                            (constructor StdOption StdSome Nat index)))
                        (naturalEqual head (combineReferenceSlot reference))))))
                0)))
          (naturalEqual role (combineReferenceOwner reference))))))

-- Admission stops at the first named refusal; the remaining plan stays lazy.
def combineRequire =
  (lambda erased value : Type 0 .
    (lambda unrestricted flag : Nat .
      (lambda unrestricted failure : (family OrderedCombineFailure) .
        (lambda unrestricted next : (family StdResult (family OrderedCombineFailure) value) .
          (nat-eliminate
            (lambda unrestricted current : Nat .
              (family StdResult (family OrderedCombineFailure) value))
            (constructor StdResult StdFailure (family OrderedCombineFailure) value failure)
            (lambda unrestricted prior : Nat .
              (lambda unrestricted ignored : (family StdResult (family OrderedCombineFailure) value) .
                next))
            flag)))))

-- Combined with the distinct-leaf check, cardinality plus containment proves
-- exact set coverage without enumerating a compact group's ranks. Lookup uses
-- the admitted index. This explicit-tree planner still traverses every tree
-- node and retains its existing duplicate check; compact membership alone is
-- not a fleet collective schedule or a proof of linear planning complexity.
def combineCoverageValid =
  (lambda unrestricted participants : Nat .
    (lambda unrestricted coverage : (family CombineCoverage) .
      (lambda unrestricted leaves : (family StdList Nat) .
        (eliminate
          CombineCoverage
          (lambda unrestricted current : (family CombineCoverage) . Nat)
          coverage
          (branch
            CombineOrderedMembers
            members
            .
            (stdBoolToNatural (stdListNaturalEqual members leaves)))
          (branch
            CombineParticipantGroup
            group
            nodes
            depth
            .
            (eliminate
              StdResult
              (lambda unrestricted current : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) .
                Nat)
              (participantAdmit group nodes depth)
              (branch StdFailure reason . 0)
              (branch
                StdSuccess
                index
                .
                (naturalAnd
                  (naturalEqual participants (participantUniverseOf group))
                  (naturalAnd
                    (naturalEqual (bytes-length (participantGroupDigest group)) 32)
                    (naturalAnd
                      (naturalEqual (stdListLength Nat leaves) (participantCountOf index))
                      (eliminate
                        StdList
                        (lambda unrestricted current : (family StdList Nat) . Nat)
                        leaves
                        (branch StdListEmpty . 1)
                        (branch
                          StdListCons
                          head
                          tail
                          induction
                          .
                          (naturalAnd (participantContains index head) induction)))))))))))))

-- The requested ordered contribution set is checked independently of the tree.
-- This refuses missing/duplicated contributors before producing any participant.
def planOrderedCombineAndDeliver =
  (lambda erased payload : Type 0 .
    (lambda unrestricted participants : Nat .
      (lambda unrestricted members : (family CombineCoverage) .
        (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
          (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
            (lambda unrestricted local : (pi unrestricted role : Nat . (pi unrestricted operation : (family OrderedCombineOperation payload) . Nat)) .
              (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
                (lambda unrestricted delivery : (family CombineDelivery) .
                  (lambda unrestricted tree : (family OrderedCombineTree) .
                    (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                      (let unrestricted anchor =
                        (combineCoverageAnchor members baseAnchor)
                        in
                        (combineRequire
                          (family
                            GlobalProtocol
                            (family OrderedCombineOperation payload)
                            payload
                            (family ProtocolNoDecision))
                          (naturalAnd
                            (naturalNonzero participants)
                            (naturalLessOrEqual participants regionFrameWordLimit))
                          (constructor OrderedCombineFailure CombineMembershipBounds)
                          (combineRequire
                            (family
                              GlobalProtocol
                              (family OrderedCombineOperation payload)
                              payload
                              (family ProtocolNoDecision))
                            (combineOwnersValid participants tree)
                            (constructor OrderedCombineFailure CombineOwnerOutsideChildren)
                            (combineRequire
                              (family
                                GlobalProtocol
                                (family OrderedCombineOperation payload)
                                payload
                                (family ProtocolNoDecision))
                              (combineDistinct (combineLeaves tree))
                              (constructor OrderedCombineFailure CombineDuplicateLeaf)
                              (combineRequire
                                (family
                                  GlobalProtocol
                                  (family OrderedCombineOperation payload)
                                  payload
                                  (family ProtocolNoDecision))
                                (combineCoverageValid participants members (combineLeaves tree))
                                (constructor OrderedCombineFailure CombineCoverageMismatch)
                                (combineRequire
                                  (family
                                    GlobalProtocol
                                    (family OrderedCombineOperation payload)
                                    payload
                                    (family ProtocolNoDecision))
                                  (combineDeliveryAdmitted delivery tree)
                                  (constructor OrderedCombineFailure CombineCoverageMismatch)
                                  (combineRequire
                                    (family
                                      GlobalProtocol
                                      (family OrderedCombineOperation payload)
                                      payload
                                      (family ProtocolNoDecision))
                                    (naturalLessOrEqual
                                      (combineNodeCount tree)
                                      (naturalDivideUnchecked regionFrameWordLimit 3))
                                    (constructor OrderedCombineFailure CombineReferenceBounds)
                                    (let unrestricted digest =
                                      (combineTreeDigest tree)
                                      in
                                      (combineRequire
                                        (family
                                        GlobalProtocol
                                        (family OrderedCombineOperation payload)
                                        payload
                                        (family ProtocolNoDecision))
                                        (naturalEqual (bytes-length digest) 32)
                                        (constructor
                                        OrderedCombineFailure
                                        CombineIdentityUnavailable)
                                        (let unrestricted program =
                                        (compileOrderedCombine
                                        payload
                                        anchor
                                        digest
                                        binding
                                        tree
                                        0
                                        (compileTreeDelivery
                                        payload
                                        anchor
                                        digest
                                        binding
                                        delivery
                                        tree
                                        0
                                        tail))
                                        in
                                        (eliminate
                                        StdResult
                                        (lambda unrestricted current : (family StdResult (family ProtocolFailure) Nat) .
                                        (family
                                        StdResult
                                        (family OrderedCombineFailure)
                                        (family
                                        GlobalProtocol
                                        (family OrderedCombineOperation payload)
                                        payload
                                        (family ProtocolNoDecision))))
                                        (checkGlobalProtocol
                                        (family OrderedCombineOperation payload)
                                        payload
                                        (family ProtocolNoDecision)
                                        participants
                                        local
                                        transfer
                                        (protocolNoDecision payload)
                                        program)
                                        (branch
                                        StdFailure
                                        error
                                        .
                                        (constructor
                                        StdResult
                                        StdFailure
                                        (family OrderedCombineFailure)
                                        (family
                                        GlobalProtocol
                                        (family OrderedCombineOperation payload)
                                        payload
                                        (family ProtocolNoDecision))
                                        (constructor
                                        OrderedCombineFailure
                                        CombineProtocolRefused
                                        error)))
                                        (branch
                                        StdSuccess
                                        value
                                        .
                                        (constructor
                                        StdResult
                                        StdSuccess
                                        (family OrderedCombineFailure)
                                        (family
                                        GlobalProtocol
                                        (family OrderedCombineOperation payload)
                                        payload
                                        (family ProtocolNoDecision))
                                        program)))))))))))))))))))))))

def planOrderedCombineAndReplicate =
  (lambda erased payload : Type 0 .
    (lambda unrestricted participants : Nat .
      (lambda unrestricted members : (family CombineCoverage) .
        (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
          (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
            (lambda unrestricted local : (pi unrestricted role : Nat . (pi unrestricted operation : (family OrderedCombineOperation payload) . Nat)) .
              (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
                (planOrderedCombineAndDeliver
                  payload
                  participants
                  members
                  baseAnchor
                  binding
                  local
                  transfer
                  (constructor CombineDelivery CombineReplicateAll)))))))))

-- Numeric specialization checks its declared realization before constructing
-- any participant. Generic non-numeric payloads retain the underlying planner.
def planNumericalCombineAndDeliver =
  (lambda erased payload : Type 0 .
    (lambda unrestricted required : (family NumericalContract) .
      (lambda unrestricted realized : (family NumericalContract) .
        (lambda unrestricted participants : Nat .
          (lambda unrestricted members : (family CombineCoverage) .
            (lambda unrestricted anchor : (family RegionTransferIdentity) .
              (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
                (lambda unrestricted local : (pi unrestricted role : Nat . (pi unrestricted operation : (family OrderedCombineOperation payload) . Nat)) .
                  (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
                    (lambda unrestricted delivery : (family CombineDelivery) .
                      (lambda unrestricted tree : (family OrderedCombineTree) .
                        (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
                          (eliminate
                            StdResult
                            (lambda unrestricted current : (family StdResult (family NumericalFailure) Nat) .
                              (family
                                StdResult
                                (family OrderedCombineFailure)
                                (family
                                  GlobalProtocol
                                  (family OrderedCombineOperation payload)
                                  payload
                                  (family ProtocolNoDecision))))
                            (numericalCompatibility required realized)
                            (branch
                              StdFailure
                              error
                              .
                              (constructor
                                StdResult
                                StdFailure
                                (family OrderedCombineFailure)
                                (family
                                  GlobalProtocol
                                  (family OrderedCombineOperation payload)
                                  payload
                                  (family ProtocolNoDecision))
                                (constructor OrderedCombineFailure CombineNumericalRefused error)))
                            (branch
                              StdSuccess
                              admitted
                              .
                              (combineRequire
                                (family
                                  GlobalProtocol
                                  (family OrderedCombineOperation payload)
                                  payload
                                  (family ProtocolNoDecision))
                                (naturalEqual
                                  (bytes-length (numericalExactContractDigest required))
                                  32)
                                (constructor OrderedCombineFailure CombineIdentityUnavailable)
                                (planOrderedCombineAndDeliver
                                  payload
                                  participants
                                  members
                                  (combineNumericalAnchor required anchor)
                                  binding
                                  local
                                  transfer
                                  delivery
                                  tree
                                  tail))))))))))))))))

def planNumericalCombineAndReplicate =
  (lambda erased payload : Type 0 .
    (lambda unrestricted required : (family NumericalContract) .
      (lambda unrestricted realized : (family NumericalContract) .
        (lambda unrestricted participants : Nat .
          (lambda unrestricted members : (family CombineCoverage) .
            (lambda unrestricted anchor : (family RegionTransferIdentity) .
              (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
                (lambda unrestricted local : (pi unrestricted role : Nat . (pi unrestricted operation : (family OrderedCombineOperation payload) . Nat)) .
                  (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
                    (planNumericalCombineAndDeliver
                      payload
                      required
                      realized
                      participants
                      members
                      anchor
                      binding
                      local
                      transfer
                      (constructor CombineDelivery CombineReplicateAll)))))))))))