module NativeCombineDeliveryLaws

import Runtime.NativeCombine
import Runtime.OrderedCombine
import Runtime.RegionTransfer
import Runtime.Protocol
import Compiler.Planning.Protocol
import Compiler.Planning.OrderedCombine
import Learning.Transition
import Representation.Partition
import Representation.ParticipantTree
import Std.Foundation
import Std.List
import Std.Natural

-- Reduction to one owner (CombineDeliverTo): the ordered combine as before,
-- then the root value moves only along the tree path to the target's leaf.
-- Laws count the payloads each role exchanges (one frame each).
def anchor =
  (constructor
    RegionTransferIdentity
    RegionTransferIdentityOf
    b"delivery-laws"
    b"run"
    b"values"
    b"binary64"
    (constructor LearningRound LearningRoundOf 1 0)
    0
    0
    0
    (constructor LogicalInterval LogicalIntervalOf 0 8))

def payloads =
  (lambda unrestricted delivery : (family CombineDelivery) .
    (lambda unrestricted role : Nat .
      (lambda unrestricted tree : (family OrderedCombineTree) .
        (stdListLength
          (family RegionTransferIdentity)
          (nativeCombinePayloads (nativeCombineDeliveringContextFor anchor delivery role tree))))))

def everyone =
  (constructor CombineDelivery CombineReplicateAll)

def toOwner =
  (lambda unrestricted target : Nat . (constructor CombineDelivery CombineDeliverTo target))

-- The star's chain at owner 0 over four owners. With replication owner 0
-- receives three leaves and sends three results; delivered to owner 2 it
-- sends one.
def chainHubReplicates : (equal Nat (payloads everyone 0 (nativeCombineChain 0 4)) 6) =
  (refl Nat 6)

def chainHubDelivers : (equal Nat (payloads (toOwner 2) 0 (nativeCombineChain 0 4)) 4) =
  (refl Nat 4)

def chainTargetReceives : (equal Nat (payloads (toOwner 2) 2 (nativeCombineChain 0 4)) 2) =
  (refl Nat 2)

def chainOtherOnlySends : (equal Nat (payloads (toOwner 2) 1 (nativeCombineChain 0 4)) 1) =
  (refl Nat 1)

-- Delivery to owner 0 itself moves nothing after the reduction.
def chainToHub : (equal Nat (payloads (toOwner 0) 0 (nativeCombineChain 0 4)) 3) =
  (refl Nat 3)

-- Seven owners at fan-out two: root 0, children 1 (roles 1..3) and 4
-- (roles 4..6). Delivered to role 3 the value runs 0 -> 1 -> 3: role 1
-- forwards it, role 4's subtree receives nothing.
def treeForwarder : (equal Nat (payloads (toOwner 3) 1 (nativeCombineHierarchy 2 7)) 5) =
  (refl Nat 5)

def treeForwarderReplicates : (equal Nat (payloads everyone 1 (nativeCombineHierarchy 2 7)) 6) =
  (refl Nat 6)

def treeOtherSubtree : (equal Nat (payloads (toOwner 3) 4 (nativeCombineHierarchy 2 7)) 3) =
  (refl Nat 3)

def treeSibling : (equal Nat (payloads (toOwner 3) 2 (nativeCombineHierarchy 2 7)) 1) =
  (refl Nat 1)

def treeTarget : (equal Nat (payloads (toOwner 3) 3 (nativeCombineHierarchy 2 7)) 2) =
  (refl Nat 2)

-- A target that is no leaf owner is refused by admission.
def outsideRefused : (equal Nat (combineDeliveryAdmitted (toOwner 9) (nativeCombineChain 0 4)) 0) =
  (refl Nat 0)

def insideAdmitted :
  (equal Nat (combineDeliveryAdmitted (toOwner 3) (nativeCombineHierarchy 2 7)) 1) =
  (refl Nat 1)

def main : Nat =
  0