1module PartitionedRegression.CoordinateHost
2
3import PartitionedRegression.Coordinates
4import Checkpoint.Envelope
5import Checkpoint.NativeEnvelope
6import Checkpoint.NativeRegions
7import Checkpoint.NativePeerPublication
8import Checkpoint.RegionManifest
9import Compiler.Planning.Protocol
10import Compiler.Planning.OrderedCombine
11import Runtime.OrderedCombine
12import Learning.Numerics
13import Std.Numeric.Profile
14import Runtime.Protocol
15import Runtime.NativeProtocol
16import Compiler.Planning.RegionFrame
17import Runtime.ArenaCertificate
18import Runtime.NativeFloatPlan
19import Runtime.NativePeerEndpoint
20import Runtime.NativeFilePlan
21import Runtime.NativeMemoryPlan
22import Runtime.NativeWordArithmetic
23import Runtime.NativeRegionFrame
24import Runtime.NativePhysicalProgram
25import Runtime.NativePhysicalNativeELF
26import Runtime.NativeResourcePlan
27import Runtime.NativeLaunchRecipeLoad
28import Runtime.NativeSocketPlan
29import Runtime.RegionFrame
30import Runtime.RegionTransfer
31import Runtime.SocketAddress
32import Learning.Transition
33import Representation.ParticipantGroup
34import Representation.Partition
35import Model.Parameter
36import Model.Word64
37import Data.Bytes
38import Data.SHA256
39import Data.SHA256Padding
40import Std.Byte
41import Std.Foundation
42import Std.List
43import Std.Natural
44import Runtime.NativeHostTarget
45
46-- A synchronous coordinate-owned learner. Only predictions, one residual and
47-- acknowledgments cross the edge during an update. Parameters/accumulators are
48-- local live state; final capture transfers immutable bytes to the designated
49-- durable publisher. Both participant successes wait for manifest publication.
50family CoordinateHostLayout : Type 0
51constructor CoordinateHostLayoutOf
52field unrestricted chPredictionValue : (family RegionFrameLayout)
53field unrestricted chResidualValue : (family RegionFrameLayout)
54field unrestricted chAcknowledgmentValue : (family RegionFrameLayout)
55field unrestricted chCaptureValue : (family RegionFrameLayout)
56field unrestricted chCommittedValue : (family RegionFrameLayout)
57field unrestricted chCheckpointValue : (family NativeRegionCheckpoint)
58field unrestricted chNumericsValue : Bytes
59
60end-family
61
62-- Typed local work in one dependency round. Transfers are declared separately
63-- and projected, so no local operation hides a network send or receive.
64family CoordinateRoundOperation : Type 0
65constructor CoordinateCombine
66field unrestricted coordinateCombineOperation : (family OrderedCombineOperation (family RegionFrameLayout))
67constructor CoordinateInstallCombined
68constructor CoordinateBackwardUpdate
69constructor CoordinatePrepareAcknowledgment
70constructor CoordinateAcceptAcknowledgment
71
72end-family
73
74-- Prediction has a separate arena: no training frames or endpoint slots are
75-- retained. The common checkpoint plan still validates every learner shard.
76family CoordinatePredictionLayout : Type 0
77constructor CoordinatePredictionLayoutOf
78field unrestricted cpCheckpointValue : (family NativeRegionCheckpoint)
79
80end-family
81
82def chPrediction =
83 (lambda unrestricted layout : (family CoordinateHostLayout) .
84 (eliminate
85 CoordinateHostLayout
86 (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout))
87 layout
88 (branch
89 CoordinateHostLayoutOf
90 chPrediction
91 chResidual
92 chAcknowledgment
93 chCapture
94 chCommitted
95 chCheckpoint
96 numerics
97 .
98 chPrediction)))
99
100def chResidual =
101 (lambda unrestricted layout : (family CoordinateHostLayout) .
102 (eliminate
103 CoordinateHostLayout
104 (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout))
105 layout
106 (branch
107 CoordinateHostLayoutOf
108 chPrediction
109 chResidual
110 chAcknowledgment
111 chCapture
112 chCommitted
113 chCheckpoint
114 numerics
115 .
116 chResidual)))
117
118def chAcknowledgment =
119 (lambda unrestricted layout : (family CoordinateHostLayout) .
120 (eliminate
121 CoordinateHostLayout
122 (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout))
123 layout
124 (branch
125 CoordinateHostLayoutOf
126 chPrediction
127 chResidual
128 chAcknowledgment
129 chCapture
130 chCommitted
131 chCheckpoint
132 numerics
133 .
134 chAcknowledgment)))
135
136def chCapture =
137 (lambda unrestricted layout : (family CoordinateHostLayout) .
138 (eliminate
139 CoordinateHostLayout
140 (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout))
141 layout
142 (branch
143 CoordinateHostLayoutOf
144 chPrediction
145 chResidual
146 chAcknowledgment
147 chCapture
148 chCommitted
149 chCheckpoint
150 numerics
151 .
152 chCapture)))
153
154def chCommitted =
155 (lambda unrestricted layout : (family CoordinateHostLayout) .
156 (eliminate
157 CoordinateHostLayout
158 (lambda unrestricted current : (family CoordinateHostLayout) . (family RegionFrameLayout))
159 layout
160 (branch
161 CoordinateHostLayoutOf
162 chPrediction
163 chResidual
164 chAcknowledgment
165 chCapture
166 chCommitted
167 chCheckpoint
168 numerics
169 .
170 chCommitted)))
171
172def chCheckpoint =
173 (lambda unrestricted layout : (family CoordinateHostLayout) .
174 (eliminate
175 CoordinateHostLayout
176 (lambda unrestricted current : (family CoordinateHostLayout) .
177 (family NativeRegionCheckpoint))
178 layout
179 (branch
180 CoordinateHostLayoutOf
181 chPrediction
182 chResidual
183 chAcknowledgment
184 chCapture
185 chCommitted
186 chCheckpoint
187 numerics
188 .
189 chCheckpoint)))
190
191def chNumerics =
192 (lambda unrestricted layout : (family CoordinateHostLayout) .
193 (eliminate
194 CoordinateHostLayout
195 (lambda unrestricted current : (family CoordinateHostLayout) . Bytes)
196 layout
197 (branch
198 CoordinateHostLayoutOf
199 prediction
200 residual
201 acknowledgment
202 capture
203 committed
204 checkpoint
205 numerics
206 .
207 numerics)))
208
209def chFloat =
210 (nativeFloat64 b"coordinate-arithmetic")
211
212def chNatural =
213 (nativeFloat64Natural b"coordinate-arithmetic")
214
215def chBinary =
216 (nativeFloat64Binary b"coordinate-arithmetic")
217
218def chStore =
219 (nativeMemoryStoreWord64 b"coordinate-state")
220
221def chAdd =
222 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Add)
223
224def chSubtract =
225 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Subtract)
226
227def chMultiply =
228 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Multiply)
229
230def chDivide =
231 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Divide)
232
233def chEnd =
234 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
235
236def chHalt =
237 (nativeLaunchRecipeCommand
238 (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
239 b"coordinate-done"
240 chEnd)
241
242def chConnection =
243 (nativeLaunchRecipeSlotValue nativePeerConnectionSlot)
244
245def chStateBytes =
246 (naturalAdd nativeRegionCaptureBytes (naturalMultiply 2 coordinateWordBytes))
247
248def chArgument =
249 nativeRegionPathArgument
250
251-- All consumers, including GPU endpoint arguments, use the shared path layout.
252def chSavedShardCount =
253 (nativeRegionShardCount coordinatePartitions)
254
255def chManifestInputIndex : Nat =
256 1
257
258def chPaths =
259 (constructor NativeRegionPaths NativeRegionPathsOf chManifestInputIndex chSavedShardCount)
260
261def chInputShardBase =
262 (nativeRegionInputShardBase chPaths)
263
264def chOutputShardBase =
265 (nativeRegionOutputShardBase chPaths)
266
267def chManifestCandidateIndex =
268 (nativeRegionManifestCandidateIndex chPaths)
269
270def chManifestCommittedIndex =
271 (nativeRegionManifestCommittedIndex chPaths)
272
273def chDirectoryIndex =
274 (nativeRegionDirectoryIndex chPaths)
275
276def chStateAt =
277 (lambda unrestricted layout : (family CoordinateHostLayout) .
278 (nativeRegionEnd (chCheckpoint layout)))
279
280def chVersion =
281 (lambda unrestricted layout : (family CoordinateHostLayout) .
282 (naturalAdd (chStateAt layout) (naturalMultiply 0 coordinateWordBytes)))
283
284def chCursor =
285 (lambda unrestricted layout : (family CoordinateHostLayout) .
286 (naturalAdd (chStateAt layout) (naturalMultiply 1 coordinateWordBytes)))
287
288def chEpoch =
289 (lambda unrestricted layout : (family CoordinateHostLayout) .
290 (naturalAdd (chStateAt layout) (naturalMultiply 2 coordinateWordBytes)))
291
292def chWeight =
293 (lambda unrestricted layout : (family CoordinateHostLayout) .
294 (naturalAdd (chStateAt layout) (naturalMultiply 3 coordinateWordBytes)))
295
296def chAccumulator =
297 (lambda unrestricted layout : (family CoordinateHostLayout) .
298 (naturalAdd (chStateAt layout) (naturalMultiply 4 coordinateWordBytes)))
299
300def chFeature =
301 (lambda unrestricted layout : (family CoordinateHostLayout) .
302 (naturalAdd (chStateAt layout) (naturalMultiply 5 coordinateWordBytes)))
303
304def chPartial =
305 (lambda unrestricted layout : (family CoordinateHostLayout) .
306 (naturalAdd (chStateAt layout) (naturalMultiply 6 coordinateWordBytes)))
307
308def chError =
309 (lambda unrestricted layout : (family CoordinateHostLayout) .
310 (naturalAdd (chStateAt layout) (naturalMultiply 7 coordinateWordBytes)))
311
312def chGradient =
313 (lambda unrestricted layout : (family CoordinateHostLayout) .
314 (naturalAdd (chStateAt layout) (naturalMultiply 8 coordinateWordBytes)))
315
316def chDecay =
317 (lambda unrestricted layout : (family CoordinateHostLayout) .
318 (naturalAdd (chStateAt layout) (naturalMultiply 9 coordinateWordBytes)))
319
320def chRate =
321 (lambda unrestricted layout : (family CoordinateHostLayout) .
322 (naturalAdd (chStateAt layout) (naturalMultiply 10 coordinateWordBytes)))
323
324def chScratch =
325 (lambda unrestricted layout : (family CoordinateHostLayout) .
326 (naturalAdd (chStateAt layout) (naturalMultiply 11 coordinateWordBytes)))
327
328def chEndpoint =
329 (lambda unrestricted layout : (family CoordinateHostLayout) .
330 (naturalAdd (chScratch layout) coordinateWordBytes))
331
332def chExtent =
333 (lambda unrestricted layout : (family CoordinateHostLayout) .
334 (nativePeerEndpointEnd (chEndpoint layout)))
335
336-- Only the combined prediction uses this profile. Device-local products
337-- retain their explicit policy; their results enter a host binary64 combine.
338def chCombineArithmetic =
339 (constructor
340 NumericalContract
341 NumericalContractOf
342 nativeFiniteFloat64Profile
343 (constructor
344 StdList
345 StdListCons
346 (family StdNumericOperation)
347 stdOpAdd
348 (constructor StdList StdListEmpty (family StdNumericOperation)))
349 (constructor NumericalRelation NumericalExactOrder b"coordinate-prediction-add-v1"))
350
351def chCombineArithmeticDigest =
352 (numericalExactContractDigest chCombineArithmetic)
353
354-- Membership is independent of numerical tree order and device placement.
355-- Changing its epoch or relation changes both frames and checkpoint context.
356def chMemberGroup =
357 (constructor
358 ParticipantGroup
359 ParticipantGroupOf
360 coordinateCount
361 0
362 b"coordinate-owner-members-v1"
363 (constructor ParticipantSelection ParticipantStride 0 1 coordinateCount))
364
365def chMemberCoverage =
366 (constructor CombineCoverage CombineParticipantGroup chMemberGroup 1 1)
367
368def chContext =
369 (lambda unrestricted numerics : Bytes .
370 (constructor
371 CheckpointEnvelopeContract
372 CheckpointEnvelopeContractValue
373 (bytes-append
374 b"coordinate-regression-v1;"
375 (bytes-append
376 numerics
377 (bytes-append chCombineArithmeticDigest (participantGroupDigest chMemberGroup))))
378 b"scaled-accumulation:decay=1/2;subtract-update:rate=1/8"
379 b"repeated-input:[1,2];target=0;one-batch-per-update"
380 b"weights:[3,1];accumulators:[0,0];no-randomness"
381 1
382 1
383 1))
384
385def chIdentity =
386 (lambda unrestricted numerics : Bytes .
387 (lambda unrestricted operation : Nat .
388 (lambda unrestricted sender : Nat .
389 (lambda unrestricted receiver : Nat .
390 (lambda unrestricted region : Bytes .
391 (constructor
392 RegionTransferIdentity
393 RegionTransferIdentityOf
394 b"coordinate-squared-error"
395 b"coordinate-learning-v1"
396 region
397 numerics
398 (constructor LearningRound LearningRoundOf 1 0)
399 operation
400 sender
401 receiver
402 (constructor LogicalInterval LogicalIntervalOf 0 coordinateCount)))))))
403
404def chPublicationPlan =
405 (lambda unrestricted layout : (family CoordinateHostLayout) .
406 (lambda unrestricted resume : Nat .
407 (constructor
408 NativeRegionCheckpoint
409 NativeRegionCheckpointOf
410 (nativeRegionManifest (chCheckpoint layout))
411 (nativeRegionShards (chCheckpoint layout))
412 (naturalAdd (nativeRegionEpoch (chCheckpoint layout)) resume)
413 (nativeRegionEnd (chCheckpoint layout)))))
414
415-- Two coordinate owners: owner 0 publishes, owner 1 is its one peer over
416-- the pair's single edge. A shard's owner is the coordinate its interval
417-- holds; parameter and accumulator follow the capture prefix in that
418-- owner's state, in ordinal order.
419def chPublication =
420 (lambda unrestricted layout : (family CoordinateHostLayout) .
421 (lambda unrestricted resume : Nat .
422 (constructor
423 NativePeerRegionPublication
424 NativePeerRegionPublicationOf
425 (chPublicationPlan layout resume)
426 1
427 (lambda unrestricted owner : Nat . (chCapture layout))
428 (lambda unrestricted owner : Nat . (chCommitted layout))
429 (lambda unrestricted peer : Nat . nativePeerConnectionSlot)
430 (chStateAt layout)
431 chStateBytes
432 nativeRegionCaptureBytes
433 (lambda unrestricted shard : (family NativeRegionShard) .
434 (naturalDivideUnchecked (intervalBegin (nativeRegionInterval shard)) coordinateWordBytes))
435 (lambda unrestricted shard : (family NativeRegionShard) .
436 (naturalAdd
437 nativeRegionCaptureBytes
438 (naturalMultiply (nativeRegionOrdinal shard) coordinateWordBytes)))
439 chPaths)))
440
441def chDestinations =
442 (lambda unrestricted layout : (family CoordinateHostLayout) .
443 (lambda unrestricted worker : Nat .
444 (constructor
445 StdList
446 StdListCons
447 (family NativeRegionDestination)
448 (constructor
449 NativeRegionDestination
450 NativeRegionDestinationOf
451 0
452 (coordinateInterval worker)
453 (chWeight layout))
454 (constructor
455 StdList
456 StdListCons
457 (family NativeRegionDestination)
458 (constructor
459 NativeRegionDestination
460 NativeRegionDestinationOf
461 1
462 (coordinateInterval worker)
463 (chAccumulator layout))
464 (constructor StdList StdListEmpty (family NativeRegionDestination))))))
465
466-- These are source-layout admission checks, before artifact emission. An
467-- unavailable placement never becomes an empty successful restore program.
468def chRestoreAdmitted =
469 (lambda unrestricted layout : (family CoordinateHostLayout) .
470 (lambda unrestricted worker : Nat .
471 (stdBoolToNatural
472 (stdResultIsSuccess
473 (family NativeCheckpointFailure)
474 (family NativePhysicalCommands)
475 (planNativeRegionRestore
476 (chCheckpoint layout)
477 (chArgument chManifestInputIndex)
478 chArgument
479 nativePeerListenerSlot
480 nativePeerScratchSlot
481 (chExtent layout)
482 (chDestinations layout worker)
483 chEnd)))))
484
485-- Aggregate every independently admitted frame/checkpoint arena and the
486-- local state/endpoint block. The whole host must fit with no live aliases.
487def chResidents =
488 (lambda unrestricted layout : (family CoordinateHostLayout) .
489 (stdListFold
490 (family RegionFrameLayout)
491 (family ArenaResidents)
492 (lambda unrestricted frame : (family RegionFrameLayout) .
493 (lambda unrestricted rest : (family ArenaResidents) .
494 (constructor
495 ArenaResidents
496 ArenaResidentsNext
497 (constructor
498 ArenaResident
499 ArenaResidentValue
500 b"coordinate-frame"
501 (frameBase frame)
502 (naturalSaturatingSubtract (frameEnd frame) (frameBase frame))
503 1)
504 rest)))
505 (constructor
506 ArenaResidents
507 ArenaResidentsNext
508 (constructor
509 ArenaResident
510 ArenaResidentValue
511 b"coordinate-owned-state"
512 (chStateAt layout)
513 (naturalSaturatingSubtract (chExtent layout) (chStateAt layout))
514 coordinateWordBytes)
515 (nativeRegionResidents (chCheckpoint layout)))
516 (constructor
517 StdList
518 StdListCons
519 (family RegionFrameLayout)
520 (chPrediction layout)
521 (constructor
522 StdList
523 StdListCons
524 (family RegionFrameLayout)
525 (chResidual layout)
526 (constructor
527 StdList
528 StdListCons
529 (family RegionFrameLayout)
530 (chAcknowledgment layout)
531 (constructor
532 StdList
533 StdListCons
534 (family RegionFrameLayout)
535 (chCapture layout)
536 (constructor
537 StdList
538 StdListCons
539 (family RegionFrameLayout)
540 (chCommitted layout)
541 (constructor StdList StdListEmpty (family RegionFrameLayout)))))))))
542
543-- The whole round has one communication order. Projection removes unrelated
544-- local work and selects send/receive from the exact frame identity. Each local
545-- callback owns arithmetic or payload preparation/consumption, not transport.
546-- The coordinate prediction is one declared numerical tree. Its reduction
547-- and replication transfers, references and identity derive from this tree.
548def chCombineLeft =
549 (constructor OrderedCombineTree OrderedCombineLeaf 0)
550
551def chCombineRight =
552 (constructor OrderedCombineTree OrderedCombineLeaf 1)
553
554def chCombineTree =
555 (constructor OrderedCombineTree OrderedCombineBranch 0 chCombineLeft chCombineRight)
556
557def chCombineDigest =
558 (combineTreeDigest chCombineTree)
559
560def chCombineNode =
561 (naturalAdd (combineNodeCount chCombineLeft) (combineNodeCount chCombineRight))
562
563def chCombineLeftReference =
564 (combineTreeReference chCombineLeft 0)
565
566def chCombineRightReference =
567 (combineTreeReference chCombineRight (combineNodeCount chCombineLeft))
568
569def chCombineResult =
570 (combineReference 0 chCombineNode 0)
571
572def chCombineLeftInput =
573 (combineReference 0 chCombineNode 1)
574
575def chCombineRightInput =
576 (combineReference 0 chCombineNode 2)
577
578def chCombineBaseAnchor =
579 (lambda unrestricted numerics : Bytes . (chIdentity numerics 0 0 0 b"coordinate-prediction"))
580
581def chCombineAnchor =
582 (lambda unrestricted numerics : Bytes .
583 (combineCoverageAnchor
584 chMemberCoverage
585 (combineNumericalAnchor chCombineArithmetic (chCombineBaseAnchor numerics))))
586
587def chCombinePredictionIdentity =
588 (lambda unrestricted numerics : Bytes .
589 (combineTransferIdentity
590 (chCombineAnchor numerics)
591 chCombineDigest
592 (constructor CombineStage CombineReduce)
593 chCombineRightReference
594 chCombineRightInput))
595
596def chCombineResidualIdentity =
597 (lambda unrestricted numerics : Bytes .
598 (combineTransferIdentity
599 (chCombineAnchor numerics)
600 chCombineDigest
601 (constructor CombineStage CombineReplicate)
602 chCombineResult
603 chCombineRightReference))
604
605def chCombineBinding =
606 (lambda unrestricted layout : (family CoordinateHostLayout) .
607 (lambda unrestricted stage : (family CombineStage) .
608 (lambda unrestricted source : (family CombineReference) .
609 (lambda unrestricted destination : (family CombineReference) .
610 (lambda unrestricted identity : (family RegionTransferIdentity) .
611 (eliminate
612 CombineStage
613 (lambda unrestricted current : (family CombineStage) . (family RegionFrameLayout))
614 stage
615 (branch CombineReduce . (chPrediction layout))
616 (branch CombineReplicate . (chResidual layout))))))))
617
618-- These are locations already owned by the coordinate host layout. The
619-- planner admits each logical reference against this exact tree before use.
620-- An unknown reference maps outside the arena and is rejected by admission.
621def chCombineAddress =
622 (lambda unrestricted layout : (family CoordinateHostLayout) .
623 (lambda unrestricted reference : (family CombineReference) .
624 (nat-eliminate
625 (lambda unrestricted flag : Nat . Nat)
626 (nat-eliminate
627 (lambda unrestricted flag : Nat . Nat)
628 (nat-eliminate
629 (lambda unrestricted flag : Nat . Nat)
630 (nat-eliminate
631 (lambda unrestricted flag : Nat . Nat)
632 (nat-eliminate
633 (lambda unrestricted flag : Nat . Nat)
634 (chExtent layout)
635 (lambda unrestricted prior : Nat .
636 (lambda unrestricted ignored : Nat . (framePayloadAt (chPrediction layout))))
637 (naturalEqual
638 (combineReferenceSlot reference)
639 (combineReferenceSlot chCombineRightInput)))
640 (lambda unrestricted prior : Nat .
641 (lambda unrestricted ignored : Nat . (chScratch layout)))
642 (naturalEqual
643 (combineReferenceSlot reference)
644 (combineReferenceSlot chCombineLeftInput)))
645 (lambda unrestricted prior : Nat .
646 (lambda unrestricted ignored : Nat . (chError layout)))
647 (naturalEqual (combineReferenceSlot reference) (combineReferenceSlot chCombineResult)))
648 (lambda unrestricted prior : Nat .
649 (lambda unrestricted ignored : Nat . (chPartial layout)))
650 (naturalEqual
651 (combineReferenceSlot reference)
652 (combineReferenceSlot chCombineRightReference)))
653 (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . (chPartial layout)))
654 (naturalEqual
655 (combineReferenceSlot reference)
656 (combineReferenceSlot chCombineLeftReference)))))
657
658def chCombineReferenceAdmitted =
659 (lambda unrestricted role : Nat .
660 (lambda unrestricted reference : (family CombineReference) .
661 (eliminate
662 StdOption
663 (lambda unrestricted current : (family StdOption Nat) . Nat)
664 (combineReferenceIndex role chCombineTree reference)
665 (branch StdNone . 0)
666 (branch StdSome index . 1))))
667
668def chCombineOperationAdmitted =
669 (lambda unrestricted role : Nat .
670 (lambda unrestricted operation : (family OrderedCombineOperation (family RegionFrameLayout)) .
671 (eliminate
672 OrderedCombineOperation
673 (lambda unrestricted current : (family OrderedCombineOperation (family RegionFrameLayout)) .
674 Nat)
675 operation
676 (branch CombineReadLeaf destination . (chCombineReferenceAdmitted role destination))
677 (branch
678 CombineCopy
679 source
680 destination
681 .
682 (naturalAnd
683 (chCombineReferenceAdmitted role source)
684 (naturalAnd (chCombineReferenceAdmitted role destination) 1)))
685 (branch
686 CombineApply
687 left
688 right
689 destination
690 .
691 (naturalAnd
692 (chCombineReferenceAdmitted role left)
693 (naturalAnd
694 (chCombineReferenceAdmitted role right)
695 (naturalAnd (chCombineReferenceAdmitted role destination) 1))))
696 (branch CombinePrepare source frame . (chCombineReferenceAdmitted role source))
697 (branch CombineConsume frame destination . (chCombineReferenceAdmitted role destination)))))
698
699def chCombineEnd =
700 (constructor
701 GlobalProtocol
702 GlobalProtocolEnd
703 (family OrderedCombineOperation (family RegionFrameLayout))
704 (family RegionFrameLayout)
705 (family ProtocolNoDecision))
706
707def chCombinePlan =
708 (lambda unrestricted layout : (family CoordinateHostLayout) .
709 (planNumericalCombineAndReplicate
710 (family RegionFrameLayout)
711 chCombineArithmetic
712 chCombineArithmetic
713 coordinateCount
714 chMemberCoverage
715 (chCombineBaseAnchor (chNumerics layout))
716 (chCombineBinding layout)
717 chCombineOperationAdmitted
718 nativeProtocolFrameAdmitted
719 chCombineTree
720 chCombineEnd))
721
722def chGlobalRound =
723 (lambda unrestricted layout : (family CoordinateHostLayout) .
724 (appendGlobalProtocol
725 (family CoordinateRoundOperation)
726 (family RegionFrameLayout)
727 (family ProtocolNoDecision)
728 (mapGlobalProtocolOperations
729 (family OrderedCombineOperation (family RegionFrameLayout))
730 (family CoordinateRoundOperation)
731 (family RegionFrameLayout)
732 (family ProtocolNoDecision)
733 (lambda unrestricted operation : (family OrderedCombineOperation (family RegionFrameLayout)) .
734 (constructor CoordinateRoundOperation CoordinateCombine operation))
735 (stdResultValueOr
736 (family OrderedCombineFailure)
737 (family
738 GlobalProtocol
739 (family OrderedCombineOperation (family RegionFrameLayout))
740 (family RegionFrameLayout)
741 (family ProtocolNoDecision))
742 chCombineEnd
743 (chCombinePlan layout)))
744 (protocolLocal
745 (family CoordinateRoundOperation)
746 (family RegionFrameLayout)
747 (family ProtocolNoDecision)
748 0
749 (constructor CoordinateRoundOperation CoordinateInstallCombined)
750 (protocolLocal
751 (family CoordinateRoundOperation)
752 (family RegionFrameLayout)
753 (family ProtocolNoDecision)
754 1
755 (constructor CoordinateRoundOperation CoordinateInstallCombined)
756 (protocolLocal
757 (family CoordinateRoundOperation)
758 (family RegionFrameLayout)
759 (family ProtocolNoDecision)
760 0
761 (constructor CoordinateRoundOperation CoordinateBackwardUpdate)
762 (protocolLocal
763 (family CoordinateRoundOperation)
764 (family RegionFrameLayout)
765 (family ProtocolNoDecision)
766 1
767 (constructor CoordinateRoundOperation CoordinateBackwardUpdate)
768 (protocolLocal
769 (family CoordinateRoundOperation)
770 (family RegionFrameLayout)
771 (family ProtocolNoDecision)
772 1
773 (constructor CoordinateRoundOperation CoordinatePrepareAcknowledgment)
774 (protocolTransfer
775 (family CoordinateRoundOperation)
776 (family RegionFrameLayout)
777 (family ProtocolNoDecision)
778 (chIdentity (chNumerics layout) 2 1 0 b"updated-coordinate")
779 (chAcknowledgment layout)
780 (protocolLocal
781 (family CoordinateRoundOperation)
782 (family RegionFrameLayout)
783 (family ProtocolNoDecision)
784 0
785 (constructor CoordinateRoundOperation CoordinateAcceptAcknowledgment)
786 (constructor
787 GlobalProtocol
788 GlobalProtocolEnd
789 (family CoordinateRoundOperation)
790 (family RegionFrameLayout)
791 (family ProtocolNoDecision)))))))))))
792
793def chOperationAdmitted =
794 (lambda unrestricted role : Nat .
795 (lambda unrestricted operation : (family CoordinateRoundOperation) .
796 (eliminate
797 CoordinateRoundOperation
798 (lambda unrestricted current : (family CoordinateRoundOperation) . Nat)
799 operation
800 (branch CoordinateCombine value . (chCombineOperationAdmitted role value))
801 (branch CoordinateInstallCombined . (naturalLess role coordinateCount))
802 (branch CoordinateBackwardUpdate . (naturalLess role coordinateCount))
803 (branch CoordinatePrepareAcknowledgment . (naturalEqual role 1))
804 (branch CoordinateAcceptAcknowledgment . (naturalEqual role 0)))))
805
806def chProtocolAdmitted =
807 (lambda unrestricted layout : (family CoordinateHostLayout) .
808 (naturalAnd
809 (stdBoolToNatural
810 (stdResultIsSuccess
811 (family OrderedCombineFailure)
812 (family
813 GlobalProtocol
814 (family OrderedCombineOperation (family RegionFrameLayout))
815 (family RegionFrameLayout)
816 (family ProtocolNoDecision))
817 (chCombinePlan layout)))
818 (naturalAnd
819 (stdBoolToNatural
820 (stdResultIsSuccess
821 (family ProtocolFailure)
822 Nat
823 (checkGlobalProtocol
824 (family CoordinateRoundOperation)
825 (family RegionFrameLayout)
826 (family ProtocolNoDecision)
827 coordinateCount
828 chOperationAdmitted
829 nativeProtocolFrameAdmitted
830 (protocolNoDecision (family RegionFrameLayout))
831 (chGlobalRound layout))))
832 1)))
833
834-- Declared metadata ceiling; RegionFrame derives actual storage from the
835-- canonical identity. The collective scope includes its tree and references.
836def chFrameMaximumHeader : Nat =
837 512
838
839def chWithLayout =
840 (lambda unrestricted numerics : Bytes .
841 (lambda unrestricted epoch : Nat .
842 (lambda unrestricted base : Nat .
843 (lambda unrestricted emit : (pi unrestricted layout : (family CoordinateHostLayout) . Bytes) .
844 (eliminate
845 StdResult
846 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
847 Bytes)
848 (planRegionFrameLayout
849 (chCombinePredictionIdentity numerics)
850 coordinateWordBytes
851 chFrameMaximumHeader
852 base
853 1048576)
854 (branch StdFailure error . b"")
855 (branch
856 StdSuccess
857 prediction
858 .
859 (eliminate
860 StdResult
861 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
862 Bytes)
863 (planRegionFrameLayout
864 (chCombineResidualIdentity numerics)
865 coordinateWordBytes
866 chFrameMaximumHeader
867 (frameAlign (frameEnd prediction))
868 1048576)
869 (branch StdFailure error . b"")
870 (branch
871 StdSuccess
872 residual
873 .
874 (eliminate
875 StdResult
876 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
877 Bytes)
878 (planRegionFrameLayout
879 (chIdentity numerics 2 1 0 b"updated-coordinate")
880 coordinateWordBytes
881 chFrameMaximumHeader
882 (frameAlign (frameEnd residual))
883 1048576)
884 (branch StdFailure error . b"")
885 (branch
886 StdSuccess
887 acknowledgment
888 .
889 (eliminate
890 StdResult
891 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
892 Bytes)
893 (planRegionFrameLayout
894 (chIdentity numerics 3 1 0 b"prepared-owned-state")
895 chStateBytes
896 chFrameMaximumHeader
897 (frameAlign (frameEnd acknowledgment))
898 1048576)
899 (branch StdFailure error . b"")
900 (branch
901 StdSuccess
902 capture
903 .
904 (eliminate
905 StdResult
906 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
907 Bytes)
908 (planRegionFrameLayout
909 (chIdentity numerics 4 0 1 b"manifest-published")
910 coordinateWordBytes
911 chFrameMaximumHeader
912 (frameAlign (frameEnd capture))
913 1048576)
914 (branch StdFailure error . b"")
915 (branch
916 StdSuccess
917 committed
918 .
919 (eliminate
920 StdResult
921 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
922 Bytes)
923 (planNativeRegionCheckpoint
924 (chContext numerics)
925 coordinateRegions
926 coordinatePartitions
927 epoch
928 (frameAlign (frameEnd committed))
929 1048576
930 (naturalMultiply
931 coordinateCount
932 (stdListLength
933 (family CheckpointLogicalRegion)
934 coordinateRegions)))
935 (branch StdFailure error . b"")
936 (branch
937 StdSuccess
938 checkpoint
939 .
940 (let unrestricted layout =
941 (constructor
942 CoordinateHostLayout
943 CoordinateHostLayoutOf
944 prediction
945 residual
946 acknowledgment
947 capture
948 committed
949 checkpoint
950 numerics)
951 in
952 (nat-eliminate
953 (lambda unrestricted admitted : Nat . Bytes)
954 b""
955 (lambda unrestricted previous : Nat .
956 (lambda unrestricted ignored : Bytes . (emit layout)))
957 (naturalAnd
958 (naturalAnd
959 (arenaCertificate (chExtent layout) (chResidents layout))
960 (naturalAnd
961 (chProtocolAdmitted layout)
962 (nativePeerPublicationAdmitted
963 (chPublication layout 0)
964 (chExtent layout)
965 0)))
966 (naturalAnd
967 (chRestoreAdmitted layout 0)
968 (chRestoreAdmitted layout 1)))))))))))))))))))))
969
970def chStart =
971 (lambda unrestricted layout : (family CoordinateHostLayout) .
972 (lambda unrestricted worker : Nat .
973 (lambda unrestricted resume : Nat .
974 (lambda unrestricted tail : (family NativePhysicalCommands) .
975 (nat-eliminate
976 (lambda unrestricted mode : Nat . (family NativePhysicalCommands))
977 (chStore
978 (chVersion layout)
979 (nativeLaunchRecipeImmediate 0)
980 (chStore
981 (chCursor layout)
982 (nativeLaunchRecipeImmediate 0)
983 (chStore
984 (chEpoch layout)
985 (nativeLaunchRecipeImmediate (nativeRegionEpoch (chCheckpoint layout)))
986 (chNatural
987 (chWeight layout)
988 (naturalSelect worker 1 3)
989 (chNatural (chAccumulator layout) 0 tail)))))
990 (lambda unrestricted previous : Nat .
991 (lambda unrestricted ignored : (family NativePhysicalCommands) .
992 (eliminate
993 StdResult
994 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
995 (family NativePhysicalCommands))
996 (planNativeRegionRestore
997 (chCheckpoint layout)
998 (chArgument chManifestInputIndex)
999 (lambda unrestricted index : Nat .
1000 (chArgument (naturalAdd chInputShardBase index)))
1001 nativePeerListenerSlot
1002 nativePeerScratchSlot
1003 (chExtent layout)
1004 (chDestinations layout worker)
1005 (nativeMemoryCopyOperands
1006 (nativeMemoryState (chStateAt layout))
1007 (nativeMemoryState (nativeRegionCaptureAt (chCheckpoint layout)))
1008 nativeRegionCaptureBytes
1009 nativePeerScratchSlot
1010 b"coordinate-restore-capture"
1011 (nativeLaunchRecipeAssertEqual
1012 (nativeMemoryLoad (chVersion layout))
1013 (nativeMemoryLoad (chCursor layout))
1014 b"coordinate-input-position"
1015 (nativeCheckedWordAdd
1016 (nativeMemoryState (chEpoch layout))
1017 (nativeMemoryLoad (chEpoch layout))
1018 (nativeLaunchRecipeImmediate 1)
1019 nativePeerScratchSlot
1020 b"coordinate-epoch-overflow"
1021 tail))))
1022 (branch
1023 StdFailure
1024 error
1025 .
1026 (nativeLaunchRecipeAssertEqual
1027 (nativeLaunchRecipeImmediate 0)
1028 (nativeLaunchRecipeImmediate 1)
1029 b"coordinate-restore-admission"
1030 chEnd))
1031 (branch StdSuccess commands . commands))))
1032 resume)))))
1033
1034def chConstants =
1035 (lambda unrestricted layout : (family CoordinateHostLayout) .
1036 (lambda unrestricted worker : Nat .
1037 (lambda unrestricted tail : (family NativePhysicalCommands) .
1038 (chNatural
1039 (chFeature layout)
1040 (succ worker)
1041 (chNatural
1042 (chScratch layout)
1043 1
1044 (chNatural
1045 (chDecay layout)
1046 2
1047 (chBinary
1048 chDivide
1049 (chDecay layout)
1050 (chScratch layout)
1051 (chDecay layout)
1052 (chNatural
1053 (chRate layout)
1054 8
1055 (chBinary chDivide (chRate layout) (chScratch layout) (chRate layout) tail)))))))))
1056
1057def chHostForward =
1058 (lambda unrestricted layout : (family CoordinateHostLayout) .
1059 (chBinary chMultiply (chPartial layout) (chWeight layout) (chFeature layout)))
1060
1061def chHostBackward =
1062 (lambda unrestricted layout : (family CoordinateHostLayout) .
1063 (chBinary chMultiply (chGradient layout) (chError layout) (chFeature layout)))
1064
1065def chUpdate =
1066 (lambda unrestricted layout : (family CoordinateHostLayout) .
1067 (lambda unrestricted tail : (family NativePhysicalCommands) .
1068 (chBinary
1069 chMultiply
1070 (chAccumulator layout)
1071 (chDecay layout)
1072 (chAccumulator layout)
1073 (chBinary
1074 chAdd
1075 (chAccumulator layout)
1076 (chAccumulator layout)
1077 (chGradient layout)
1078 (chBinary
1079 chMultiply
1080 (chScratch layout)
1081 (chRate layout)
1082 (chAccumulator layout)
1083 (chBinary chSubtract (chWeight layout) (chWeight layout) (chScratch layout) tail))))))
1084
1085-- Progress advances after the selected target transition and finite checks.
1086def chAdvance =
1087 (lambda unrestricted layout : (family CoordinateHostLayout) .
1088 (lambda unrestricted tail : (family NativePhysicalCommands) .
1089 (nativeCheckedWordAdd
1090 (nativeMemoryState (chVersion layout))
1091 (nativeMemoryLoad (chVersion layout))
1092 (nativeLaunchRecipeImmediate 1)
1093 nativePeerScratchSlot
1094 b"coordinate-update-overflow"
1095 (nativeCheckedWordAdd
1096 (nativeMemoryState (chCursor layout))
1097 (nativeMemoryLoad (chCursor layout))
1098 (nativeLaunchRecipeImmediate 1)
1099 nativePeerScratchSlot
1100 b"coordinate-cursor-overflow"
1101 tail))))
1102
1103-- Arithmetic is shared by both projections; the next acknowledgment is a
1104-- separate global transfer after local state and progress have advanced.
1105def chBackwardUpdate =
1106 (lambda unrestricted layout : (family CoordinateHostLayout) .
1107 (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1108 (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1109 (lambda unrestricted tail : (family NativePhysicalCommands) .
1110 (nativeFloat64RequireFinite
1111 (nativeMemoryLoad (chError layout))
1112 nativePeerScratchSlot
1113 b"coordinate-residual-nonfinite"
1114 (backward
1115 (nativeFloat64RequireFinite
1116 (nativeMemoryLoad (chGradient layout))
1117 nativePeerScratchSlot
1118 b"coordinate-gradient-nonfinite"
1119 (update
1120 (nativeFloat64RequireFinite
1121 (nativeMemoryLoad (chWeight layout))
1122 nativePeerScratchSlot
1123 b"coordinate-parameter-nonfinite"
1124 (nativeFloat64RequireFinite
1125 (nativeMemoryLoad (chAccumulator layout))
1126 nativePeerScratchSlot
1127 b"coordinate-accumulator-nonfinite"
1128 (chAdvance layout tail)))))))))))
1129
1130def chCombineLocal =
1131 (lambda unrestricted layout : (family CoordinateHostLayout) .
1132 (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1133 (lambda unrestricted operation : (family OrderedCombineOperation (family RegionFrameLayout)) .
1134 (eliminate
1135 OrderedCombineOperation
1136 (lambda unrestricted current : (family OrderedCombineOperation (family RegionFrameLayout)) .
1137 (pi unrestricted tail : (family NativePhysicalCommands) .
1138 (family NativePhysicalCommands)))
1139 operation
1140 (branch
1141 CombineReadLeaf
1142 destination
1143 .
1144 (lambda unrestricted tail : (family NativePhysicalCommands) .
1145 (forward
1146 (nativeFloat64RequireFinite
1147 (nativeMemoryLoad (chPartial layout))
1148 nativePeerScratchSlot
1149 b"coordinate-partial-nonfinite"
1150 tail))))
1151 (branch
1152 CombineCopy
1153 source
1154 destination
1155 .
1156 (chStore
1157 (chCombineAddress layout destination)
1158 (nativeMemoryLoad (chCombineAddress layout source))))
1159 (branch
1160 CombineApply
1161 left
1162 right
1163 destination
1164 .
1165 (lambda unrestricted tail : (family NativePhysicalCommands) .
1166 (let unrestricted a =
1167 (chCombineAddress layout left)
1168 in
1169 (let unrestricted z =
1170 (chCombineAddress layout right)
1171 in
1172 (let unrestricted out =
1173 (chCombineAddress layout destination)
1174 in
1175 (nativeFloat64RequireFinite
1176 (nativeMemoryLoad a)
1177 nativePeerScratchSlot
1178 b"coordinate-partial-nonfinite"
1179 (nativeFloat64RequireFinite
1180 (nativeMemoryLoad z)
1181 nativePeerScratchSlot
1182 b"coordinate-partial-nonfinite"
1183 (chBinary
1184 chAdd
1185 out
1186 a
1187 z
1188 (nativeFloat64RequireFinite
1189 (nativeMemoryLoad out)
1190 nativePeerScratchSlot
1191 b"coordinate-partial-nonfinite"
1192 tail)))))))))
1193 (branch
1194 CombinePrepare
1195 source
1196 frame
1197 .
1198 (chStore (framePayloadAt frame) (nativeMemoryLoad (chCombineAddress layout source))))
1199 (branch
1200 CombineConsume
1201 frame
1202 destination
1203 .
1204 (lambda unrestricted tail : (family NativePhysicalCommands) .
1205 (nativeFrameConsume
1206 frame
1207 (nativeFloat64RequireFinite
1208 (nativeMemoryLoad (framePayloadAt frame))
1209 nativePeerScratchSlot
1210 b"coordinate-partial-nonfinite"
1211 (chStore
1212 (chCombineAddress layout destination)
1213 (nativeMemoryLoad (framePayloadAt frame))
1214 tail)))))))))
1215
1216def chLocalRound =
1217 (lambda unrestricted layout : (family CoordinateHostLayout) .
1218 (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1219 (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1220 (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1221 (lambda unrestricted operation : (family CoordinateRoundOperation) .
1222 (eliminate
1223 CoordinateRoundOperation
1224 (lambda unrestricted current : (family CoordinateRoundOperation) .
1225 (pi unrestricted tail : (family NativePhysicalCommands) .
1226 (family NativePhysicalCommands)))
1227 operation
1228 (branch CoordinateCombine value . (chCombineLocal layout forward value))
1229 (branch
1230 CoordinateInstallCombined
1231 .
1232 (chStore (chError layout) (nativeMemoryLoad (chPartial layout))))
1233 (branch CoordinateBackwardUpdate . (chBackwardUpdate layout backward update))
1234 (branch
1235 CoordinatePrepareAcknowledgment
1236 .
1237 (chStore
1238 (framePayloadAt (chAcknowledgment layout))
1239 (nativeMemoryLoad (chVersion layout))))
1240 (branch
1241 CoordinateAcceptAcknowledgment
1242 .
1243 (lambda unrestricted tail : (family NativePhysicalCommands) .
1244 (nativeFrameConsume
1245 (chAcknowledgment layout)
1246 (nativeLaunchRecipeAssertEqual
1247 (nativeMemoryLoad (framePayloadAt (chAcknowledgment layout)))
1248 (nativeMemoryLoad (chVersion layout))
1249 b"coordinate-acknowledged-version"
1250 tail))))))))))
1251
1252def chProjectedRound =
1253 (lambda unrestricted layout : (family CoordinateHostLayout) .
1254 (lambda unrestricted worker : Nat .
1255 (projectGlobalProtocol
1256 (family CoordinateRoundOperation)
1257 (family RegionFrameLayout)
1258 (family ProtocolNoDecision)
1259 worker
1260 (chGlobalRound layout))))
1261
1262def chTransferRound =
1263 (lambda unrestricted direction : (family ProtocolDirection) .
1264 (lambda unrestricted identity : (family RegionTransferIdentity) .
1265 (lambda unrestricted layout : (family RegionFrameLayout) .
1266 (nativePeerIO
1267 chConnection
1268 (eliminate
1269 ProtocolDirection
1270 (lambda unrestricted current : (family ProtocolDirection) . Nat)
1271 direction
1272 (branch ProtocolSend . 1)
1273 (branch ProtocolReceive . 0))
1274 layout))))
1275
1276-- chWithLayout checks the complete global program and every frame binding
1277-- before either role's artifact is emitted. These lowerings use that admitted
1278-- projection; they cannot independently select a peer or reorder messages.
1279def chRound =
1280 (lambda unrestricted layout : (family CoordinateHostLayout) .
1281 (lambda unrestricted worker : Nat .
1282 (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1283 (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1284 (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1285 (nativeProtocolCommands
1286 (family CoordinateRoundOperation)
1287 (family RegionFrameLayout)
1288 (family ProtocolNoDecision)
1289 (chLocalRound layout forward backward update)
1290 chTransferRound
1291 nativeProtocolNoFrameDecisions
1292 b"coordinate-protocol"
1293 (chProjectedRound layout worker)))))))
1294
1295-- Reuse phases come from the same projection as the actual transfers. This
1296-- removes a second manually maintained sender/consumer table for each role.
1297def chAdvanceRound =
1298 (lambda unrestricted layout : (family CoordinateHostLayout) .
1299 (lambda unrestricted worker : Nat .
1300 (nativeProtocolCommands
1301 (family CoordinateRoundOperation)
1302 (family RegionFrameLayout)
1303 (family ProtocolNoDecision)
1304 (lambda unrestricted operation : (family CoordinateRoundOperation) .
1305 (lambda unrestricted tail : (family NativePhysicalCommands) . tail))
1306 (lambda unrestricted direction : (family ProtocolDirection) .
1307 (lambda unrestricted identity : (family RegionTransferIdentity) .
1308 (lambda unrestricted frame : (family RegionFrameLayout) .
1309 (nativeFrameAdvance
1310 frame
1311 (eliminate
1312 ProtocolDirection
1313 (lambda unrestricted current : (family ProtocolDirection) .
1314 (family NativeFrameTerminal))
1315 direction
1316 (branch ProtocolSend . (constructor NativeFrameTerminal NativeFrameSendComplete))
1317 (branch
1318 ProtocolReceive
1319 .
1320 (constructor NativeFrameTerminal NativeFrameConsumeComplete)))
1321 nativePeerScratchSlot))))
1322 nativeProtocolNoFrameDecisions
1323 b"coordinate-rearm"
1324 (chProjectedRound layout worker))))
1325
1326def chRounds =
1327 (lambda unrestricted layout : (family CoordinateHostLayout) .
1328 (lambda unrestricted worker : Nat .
1329 (lambda unrestricted steps : Nat .
1330 (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1331 (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1332 (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1333 (lambda unrestricted finish : (family NativePhysicalCommands) .
1334 (nativeCheckedWordAdd
1335 (nativeMemoryState (chScratch layout))
1336 (nativeMemoryLoad (chVersion layout))
1337 (nativeLaunchRecipeImmediate steps)
1338 nativePeerScratchSlot
1339 b"coordinate-version-range"
1340 (nativeCheckedWordAdd
1341 (nativeMemoryState (chScratch layout))
1342 (nativeMemoryLoad (chCursor layout))
1343 (nativeLaunchRecipeImmediate steps)
1344 nativePeerScratchSlot
1345 b"coordinate-cursor-range"
1346 (nat-eliminate
1347 (lambda unrestricted count : Nat . (family NativePhysicalCommands))
1348 finish
1349 (lambda unrestricted previous : Nat .
1350 (lambda unrestricted ignored : (family NativePhysicalCommands) .
1351 (nativeCheckedWordAdd
1352 (nativeMemoryState (chScratch layout))
1353 (nativeMemoryLoad (chVersion layout))
1354 (nativeLaunchRecipeImmediate 1)
1355 nativePeerScratchSlot
1356 b"coordinate-first-version"
1357 (nativeFrameInitializeRound
1358 (chPrediction layout)
1359 (nativeMemoryLoad (chEpoch layout))
1360 (nativeMemoryLoad (chVersion layout))
1361 (nativeFrameInitializeRound
1362 (chResidual layout)
1363 (nativeMemoryLoad (chEpoch layout))
1364 (nativeMemoryLoad (chVersion layout))
1365 (nativeFrameInitializeRound
1366 (chAcknowledgment layout)
1367 (nativeMemoryLoad (chEpoch layout))
1368 (nativeMemoryLoad (chScratch layout))
1369 (chRound
1370 layout
1371 worker
1372 forward
1373 backward
1374 update
1375 (nativeLaunchRecipeCommand
1376 (constructor
1377 NativePhysicalOperation
1378 NativePhysicalRepeatBeginCounted
1379 (nativeLaunchRecipeImmediate previous))
1380 b"coordinate-repeat"
1381 (chAdvanceRound
1382 layout
1383 worker
1384 (chRound
1385 layout
1386 worker
1387 forward
1388 backward
1389 update
1390 (nativeLaunchRecipeCommand
1391 (constructor
1392 NativePhysicalOperation
1393 NativePhysicalRepeatEnd)
1394 b"coordinate-repeat-end"
1395 finish)))))))))))
1396 steps))))))))))
1397
1398def chOutput =
1399 (lambda unrestricted layout : (family CoordinateHostLayout) .
1400 (lambda unrestricted tail : (family NativePhysicalCommands) .
1401 (nativeFileCall
1402 1
1403 (nativeLaunchRecipeArguments
1404 (nativeLaunchRecipeImmediate 1)
1405 (nativeMemoryState (chStateAt layout))
1406 (nativeLaunchRecipeImmediate chStateBytes)
1407 (nativeLaunchRecipeImmediate 0))
1408 nativePeerScratchSlot
1409 chStateBytes
1410 b"coordinate-result"
1411 tail)))
1412
1413-- The shared publisher handles capture agreement and durability. This system
1414-- supplies only its region-to-state placement and final result protocol.
1415def chFinish =
1416 (lambda unrestricted layout : (family CoordinateHostLayout) .
1417 (lambda unrestricted worker : Nat .
1418 (lambda unrestricted resume : Nat .
1419 (eliminate
1420 StdResult
1421 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
1422 (family NativePhysicalCommands))
1423 (planNativePeerRegionPublish
1424 (chPublication layout resume)
1425 (chExtent layout)
1426 worker
1427 (nativeSocketCloseChecked chConnection nativePeerScratchSlot (chOutput layout chHalt)))
1428 (branch
1429 StdFailure
1430 error
1431 .
1432 (nativeLaunchRecipeAssertEqual
1433 (nativeLaunchRecipeImmediate 0)
1434 (nativeLaunchRecipeImmediate 1)
1435 b"coordinate-publication-admission"
1436 chEnd))
1437 (branch StdSuccess commands . commands)))))
1438
1439def chCommandsWithSession =
1440 (lambda unrestricted layout : (family CoordinateHostLayout) .
1441 (lambda unrestricted worker : Nat .
1442 (lambda unrestricted address : Bytes .
1443 (lambda unrestricted resume : Nat .
1444 (lambda unrestricted steps : Nat .
1445 (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1446 (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1447 (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1448 (lambda unrestricted prepare : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1449 (lambda unrestricted finish : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1450 (chStart
1451 layout
1452 worker
1453 resume
1454 (nativeFloat64RequireFinite
1455 (nativeMemoryLoad (chWeight layout))
1456 nativePeerScratchSlot
1457 b"coordinate-parameter-nonfinite"
1458 (nativeFloat64RequireFinite
1459 (nativeMemoryLoad (chAccumulator layout))
1460 nativePeerScratchSlot
1461 b"coordinate-accumulator-nonfinite"
1462 (chConstants
1463 layout
1464 worker
1465 (prepare
1466 (nativePeerSetup
1467 worker
1468 address
1469 (chEndpoint layout)
1470 (chStore
1471 (chScratch layout)
1472 (nativeLaunchRecipeImmediate 1)
1473 (nativeSocketRequireZero
1474 (nativeSocketNoDelay
1475 chConnection
1476 (nativeMemoryState (chScratch layout))
1477 (nativeLaunchRecipeStore nativePeerScratchSlot))
1478 nativePeerScratchSlot
1479 b"coordinate-tcp-nodelay"
1480 (chRounds
1481 layout
1482 worker
1483 steps
1484 forward
1485 backward
1486 update
1487 (finish (chFinish layout worker resume)))))))))))))))))))))
1488
1489-- Host reference chooses no device lifecycle. GPU callers supply their
1490-- admitted, relocated setup and readback/release fragments explicitly.
1491def chCommands =
1492 (lambda unrestricted layout : (family CoordinateHostLayout) .
1493 (lambda unrestricted worker : Nat .
1494 (lambda unrestricted address : Bytes .
1495 (lambda unrestricted resume : Nat .
1496 (lambda unrestricted steps : Nat .
1497 (lambda unrestricted forward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1498 (lambda unrestricted backward : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1499 (chCommandsWithSession
1500 layout
1501 worker
1502 address
1503 resume
1504 steps
1505 forward
1506 backward
1507 (chUpdate layout)
1508 (lambda unrestricted tail : (family NativePhysicalCommands) . tail)
1509 (lambda unrestricted tail : (family NativePhysicalCommands) . tail)))))))))
1510
1511def chProgramFor =
1512 (lambda unrestricted slots : Nat .
1513 (lambda unrestricted extent : Nat .
1514 (nativePhysicalProgramFromCommands
1515 (bytes-append
1516 b"coordinate-owned-learning-v1"
1517 (dataBytesRepeatByte
1518 (byte 0)
1519 (naturalSaturatingSubtract 64 (bytes-length b"coordinate-owned-learning-v1"))))
1520 extent
1521 slots)))
1522
1523def chProgram =
1524 (lambda unrestricted layout : (family CoordinateHostLayout) .
1525 (chProgramFor nativePeerEndpointSlots (chExtent layout)))
1526
1527-- The host target selects this participant's instruction set and ABI
1528-- (Runtime.NativeHostTarget). Both coordinate owners derive the same program,
1529-- frames and checkpoint encoding on every target, so they may run on
1530-- different host architectures within one session.
1531def coordinateHostTargetArtifact =
1532 (lambda unrestricted target : (family NativeHostTarget) .
1533 (lambda unrestricted resources : (family NativeResourceContext) .
1534 (lambda unrestricted worker : Nat .
1535 (lambda unrestricted port : Nat .
1536 (lambda unrestricted resume : Nat .
1537 (lambda unrestricted epoch : Nat .
1538 (lambda unrestricted steps : Nat .
1539 (nat-eliminate
1540 (lambda unrestricted valid : Nat . Bytes)
1541 b""
1542 (lambda unrestricted previous : Nat .
1543 (lambda unrestricted ignored : Bytes .
1544 (chWithLayout
1545 b"f64-local-and-update"
1546 epoch
1547 0
1548 (lambda unrestricted layout : (family CoordinateHostLayout) .
1549 (eliminate
1550 StdResult
1551 (lambda unrestricted result : (family StdResult (family SocketAddressFailure) Bytes) .
1552 Bytes)
1553 (linuxIPv4SocketAddress ipv4Loopback port)
1554 (branch StdFailure error . b"")
1555 (branch
1556 StdSuccess
1557 address
1558 .
1559 (nativeHostTargetResourceArtifact
1560 target
1561 resources
1562 (chProgram
1563 layout
1564 (chCommands
1565 layout
1566 worker
1567 address
1568 resume
1569 steps
1570 (chHostForward layout)
1571 (chHostBackward layout))))))))))
1572 (naturalAnd
1573 (naturalLessOrEqual worker 1)
1574 (naturalAnd
1575 (naturalLessOrEqual resume 1)
1576 (naturalAnd
1577 (naturalNonzero epoch)
1578 (naturalAnd
1579 (naturalLessOrEqual (naturalAdd epoch resume) regionFrameWordLimit)
1580 (naturalAnd
1581 (naturalNonzero steps)
1582 (naturalLessOrEqual steps regionFrameWordLimit))))))))))))))
1583
1584-- The Linux x86-64 pairing.
1585def coordinateHostArtifact =
1586 (coordinateHostTargetArtifact nativeHostTargetX86_64Linux)
1587
1588def cpCheckpoint =
1589 (lambda unrestricted layout : (family CoordinatePredictionLayout) .
1590 (eliminate
1591 CoordinatePredictionLayout
1592 (lambda unrestricted current : (family CoordinatePredictionLayout) .
1593 (family NativeRegionCheckpoint))
1594 layout
1595 (branch CoordinatePredictionLayoutOf checkpoint . checkpoint)))
1596
1597def cpLeft =
1598 (lambda unrestricted layout : (family CoordinatePredictionLayout) .
1599 (nativeRegionEnd (cpCheckpoint layout)))
1600
1601def cpRight =
1602 (lambda unrestricted layout : (family CoordinatePredictionLayout) .
1603 (naturalAdd (cpLeft layout) coordinateWordBytes))
1604
1605def cpFeature =
1606 (lambda unrestricted layout : (family CoordinatePredictionLayout) .
1607 (naturalAdd (cpRight layout) coordinateWordBytes))
1608
1609def cpPrediction =
1610 (lambda unrestricted layout : (family CoordinatePredictionLayout) .
1611 (naturalAdd (cpFeature layout) coordinateWordBytes))
1612
1613def cpExtent =
1614 (lambda unrestricted layout : (family CoordinatePredictionLayout) .
1615 (naturalAdd (cpPrediction layout) coordinateWordBytes))
1616
1617def cpSlots =
1618 (succ nativePeerListenerSlot)
1619
1620def cpWithLayout =
1621 (lambda unrestricted numerics : Bytes .
1622 (lambda unrestricted epoch : Nat .
1623 (lambda unrestricted base : Nat .
1624 (lambda unrestricted emit : (pi unrestricted layout : (family CoordinatePredictionLayout) . Bytes) .
1625 (eliminate
1626 StdResult
1627 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
1628 Bytes)
1629 (planNativeRegionCheckpoint
1630 (chContext numerics)
1631 coordinateRegions
1632 coordinatePartitions
1633 epoch
1634 base
1635 1048576
1636 chSavedShardCount)
1637 (branch StdFailure error . b"")
1638 (branch
1639 StdSuccess
1640 checkpoint
1641 .
1642 (emit
1643 (constructor CoordinatePredictionLayout CoordinatePredictionLayoutOf checkpoint))))))))
1644
1645-- Compile only an admitted full-vector restore. The realization chooses the
1646-- computation after validation; both host and device predictions use exactly
1647-- this saved-state interpretation and finite-input check.
1648def cpWithRestore =
1649 (lambda unrestricted layout : (family CoordinatePredictionLayout) .
1650 (lambda unrestricted tail : (family NativePhysicalCommands) .
1651 (lambda unrestricted emit : (pi unrestricted commands : (family NativePhysicalCommands) . Bytes) .
1652 (eliminate
1653 StdResult
1654 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
1655 Bytes)
1656 (planNativeRegionRestore
1657 (cpCheckpoint layout)
1658 (chArgument chManifestInputIndex)
1659 (lambda unrestricted index : Nat . (chArgument (naturalAdd chInputShardBase index)))
1660 nativePeerListenerSlot
1661 nativePeerScratchSlot
1662 (cpExtent layout)
1663 (constructor
1664 StdList
1665 StdListCons
1666 (family NativeRegionDestination)
1667 (constructor
1668 NativeRegionDestination
1669 NativeRegionDestinationOf
1670 0
1671 (constructor LogicalInterval LogicalIntervalOf 0 coordinateVectorBytes)
1672 (cpLeft layout))
1673 (constructor StdList StdListEmpty (family NativeRegionDestination)))
1674 (nativeFloat64RequireFinite
1675 (nativeMemoryLoad (cpLeft layout))
1676 nativePeerScratchSlot
1677 b"prediction-parameter-nonfinite"
1678 (nativeFloat64RequireFinite
1679 (nativeMemoryLoad (cpRight layout))
1680 nativePeerScratchSlot
1681 b"prediction-parameter-nonfinite"
1682 tail)))
1683 (branch StdFailure error . b"")
1684 (branch StdSuccess commands . (emit commands))))))
1685
1686def cpOutput =
1687 (lambda unrestricted layout : (family CoordinatePredictionLayout) .
1688 (lambda unrestricted tail : (family NativePhysicalCommands) .
1689 (nativeFloat64RequireFinite
1690 (nativeMemoryLoad (cpPrediction layout))
1691 nativePeerScratchSlot
1692 b"prediction-result-nonfinite"
1693 (nativeFileCall
1694 1
1695 (nativeLaunchRecipeArguments
1696 (nativeLaunchRecipeImmediate 1)
1697 (nativeMemoryState (cpPrediction layout))
1698 (nativeLaunchRecipeImmediate coordinateWordBytes)
1699 (nativeLaunchRecipeImmediate 0))
1700 nativePeerScratchSlot
1701 coordinateWordBytes
1702 b"coordinate-prediction"
1703 tail))))
1704
1705-- Prediction validates the full committed checkpoint but materializes only the
1706-- parameter region. Its state extent contains no communication-frame arenas.
1707def coordinateHostTargetPredictionArtifact =
1708 (lambda unrestricted target : (family NativeHostTarget) .
1709 (lambda unrestricted resources : (family NativeResourceContext) .
1710 (lambda unrestricted epoch : Nat .
1711 (cpWithLayout
1712 b"f64-local-and-update"
1713 epoch
1714 0
1715 (lambda unrestricted layout : (family CoordinatePredictionLayout) .
1716 (cpWithRestore
1717 layout
1718 (chNatural
1719 (cpFeature layout)
1720 2
1721 (chBinary
1722 chMultiply
1723 (cpPrediction layout)
1724 (cpRight layout)
1725 (cpFeature layout)
1726 (chBinary
1727 chAdd
1728 (cpPrediction layout)
1729 (cpLeft layout)
1730 (cpPrediction layout)
1731 (cpOutput layout chHalt))))
1732 (lambda unrestricted commands : (family NativePhysicalCommands) .
1733 (nativeHostTargetResourceArtifact
1734 target
1735 resources
1736 (chProgramFor cpSlots (cpExtent layout) commands)))))))))
1737
1738def coordinateHostPredictionArtifact =
1739 (coordinateHostTargetPredictionArtifact nativeHostTargetX86_64Linux)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.