NativeCombineDeliveryLaws

1module NativeCombineDeliveryLaws
2
3import Runtime.NativeCombine
4import Runtime.OrderedCombine
5import Runtime.RegionTransfer
6import Runtime.Protocol
7import Compiler.Planning.Protocol
8import Compiler.Planning.OrderedCombine
9import Learning.Transition
10import Representation.Partition
11import Representation.ParticipantTree
12import Std.Foundation
13import Std.List
14import Std.Natural
15
16-- Reduction to one owner (CombineDeliverTo): the ordered combine as before,
17-- then the root value moves only along the tree path to the target's leaf.
18-- Laws count the payloads each role exchanges (one frame each).
19def anchor =
20  (constructor
21    RegionTransferIdentity
22    RegionTransferIdentityOf
23    b"delivery-laws"
24    b"run"
25    b"values"
26    b"binary64"
27    (constructor LearningRound LearningRoundOf 1 0)
28    0
29    0
30    0
31    (constructor LogicalInterval LogicalIntervalOf 0 8))
32
33def payloads =
34  (lambda unrestricted delivery : (family CombineDelivery) .
35    (lambda unrestricted role : Nat .
36      (lambda unrestricted tree : (family OrderedCombineTree) .
37        (stdListLength
38          (family RegionTransferIdentity)
39          (nativeCombinePayloads (nativeCombineDeliveringContextFor anchor delivery role tree))))))
40
41def everyone =
42  (constructor CombineDelivery CombineReplicateAll)
43
44def toOwner =
45  (lambda unrestricted target : Nat . (constructor CombineDelivery CombineDeliverTo target))
46
47-- The star's chain at owner 0 over four owners. With replication owner 0
48-- receives three leaves and sends three results; delivered to owner 2 it
49-- sends one.
50def chainHubReplicates : (equal Nat (payloads everyone 0 (nativeCombineChain 0 4)) 6) =
51  (refl Nat 6)
52
53def chainHubDelivers : (equal Nat (payloads (toOwner 2) 0 (nativeCombineChain 0 4)) 4) =
54  (refl Nat 4)
55
56def chainTargetReceives : (equal Nat (payloads (toOwner 2) 2 (nativeCombineChain 0 4)) 2) =
57  (refl Nat 2)
58
59def chainOtherOnlySends : (equal Nat (payloads (toOwner 2) 1 (nativeCombineChain 0 4)) 1) =
60  (refl Nat 1)
61
62-- Delivery to owner 0 itself moves nothing after the reduction.
63def chainToHub : (equal Nat (payloads (toOwner 0) 0 (nativeCombineChain 0 4)) 3) =
64  (refl Nat 3)
65
66-- Seven owners at fan-out two: root 0, children 1 (roles 1..3) and 4
67-- (roles 4..6). Delivered to role 3 the value runs 0 -> 1 -> 3: role 1
68-- forwards it, role 4's subtree receives nothing.
69def treeForwarder : (equal Nat (payloads (toOwner 3) 1 (nativeCombineHierarchy 2 7)) 5) =
70  (refl Nat 5)
71
72def treeForwarderReplicates : (equal Nat (payloads everyone 1 (nativeCombineHierarchy 2 7)) 6) =
73  (refl Nat 6)
74
75def treeOtherSubtree : (equal Nat (payloads (toOwner 3) 4 (nativeCombineHierarchy 2 7)) 3) =
76  (refl Nat 3)
77
78def treeSibling : (equal Nat (payloads (toOwner 3) 2 (nativeCombineHierarchy 2 7)) 1) =
79  (refl Nat 1)
80
81def treeTarget : (equal Nat (payloads (toOwner 3) 3 (nativeCombineHierarchy 2 7)) 2) =
82  (refl Nat 2)
83
84-- A target that is no leaf owner is refused by admission.
85def outsideRefused : (equal Nat (combineDeliveryAdmitted (toOwner 9) (nativeCombineChain 0 4)) 0) =
86  (refl Nat 0)
87
88def insideAdmitted :
89  (equal Nat (combineDeliveryAdmitted (toOwner 3) (nativeCombineHierarchy 2 7)) 1) =
90  (refl Nat 1)
91
92def main : Nat =
93  0