1module Runtime.NativeCombine
2
3import Runtime.OrderedCombine
4import Compiler.Planning.OrderedCombine
5import Runtime.Protocol
6import Compiler.Planning.Protocol
7import Runtime.NativeProtocol
8import Runtime.RegionTransfer
9import Runtime.RegionFrame
10import Compiler.Planning.RegionFrame
11import Runtime.NativeRegionFrame
12import Runtime.NativePeerEndpoint
13import Runtime.NativeMemoryPlan
14import Runtime.NativeLaunchRecipeLoad
15import Runtime.NativePhysicalProgram
16import Runtime.ArenaCertificate
17import Representation.ParticipantTree
18import Learning.Numerics
19import Data.Bytes
20import Std.Foundation
21import Std.List
22import Std.Natural
23
24-- The native realization of an ordered combine and replication
25-- (Runtime.OrderedCombine, Compiler.Planning.OrderedCombine) for one role.
26--
27-- The caller supplies the numerical tree, its anchor, the payload extent of
28-- one value, where in the arena the combine lives, the leaf value's address,
29-- the arithmetic that combines two values (`apply out left right`) and the
30-- descriptor of each peer's connection. This owner supplies everything that
31-- follows from the tree: the reduce and replicate global protocol and this
32-- role's projection, one frame per payload identity the role exchanges, the
33-- address of every logical reference the role holds, and the local and
34-- transfer commands. After the projected protocol runs, the role's leaf
35-- reference holds the replicated root value.
36--
37-- Placement: `base` begins the frames (one stride per payload identity, in
38-- the projection's payload order), then the role's local value slots in
39-- combineLocalSlots order. A reference the role does not hold maps to the
40-- end of that region, outside every admitted resident, so admission refuses
41-- it. Sharing: the global protocol, its projection and the payload list are
42-- computed once per context and reused for every frame lookup, because
43-- rebuilding them per address repeats hashing and traversal.
44family NativeCombineContext : Type 0
45constructor NativeCombineContextOf
46field unrestricted nativeCombineRoleValue : Nat
47field unrestricted nativeCombineTreeValue : (family OrderedCombineTree)
48field unrestricted nativeCombineDigestValue : Bytes
49field unrestricted nativeCombineAnchorValue : (family RegionTransferIdentity)
50field unrestricted nativeCombineGlobalValue : (family GlobalProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision))
51field unrestricted nativeCombineProjectedValue : (family ParticipantProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision))
52field unrestricted nativeCombinePayloadsValue : (family StdList (family RegionTransferIdentity))
53
54end-family
55
56family NativeCombinePlacement : Type 0
57constructor NativeCombinePlacementOf
58field unrestricted nativeCombineContextValue : (family NativeCombineContext)
59field unrestricted nativeCombineBaseValue : Nat
60field unrestricted nativeCombineValueBytes : Nat
61
62end-family
63
64def nativeCombineRole =
65 (lambda unrestricted context : (family NativeCombineContext) .
66 (eliminate
67 NativeCombineContext
68 (lambda unrestricted current : (family NativeCombineContext) . Nat)
69 context
70 (branch NativeCombineContextOf role tree digest anchor global projected payloads . role)))
71
72def nativeCombineTree =
73 (lambda unrestricted context : (family NativeCombineContext) .
74 (eliminate
75 NativeCombineContext
76 (lambda unrestricted current : (family NativeCombineContext) . (family OrderedCombineTree))
77 context
78 (branch NativeCombineContextOf role tree digest anchor global projected payloads . tree)))
79
80def nativeCombineDigest =
81 (lambda unrestricted context : (family NativeCombineContext) .
82 (eliminate
83 NativeCombineContext
84 (lambda unrestricted current : (family NativeCombineContext) . Bytes)
85 context
86 (branch NativeCombineContextOf role tree digest anchor global projected payloads . digest)))
87
88def nativeCombineAnchor =
89 (lambda unrestricted context : (family NativeCombineContext) .
90 (eliminate
91 NativeCombineContext
92 (lambda unrestricted current : (family NativeCombineContext) .
93 (family RegionTransferIdentity))
94 context
95 (branch NativeCombineContextOf role tree digest anchor global projected payloads . anchor)))
96
97def nativeCombineGlobal =
98 (lambda unrestricted context : (family NativeCombineContext) .
99 (eliminate
100 NativeCombineContext
101 (lambda unrestricted current : (family NativeCombineContext) .
102 (family
103 GlobalProtocol
104 (family OrderedCombineOperation (family RegionTransferIdentity))
105 (family RegionTransferIdentity)
106 (family ProtocolNoDecision)))
107 context
108 (branch NativeCombineContextOf role tree digest anchor global projected payloads . global)))
109
110def nativeCombineProjected =
111 (lambda unrestricted context : (family NativeCombineContext) .
112 (eliminate
113 NativeCombineContext
114 (lambda unrestricted current : (family NativeCombineContext) .
115 (family
116 ParticipantProtocol
117 (family OrderedCombineOperation (family RegionTransferIdentity))
118 (family RegionTransferIdentity)
119 (family ProtocolNoDecision)))
120 context
121 (branch NativeCombineContextOf role tree digest anchor global projected payloads . projected)))
122
123def nativeCombinePayloads =
124 (lambda unrestricted context : (family NativeCombineContext) .
125 (eliminate
126 NativeCombineContext
127 (lambda unrestricted current : (family NativeCombineContext) .
128 (family StdList (family RegionTransferIdentity)))
129 context
130 (branch NativeCombineContextOf role tree digest anchor global projected payloads . payloads)))
131
132def nativeCombinePlacementContext =
133 (lambda unrestricted placement : (family NativeCombinePlacement) .
134 (eliminate
135 NativeCombinePlacement
136 (lambda unrestricted current : (family NativeCombinePlacement) .
137 (family NativeCombineContext))
138 placement
139 (branch NativeCombinePlacementOf context base bytes . context)))
140
141def nativeCombineBase =
142 (lambda unrestricted placement : (family NativeCombinePlacement) .
143 (eliminate
144 NativeCombinePlacement
145 (lambda unrestricted current : (family NativeCombinePlacement) . Nat)
146 placement
147 (branch NativeCombinePlacementOf context base bytes . base)))
148
149def nativeCombineBytes =
150 (lambda unrestricted placement : (family NativeCombinePlacement) .
151 (eliminate
152 NativeCombinePlacement
153 (lambda unrestricted current : (family NativeCombinePlacement) . Nat)
154 placement
155 (branch NativeCombinePlacementOf context base bytes . bytes)))
156
157-- A transfer's payload is its canonical identity; the frame is found by it.
158def nativeCombineBinding =
159 (lambda unrestricted stage : (family CombineStage) .
160 (lambda unrestricted source : (family CombineReference) .
161 (lambda unrestricted destination : (family CombineReference) .
162 (lambda unrestricted identity : (family RegionTransferIdentity) . identity))))
163
164def nativeCombineEnd =
165 (constructor
166 GlobalProtocol
167 GlobalProtocolEnd
168 (family OrderedCombineOperation (family RegionTransferIdentity))
169 (family RegionTransferIdentity)
170 (family ProtocolNoDecision))
171
172-- Reduce the tree, then deliver the root value (to every leaf owner, or
173-- along the path to one), projected for `role`.
174def nativeCombineDeliveringContextFor =
175 (lambda unrestricted anchor : (family RegionTransferIdentity) .
176 (lambda unrestricted delivery : (family CombineDelivery) .
177 (lambda unrestricted role : Nat .
178 (lambda unrestricted tree : (family OrderedCombineTree) .
179 (let unrestricted digest =
180 (combineTreeDigest tree)
181 in
182 (let unrestricted global =
183 (compileOrderedCombine
184 (family RegionTransferIdentity)
185 anchor
186 digest
187 nativeCombineBinding
188 tree
189 0
190 (compileTreeDelivery
191 (family RegionTransferIdentity)
192 anchor
193 digest
194 nativeCombineBinding
195 delivery
196 tree
197 0
198 nativeCombineEnd))
199 in
200 (let unrestricted projected =
201 (projectGlobalProtocol
202 (family OrderedCombineOperation (family RegionTransferIdentity))
203 (family RegionTransferIdentity)
204 (family ProtocolNoDecision)
205 role
206 global)
207 in
208 (constructor
209 NativeCombineContext
210 NativeCombineContextOf
211 role
212 tree
213 digest
214 anchor
215 global
216 projected
217 (participantProtocolPayloads
218 (family OrderedCombineOperation (family RegionTransferIdentity))
219 (family RegionTransferIdentity)
220 (family ProtocolNoDecision)
221 projected)))))))))
222
223-- Reduce then replicate the tree, projected for `role`.
224def nativeCombineContextFor =
225 (lambda unrestricted anchor : (family RegionTransferIdentity) .
226 (nativeCombineDeliveringContextFor anchor (constructor CombineDelivery CombineReplicateAll)))
227
228-- The same tree and global protocol, projected for another role (admission
229-- checks both ends of every transfer).
230def nativeCombineForRole =
231 (lambda unrestricted context : (family NativeCombineContext) .
232 (lambda unrestricted role : Nat .
233 (nat-eliminate
234 (lambda unrestricted flag : Nat . (family NativeCombineContext))
235 (let unrestricted projected =
236 (projectGlobalProtocol
237 (family OrderedCombineOperation (family RegionTransferIdentity))
238 (family RegionTransferIdentity)
239 (family ProtocolNoDecision)
240 role
241 (nativeCombineGlobal context))
242 in
243 (constructor
244 NativeCombineContext
245 NativeCombineContextOf
246 role
247 (nativeCombineTree context)
248 (nativeCombineDigest context)
249 (nativeCombineAnchor context)
250 (nativeCombineGlobal context)
251 projected
252 (participantProtocolPayloads
253 (family OrderedCombineOperation (family RegionTransferIdentity))
254 (family RegionTransferIdentity)
255 (family ProtocolNoDecision)
256 projected)))
257 (lambda unrestricted prior : Nat .
258 (lambda unrestricted ignored : (family NativeCombineContext) . context))
259 (naturalEqual role (nativeCombineRole context)))))
260
261def nativeCombineForPlacementRole =
262 (lambda unrestricted placement : (family NativeCombinePlacement) .
263 (lambda unrestricted role : Nat .
264 (constructor
265 NativeCombinePlacement
266 NativeCombinePlacementOf
267 (nativeCombineForRole (nativeCombinePlacementContext placement) role)
268 (nativeCombineBase placement)
269 (nativeCombineBytes placement))))
270
271-- One frame per payload identity, laid out at a common stride: identities of
272-- one tree have the same canonical shape, so one prototype sizes them all.
273def nativeCombinePrototype =
274 (lambda unrestricted context : (family NativeCombineContext) .
275 (combineTransferIdentity
276 (nativeCombineAnchor context)
277 (nativeCombineDigest context)
278 (constructor CombineStage CombineReduce)
279 (combineReference 0 0 0)
280 (combineReference 1 2 1)))
281
282def nativeCombineLayoutAt =
283 (lambda unrestricted bytes : Nat .
284 (lambda unrestricted identity : (family RegionTransferIdentity) .
285 (lambda unrestricted base : Nat .
286 (stdResultValueOr
287 (family RegionFrameLayoutFailure)
288 (family RegionFrameLayout)
289 (constructor RegionFrameLayout RegionFrameLayoutOf b"" 0 0 b"")
290 (planRegionFrameLayout identity bytes 512 base 1073741824)))))
291
292def nativeCombineStride =
293 (lambda unrestricted placement : (family NativeCombinePlacement) .
294 (frameAlign
295 (frameEnd
296 (nativeCombineLayoutAt
297 (nativeCombineBytes placement)
298 (nativeCombinePrototype (nativeCombinePlacementContext placement))
299 0))))
300
301def nativeCombineFrameCount =
302 (lambda unrestricted placement : (family NativeCombinePlacement) .
303 (stdListLength
304 (family RegionTransferIdentity)
305 (nativeCombinePayloads (nativeCombinePlacementContext placement))))
306
307def nativeCombineFrameIndex =
308 (lambda unrestricted placement : (family NativeCombinePlacement) .
309 (lambda unrestricted identity : (family RegionTransferIdentity) .
310 (app
311 (eliminate
312 StdList
313 (lambda unrestricted current : (family StdList (family RegionTransferIdentity)) .
314 (pi unrestricted index : Nat . Nat))
315 (nativeCombinePayloads (nativeCombinePlacementContext placement))
316 (branch StdListEmpty . (lambda unrestricted index : Nat . index))
317 (branch
318 StdListCons
319 head
320 rest
321 induction
322 .
323 (lambda unrestricted index : Nat .
324 (nat-eliminate
325 (lambda unrestricted flag : Nat . Nat)
326 (induction (naturalAdd index 1))
327 (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . index))
328 (regionTransferIdentityEqual identity head)))))
329 0)))
330
331def nativeCombineFrame =
332 (lambda unrestricted placement : (family NativeCombinePlacement) .
333 (lambda unrestricted identity : (family RegionTransferIdentity) .
334 (nativeCombineLayoutAt
335 (nativeCombineBytes placement)
336 identity
337 (naturalAdd
338 (nativeCombineBase placement)
339 (naturalMultiply
340 (nativeCombineStride placement)
341 (nativeCombineFrameIndex placement identity))))))
342
343def nativeCombineValuesAt =
344 (lambda unrestricted placement : (family NativeCombinePlacement) .
345 (naturalAdd
346 (nativeCombineBase placement)
347 (naturalMultiply (nativeCombineStride placement) (nativeCombineFrameCount placement))))
348
349def nativeCombineRegionEnd =
350 (lambda unrestricted placement : (family NativeCombinePlacement) .
351 (naturalAdd
352 (nativeCombineValuesAt placement)
353 (naturalMultiply
354 (nativeCombineBytes placement)
355 (stdListLength
356 Nat
357 (combineLocalSlots
358 (nativeCombineRole (nativeCombinePlacementContext placement))
359 (nativeCombineTree (nativeCombinePlacementContext placement)))))))
360
361def nativeCombineAddress =
362 (lambda unrestricted placement : (family NativeCombinePlacement) .
363 (lambda unrestricted reference : (family CombineReference) .
364 (eliminate
365 StdOption
366 (lambda unrestricted current : (family StdOption Nat) . Nat)
367 (combineReferenceIndex
368 (nativeCombineRole (nativeCombinePlacementContext placement))
369 (nativeCombineTree (nativeCombinePlacementContext placement))
370 reference)
371 (branch StdNone . (nativeCombineRegionEnd placement))
372 (branch
373 StdSome
374 index
375 .
376 (naturalAdd
377 (nativeCombineValuesAt placement)
378 (naturalMultiply (nativeCombineBytes placement) index))))))
379
380def nativeCombineReferenceValid =
381 (lambda unrestricted placement : (family NativeCombinePlacement) .
382 (lambda unrestricted reference : (family CombineReference) .
383 (naturalLess (nativeCombineAddress placement reference) (nativeCombineRegionEnd placement))))
384
385-- The reference holding `role`'s own leaf value: after replication it holds
386-- the root value.
387def nativeCombineLeafReferenceFrom =
388 (lambda unrestricted role : Nat .
389 (lambda unrestricted tree : (family OrderedCombineTree) .
390 (eliminate
391 OrderedCombineTree
392 (lambda unrestricted current : (family OrderedCombineTree) .
393 (pi unrestricted base : Nat . (family CombineReference)))
394 tree
395 (branch
396 OrderedCombineLeaf
397 owner
398 .
399 (lambda unrestricted base : Nat . (combineReference owner base 0)))
400 (branch
401 OrderedCombineBranch
402 owner
403 left
404 right
405 leftResult
406 rightResult
407 .
408 (lambda unrestricted base : Nat .
409 (nat-eliminate
410 (lambda unrestricted flag : Nat . (family CombineReference))
411 (rightResult (naturalAdd base (combineNodeCount left)))
412 (lambda unrestricted prior : Nat .
413 (lambda unrestricted ignored : (family CombineReference) . (leftResult base)))
414 (combineContains role (combineLeaves left))))))))
415
416def nativeCombineResultAt =
417 (lambda unrestricted placement : (family NativeCombinePlacement) .
418 (nativeCombineAddress
419 placement
420 (nativeCombineLeafReferenceFrom
421 (nativeCombineRole (nativeCombinePlacementContext placement))
422 (nativeCombineTree (nativeCombinePlacementContext placement))
423 0)))
424
425def nativeCombineCopy =
426 (lambda unrestricted placement : (family NativeCombinePlacement) .
427 (lambda unrestricted source : Nat .
428 (lambda unrestricted destination : Nat .
429 (nativeMemoryCopyOperands
430 (nativeMemoryState destination)
431 (nativeMemoryState source)
432 (nativeCombineBytes placement)
433 0
434 b"combine-copy"))))
435
436-- Local work: the leaf reads `leafAt`; branches apply the caller's arithmetic.
437def nativeCombineLocal =
438 (lambda unrestricted placement : (family NativeCombinePlacement) .
439 (lambda unrestricted leafAt : Nat .
440 (lambda unrestricted apply : (pi unrestricted out : Nat . (pi unrestricted left : Nat . (pi unrestricted right : Nat . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) .
441 (lambda unrestricted operation : (family OrderedCombineOperation (family RegionTransferIdentity)) .
442 (eliminate
443 OrderedCombineOperation
444 (lambda unrestricted current : (family OrderedCombineOperation (family RegionTransferIdentity)) .
445 (pi unrestricted tail : (family NativePhysicalCommands) .
446 (family NativePhysicalCommands)))
447 operation
448 (branch
449 CombineReadLeaf
450 destination
451 .
452 (nativeCombineCopy placement leafAt (nativeCombineAddress placement destination)))
453 (branch
454 CombineCopy
455 source
456 destination
457 .
458 (nativeCombineCopy
459 placement
460 (nativeCombineAddress placement source)
461 (nativeCombineAddress placement destination)))
462 (branch
463 CombineApply
464 left
465 right
466 destination
467 .
468 (apply
469 (nativeCombineAddress placement destination)
470 (nativeCombineAddress placement left)
471 (nativeCombineAddress placement right)))
472 (branch
473 CombinePrepare
474 source
475 identity
476 .
477 (nativeCombineCopy
478 placement
479 (nativeCombineAddress placement source)
480 (framePayloadAt (nativeCombineFrame placement identity))))
481 (branch
482 CombineConsume
483 identity
484 destination
485 .
486 (lambda unrestricted tail : (family NativePhysicalCommands) .
487 (let unrestricted frame =
488 (nativeCombineFrame placement identity)
489 in
490 (nativeFrameConsume
491 frame
492 (nativeCombineCopy
493 placement
494 (framePayloadAt frame)
495 (nativeCombineAddress placement destination)
496 (nativeFrameAdvance
497 frame
498 (constructor NativeFrameTerminal NativeFrameConsumeComplete)
499 0
500 tail)))))))))))
501
502def nativeCombineTransfer =
503 (lambda unrestricted placement : (family NativeCombinePlacement) .
504 (lambda unrestricted descriptor : (pi unrestricted peer : Nat . (family NativePhysicalOperand)) .
505 (lambda unrestricted direction : (family ProtocolDirection) .
506 (lambda unrestricted identity : (family RegionTransferIdentity) .
507 (lambda unrestricted value : (family RegionTransferIdentity) .
508 (lambda unrestricted tail : (family NativePhysicalCommands) .
509 (let unrestricted frame =
510 (nativeCombineFrame placement value)
511 in
512 (eliminate
513 ProtocolDirection
514 (lambda unrestricted current : (family ProtocolDirection) .
515 (family NativePhysicalCommands))
516 direction
517 (branch
518 ProtocolSend
519 .
520 (nativePeerIO
521 (descriptor (regionTransferReceiver identity))
522 1
523 frame
524 (nativeFrameAdvance
525 frame
526 (constructor NativeFrameTerminal NativeFrameSendComplete)
527 0
528 tail)))
529 (branch
530 ProtocolReceive
531 .
532 (nativePeerIO (descriptor (regionTransferSender identity)) 0 frame tail))))))))))
533
534def nativeCombineDecisions =
535 (lambda unrestricted placement : (family NativeCombinePlacement) .
536 (constructor
537 NativeProtocolDecisionBinding
538 NativeProtocolDecisionBindingOf
539 (family ProtocolNoDecision)
540 (family RegionTransferIdentity)
541 (lambda unrestricted selector : (family ProtocolNoDecision) .
542 (eliminate
543 ProtocolNoDecision
544 (lambda unrestricted current : (family ProtocolNoDecision) .
545 (family NativePhysicalOperand))
546 selector))
547 (lambda unrestricted selector : (family ProtocolNoDecision) .
548 (eliminate
549 ProtocolNoDecision
550 (lambda unrestricted current : (family ProtocolNoDecision) . Nat)
551 selector))
552 0
553 (nativeCombineFrame placement)))
554
555def nativeCombineInitialize =
556 (lambda unrestricted placement : (family NativeCombinePlacement) .
557 (lambda unrestricted program : (family ParticipantProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision)) .
558 (nativeProtocolFrames
559 (family OrderedCombineOperation (family RegionTransferIdentity))
560 (family RegionTransferIdentity)
561 (family ProtocolNoDecision)
562 (lambda unrestricted direction : (family ProtocolDirection) .
563 (lambda unrestricted identity : (family RegionTransferIdentity) .
564 (lambda unrestricted value : (family RegionTransferIdentity) .
565 (nativeFrameInitialize (nativeCombineFrame placement value)))))
566 program)))
567
568-- ---- admission ----
569def nativeCombineLocalAdmitted =
570 (lambda unrestricted placement : (family NativeCombinePlacement) .
571 (lambda unrestricted role : Nat .
572 (let unrestricted placement =
573 (nativeCombineForPlacementRole placement role)
574 in
575 (lambda unrestricted operation : (family OrderedCombineOperation (family RegionTransferIdentity)) .
576 (eliminate
577 OrderedCombineOperation
578 (lambda unrestricted current : (family OrderedCombineOperation (family RegionTransferIdentity)) .
579 Nat)
580 operation
581 (branch
582 CombineReadLeaf
583 destination
584 .
585 (nativeCombineReferenceValid placement destination))
586 (branch
587 CombineCopy
588 source
589 destination
590 .
591 (naturalAnd
592 (nativeCombineReferenceValid placement source)
593 (nativeCombineReferenceValid placement destination)))
594 (branch
595 CombineApply
596 left
597 right
598 destination
599 .
600 (naturalAnd
601 (nativeCombineReferenceValid placement left)
602 (naturalAnd
603 (nativeCombineReferenceValid placement right)
604 (nativeCombineReferenceValid placement destination))))
605 (branch
606 CombinePrepare
607 source
608 identity
609 .
610 (naturalAnd
611 (nativeCombineReferenceValid placement source)
612 (naturalLess
613 (nativeCombineFrameIndex placement identity)
614 (nativeCombineFrameCount placement))))
615 (branch
616 CombineConsume
617 identity
618 destination
619 .
620 (naturalAnd
621 (nativeCombineReferenceValid placement destination)
622 (naturalLess
623 (nativeCombineFrameIndex placement identity)
624 (nativeCombineFrameCount placement)))))))))
625
626def nativeCombineTransferAdmitted =
627 (lambda unrestricted placement : (family NativeCombinePlacement) .
628 (lambda unrestricted identity : (family RegionTransferIdentity) .
629 (lambda unrestricted value : (family RegionTransferIdentity) .
630 (let unrestricted sender =
631 (nativeCombineForPlacementRole placement (regionTransferSender identity))
632 in
633 (let unrestricted receiver =
634 (nativeCombineForPlacementRole placement (regionTransferReceiver identity))
635 in
636 (naturalAnd
637 (regionTransferIdentityEqual identity value)
638 (naturalAnd
639 (naturalLess
640 (nativeCombineFrameIndex sender identity)
641 (nativeCombineFrameCount sender))
642 (naturalAnd
643 (naturalLess
644 (nativeCombineFrameIndex receiver identity)
645 (nativeCombineFrameCount receiver))
646 (naturalAnd
647 (nativeProtocolFrameAdmitted identity (nativeCombineFrame sender identity))
648 (nativeProtocolFrameAdmitted identity (nativeCombineFrame receiver identity)))))))))))
649
650-- Every frame and the local value slots of this role; `tail` continues the
651-- caller's residents.
652def nativeCombineResidents =
653 (lambda unrestricted placement : (family NativeCombinePlacement) .
654 (lambda unrestricted tail : (family ArenaResidents) .
655 (stdListFold
656 (family RegionTransferIdentity)
657 (family ArenaResidents)
658 (lambda unrestricted identity : (family RegionTransferIdentity) .
659 (lambda unrestricted rest : (family ArenaResidents) .
660 (let unrestricted frame =
661 (nativeCombineFrame placement identity)
662 in
663 (constructor
664 ArenaResidents
665 ArenaResidentsNext
666 (constructor
667 ArenaResident
668 ArenaResidentValue
669 b"combine-frame"
670 (frameBase frame)
671 (naturalSaturatingSubtract (frameEnd frame) (frameBase frame))
672 8)
673 rest))))
674 (constructor
675 ArenaResidents
676 ArenaResidentsNext
677 (constructor
678 ArenaResident
679 ArenaResidentValue
680 b"combine-local-values"
681 (nativeCombineValuesAt placement)
682 (naturalSaturatingSubtract
683 (nativeCombineRegionEnd placement)
684 (nativeCombineValuesAt placement))
685 8)
686 tail)
687 (nativeCombinePayloads (nativeCombinePlacementContext placement)))))
688
689-- The left-deep ordered sum of leaves 0..count-1 combined at `owner`:
690-- (((l0 + l1) + l2) + ...). Every transfer is between `owner` and a leaf,
691-- so it runs over a star whose centre is `owner`.
692def nativeCombineChain =
693 (lambda unrestricted owner : Nat .
694 (lambda unrestricted count : Nat .
695 (stdListFold
696 Nat
697 (pi unrestricted acc : (family OrderedCombineTree) . (family OrderedCombineTree))
698 (lambda unrestricted leaf : Nat .
699 (lambda unrestricted next : (pi unrestricted acc : (family OrderedCombineTree) . (family OrderedCombineTree)) .
700 (lambda unrestricted acc : (family OrderedCombineTree) .
701 (next
702 (constructor
703 OrderedCombineTree
704 OrderedCombineBranch
705 owner
706 acc
707 (constructor OrderedCombineTree OrderedCombineLeaf (succ leaf)))))))
708 (lambda unrestricted acc : (family OrderedCombineTree) . acc)
709 (stdListNaturalsBelow (naturalPredecessor count))
710 (constructor OrderedCombineTree OrderedCombineLeaf 0))))
711
712-- The ordered sum over a bounded-fan-out hierarchy
713-- (Representation.ParticipantTree): a node's value is its own leaf followed
714-- by each child's subtree value in role order, combined left-deep at the node:
715-- S(p) = ((l_p + S(c1)) + S(c2)) + ...
716-- Every transfer is between a node and one of its children, so reduction and
717-- replication run over the hierarchy's edges and no participant combines
718-- more than fanout + 1 values. With fan-out count - 1 it is the chain at 0.
719def nativeCombineHierarchy =
720 (lambda unrestricted fanout : Nat .
721 (lambda unrestricted count : Nat .
722 (let unrestricted subtree =
723 (nat-eliminate
724 (lambda unrestricted fuel : Nat .
725 (pi unrestricted node : (family ParticipantTreeNode) . (family OrderedCombineTree)))
726 (lambda unrestricted node : (family ParticipantTreeNode) .
727 (constructor OrderedCombineTree OrderedCombineLeaf (participantTreeRoleOf node)))
728 (lambda unrestricted fuel : Nat .
729 (lambda unrestricted below : (pi unrestricted node : (family ParticipantTreeNode) . (family OrderedCombineTree)) .
730 (lambda unrestricted node : (family ParticipantTreeNode) .
731 (let unrestricted role =
732 (participantTreeRoleOf node)
733 in
734 (stdListFold
735 (family ParticipantTreeNode)
736 (pi unrestricted acc : (family OrderedCombineTree) .
737 (family OrderedCombineTree))
738 (lambda unrestricted child : (family ParticipantTreeNode) .
739 (lambda unrestricted next : (pi unrestricted acc : (family OrderedCombineTree) . (family OrderedCombineTree)) .
740 (lambda unrestricted acc : (family OrderedCombineTree) .
741 (next
742 (constructor
743 OrderedCombineTree
744 OrderedCombineBranch
745 role
746 acc
747 (below child))))))
748 (lambda unrestricted acc : (family OrderedCombineTree) . acc)
749 (participantTreeChildren fanout node)
750 (constructor OrderedCombineTree OrderedCombineLeaf role))))))
751 (participantTreeFuel fanout count))
752 in
753 (subtree (participantTreeRoot count)))))
754
755-- The reduce-and-deliver global protocol under an admitted numerical
756-- contract, for a caller composing it into a larger round; the delivery
757-- must be the placement context's.
758def planNativeCombineGlobalDelivering =
759 (lambda unrestricted placement : (family NativeCombinePlacement) .
760 (lambda unrestricted delivery : (family CombineDelivery) .
761 (lambda unrestricted required : (family NumericalContract) .
762 (lambda unrestricted participants : Nat .
763 (lambda unrestricted members : (family CombineCoverage) .
764 (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
765 (planNumericalCombineAndDeliver
766 (family RegionTransferIdentity)
767 required
768 required
769 participants
770 members
771 baseAnchor
772 nativeCombineBinding
773 (nativeCombineLocalAdmitted placement)
774 (nativeCombineTransferAdmitted placement)
775 delivery
776 (nativeCombineTree (nativeCombinePlacementContext placement))
777 nativeCombineEnd)))))))
778
779-- The reduce-and-replicate global protocol under an admitted numerical
780-- contract, for a caller composing it into a larger round.
781def planNativeCombineGlobal =
782 (lambda unrestricted placement : (family NativeCombinePlacement) .
783 (planNativeCombineGlobalDelivering placement (constructor CombineDelivery CombineReplicateAll)))
784
785-- Plan, check and project the reduce-and-replicate protocol for `rounds`
786-- repetitions under an admitted numerical contract; the caller emits it with
787-- nativeProtocolCommands and the callbacks above.
788def planNativeCombineRounds =
789 (lambda unrestricted placement : (family NativeCombinePlacement) .
790 (lambda unrestricted required : (family NumericalContract) .
791 (lambda unrestricted participants : Nat .
792 (lambda unrestricted members : (family CombineCoverage) .
793 (lambda unrestricted baseAnchor : (family RegionTransferIdentity) .
794 (lambda unrestricted rounds : Nat .
795 (stdResultBind
796 (family OrderedCombineFailure)
797 (family
798 GlobalProtocol
799 (family OrderedCombineOperation (family RegionTransferIdentity))
800 (family RegionTransferIdentity)
801 (family ProtocolNoDecision))
802 (family
803 ParticipantProtocol
804 (family OrderedCombineOperation (family RegionTransferIdentity))
805 (family RegionTransferIdentity)
806 (family ProtocolNoDecision))
807 (planNumericalCombineAndReplicate
808 (family RegionTransferIdentity)
809 required
810 required
811 participants
812 members
813 baseAnchor
814 nativeCombineBinding
815 (nativeCombineLocalAdmitted placement)
816 (nativeCombineTransferAdmitted placement)
817 (nativeCombineTree (nativeCombinePlacementContext placement))
818 nativeCombineEnd)
819 (lambda unrestricted global : (family GlobalProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision)) .
820 (eliminate
821 StdResult
822 (lambda unrestricted result : (family StdResult (family ProtocolFailure) (family ParticipantProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision))) .
823 (family
824 StdResult
825 (family OrderedCombineFailure)
826 (family
827 ParticipantProtocol
828 (family OrderedCombineOperation (family RegionTransferIdentity))
829 (family RegionTransferIdentity)
830 (family ProtocolNoDecision))))
831 (planParticipantProtocol
832 (family OrderedCombineOperation (family RegionTransferIdentity))
833 (family RegionTransferIdentity)
834 (family ProtocolNoDecision)
835 participants
836 (nativeCombineRole (nativeCombinePlacementContext placement))
837 (nativeCombineLocalAdmitted placement)
838 (nativeCombineTransferAdmitted placement)
839 (protocolNoDecision (family RegionTransferIdentity))
840 (protocolRepeat
841 (family OrderedCombineOperation (family RegionTransferIdentity))
842 (family RegionTransferIdentity)
843 (family ProtocolNoDecision)
844 rounds
845 global
846 nativeCombineEnd))
847 (branch
848 StdFailure
849 failure
850 .
851 (constructor
852 StdResult
853 StdFailure
854 (family OrderedCombineFailure)
855 (family
856 ParticipantProtocol
857 (family OrderedCombineOperation (family RegionTransferIdentity))
858 (family RegionTransferIdentity)
859 (family ProtocolNoDecision))
860 (constructor OrderedCombineFailure CombineProtocolRefused failure)))
861 (branch
862 StdSuccess
863 projected
864 .
865 (constructor
866 StdResult
867 StdSuccess
868 (family OrderedCombineFailure)
869 (family
870 ParticipantProtocol
871 (family OrderedCombineOperation (family RegionTransferIdentity))
872 (family RegionTransferIdentity)
873 (family ProtocolNoDecision))
874 projected)))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.