1module PartitionedRegression.NativeHost
2
3import Checkpoint.Envelope
4import Checkpoint.NativeEnvelope
5import Runtime.NativeFloatPlan
6import Runtime.NativePeerEndpoint
7import Runtime.NativeFilePlan
8import Runtime.NativeMemoryPlan
9import Compiler.Planning.RegionFrame
10import Runtime.RegionTransfer
11import Runtime.RegionFrame
12import Runtime.NativeWordArithmetic
13import Runtime.NativeRegionFrame
14import Runtime.NativeSocketPlan
15import Runtime.SocketAddress
16import Runtime.NativePhysicalProgram
17import Runtime.NativePhysicalNativeELF
18import Runtime.NativeLaunchRecipeLoad
19import Runtime.WordDigest
20import Learning.Transition
21import Representation.Partition
22import Model.Word64
23import Data.Bytes
24import Std.Foundation
25import Std.Natural
26
27-- Partitioned scalar squared-error learner. Transport, weighted combination,
28-- version consumption and recovery are shared by explicitly selected local
29-- realizations. The binary64 realization is a host reference, never a fallback
30-- for an unavailable device target.
31def peerWordBytes =
32 nativePeerWordBytes
33
34def peerIdentityFor =
35 (lambda unrestricted run : Bytes .
36 (lambda unrestricted schema : Bytes .
37 (lambda unrestricted version : Nat .
38 (lambda unrestricted operation : Nat .
39 (lambda unrestricted sender : Nat .
40 (lambda unrestricted receiver : Nat .
41 (lambda unrestricted region : Bytes .
42 (constructor
43 RegionTransferIdentity
44 RegionTransferIdentityOf
45 b"squared-error-scalar"
46 run
47 region
48 schema
49 (constructor LearningRound LearningRoundOf 1 version)
50 operation
51 sender
52 receiver
53 (constructor LogicalInterval LogicalIntervalOf 0 1)))))))))
54
55def peerIdentity =
56 (peerIdentityFor b"native-two-peer-test" b"f64-le-with-u64-mass")
57
58def peerInitialIdentity =
59 (peerIdentity 0 0 0 1 b"parameter")
60
61def peerContributionIdentity =
62 (peerIdentity 0 1 1 0 b"gradient-numerator-and-mass")
63
64def peerUpdatedIdentity =
65 (peerIdentity 1 2 0 1 b"parameter")
66
67def peerAcknowledgedIdentity =
68 (peerIdentity 1 3 1 0 b"consumed-version")
69
70def peerPlan =
71 (lambda unrestricted identity : (family RegionTransferIdentity) .
72 (lambda unrestricted bytes : Nat .
73 (lambda unrestricted base : Nat . (planRegionFrameLayout identity bytes 256 base 1048576))))
74
75def peerEnd =
76 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
77
78def peerHalt =
79 (nativeLaunchRecipeCommand
80 (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
81 b"peer-done"
82 peerEnd)
83
84def peerIO =
85 nativePeerIO
86
87def peerFloat =
88 (nativeFloat64 b"peer-arithmetic")
89
90def peerNatural =
91 (nativeFloat64Natural b"peer-arithmetic")
92
93def peerBinary =
94 (nativeFloat64Binary b"peer-arithmetic")
95
96def peerStore =
97 (nativeMemoryStoreWord64 b"peer-state")
98
99def peerOutput =
100 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
101 (lambda unrestricted offset : Nat .
102 (nativeLaunchRecipeCommand
103 (constructor
104 NativePhysicalOperation
105 NativePhysicalSystemCall
106 (nativeLaunchRecipeImmediate 1)
107 (nativeLaunchRecipeArguments
108 (nativeLaunchRecipeImmediate 1)
109 (frameNativeState offset)
110 (nativeLaunchRecipeImmediate peerWordBytes)
111 (nativeLaunchRecipeImmediate 0))
112 b""
113 (nativeLaunchRecipeStore 0))
114 b"peer-result"
115 (nativeLaunchRecipeAssertEqual
116 (nativeLaunchRecipeSlotValue 0)
117 (nativeLaunchRecipeImmediate peerWordBytes)
118 b"peer-result-count"
119 (nativeSocketCloseChecked descriptor 0 peerHalt)))))
120
121def peerAdd =
122 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Add)
123
124def peerMultiply =
125 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Multiply)
126
127def peerDivide =
128 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Divide)
129
130def peerSubtract =
131 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Subtract)
132
133-- The combiner has sample x=1, y=0, gradient w. The worker has x=1 and x=2,
134-- hence numerator w*1*1 + w*2*2. Its mass is carried as an integer, not a mean.
135-- Divide by the total sample mass, then apply w - (1/4)*g. No gradient or
136-- learning-rate byte pattern is pasted into the program.
137def peerHostContribution =
138 (lambda unrestricted worker : Nat .
139 (lambda unrestricted weight : Nat .
140 (lambda unrestricted numerator : Nat .
141 (lambda unrestricted work : Nat .
142 (lambda unrestricted tail : (family NativePhysicalCommands) .
143 (nat-eliminate
144 (lambda unrestricted role : Nat . (family NativePhysicalCommands))
145 (peerStore numerator (frameNativeLoad weight) tail)
146 (lambda unrestricted previous : Nat .
147 (lambda unrestricted ignored : (family NativePhysicalCommands) .
148 (peerNatural
149 work
150 2
151 (peerBinary
152 peerMultiply
153 work
154 work
155 work
156 (peerBinary
157 peerMultiply
158 numerator
159 weight
160 work
161 (peerBinary peerAdd numerator numerator weight tail))))))
162 worker))))))
163
164def peerCoordinatorWith =
165 (lambda unrestricted local : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
166 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
167 (lambda unrestricted wrongMean : Nat .
168 (lambda unrestricted initial : (family RegionFrameLayout) .
169 (lambda unrestricted contribution : (family RegionFrameLayout) .
170 (lambda unrestricted updated : (family RegionFrameLayout) .
171 (lambda unrestricted work : Nat .
172 (lambda unrestricted tail : (family NativePhysicalCommands) .
173 (let unrestricted weight =
174 (framePayloadAt initial)
175 in
176 (let unrestricted numerator =
177 (framePayloadAt contribution)
178 in
179 (let unrestricted mass =
180 (naturalAdd numerator peerWordBytes)
181 in
182 (let unrestricted rate =
183 (naturalAdd work peerWordBytes)
184 in
185 (let unrestricted total =
186 (naturalAdd rate peerWordBytes)
187 in
188 (peerIO
189 descriptor
190 1
191 initial
192 (peerIO
193 descriptor
194 0
195 contribution
196 (nativeFrameConsume
197 contribution
198 (nativeLaunchRecipeAssertEqual
199 (frameNativeLoad mass)
200 (nativeLaunchRecipeImmediate 2)
201 b"peer-sample-coverage"
202 (local
203 (peerNatural
204 work
205 1
206 (peerNatural
207 rate
208 4
209 (peerBinary
210 peerDivide
211 rate
212 work
213 rate
214 (nat-eliminate
215 (lambda unrestricted n : Nat .
216 (family NativePhysicalCommands))
217 (peerNatural
218 total
219 3
220 (peerBinary
221 peerAdd
222 numerator
223 (framePayloadAt updated)
224 numerator
225 (peerBinary
226 peerDivide
227 numerator
228 numerator
229 total
230 (peerBinary
231 peerMultiply
232 numerator
233 rate
234 numerator
235 (peerBinary
236 peerSubtract
237 (framePayloadAt updated)
238 weight
239 numerator
240 (peerIO descriptor 1 updated tail))))))
241 (lambda unrestricted n : Nat .
242 (lambda unrestricted ignored : (family NativePhysicalCommands) .
243 (peerNatural
244 total
245 2
246 (peerBinary
247 peerDivide
248 numerator
249 numerator
250 total
251 (peerBinary
252 peerAdd
253 numerator
254 (framePayloadAt updated)
255 numerator
256 (peerBinary
257 peerDivide
258 numerator
259 numerator
260 total
261 (peerBinary
262 peerMultiply
263 numerator
264 rate
265 numerator
266 (peerBinary
267 peerSubtract
268 (framePayloadAt updated)
269 weight
270 numerator
271 (peerIO descriptor 1 updated tail)))))))))
272 wrongMean))))))))))))))))))))))
273
274def peerWorkerWith =
275 (lambda unrestricted local : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
276 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
277 (lambda unrestricted initial : (family RegionFrameLayout) .
278 (lambda unrestricted contribution : (family RegionFrameLayout) .
279 (lambda unrestricted updated : (family RegionFrameLayout) .
280 (lambda unrestricted work : Nat .
281 (lambda unrestricted tail : (family NativePhysicalCommands) .
282 (let unrestricted weight =
283 (framePayloadAt initial)
284 in
285 (let unrestricted numerator =
286 (framePayloadAt contribution)
287 in
288 (let unrestricted mass =
289 (naturalAdd numerator peerWordBytes)
290 in
291 (peerIO
292 descriptor
293 0
294 initial
295 (nativeFrameConsume
296 initial
297 (local
298 (peerStore
299 mass
300 (nativeLaunchRecipeImmediate 2)
301 (peerIO
302 descriptor
303 1
304 contribution
305 (peerIO descriptor 0 updated (nativeFrameConsume updated tail)))))))))))))))))
306
307def peerProgram =
308 (lambda unrestricted slots : Nat .
309 (lambda unrestricted extent : Nat .
310 (nativePhysicalProgramFromCommands
311 (bytes-append
312 b"native-framed-learning-v1"
313 (dataBytesRepeatByte
314 (byte 0)
315 (naturalSaturatingSubtract 64 (bytes-length b"native-framed-learning-v1"))))
316 extent
317 slots)))
318
319-- The transport owns endpoint slots; the arithmetic keeps only its scratch.
320def peerScratchSlot =
321 nativePeerScratchSlot
322
323def peerListenerSlot =
324 nativePeerListenerSlot
325
326def peerConnectionSlot =
327 nativePeerConnectionSlot
328
329def peerEndpointSlots =
330 nativePeerEndpointSlots
331
332def peerWorkEnd =
333 (lambda unrestricted work : Nat . (naturalAdd work (naturalMultiply 3 peerWordBytes)))
334
335def peerEndpointLengthAt =
336 nativePeerEndpointLengthAt
337
338def peerEndpointEnd =
339 nativePeerEndpointEnd
340
341def peerPortWrite =
342 nativePeerPortWrite
343
344def peerNativeSetup =
345 nativePeerSetup
346
347def peerByRole =
348 nativePeerByRole
349
350def peerRoundWith =
351 (lambda unrestricted local : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
352 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
353 (lambda unrestricted worker : Nat .
354 (lambda unrestricted wrongMean : Nat .
355 (lambda unrestricted initial : (family RegionFrameLayout) .
356 (lambda unrestricted contribution : (family RegionFrameLayout) .
357 (lambda unrestricted updated : (family RegionFrameLayout) .
358 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
359 (lambda unrestricted work : Nat .
360 (lambda unrestricted tail : (family NativePhysicalCommands) .
361 (let unrestricted after =
362 (peerStore
363 (framePayloadAt initial)
364 (frameNativeLoad (framePayloadAt updated))
365 tail)
366 in
367 (let unrestricted acknowledge =
368 (peerByRole
369 worker
370 (peerIO
371 descriptor
372 0
373 acknowledged
374 (nativeFrameConsume
375 acknowledged
376 (nativeLaunchRecipeAssertEqual
377 (frameNativeLoad (framePayloadAt acknowledged))
378 (frameNativeLoad (frameExpectedVersionAt updated))
379 b"peer-acknowledged-version"
380 after)))
381 (peerStore
382 (framePayloadAt acknowledged)
383 (frameNativeLoad (frameExpectedVersionAt updated))
384 (peerIO descriptor 1 acknowledged after)))
385 in
386 (peerByRole
387 worker
388 (peerCoordinatorWith
389 local
390 descriptor
391 wrongMean
392 initial
393 contribution
394 updated
395 work
396 acknowledge)
397 (peerWorkerWith
398 local
399 descriptor
400 initial
401 contribution
402 updated
403 work
404 acknowledge))))))))))))))
405
406def peerAdvance =
407 (lambda unrestricted worker : Nat .
408 (lambda unrestricted initial : (family RegionFrameLayout) .
409 (lambda unrestricted contribution : (family RegionFrameLayout) .
410 (lambda unrestricted updated : (family RegionFrameLayout) .
411 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
412 (lambda unrestricted tail : (family NativePhysicalCommands) .
413 (let unrestricted sent =
414 (constructor NativeFrameTerminal NativeFrameSendComplete)
415 in
416 (let unrestricted consumed =
417 (constructor NativeFrameTerminal NativeFrameConsumeComplete)
418 in
419 (peerByRole
420 worker
421 (nativeFrameAdvance
422 initial
423 sent
424 0
425 (nativeFrameAdvance
426 contribution
427 consumed
428 0
429 (nativeFrameAdvance
430 updated
431 sent
432 0
433 (nativeFrameAdvance acknowledged consumed 0 tail))))
434 (nativeFrameAdvance
435 initial
436 consumed
437 0
438 (nativeFrameAdvance
439 contribution
440 sent
441 0
442 (nativeFrameAdvance
443 updated
444 consumed
445 0
446 (nativeFrameAdvance acknowledged sent 0 tail)))))))))))))
447
448-- First round uses the initialized version. Only later rounds rearm completed
449-- slots, so finishing at u64 max does not require an impossible next version.
450-- The up-front checked sum rejects an unrepresentable run before any transfer.
451def peerUpdatesWith =
452 (lambda unrestricted local : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
453 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
454 (lambda unrestricted worker : Nat .
455 (lambda unrestricted wrongMean : Nat .
456 (lambda unrestricted steps : Nat .
457 (lambda unrestricted epoch : (family NativePhysicalOperand) .
458 (lambda unrestricted version : (family NativePhysicalOperand) .
459 (lambda unrestricted initial : (family RegionFrameLayout) .
460 (lambda unrestricted contribution : (family RegionFrameLayout) .
461 (lambda unrestricted updated : (family RegionFrameLayout) .
462 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
463 (lambda unrestricted work : Nat .
464 (lambda unrestricted finish : (family NativePhysicalCommands) .
465 (nativeCheckedWordAdd
466 (frameNativeState work)
467 version
468 (nativeLaunchRecipeImmediate steps)
469 0
470 b"peer-run-version-overflow"
471 (nat-eliminate
472 (lambda unrestricted count : Nat . (family NativePhysicalCommands))
473 finish
474 (lambda unrestricted previous : Nat .
475 (lambda unrestricted ignored : (family NativePhysicalCommands) .
476 (nativeCheckedWordAdd
477 (frameNativeState work)
478 version
479 (nativeLaunchRecipeImmediate 1)
480 0
481 b"peer-initial-version-overflow"
482 (nativeFrameInitializeRound
483 initial
484 epoch
485 version
486 (nativeFrameInitializeRound
487 contribution
488 epoch
489 version
490 (nativeFrameInitializeRound
491 updated
492 epoch
493 (frameNativeLoad work)
494 (nativeFrameInitializeRound
495 acknowledged
496 epoch
497 (frameNativeLoad work)
498 (peerRoundWith
499 local
500 descriptor
501 worker
502 wrongMean
503 initial
504 contribution
505 updated
506 acknowledged
507 work
508 (nativeLaunchRecipeCommand
509 (constructor
510 NativePhysicalOperation
511 NativePhysicalRepeatBeginCounted
512 (nativeLaunchRecipeImmediate previous))
513 b"peer-repeat"
514 (peerAdvance
515 worker
516 initial
517 contribution
518 updated
519 acknowledged
520 (peerRoundWith
521 local
522 descriptor
523 worker
524 wrongMean
525 initial
526 contribution
527 updated
528 acknowledged
529 work
530 (nativeLaunchRecipeCommand
531 (constructor
532 NativePhysicalOperation
533 NativePhysicalRepeatEnd)
534 b"peer-repeat-end"
535 finish))))))))))))
536 steps)))))))))))))))
537
538def peerUpdates =
539 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
540 (lambda unrestricted worker : Nat .
541 (lambda unrestricted wrongMean : Nat .
542 (lambda unrestricted steps : Nat .
543 (lambda unrestricted epoch : (family NativePhysicalOperand) .
544 (lambda unrestricted version : (family NativePhysicalOperand) .
545 (lambda unrestricted initial : (family RegionFrameLayout) .
546 (lambda unrestricted contribution : (family RegionFrameLayout) .
547 (lambda unrestricted updated : (family RegionFrameLayout) .
548 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
549 (lambda unrestricted work : Nat .
550 (peerUpdatesWith
551 (peerHostContribution
552 worker
553 (framePayloadAt initial)
554 (naturalSelect
555 worker
556 (framePayloadAt contribution)
557 (framePayloadAt updated))
558 work)
559 descriptor
560 worker
561 wrongMean
562 steps
563 epoch
564 version
565 initial
566 contribution
567 updated
568 acknowledged
569 work))))))))))))
570
571def peerCommands =
572 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
573 (lambda unrestricted worker : Nat .
574 (lambda unrestricted initialWeight : Nat .
575 (lambda unrestricted wrongMean : Nat .
576 (lambda unrestricted steps : Nat .
577 (lambda unrestricted epoch : Nat .
578 (lambda unrestricted version : Nat .
579 (lambda unrestricted initial : (family RegionFrameLayout) .
580 (lambda unrestricted contribution : (family RegionFrameLayout) .
581 (lambda unrestricted updated : (family RegionFrameLayout) .
582 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
583 (lambda unrestricted work : Nat .
584 (peerNatural
585 (framePayloadAt initial)
586 initialWeight
587 (peerUpdates
588 descriptor
589 worker
590 wrongMean
591 steps
592 (nativeLaunchRecipeImmediate epoch)
593 (nativeLaunchRecipeImmediate version)
594 initial
595 contribution
596 updated
597 acknowledged
598 work
599 (peerOutput descriptor (framePayloadAt initial))))))))))))))))
600
601-- This deployment exchanges small synchronous messages. Select per-socket
602-- immediate transmission after endpoint establishment, before any frame. The
603-- work word is dead here and is overwritten by run preflight and arithmetic.
604def peerImmediateTransmission =
605 (lambda unrestricted work : Nat .
606 (lambda unrestricted tail : (family NativePhysicalCommands) .
607 (peerStore
608 work
609 (nativeLaunchRecipeImmediate 1)
610 (nativeSocketRequireZero
611 (nativeSocketNoDelay
612 (nativeLaunchRecipeSlotValue peerConnectionSlot)
613 (frameNativeState work)
614 (nativeLaunchRecipeStore peerScratchSlot))
615 peerScratchSlot
616 b"socket-tcp-nodelay"
617 tail))))
618
619def peerWithTransport =
620 (lambda unrestricted endpoint : Nat .
621 (lambda unrestricted worker : Nat .
622 (lambda unrestricted initialWeight : Nat .
623 (lambda unrestricted wrongMean : Nat .
624 (lambda unrestricted port : Nat .
625 (lambda unrestricted steps : Nat .
626 (lambda unrestricted epoch : Nat .
627 (lambda unrestricted version : Nat .
628 (lambda unrestricted initial : (family RegionFrameLayout) .
629 (lambda unrestricted contribution : (family RegionFrameLayout) .
630 (lambda unrestricted updated : (family RegionFrameLayout) .
631 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
632 (lambda unrestricted work : Nat .
633 (let unrestricted commands =
634 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
635 (peerCommands
636 descriptor
637 worker
638 initialWeight
639 wrongMean
640 steps
641 epoch
642 version
643 initial
644 contribution
645 updated
646 acknowledged
647 work))
648 in
649 (nat-eliminate
650 (lambda unrestricted choice : Nat . Bytes)
651 (nativePhysicalGenerateNativeELFBytesDirect
652 (peerProgram
653 (naturalAdd peerScratchSlot 1)
654 (peerWorkEnd work)
655 (commands (nativeLaunchRecipeImmediate 0))))
656 (lambda unrestricted previous : Nat .
657 (lambda unrestricted ignored : Bytes .
658 (eliminate
659 StdResult
660 (lambda unrestricted r : (family StdResult (family SocketAddressFailure) Bytes) .
661 Bytes)
662 (linuxIPv4SocketAddress ipv4Loopback port)
663 (branch StdFailure error . b"")
664 (branch
665 StdSuccess
666 address
667 .
668 (nativePhysicalGenerateNativeELFBytesDirect
669 (peerProgram
670 peerEndpointSlots
671 (peerEndpointEnd (peerWorkEnd work))
672 (peerNativeSetup
673 worker
674 address
675 (peerWorkEnd work)
676 (peerImmediateTransmission
677 work
678 (commands (nativeLaunchRecipeSlotValue peerConnectionSlot))))))))))
679 endpoint)))))))))))))))
680
681def peerLayoutsFor =
682 (lambda unrestricted run : Bytes .
683 (lambda unrestricted schema : Bytes .
684 (lambda unrestricted base : Nat .
685 (lambda unrestricted emit : (pi unrestricted initial : (family RegionFrameLayout) . (pi unrestricted contribution : (family RegionFrameLayout) . (pi unrestricted updated : (family RegionFrameLayout) . (pi unrestricted acknowledged : (family RegionFrameLayout) . (pi unrestricted work : Nat . Bytes))))) .
686 (eliminate
687 StdResult
688 (lambda unrestricted r : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
689 Bytes)
690 (peerPlan (peerIdentityFor run schema 0 0 0 1 b"parameter") peerWordBytes base)
691 (branch StdFailure error . b"")
692 (branch
693 StdSuccess
694 initial
695 .
696 (eliminate
697 StdResult
698 (lambda unrestricted r : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
699 Bytes)
700 (peerPlan
701 (peerIdentityFor run schema 0 1 1 0 b"gradient-numerator-and-mass")
702 (naturalMultiply 2 peerWordBytes)
703 (frameAlign (frameEnd initial)))
704 (branch StdFailure error . b"")
705 (branch
706 StdSuccess
707 contribution
708 .
709 (eliminate
710 StdResult
711 (lambda unrestricted r : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
712 Bytes)
713 (peerPlan
714 (peerIdentityFor run schema 1 2 0 1 b"parameter")
715 peerWordBytes
716 (frameAlign (frameEnd contribution)))
717 (branch StdFailure error . b"")
718 (branch
719 StdSuccess
720 updated
721 .
722 (eliminate
723 StdResult
724 (lambda unrestricted r : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
725 Bytes)
726 (peerPlan
727 (peerIdentityFor run schema 1 3 1 0 b"consumed-version")
728 peerWordBytes
729 (frameAlign (frameEnd updated)))
730 (branch StdFailure error . b"")
731 (branch
732 StdSuccess
733 acknowledged
734 .
735 (emit initial contribution updated acknowledged (frameEnd acknowledged))))))))))))))
736
737def peerLayoutsAt =
738 (peerLayoutsFor b"native-two-peer-test" b"f64-le-with-u64-mass")
739
740def peerLayouts =
741 (peerLayoutsAt 0)
742
743def repeatedArtifactAdmitted =
744 (lambda unrestricted endpoint : Nat .
745 (lambda unrestricted port : Nat .
746 (lambda unrestricted worker : Nat .
747 (lambda unrestricted initialWeight : Nat .
748 (lambda unrestricted wrongMean : Nat .
749 (lambda unrestricted steps : Nat .
750 (lambda unrestricted epoch : Nat .
751 (lambda unrestricted version : Nat .
752 (peerLayouts
753 (lambda unrestricted initial : (family RegionFrameLayout) .
754 (lambda unrestricted contribution : (family RegionFrameLayout) .
755 (lambda unrestricted updated : (family RegionFrameLayout) .
756 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
757 (lambda unrestricted work : Nat .
758 (peerWithTransport
759 endpoint
760 worker
761 initialWeight
762 wrongMean
763 port
764 steps
765 epoch
766 version
767 initial
768 contribution
769 updated
770 acknowledged
771 work)))))))))))))))
772
773-- Counts and epochs enter word-valued runtime state only after admission.
774-- The natural-to-binary64 conversion additionally needs the signed domain.
775def repeatedArtifactFor =
776 (lambda unrestricted endpoint : Nat .
777 (lambda unrestricted port : Nat .
778 (lambda unrestricted worker : Nat .
779 (lambda unrestricted weight : Nat .
780 (lambda unrestricted wrongMean : Nat .
781 (lambda unrestricted steps : Nat .
782 (lambda unrestricted epoch : Nat .
783 (lambda unrestricted version : Nat .
784 (nat-eliminate
785 (lambda unrestricted admitted : Nat . Bytes)
786 b""
787 (lambda unrestricted previous : Nat .
788 (lambda unrestricted ignored : Bytes .
789 (repeatedArtifactAdmitted
790 endpoint
791 port
792 worker
793 weight
794 wrongMean
795 steps
796 epoch
797 version)))
798 (naturalAnd
799 (naturalLessOrEqual steps regionFrameWordLimit)
800 (naturalAnd
801 (naturalLessOrEqual epoch regionFrameWordLimit)
802 (naturalAnd
803 (naturalLessOrEqual version regionFrameWordLimit)
804 (naturalLessOrEqual weight 9223372036854775807)))))))))))))
805
806def peerArtifactFor =
807 (lambda unrestricted endpoint : Nat .
808 (lambda unrestricted port : Nat .
809 (lambda unrestricted worker : Nat .
810 (lambda unrestricted weight : Nat .
811 (lambda unrestricted wrongMean : Nat .
812 (repeatedArtifactFor endpoint port worker weight wrongMean 1 1 0))))))
813
814def peerArtifact =
815 (peerArtifactFor 0 0)
816
817def endpointServerArtifact =
818 (lambda unrestricted weight : Nat . (peerArtifactFor 1 0 0 weight 0))
819
820def endpointWorkerArtifact =
821 (lambda unrestricted port : Nat . (peerArtifactFor 1 port 1 0 0))
822
823def coordinatorArtifact =
824 (lambda unrestricted weight : Nat . (peerArtifact 0 weight 0))
825
826def workerArtifact =
827 (peerArtifact 1 0 0)
828
829def wrongMeanArtifact =
830 (peerArtifact 0 1 1)
831
832def repeatedServerArtifact =
833 (lambda unrestricted weight : Nat .
834 (lambda unrestricted steps : Nat .
835 (lambda unrestricted epoch : Nat .
836 (lambda unrestricted version : Nat .
837 (repeatedArtifactFor 1 0 0 weight 0 steps epoch version)))))
838
839def repeatedWorkerArtifact =
840 (lambda unrestricted port : Nat .
841 (lambda unrestricted steps : Nat .
842 (lambda unrestricted epoch : Nat .
843 (lambda unrestricted version : Nat . (repeatedArtifactFor 1 port 1 0 0 steps epoch version)))))
844
845-- Complete replicated logical state for this deterministic scalar learner:
846-- parameter, completed updates, consumed batches, prior membership epoch.
847-- No optimizer accumulator or RNG state exists in this example. Their absence
848-- here is not permission for another learner to omit its continuation state.
849def peerCheckpointContract =
850 (constructor
851 CheckpointEnvelopeContract
852 CheckpointEnvelopeContractValue
853 b"scalar-parameter-updates-batches-epoch/v1"
854 b"sample-mass-squared-error;rate=1/4;binary64"
855 b"fixed-repeated-batch:x=1,1,2;y=0"
856 b"initial-natural-weight=3"
857 (naturalMultiply 4 peerWordBytes)
858 (naturalMultiply 3 peerWordBytes)
859 1)
860
861def peerCheckpointEpochAt =
862 (lambda unrestricted checkpoint : (family NativeCheckpointLayout) .
863 (naturalAdd (nativeCheckpointPayloadAt checkpoint) (naturalMultiply 3 peerWordBytes)))
864
865def peerArgument =
866 (lambda unrestricted index : Nat .
867 (constructor
868 NativePhysicalOperand
869 NativePhysicalProcessArgument
870 (modelWord64FromNaturalTruncated index)))
871
872def peerCheckpointStart =
873 (lambda unrestricted checkpoint : (family NativeCheckpointLayout) .
874 (lambda unrestricted initial : (family RegionFrameLayout) .
875 (lambda unrestricted resume : Nat .
876 (lambda unrestricted tail : (family NativePhysicalCommands) .
877 (nat-eliminate
878 (lambda unrestricted mode : Nat . (family NativePhysicalCommands))
879 (peerNatural
880 (framePayloadAt initial)
881 3
882 (peerStore
883 (nativeCheckpointUpdatesAt checkpoint)
884 (nativeLaunchRecipeImmediate 0)
885 (peerStore
886 (nativeCheckpointInvocationsAt checkpoint)
887 (nativeLaunchRecipeImmediate 0)
888 (peerStore
889 (peerCheckpointEpochAt checkpoint)
890 (nativeLaunchRecipeImmediate 1)
891 tail))))
892 (lambda unrestricted previous : Nat .
893 (lambda unrestricted ignored : (family NativePhysicalCommands) .
894 (nativeCheckpointRestore
895 checkpoint
896 (peerArgument 1)
897 peerListenerSlot
898 peerScratchSlot
899 (nativeLaunchRecipeAssertEqual
900 (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint))
901 (frameNativeLoad (nativeCheckpointInvocationsAt checkpoint))
902 b"peer-batch-position"
903 (peerStore
904 (framePayloadAt initial)
905 (frameNativeLoad (nativeCheckpointPayloadAt checkpoint))
906 (nativeCheckedWordAdd
907 (frameNativeState (peerCheckpointEpochAt checkpoint))
908 (frameNativeLoad (peerCheckpointEpochAt checkpoint))
909 (nativeLaunchRecipeImmediate 1)
910 peerScratchSlot
911 b"peer-recovery-epoch-overflow"
912 tail))))))
913 resume)))))
914
915def peerCheckpointFinish =
916 (lambda unrestricted checkpoint : (family NativeCheckpointLayout) .
917 (lambda unrestricted initial : (family RegionFrameLayout) .
918 (lambda unrestricted worker : Nat .
919 (lambda unrestricted steps : Nat .
920 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
921 (peerStore
922 (nativeCheckpointPayloadAt checkpoint)
923 (frameNativeLoad (framePayloadAt initial))
924 (nativeCheckedWordAdd
925 (frameNativeState (nativeCheckpointUpdatesAt checkpoint))
926 (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint))
927 (nativeLaunchRecipeImmediate steps)
928 peerScratchSlot
929 b"peer-update-counter-overflow"
930 (nativeCheckedWordAdd
931 (frameNativeState (nativeCheckpointInvocationsAt checkpoint))
932 (frameNativeLoad (nativeCheckpointInvocationsAt checkpoint))
933 (nativeLaunchRecipeImmediate steps)
934 peerScratchSlot
935 b"peer-batch-counter-overflow"
936 (peerByRole
937 worker
938 (nativeCheckpointPublish
939 checkpoint
940 (peerArgument 2)
941 (peerArgument 3)
942 (peerArgument 4)
943 peerListenerSlot
944 peerScratchSlot
945 6
946 (peerOutput descriptor (framePayloadAt initial)))
947 (peerOutput descriptor (framePayloadAt initial)))))))))))
948
949def peerCheckpointWithLayouts =
950 (lambda unrestricted worker : Nat .
951 (lambda unrestricted port : Nat .
952 (lambda unrestricted resume : Nat .
953 (lambda unrestricted steps : Nat .
954 (lambda unrestricted initial : (family RegionFrameLayout) .
955 (lambda unrestricted contribution : (family RegionFrameLayout) .
956 (lambda unrestricted updated : (family RegionFrameLayout) .
957 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
958 (lambda unrestricted work : Nat .
959 (eliminate
960 StdResult
961 (lambda unrestricted r : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
962 Bytes)
963 (planNativeCheckpoint
964 peerCheckpointContract
965 (frameAlign (peerEndpointEnd (peerWorkEnd work)))
966 peerWordBytes
967 (naturalMultiply 2 peerWordBytes)
968 1048576)
969 (branch StdFailure error . b"")
970 (branch
971 StdSuccess
972 checkpoint
973 .
974 (eliminate
975 StdResult
976 (lambda unrestricted addressResult : (family StdResult (family SocketAddressFailure) Bytes) .
977 Bytes)
978 (linuxIPv4SocketAddress ipv4Loopback port)
979 (branch StdFailure error . b"")
980 (branch
981 StdSuccess
982 address
983 .
984 (nativePhysicalGenerateNativeELFBytesDirect
985 (peerProgram
986 peerEndpointSlots
987 (nativeCheckpointEnd checkpoint)
988 (peerCheckpointStart
989 checkpoint
990 initial
991 resume
992 (peerNativeSetup
993 worker
994 address
995 (peerWorkEnd work)
996 (peerImmediateTransmission
997 work
998 (peerUpdates
999 (nativeLaunchRecipeSlotValue peerConnectionSlot)
1000 worker
1001 0
1002 steps
1003 (frameNativeLoad (peerCheckpointEpochAt checkpoint))
1004 (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint))
1005 initial
1006 contribution
1007 updated
1008 acknowledged
1009 work
1010 (peerCheckpointFinish
1011 checkpoint
1012 initial
1013 worker
1014 steps
1015 (nativeLaunchRecipeSlotValue peerConnectionSlot)))))))))))))))))))))
1016
1017def checkpointPeerArtifact =
1018 (lambda unrestricted worker : Nat .
1019 (lambda unrestricted port : Nat .
1020 (lambda unrestricted resume : Nat .
1021 (lambda unrestricted steps : Nat .
1022 (nat-eliminate
1023 (lambda unrestricted fits : Nat . Bytes)
1024 b""
1025 (lambda unrestricted previous : Nat .
1026 (lambda unrestricted ignored : Bytes .
1027 (peerLayouts
1028 (lambda unrestricted initial : (family RegionFrameLayout) .
1029 (lambda unrestricted contribution : (family RegionFrameLayout) .
1030 (lambda unrestricted updated : (family RegionFrameLayout) .
1031 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
1032 (lambda unrestricted work : Nat .
1033 (peerCheckpointWithLayouts
1034 worker
1035 port
1036 resume
1037 steps
1038 initial
1039 contribution
1040 updated
1041 acknowledged
1042 work)))))))))
1043 (naturalLessOrEqual steps regionFrameWordLimit))))))
1044
1045def checkpointPredictionArtifactFor =
1046 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
1047 (eliminate
1048 StdResult
1049 (lambda unrestricted r : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
1050 Bytes)
1051 (planNativeCheckpoint contract 0 peerWordBytes (naturalMultiply 2 peerWordBytes) 1048576)
1052 (branch StdFailure error . b"")
1053 (branch
1054 StdSuccess
1055 checkpoint
1056 .
1057 (nativePhysicalGenerateNativeELFBytesDirect
1058 (peerProgram
1059 peerEndpointSlots
1060 (nativeCheckpointEnd checkpoint)
1061 (nativeCheckpointRestore
1062 checkpoint
1063 (peerArgument 1)
1064 peerListenerSlot
1065 peerScratchSlot
1066 (nativeLaunchRecipeAssertEqual
1067 (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint))
1068 (frameNativeLoad (nativeCheckpointInvocationsAt checkpoint))
1069 b"peer-batch-position"
1070 (peerNatural
1071 (nativeCheckpointSourcePointerAt checkpoint)
1072 2
1073 (peerBinary
1074 peerMultiply
1075 (nativeCheckpointPayloadAt checkpoint)
1076 (nativeCheckpointPayloadAt checkpoint)
1077 (nativeCheckpointSourcePointerAt checkpoint)
1078 (nativeFileCall
1079 1
1080 (nativeLaunchRecipeArguments
1081 (nativeLaunchRecipeImmediate 1)
1082 (nativeMemoryState (nativeCheckpointPayloadAt checkpoint))
1083 (nativeLaunchRecipeImmediate peerWordBytes)
1084 (nativeLaunchRecipeImmediate 0))
1085 peerScratchSlot
1086 peerWordBytes
1087 b"peer-prediction"
1088 peerHalt))))))))))
1089
1090def checkpointPredictionArtifact =
1091 (checkpointPredictionArtifactFor peerCheckpointContract)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.