Compiler.Planning.OrderedCombine

1module Compiler.Planning.OrderedCombine
2
3import Runtime.OrderedCombine
4import Representation.ParticipantGroup
5import Learning.Numerics
6import Runtime.Protocol
7import Runtime.RegionTransfer
8import Runtime.RegionFrame
9import Compiler.Planning.Protocol
10import Std.Foundation
11import Std.List
12import Std.Natural
13
14-- Where a reduced value goes after the ordered combine: to every leaf owner
15-- (replication), or only to one target owner, moved from the root down the
16-- tree path to the target's leaf (a reduction to one owner, for instance a
17-- coordinate's owner). Every other owner's leaf value is left as it was.
18family CombineDelivery : Type 0
19constructor CombineReplicateAll
20constructor CombineDeliverTo
21field unrestricted combineDeliveryTarget : Nat
22
23end-family
24
25-- Fixed, explicit trees are admitted without enumerating unrelated fleet
26-- members. Duplicate checking is quadratic in the leaf count; this is not the
27-- future hierarchical fleet planner. A combine runs at one of its child owners,
28-- so every execution role belongs to the declared contribution set.
29def combineContains =
30  (lambda unrestricted role : Nat .
31    (lambda unrestricted members : (family StdList Nat) .
32      (eliminate
33        StdList
34        (lambda unrestricted current : (family StdList Nat) . Nat)
35        members
36        (branch StdListEmpty . 0)
37        (branch StdListCons head tail induction . (naturalOr (naturalEqual role head) induction)))))
38
39-- Whether `subtree` receives the value under `delivery`.
40def combineDeliveryReaches =
41  (lambda unrestricted delivery : (family CombineDelivery) .
42    (lambda unrestricted subtree : (family OrderedCombineTree) .
43      (eliminate
44        CombineDelivery
45        (lambda unrestricted current : (family CombineDelivery) . Nat)
46        delivery
47        (branch CombineReplicateAll . 1)
48        (branch CombineDeliverTo target . (combineContains target (combineLeaves subtree))))))
49
50-- A delivery is admitted when its target, if any, is a leaf owner.
51def combineDeliveryAdmitted =
52  (lambda unrestricted delivery : (family CombineDelivery) .
53    (lambda unrestricted tree : (family OrderedCombineTree) .
54      (combineDeliveryReaches delivery tree)))
55
56def combineDistinct =
57  (lambda unrestricted members : (family StdList Nat) .
58    (eliminate
59      StdList
60      (lambda unrestricted current : (family StdList Nat) . Nat)
61      members
62      (branch StdListEmpty . 1)
63      (branch
64        StdListCons
65        head
66        tail
67        induction
68        .
69        (naturalAnd (naturalIsZero (combineContains head tail)) induction))))
70
71def combineOwnersValid =
72  (lambda unrestricted participants : Nat .
73    (lambda unrestricted tree : (family OrderedCombineTree) .
74      (eliminate
75        OrderedCombineTree
76        (lambda unrestricted current : (family OrderedCombineTree) . Nat)
77        tree
78        (branch OrderedCombineLeaf owner . (naturalLess owner participants))
79        (branch
80          OrderedCombineBranch
81          owner
82          left
83          right
84          leftResult
85          rightResult
86          .
87          (naturalAnd
88            leftResult
89            (naturalAnd
90              rightResult
91              (naturalAnd
92                (naturalOr
93                  (naturalEqual owner (combineOwner left))
94                  (naturalEqual owner (combineOwner right)))
95                1)))))))
96
97def combineTreeAdmitted =
98  (lambda unrestricted participants : Nat .
99    (lambda unrestricted tree : (family OrderedCombineTree) .
100      (naturalAnd
101        (naturalNonzero participants)
102        (naturalAnd
103          (naturalLessOrEqual participants regionFrameWordLimit)
104          (naturalAnd
105            (combineOwnersValid participants tree)
106            (naturalAnd
107              (combineDistinct (combineLeaves tree))
108              (naturalAnd
109                (naturalLessOrEqual
110                  (combineNodeCount tree)
111                  (naturalDivideUnchecked regionFrameWordLimit 3))
112                1)))))))
113
114def combineLocal =
115  (lambda erased payload : Type 0 .
116    (lambda unrestricted owner : Nat .
117      (lambda unrestricted operation : (family OrderedCombineOperation payload) .
118        (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
119          (protocolLocal
120            (family OrderedCombineOperation payload)
121            payload
122            (family ProtocolNoDecision)
123            owner
124            operation
125            tail)))))
126
127-- A local move remains an explicit copy. A remote move is prepare,
128-- transfer, consume in that order, and never invokes numerical arithmetic.
129-- The payload binding cannot change the derived canonical identity.
130def combineMove =
131  (lambda erased payload : Type 0 .
132    (lambda unrestricted anchor : (family RegionTransferIdentity) .
133      (lambda unrestricted digest : Bytes .
134        (lambda unrestricted stage : (family CombineStage) .
135          (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
136            (lambda unrestricted source : (family CombineReference) .
137              (lambda unrestricted destination : (family CombineReference) .
138                (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
139                  (nat-eliminate
140                    (lambda unrestricted flag : Nat .
141                      (family
142                        GlobalProtocol
143                        (family OrderedCombineOperation payload)
144                        payload
145                        (family ProtocolNoDecision)))
146                    (let unrestricted identity =
147                      (combineTransferIdentity anchor digest stage source destination)
148                      in
149                      (let unrestricted value =
150                        (binding stage source destination identity)
151                        in
152                        (combineLocal
153                          payload
154                          (combineReferenceOwner source)
155                          (constructor OrderedCombineOperation CombinePrepare payload source value)
156                          (protocolTransfer
157                            (family OrderedCombineOperation payload)
158                            payload
159                            (family ProtocolNoDecision)
160                            identity
161                            value
162                            (combineLocal
163                              payload
164                              (combineReferenceOwner destination)
165                              (constructor
166                                OrderedCombineOperation
167                                CombineConsume
168                                payload
169                                value
170                                destination)
171                              tail)))))
172                    (lambda unrestricted prior : Nat .
173                      (lambda unrestricted ignored : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
174                        (combineLocal
175                          payload
176                          (combineReferenceOwner source)
177                          (constructor
178                            OrderedCombineOperation
179                            CombineCopy
180                            payload
181                            source
182                            destination)
183                          tail)))
184                    (naturalEqual
185                      (combineReferenceOwner source)
186                      (combineReferenceOwner destination)))))))))))
187
188def compileOrderedCombine =
189  (lambda erased payload : Type 0 .
190    (lambda unrestricted anchor : (family RegionTransferIdentity) .
191      (lambda unrestricted digest : Bytes .
192        (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
193          (lambda unrestricted tree : (family OrderedCombineTree) .
194            (eliminate
195              OrderedCombineTree
196              (lambda unrestricted current : (family OrderedCombineTree) .
197                (pi unrestricted base : Nat .
198                  (pi unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
199                    (family
200                      GlobalProtocol
201                      (family OrderedCombineOperation payload)
202                      payload
203                      (family ProtocolNoDecision)))))
204              tree
205              (branch
206                OrderedCombineLeaf
207                owner
208                .
209                (lambda unrestricted base : Nat .
210                  (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
211                    (combineLocal
212                      payload
213                      owner
214                      (constructor
215                        OrderedCombineOperation
216                        CombineReadLeaf
217                        payload
218                        (combineReference owner base 0))
219                      tail))))
220              (branch
221                OrderedCombineBranch
222                owner
223                left
224                right
225                leftResult
226                rightResult
227                .
228                (lambda unrestricted base : Nat .
229                  (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
230                    (let unrestricted rightBase =
231                      (naturalAdd base (combineNodeCount left))
232                      in
233                      (let unrestricted node =
234                        (naturalAdd rightBase (combineNodeCount right))
235                        in
236                        (let unrestricted leftInput =
237                          (combineReference owner node 1)
238                          in
239                          (let unrestricted rightInput =
240                            (combineReference owner node 2)
241                            in
242                            (leftResult
243                              base
244                              (rightResult
245                                rightBase
246                                (combineMove
247                                  payload
248                                  anchor
249                                  digest
250                                  (constructor CombineStage CombineReduce)
251                                  binding
252                                  (combineTreeReference left base)
253                                  leftInput
254                                  (combineMove
255                                    payload
256                                    anchor
257                                    digest
258                                    (constructor CombineStage CombineReduce)
259                                    binding
260                                    (combineTreeReference right rightBase)
261                                    rightInput
262                                    (combineLocal
263                                      payload
264                                      owner
265                                      (constructor
266                                        OrderedCombineOperation
267                                        CombineApply
268                                        payload
269                                        leftInput
270                                        rightInput
271                                        (combineReference owner node 0))
272                                      tail))))))))))))))))))
273
274-- `moves rest` when the subtree is reached, otherwise `rest` alone.
275def combineDeliverInto =
276  (lambda erased payload : Type 0 .
277    (lambda unrestricted reached : Nat .
278      (lambda unrestricted moves : (pi unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) . (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision))) .
279        (lambda unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
280          (nat-eliminate
281            (lambda unrestricted current : Nat .
282              (family
283                GlobalProtocol
284                (family OrderedCombineOperation payload)
285                payload
286                (family ProtocolNoDecision)))
287            rest
288            (lambda unrestricted previous : Nat .
289              (lambda unrestricted ignored : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
290                (moves rest)))
291            reached)))))
292
293def compileTreeDelivery =
294  (lambda erased payload : Type 0 .
295    (lambda unrestricted anchor : (family RegionTransferIdentity) .
296      (lambda unrestricted digest : Bytes .
297        (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
298          (lambda unrestricted delivery : (family CombineDelivery) .
299            (lambda unrestricted tree : (family OrderedCombineTree) .
300              (eliminate
301                OrderedCombineTree
302                (lambda unrestricted current : (family OrderedCombineTree) .
303                  (pi unrestricted base : Nat .
304                    (pi unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
305                      (family
306                        GlobalProtocol
307                        (family OrderedCombineOperation payload)
308                        payload
309                        (family ProtocolNoDecision)))))
310                tree
311                (branch
312                  OrderedCombineLeaf
313                  owner
314                  .
315                  (lambda unrestricted base : Nat .
316                    (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
317                      tail)))
318                (branch
319                  OrderedCombineBranch
320                  owner
321                  left
322                  right
323                  leftResult
324                  rightResult
325                  .
326                  (lambda unrestricted base : Nat .
327                    (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
328                      (let unrestricted rightBase =
329                        (naturalAdd base (combineNodeCount left))
330                        in
331                        (let unrestricted node =
332                          (naturalAdd rightBase (combineNodeCount right))
333                          in
334                          (let unrestricted source =
335                            (combineReference owner node 0)
336                            in
337                            (combineDeliverInto
338                              payload
339                              (combineDeliveryReaches delivery left)
340                              (lambda unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
341                                (combineMove
342                                  payload
343                                  anchor
344                                  digest
345                                  (constructor CombineStage CombineReplicate)
346                                  binding
347                                  source
348                                  (combineTreeReference left base)
349                                  (leftResult base rest)))
350                              (combineDeliverInto
351                                payload
352                                (combineDeliveryReaches delivery right)
353                                (lambda unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
354                                  (combineMove
355                                    payload
356                                    anchor
357                                    digest
358                                    (constructor CombineStage CombineReplicate)
359                                    binding
360                                    source
361                                    (combineTreeReference right rightBase)
362                                    (rightResult rightBase rest)))
363                                tail)))))))))))))))
364
365-- Replication to every leaf owner.
366def compileTreeReplication =
367  (lambda erased payload : Type 0 .
368    (lambda unrestricted anchor : (family RegionTransferIdentity) .
369      (lambda unrestricted digest : Bytes .
370        (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
371          (compileTreeDelivery
372            payload
373            anchor
374            digest
375            binding
376            (constructor CombineDelivery CombineReplicateAll))))))
377
378-- Exact round contracts still pass through checkGlobalProtocol: this
379-- producer owns topology/order, not target admission or frame lifecycle.
380def orderedCombineAndReplicate =
381  (lambda erased payload : Type 0 .
382    (lambda unrestricted anchor : (family RegionTransferIdentity) .
383      (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
384        (lambda unrestricted tree : (family OrderedCombineTree) .
385          (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
386            (let unrestricted digest =
387              (combineTreeDigest tree)
388              in
389              (compileOrderedCombine
390                payload
391                anchor
392                digest
393                binding
394                tree
395                0
396                (compileTreeReplication payload anchor digest binding tree 0 tail))))))))
397
398-- Reachable logical slots only: unrelated participants consume no local arena.
399def combineLocalSlotsFrom =
400  (lambda unrestricted role : Nat .
401    (lambda unrestricted tree : (family OrderedCombineTree) .
402      (eliminate
403        OrderedCombineTree
404        (lambda unrestricted current : (family OrderedCombineTree) .
405          (pi unrestricted base : Nat . (family StdList Nat)))
406        tree
407        (branch
408          OrderedCombineLeaf
409          owner
410          .
411          (lambda unrestricted base : Nat .
412            (nat-eliminate
413              (lambda unrestricted flag : Nat . (family StdList Nat))
414              (constructor StdList StdListEmpty Nat)
415              (lambda unrestricted prior : Nat .
416                (lambda unrestricted ignored : (family StdList Nat) .
417                  (constructor
418                    StdList
419                    StdListCons
420                    Nat
421                    (naturalMultiply 3 base)
422                    (constructor StdList StdListEmpty Nat))))
423              (naturalEqual owner role))))
424        (branch
425          OrderedCombineBranch
426          owner
427          left
428          right
429          leftResult
430          rightResult
431          .
432          (lambda unrestricted base : Nat .
433            (let unrestricted rightBase =
434              (naturalAdd base (combineNodeCount left))
435              in
436              (let unrestricted node =
437                (naturalAdd rightBase (combineNodeCount right))
438                in
439                (stdListAppend
440                  Nat
441                  (leftResult base)
442                  (stdListAppend
443                    Nat
444                    (rightResult rightBase)
445                    (nat-eliminate
446                      (lambda unrestricted flag : Nat . (family StdList Nat))
447                      (constructor StdList StdListEmpty Nat)
448                      (lambda unrestricted prior : Nat .
449                        (lambda unrestricted ignored : (family StdList Nat) .
450                          (constructor
451                            StdList
452                            StdListCons
453                            Nat
454                            (naturalMultiply 3 node)
455                            (constructor
456                              StdList
457                              StdListCons
458                              Nat
459                              (naturalAdd (naturalMultiply 3 node) 1)
460                              (constructor
461                                StdList
462                                StdListCons
463                                Nat
464                                (naturalAdd (naturalMultiply 3 node) 2)
465                                (constructor StdList StdListEmpty Nat))))))
466                      (naturalEqual owner role)))))))))))
467
468def combineLocalSlots =
469  (lambda unrestricted role : Nat .
470    (lambda unrestricted tree : (family OrderedCombineTree) . (combineLocalSlotsFrom role tree 0)))
471
472def combineReferenceIndex =
473  (lambda unrestricted role : Nat .
474    (lambda unrestricted tree : (family OrderedCombineTree) .
475      (lambda unrestricted reference : (family CombineReference) .
476        (nat-eliminate
477          (lambda unrestricted flag : Nat . (family StdOption Nat))
478          (constructor StdOption StdNone Nat)
479          (lambda unrestricted prior : Nat .
480            (lambda unrestricted ignored : (family StdOption Nat) .
481              (app
482                (eliminate
483                  StdList
484                  (lambda unrestricted current : (family StdList Nat) .
485                    (pi unrestricted index : Nat . (family StdOption Nat)))
486                  (combineLocalSlots role tree)
487                  (branch
488                    StdListEmpty
489                    .
490                    (lambda unrestricted index : Nat . (constructor StdOption StdNone Nat)))
491                  (branch
492                    StdListCons
493                    head
494                    tail
495                    induction
496                    .
497                    (lambda unrestricted index : Nat .
498                      (nat-eliminate
499                        (lambda unrestricted flag : Nat . (family StdOption Nat))
500                        (induction (naturalAdd index 1))
501                        (lambda unrestricted prior : Nat .
502                          (lambda unrestricted ignored : (family StdOption Nat) .
503                            (constructor StdOption StdSome Nat index)))
504                        (naturalEqual head (combineReferenceSlot reference))))))
505                0)))
506          (naturalEqual role (combineReferenceOwner reference))))))
507
508-- Admission stops at the first named refusal; the remaining plan stays lazy.
509def combineRequire =
510  (lambda erased value : Type 0 .
511    (lambda unrestricted flag : Nat .
512      (lambda unrestricted failure : (family OrderedCombineFailure) .
513        (lambda unrestricted next : (family StdResult (family OrderedCombineFailure) value) .
514          (nat-eliminate
515            (lambda unrestricted current : Nat .
516              (family StdResult (family OrderedCombineFailure) value))
517            (constructor StdResult StdFailure (family OrderedCombineFailure) value failure)
518            (lambda unrestricted prior : Nat .
519              (lambda unrestricted ignored : (family StdResult (family OrderedCombineFailure) value) .
520                next))
521            flag)))))
522
523-- Combined with the distinct-leaf check, cardinality plus containment proves
524-- exact set coverage without enumerating a compact group's ranks. Lookup uses
525-- the admitted index. This explicit-tree planner still traverses every tree
526-- node and retains its existing duplicate check; compact membership alone is
527-- not a fleet collective schedule or a proof of linear planning complexity.
528def combineCoverageValid =
529  (lambda unrestricted participants : Nat .
530    (lambda unrestricted coverage : (family CombineCoverage) .
531      (lambda unrestricted leaves : (family StdList Nat) .
532        (eliminate
533          CombineCoverage
534          (lambda unrestricted current : (family CombineCoverage) . Nat)
535          coverage
536          (branch
537            CombineOrderedMembers
538            members
539            .
540            (stdBoolToNatural (stdListNaturalEqual members leaves)))
541          (branch
542            CombineParticipantGroup
543            group
544            nodes
545            depth
546            .
547            (eliminate
548              StdResult
549              (lambda unrestricted current : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) .
550                Nat)
551              (participantAdmit group nodes depth)
552              (branch StdFailure reason . 0)
553              (branch
554                StdSuccess
555                index
556                .
557                (naturalAnd
558                  (naturalEqual participants (participantUniverseOf group))
559                  (naturalAnd
560                    (naturalEqual (bytes-length (participantGroupDigest group)) 32)
561                    (naturalAnd
562                      (naturalEqual (stdListLength Nat leaves) (participantCountOf index))
563                      (eliminate
564                        StdList
565                        (lambda unrestricted current : (family StdList Nat) . Nat)
566                        leaves
567                        (branch StdListEmpty . 1)
568                        (branch
569                          StdListCons
570                          head
571                          tail
572                          induction
573                          .
574                          (naturalAnd (participantContains index head) induction)))))))))))))
575
576-- The requested ordered contribution set is checked independently of the tree.
577-- This refuses missing/duplicated contributors before producing any participant.
578def planOrderedCombineAndDeliver =
579  (lambda erased payload : Type 0 .
580    (lambda unrestricted participants : Nat .
581      (lambda unrestricted members : (family CombineCoverage) .
582        (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
583          (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
584            (lambda unrestricted local : (pi unrestricted role : Nat . (pi unrestricted operation : (family OrderedCombineOperation payload) . Nat)) .
585              (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
586                (lambda unrestricted delivery : (family CombineDelivery) .
587                  (lambda unrestricted tree : (family OrderedCombineTree) .
588                    (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
589                      (let unrestricted anchor =
590                        (combineCoverageAnchor members baseAnchor)
591                        in
592                        (combineRequire
593                          (family
594                            GlobalProtocol
595                            (family OrderedCombineOperation payload)
596                            payload
597                            (family ProtocolNoDecision))
598                          (naturalAnd
599                            (naturalNonzero participants)
600                            (naturalLessOrEqual participants regionFrameWordLimit))
601                          (constructor OrderedCombineFailure CombineMembershipBounds)
602                          (combineRequire
603                            (family
604                              GlobalProtocol
605                              (family OrderedCombineOperation payload)
606                              payload
607                              (family ProtocolNoDecision))
608                            (combineOwnersValid participants tree)
609                            (constructor OrderedCombineFailure CombineOwnerOutsideChildren)
610                            (combineRequire
611                              (family
612                                GlobalProtocol
613                                (family OrderedCombineOperation payload)
614                                payload
615                                (family ProtocolNoDecision))
616                              (combineDistinct (combineLeaves tree))
617                              (constructor OrderedCombineFailure CombineDuplicateLeaf)
618                              (combineRequire
619                                (family
620                                  GlobalProtocol
621                                  (family OrderedCombineOperation payload)
622                                  payload
623                                  (family ProtocolNoDecision))
624                                (combineCoverageValid participants members (combineLeaves tree))
625                                (constructor OrderedCombineFailure CombineCoverageMismatch)
626                                (combineRequire
627                                  (family
628                                    GlobalProtocol
629                                    (family OrderedCombineOperation payload)
630                                    payload
631                                    (family ProtocolNoDecision))
632                                  (combineDeliveryAdmitted delivery tree)
633                                  (constructor OrderedCombineFailure CombineCoverageMismatch)
634                                  (combineRequire
635                                    (family
636                                      GlobalProtocol
637                                      (family OrderedCombineOperation payload)
638                                      payload
639                                      (family ProtocolNoDecision))
640                                    (naturalLessOrEqual
641                                      (combineNodeCount tree)
642                                      (naturalDivideUnchecked regionFrameWordLimit 3))
643                                    (constructor OrderedCombineFailure CombineReferenceBounds)
644                                    (let unrestricted digest =
645                                      (combineTreeDigest tree)
646                                      in
647                                      (combineRequire
648                                        (family
649                                        GlobalProtocol
650                                        (family OrderedCombineOperation payload)
651                                        payload
652                                        (family ProtocolNoDecision))
653                                        (naturalEqual (bytes-length digest) 32)
654                                        (constructor
655                                        OrderedCombineFailure
656                                        CombineIdentityUnavailable)
657                                        (let unrestricted program =
658                                        (compileOrderedCombine
659                                        payload
660                                        anchor
661                                        digest
662                                        binding
663                                        tree
664                                        0
665                                        (compileTreeDelivery
666                                        payload
667                                        anchor
668                                        digest
669                                        binding
670                                        delivery
671                                        tree
672                                        0
673                                        tail))
674                                        in
675                                        (eliminate
676                                        StdResult
677                                        (lambda unrestricted current : (family StdResult (family ProtocolFailure) Nat) .
678                                        (family
679                                        StdResult
680                                        (family OrderedCombineFailure)
681                                        (family
682                                        GlobalProtocol
683                                        (family OrderedCombineOperation payload)
684                                        payload
685                                        (family ProtocolNoDecision))))
686                                        (checkGlobalProtocol
687                                        (family OrderedCombineOperation payload)
688                                        payload
689                                        (family ProtocolNoDecision)
690                                        participants
691                                        local
692                                        transfer
693                                        (protocolNoDecision payload)
694                                        program)
695                                        (branch
696                                        StdFailure
697                                        error
698                                        .
699                                        (constructor
700                                        StdResult
701                                        StdFailure
702                                        (family OrderedCombineFailure)
703                                        (family
704                                        GlobalProtocol
705                                        (family OrderedCombineOperation payload)
706                                        payload
707                                        (family ProtocolNoDecision))
708                                        (constructor
709                                        OrderedCombineFailure
710                                        CombineProtocolRefused
711                                        error)))
712                                        (branch
713                                        StdSuccess
714                                        value
715                                        .
716                                        (constructor
717                                        StdResult
718                                        StdSuccess
719                                        (family OrderedCombineFailure)
720                                        (family
721                                        GlobalProtocol
722                                        (family OrderedCombineOperation payload)
723                                        payload
724                                        (family ProtocolNoDecision))
725                                        program)))))))))))))))))))))))
726
727def planOrderedCombineAndReplicate =
728  (lambda erased payload : Type 0 .
729    (lambda unrestricted participants : Nat .
730      (lambda unrestricted members : (family CombineCoverage) .
731        (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
732          (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
733            (lambda unrestricted local : (pi unrestricted role : Nat . (pi unrestricted operation : (family OrderedCombineOperation payload) . Nat)) .
734              (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
735                (planOrderedCombineAndDeliver
736                  payload
737                  participants
738                  members
739                  baseAnchor
740                  binding
741                  local
742                  transfer
743                  (constructor CombineDelivery CombineReplicateAll)))))))))
744
745-- Numeric specialization checks its declared realization before constructing
746-- any participant. Generic non-numeric payloads retain the underlying planner.
747def planNumericalCombineAndDeliver =
748  (lambda erased payload : Type 0 .
749    (lambda unrestricted required : (family NumericalContract) .
750      (lambda unrestricted realized : (family NumericalContract) .
751        (lambda unrestricted participants : Nat .
752          (lambda unrestricted members : (family CombineCoverage) .
753            (lambda unrestricted anchor : (family RegionTransferIdentity) .
754              (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
755                (lambda unrestricted local : (pi unrestricted role : Nat . (pi unrestricted operation : (family OrderedCombineOperation payload) . Nat)) .
756                  (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
757                    (lambda unrestricted delivery : (family CombineDelivery) .
758                      (lambda unrestricted tree : (family OrderedCombineTree) .
759                        (lambda unrestricted tail : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
760                          (eliminate
761                            StdResult
762                            (lambda unrestricted current : (family StdResult (family NumericalFailure) Nat) .
763                              (family
764                                StdResult
765                                (family OrderedCombineFailure)
766                                (family
767                                  GlobalProtocol
768                                  (family OrderedCombineOperation payload)
769                                  payload
770                                  (family ProtocolNoDecision))))
771                            (numericalCompatibility required realized)
772                            (branch
773                              StdFailure
774                              error
775                              .
776                              (constructor
777                                StdResult
778                                StdFailure
779                                (family OrderedCombineFailure)
780                                (family
781                                  GlobalProtocol
782                                  (family OrderedCombineOperation payload)
783                                  payload
784                                  (family ProtocolNoDecision))
785                                (constructor OrderedCombineFailure CombineNumericalRefused error)))
786                            (branch
787                              StdSuccess
788                              admitted
789                              .
790                              (combineRequire
791                                (family
792                                  GlobalProtocol
793                                  (family OrderedCombineOperation payload)
794                                  payload
795                                  (family ProtocolNoDecision))
796                                (naturalEqual
797                                  (bytes-length (numericalExactContractDigest required))
798                                  32)
799                                (constructor OrderedCombineFailure CombineIdentityUnavailable)
800                                (planOrderedCombineAndDeliver
801                                  payload
802                                  participants
803                                  members
804                                  (combineNumericalAnchor required anchor)
805                                  binding
806                                  local
807                                  transfer
808                                  delivery
809                                  tree
810                                  tail))))))))))))))))
811
812def planNumericalCombineAndReplicate =
813  (lambda erased payload : Type 0 .
814    (lambda unrestricted required : (family NumericalContract) .
815      (lambda unrestricted realized : (family NumericalContract) .
816        (lambda unrestricted participants : Nat .
817          (lambda unrestricted members : (family CombineCoverage) .
818            (lambda unrestricted anchor : (family RegionTransferIdentity) .
819              (lambda unrestricted binding : (pi unrestricted stage : (family CombineStage) . (pi unrestricted source : (family CombineReference) . (pi unrestricted destination : (family CombineReference) . (pi unrestricted identity : (family RegionTransferIdentity) . payload)))) .
820                (lambda unrestricted local : (pi unrestricted role : Nat . (pi unrestricted operation : (family OrderedCombineOperation payload) . Nat)) .
821                  (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
822                    (planNumericalCombineAndDeliver
823                      payload
824                      required
825                      realized
826                      participants
827                      members
828                      anchor
829                      binding
830                      local
831                      transfer
832                      (constructor CombineDelivery CombineReplicateAll)))))))))))