1module Runtime.NativeIndependentState
2
3import Learning.IndependentState
4import Component.Pointwise
5import Checkpoint.Envelope
6import Checkpoint.NativeEnvelope
7import Checkpoint.NativeRegions
8import Checkpoint.NativePeerPublication
9import Checkpoint.RegionManifest
10import Compiler.Planning.RegionFrame
11import Runtime.NativePointwisePlan
12import Runtime.NativePhysicalProgram
13import Runtime.NativePhysicalProgramComposer
14import Runtime.NativePhysicalNativeELF
15import Runtime.NativeHostTarget
16import Runtime.NativeResourcePlan
17import Runtime.NativeLaunchRecipeLoad
18import Runtime.NativeMemoryPlan
19import Runtime.NativeFloatPlan
20import Runtime.NativeFilePlan
21import Runtime.NativeSocketPlan
22import Runtime.NativePeerEndpoint
23import Runtime.NativeRegionFrame
24import Runtime.NativeWordArithmetic
25import Runtime.RegionTransfer
26import Runtime.ArenaCertificate
27import Learning.Transition
28import Representation.Partition
29import Data.Bytes
30import Data.SHA256Padding
31import Data.SHA256Digest
32import Model.Word64
33import Std.Byte
34import Std.Foundation
35import Std.List
36import Std.Natural
37import Std.Word
38
39-- This realization compiles separately owned state transitions, one per
40-- observation row of the system: owners 0..n-1 over a star. There is no
41-- per-step collective because the admitted transition reads only local state
42-- and immutable local inputs. The final capture joins every authority at
43-- owner 0 (Checkpoint.NativePeerPublication); a missing or differently
44-- advanced owner cannot publish a logical checkpoint.
45-- Execution is selected explicitly: target callbacks supply local state work,
46-- while this owner supplies versions, transport and durable publication.
47family NativeIndependentLayout : Type 0
48constructor NativeIndependentLayoutOf
49field unrestricted independentCaptureFrame : (family RegionFrameLayout)
50field unrestricted independentCommittedFrame : (family RegionFrameLayout)
51field unrestricted independentCheckpointPlan : (family NativeRegionCheckpoint)
52field unrestricted independentHostScratchWords : Nat
53-- the system identity's digest, computed once per artifact: every frame
54-- identity of the owner names it
55field unrestricted independentDigest : Bytes
56
57end-family
58
59def niCapture =
60 (lambda unrestricted layout : (family NativeIndependentLayout) .
61 (eliminate
62 NativeIndependentLayout
63 (lambda unrestricted current : (family NativeIndependentLayout) . (family RegionFrameLayout))
64 layout
65 (branch NativeIndependentLayoutOf capture committed checkpoint scratchWords digest . capture)))
66
67def niCommitted =
68 (lambda unrestricted layout : (family NativeIndependentLayout) .
69 (eliminate
70 NativeIndependentLayout
71 (lambda unrestricted current : (family NativeIndependentLayout) . (family RegionFrameLayout))
72 layout
73 (branch
74 NativeIndependentLayoutOf
75 capture
76 committed
77 checkpoint
78 scratchWords
79 digest
80 .
81 committed)))
82
83def niCheckpoint =
84 (lambda unrestricted layout : (family NativeIndependentLayout) .
85 (eliminate
86 NativeIndependentLayout
87 (lambda unrestricted current : (family NativeIndependentLayout) .
88 (family NativeRegionCheckpoint))
89 layout
90 (branch
91 NativeIndependentLayoutOf
92 capture
93 committed
94 checkpoint
95 scratchWords
96 digest
97 .
98 checkpoint)))
99
100-- Scratch is selected by the realization. A GPU state program needs no host
101-- arithmetic temporaries; its callback reserves only actual session state.
102def niScratchWords =
103 (lambda unrestricted layout : (family NativeIndependentLayout) .
104 (eliminate
105 NativeIndependentLayout
106 (lambda unrestricted current : (family NativeIndependentLayout) . Nat)
107 layout
108 (branch
109 NativeIndependentLayoutOf
110 capture
111 committed
112 checkpoint
113 scratchWords
114 digest
115 .
116 scratchWords)))
117
118def niDigest =
119 (lambda unrestricted layout : (family NativeIndependentLayout) .
120 (eliminate
121 NativeIndependentLayout
122 (lambda unrestricted current : (family NativeIndependentLayout) . Bytes)
123 layout
124 (branch NativeIndependentLayoutOf capture committed checkpoint scratchWords digest . digest)))
125
126def niEnd =
127 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
128
129def niHalt =
130 (nativeLaunchRecipeCommand
131 (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
132 b"independent-done"
133 niEnd)
134
135-- The owners: one per observation row of the system.
136def niOwners =
137 (lambda unrestricted slots : Nat .
138 (lambda unrestricted system : (family IndependentStateSystem slots) .
139 (stdListLength (family StdList StdU64) (independentInitialValues slots system))))
140
141-- argv: previous manifest, one previous shard per owner, then each owner's
142-- candidate/committed output shard, the manifest pair and the directory.
143def niPaths =
144 (lambda unrestricted slots : Nat .
145 (lambda unrestricted system : (family IndependentStateSystem slots) .
146 (constructor NativeRegionPaths NativeRegionPathsOf 1 (niOwners slots system))))
147
148def niStateAt =
149 (lambda unrestricted layout : (family NativeIndependentLayout) .
150 (nativeRegionEnd (niCheckpoint layout)))
151
152def niValuesAt =
153 (lambda unrestricted layout : (family NativeIndependentLayout) .
154 (naturalAdd (niStateAt layout) nativeRegionCaptureBytes))
155
156def niWidth =
157 (lambda unrestricted slots : Nat .
158 (lambda unrestricted system : (family IndependentStateSystem slots) .
159 (nativePointwiseAt 0 (independentPersistentCount slots system))))
160
161def niCaptureBytes =
162 (lambda unrestricted slots : Nat .
163 (lambda unrestricted system : (family IndependentStateSystem slots) .
164 (naturalAdd nativeRegionCaptureBytes (niWidth slots system))))
165
166def niEndpoint =
167 (lambda unrestricted slots : Nat .
168 (lambda unrestricted system : (family IndependentStateSystem slots) .
169 (lambda unrestricted layout : (family NativeIndependentLayout) .
170 (nativePointwiseAt (niValuesAt layout) (naturalAdd slots (niScratchWords layout))))))
171
172-- The endpoint state holds one address entry per edge of this owner.
173def niExtent =
174 (lambda unrestricted slots : Nat .
175 (lambda unrestricted system : (family IndependentStateSystem slots) .
176 (lambda unrestricted layout : (family NativeIndependentLayout) .
177 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
178 (nativePeerEdgesEnd (niEndpoint slots system layout) edges)))))
179
180def niInterval =
181 (lambda unrestricted slots : Nat .
182 (lambda unrestricted system : (family IndependentStateSystem slots) .
183 (lambda unrestricted owner : Nat .
184 (constructor
185 LogicalInterval
186 LogicalIntervalOf
187 (naturalMultiply owner (niWidth slots system))
188 (naturalMultiply (succ owner) (niWidth slots system))))))
189
190def niRegions =
191 (lambda unrestricted slots : Nat .
192 (lambda unrestricted system : (family IndependentStateSystem slots) .
193 (constructor
194 StdList
195 StdListCons
196 (family CheckpointLogicalRegion)
197 (constructor
198 CheckpointLogicalRegion
199 CheckpointLogicalRegionOf
200 b"owned-state"
201 b"f64-le"
202 (naturalMultiply (niOwners slots system) (niWidth slots system)))
203 (constructor StdList StdListEmpty (family CheckpointLogicalRegion)))))
204
205def niPartitions =
206 (lambda unrestricted slots : Nat .
207 (lambda unrestricted system : (family IndependentStateSystem slots) .
208 (constructor
209 StdList
210 StdListCons
211 (family CheckpointRegionPartition)
212 (constructor
213 CheckpointRegionPartition
214 CheckpointRegionPartitionOf
215 0
216 (stdListMap
217 Nat
218 (family LogicalInterval)
219 (niInterval slots system)
220 (stdListNaturalsBelow (niOwners slots system))))
221 (constructor StdList StdListEmpty (family CheckpointRegionPartition)))))
222
223def niContext =
224 (lambda unrestricted slots : Nat .
225 (lambda unrestricted system : (family IndependentStateSystem slots) .
226 (constructor
227 CheckpointEnvelopeContract
228 CheckpointEnvelopeContractValue
229 (bytes-append
230 b"independent-owner-state-f64-finite-rne-separate-v2;"
231 (independentStateIdentity slots system))
232 b"typed-sequential-local-transitions"
233 b"immutable-local-inputs;one-input-round-per-update"
234 b"declared-initial-state;no-randomness"
235 1
236 1
237 1)))
238
239def niIdentityDigest =
240 (lambda unrestricted slots : Nat .
241 (lambda unrestricted system : (family IndependentStateSystem slots) .
242 (sha256RawDigestOrEmpty (independentStateIdentity slots system))))
243
244def niIdentity =
245 (lambda unrestricted slots : Nat .
246 (lambda unrestricted system : (family IndependentStateSystem slots) .
247 (lambda unrestricted digest : Bytes .
248 (lambda unrestricted operation : Nat .
249 (lambda unrestricted sender : Nat .
250 (lambda unrestricted receiver : Nat .
251 (constructor
252 RegionTransferIdentity
253 RegionTransferIdentityOf
254 digest
255 b"independent-state-v1"
256 b"owned-state"
257 b"finite-f64-rne-separate"
258 (constructor LearningRound LearningRoundOf 1 0)
259 operation
260 sender
261 receiver
262 (constructor
263 LogicalInterval
264 LogicalIntervalOf
265 0
266 (naturalMultiply (niOwners slots system) (niWidth slots system))))))))))
267
268-- One owner's frame in the storage the layout planned for owner 1. Frames
269-- differ only in their identity-bound header. A frame that cannot be planned
270-- there falls back to an empty header: its extent then differs from owner
271-- 1's, and Checkpoint.NativePeerPublication's shared-storage admission
272-- refuses the whole publication instead of using a misidentified frame.
273def niFrameAt =
274 (lambda unrestricted identity : (family RegionTransferIdentity) .
275 (lambda unrestricted payload : Nat .
276 (lambda unrestricted at : (family RegionFrameLayout) .
277 (eliminate
278 StdResult
279 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
280 (family RegionFrameLayout))
281 (planRegionFrameLayout identity payload 512 (frameBase at) (frameEnd at))
282 (branch
283 StdFailure
284 error
285 .
286 (constructor RegionFrameLayout RegionFrameLayoutOf b"" payload (frameBase at) b""))
287 (branch StdSuccess frame . frame)))))
288
289def niCaptureFor =
290 (lambda unrestricted slots : Nat .
291 (lambda unrestricted system : (family IndependentStateSystem slots) .
292 (lambda unrestricted layout : (family NativeIndependentLayout) .
293 (lambda unrestricted owner : Nat .
294 (niFrameAt
295 (niIdentity slots system (niDigest layout) 0 owner 0)
296 (niCaptureBytes slots system)
297 (niCapture layout))))))
298
299def niCommittedFor =
300 (lambda unrestricted slots : Nat .
301 (lambda unrestricted system : (family IndependentStateSystem slots) .
302 (lambda unrestricted layout : (family NativeIndependentLayout) .
303 (lambda unrestricted owner : Nat .
304 (niFrameAt
305 (niIdentity slots system (niDigest layout) 1 0 owner)
306 nativePointwiseWordBytes
307 (niCommitted layout))))))
308
309-- Owner 0 has an edge to every other owner, in order; every other owner has
310-- one edge, to owner 0. `addresses` are those edges' addresses.
311def niEdges =
312 (lambda unrestricted slots : Nat .
313 (lambda unrestricted system : (family IndependentStateSystem slots) .
314 (lambda unrestricted owner : Nat .
315 (lambda unrestricted addresses : (family StdList Bytes) .
316 (nativePeerStarEdges owner addresses)))))
317
318def niEdgesAdmitted =
319 (lambda unrestricted slots : Nat .
320 (lambda unrestricted system : (family IndependentStateSystem slots) .
321 (lambda unrestricted owner : Nat .
322 (lambda unrestricted addresses : (family StdList Bytes) .
323 (nativePeerStarAdmitted (niOwners slots system) owner addresses)))))
324
325def niPublication =
326 (lambda unrestricted slots : Nat .
327 (lambda unrestricted system : (family IndependentStateSystem slots) .
328 (lambda unrestricted layout : (family NativeIndependentLayout) .
329 (lambda unrestricted resume : Nat .
330 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
331 (constructor
332 NativePeerRegionPublication
333 NativePeerRegionPublicationOf
334 (constructor
335 NativeRegionCheckpoint
336 NativeRegionCheckpointOf
337 (nativeRegionManifest (niCheckpoint layout))
338 (nativeRegionShards (niCheckpoint layout))
339 (naturalAdd (nativeRegionEpoch (niCheckpoint layout)) resume)
340 (nativeRegionEnd (niCheckpoint layout)))
341 (naturalPredecessor (niOwners slots system))
342 (niCaptureFor slots system layout)
343 (niCommittedFor slots system layout)
344 (nativePeerEdgeConnectionTo edges)
345 (niStateAt layout)
346 (niCaptureBytes slots system)
347 nativeRegionCaptureBytes
348 (lambda unrestricted shard : (family NativeRegionShard) .
349 (naturalDivideUnchecked
350 (intervalBegin (nativeRegionInterval shard))
351 (niWidth slots system)))
352 (lambda unrestricted shard : (family NativeRegionShard) . nativeRegionCaptureBytes)
353 (niPaths slots system)))))))
354
355def niWithLayout =
356 (lambda unrestricted slots : Nat .
357 (lambda unrestricted system : (family IndependentStateSystem slots) .
358 (lambda unrestricted epoch : Nat .
359 (lambda unrestricted base : Nat .
360 (lambda unrestricted scratchWords : Nat .
361 (lambda unrestricted available : Nat .
362 (lambda unrestricted emit : (pi unrestricted layout : (family NativeIndependentLayout) . Bytes) .
363 (let unrestricted digest =
364 (niIdentityDigest slots system)
365 in
366 (eliminate
367 StdResult
368 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
369 Bytes)
370 (planRegionFrameLayout
371 (niIdentity slots system digest 0 1 0)
372 (niCaptureBytes slots system)
373 512
374 base
375 available)
376 (branch StdFailure error . b"")
377 (branch
378 StdSuccess
379 capture
380 .
381 (eliminate
382 StdResult
383 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
384 Bytes)
385 (planRegionFrameLayout
386 (niIdentity slots system digest 1 0 1)
387 nativePointwiseWordBytes
388 512
389 (frameAlign (frameEnd capture))
390 available)
391 (branch StdFailure error . b"")
392 (branch
393 StdSuccess
394 committed
395 .
396 (eliminate
397 StdResult
398 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
399 Bytes)
400 (planNativeRegionCheckpoint
401 (niContext slots system)
402 (niRegions slots system)
403 (niPartitions slots system)
404 epoch
405 (frameAlign (frameEnd committed))
406 available
407 (niOwners slots system))
408 (branch StdFailure error . b"")
409 (branch
410 StdSuccess
411 checkpoint
412 .
413 (emit
414 (constructor
415 NativeIndependentLayout
416 NativeIndependentLayoutOf
417 capture
418 committed
419 checkpoint
420 scratchWords
421 digest))))))))))))))))
422
423def niDestinations =
424 (lambda unrestricted slots : Nat .
425 (lambda unrestricted system : (family IndependentStateSystem slots) .
426 (lambda unrestricted layout : (family NativeIndependentLayout) .
427 (lambda unrestricted owner : Nat .
428 (constructor
429 StdList
430 StdListCons
431 (family NativeRegionDestination)
432 (constructor
433 NativeRegionDestination
434 NativeRegionDestinationOf
435 0
436 (niInterval slots system owner)
437 (niValuesAt layout))
438 (constructor StdList StdListEmpty (family NativeRegionDestination)))))))
439
440def niOutput =
441 (lambda unrestricted base : Nat .
442 (lambda unrestricted size : Nat .
443 (lambda unrestricted tail : (family NativePhysicalCommands) .
444 (nativeFileCall
445 1
446 (nativeLaunchRecipeArguments
447 (nativeLaunchRecipeImmediate 1)
448 (nativeMemoryState base)
449 (nativeLaunchRecipeImmediate size)
450 (nativeLaunchRecipeImmediate 0))
451 nativePeerScratchSlot
452 size
453 b"independent-result"
454 tail))))
455
456def niRow =
457 (lambda unrestricted slots : Nat .
458 (lambda unrestricted system : (family IndependentStateSystem slots) .
459 (lambda unrestricted owner : Nat .
460 (stdListHeadOr
461 (family StdList StdU64)
462 (constructor StdList StdListEmpty StdU64)
463 (stdListDrop (family StdList StdU64) owner (independentInitialValues slots system))))))
464
465def niInitializeAt =
466 (lambda unrestricted slots : Nat .
467 (lambda unrestricted system : (family IndependentStateSystem slots) .
468 (lambda unrestricted valuesAt : Nat .
469 (lambda unrestricted owner : Nat .
470 (lambda unrestricted tail : (family NativePhysicalCommands) .
471 (stdListFold
472 StdU64
473 (pi unrestricted index : Nat . (family NativePhysicalCommands))
474 (lambda unrestricted word : StdU64 .
475 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
476 (lambda unrestricted index : Nat .
477 (nativeMemoryStoreWord64
478 b"independent-initial"
479 (nativePointwiseAt valuesAt index)
480 (nativeLaunchRecipeImmediate (modelWord64Natural word))
481 (next (succ index))))))
482 (lambda unrestricted index : Nat . tail)
483 (niRow slots system owner)
484 0))))))
485
486def niInitialize =
487 (lambda unrestricted slots : Nat .
488 (lambda unrestricted system : (family IndependentStateSystem slots) .
489 (lambda unrestricted layout : (family NativeIndependentLayout) .
490 (niInitializeAt slots system (niValuesAt layout)))))
491
492def niFinite =
493 (lambda unrestricted base : Nat .
494 (lambda unrestricted count : Nat .
495 (lambda unrestricted tail : (family NativePhysicalCommands) .
496 (stdListFold
497 Nat
498 (family NativePhysicalCommands)
499 (lambda unrestricted index : Nat .
500 (lambda unrestricted rest : (family NativePhysicalCommands) .
501 (nativeFloat64RequireFinite
502 (nativeMemoryLoad (nativePointwiseAt base index))
503 nativePeerScratchSlot
504 b"independent-state-nonfinite"
505 rest)))
506 tail
507 (stdListNaturalsBelow count)))))
508
509-- Version and cursor advance only after the target's step returns. These
510-- address-based owners serve every topology (star and hierarchy).
511def niAdvanceAt =
512 (lambda unrestricted stateAt : Nat .
513 (lambda unrestricted tail : (family NativePhysicalCommands) .
514 (nativeCheckedWordAdd
515 (nativeMemoryState stateAt)
516 (nativeMemoryLoad stateAt)
517 (nativeLaunchRecipeImmediate 1)
518 nativePeerScratchSlot
519 b"independent-version-overflow"
520 (nativeCheckedWordAdd
521 (nativeMemoryState (nativePointwiseAt stateAt 1))
522 (nativeMemoryLoad (nativePointwiseAt stateAt 1))
523 (nativeLaunchRecipeImmediate 1)
524 nativePeerScratchSlot
525 b"independent-cursor-overflow"
526 tail))))
527
528def niAdvance =
529 (lambda unrestricted layout : (family NativeIndependentLayout) . (niAdvanceAt (niStateAt layout)))
530
531-- The target owns the step's arithmetic and refusal. Logical position advances
532-- only after that callback returns successfully; capture occurs after all steps.
533def niRoundsAt =
534 (lambda unrestricted stateAt : Nat .
535 (lambda unrestricted steps : Nat .
536 (lambda unrestricted step : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
537 (lambda unrestricted tail : (family NativePhysicalCommands) .
538 (nativeLaunchRecipeCommand
539 (constructor
540 NativePhysicalOperation
541 NativePhysicalRepeatBeginCounted
542 (nativeLaunchRecipeImmediate steps))
543 b"independent-repeat"
544 (step
545 (niAdvanceAt
546 stateAt
547 (nativeLaunchRecipeCommand
548 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
549 b"independent-repeat-end"
550 tail))))))))
551
552def niRoundsWith =
553 (lambda unrestricted layout : (family NativeIndependentLayout) . (niRoundsAt (niStateAt layout)))
554
555def niRestore =
556 (lambda unrestricted slots : Nat .
557 (lambda unrestricted system : (family IndependentStateSystem slots) .
558 (lambda unrestricted layout : (family NativeIndependentLayout) .
559 (lambda unrestricted owner : Nat .
560 (lambda unrestricted extent : Nat .
561 (lambda unrestricted tail : (family NativePhysicalCommands) .
562 (planNativeRegionRestore
563 (niCheckpoint layout)
564 (nativeRegionPathArgument (nativeRegionPathFirst (niPaths slots system)))
565 (lambda unrestricted index : Nat .
566 (nativeRegionPathArgument
567 (naturalAdd (nativeRegionInputShardBase (niPaths slots system)) index)))
568 nativePeerListenerSlot
569 nativePeerScratchSlot
570 extent
571 (niDestinations slots system layout owner)
572 (nativeMemoryCopyOperands
573 (nativeMemoryState (niStateAt layout))
574 (nativeMemoryState (nativeRegionCaptureAt (niCheckpoint layout)))
575 nativeRegionCaptureBytes
576 nativePeerScratchSlot
577 b"independent-restore-capture"
578 (nativeLaunchRecipeAssertEqual
579 (nativeMemoryLoad (niStateAt layout))
580 (nativeMemoryLoad (nativePointwiseAt (niStateAt layout) 1))
581 b"independent-input-position"
582 (nativeCheckedWordAdd
583 (nativeMemoryState (nativePointwiseAt (niStateAt layout) 2))
584 (nativeMemoryLoad (nativePointwiseAt (niStateAt layout) 2))
585 (nativeLaunchRecipeImmediate 1)
586 nativePeerScratchSlot
587 b"independent-epoch-overflow"
588 tail))))))))))
589
590def niStart =
591 (lambda unrestricted slots : Nat .
592 (lambda unrestricted system : (family IndependentStateSystem slots) .
593 (lambda unrestricted layout : (family NativeIndependentLayout) .
594 (lambda unrestricted owner : Nat .
595 (lambda unrestricted extent : Nat .
596 (lambda unrestricted resume : Nat .
597 (lambda unrestricted tail : (family NativePhysicalCommands) .
598 (nat-eliminate
599 (lambda unrestricted mode : Nat .
600 (family
601 StdResult
602 (family NativeCheckpointFailure)
603 (family NativePhysicalCommands)))
604 (constructor
605 StdResult
606 StdSuccess
607 (family NativeCheckpointFailure)
608 (family NativePhysicalCommands)
609 (nativeMemoryStoreWord64
610 b"independent-version"
611 (niStateAt layout)
612 (nativeLaunchRecipeImmediate 0)
613 (nativeMemoryStoreWord64
614 b"independent-cursor"
615 (nativePointwiseAt (niStateAt layout) 1)
616 (nativeLaunchRecipeImmediate 0)
617 (nativeMemoryStoreWord64
618 b"independent-epoch"
619 (nativePointwiseAt (niStateAt layout) 2)
620 (nativeLaunchRecipeImmediate (nativeRegionEpoch (niCheckpoint layout)))
621 tail))))
622 (lambda unrestricted previous : Nat .
623 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
624 (niRestore slots system layout owner extent tail)))
625 resume))))))))
626
627def niProgramFor =
628 (lambda unrestricted resultSlots : Nat .
629 (lambda unrestricted extent : Nat .
630 (lambda unrestricted commands : (family NativePhysicalCommands) .
631 (nativePhysicalProgramFromCommands
632 (bytes-append
633 b"independent-state-native-v1"
634 (dataBytesRepeatByte
635 (byte 0)
636 (naturalSaturatingSubtract 64 (bytes-length b"independent-state-native-v1"))))
637 extent
638 resultSlots
639 commands))))
640
641-- At least two owners: a single owner has no peer to publish with.
642def niOwnersAdmitted =
643 (lambda unrestricted slots : Nat .
644 (lambda unrestricted system : (family IndependentStateSystem slots) .
645 (naturalAnd
646 (independentStateAdmitted slots system)
647 (naturalLessOrEqual 2 (niOwners slots system)))))
648
649def niRunAdmitted =
650 (lambda unrestricted slots : Nat .
651 (lambda unrestricted system : (family IndependentStateSystem slots) .
652 (lambda unrestricted owner : Nat .
653 (lambda unrestricted resume : Nat .
654 (lambda unrestricted epoch : Nat .
655 (lambda unrestricted steps : Nat .
656 (naturalAnd
657 (niOwnersAdmitted slots system)
658 (naturalAnd
659 (naturalLess owner (niOwners slots system))
660 (naturalAnd
661 (naturalLessOrEqual resume 1)
662 (naturalAnd
663 (naturalNonzero epoch)
664 (naturalAnd
665 (naturalBelowTwoPower 64 (naturalAdd epoch resume))
666 (naturalBelowTwoPower 64 steps))))))))))))
667
668-- Preparation follows initial-state/checkpoint validation. A target uploads
669-- that state once, executes its own local steps, and captures its authoritative
670-- values before publication. The publisher never observes stale host shadows.
671def niCommandsWith =
672 (lambda unrestricted slots : Nat .
673 (lambda unrestricted system : (family IndependentStateSystem slots) .
674 (lambda unrestricted layout : (family NativeIndependentLayout) .
675 (lambda unrestricted owner : Nat .
676 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
677 (lambda unrestricted resume : Nat .
678 (lambda unrestricted steps : Nat .
679 (lambda unrestricted extent : Nat .
680 (lambda unrestricted prepare : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
681 (lambda unrestricted step : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
682 (lambda unrestricted capture : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
683 (lambda unrestricted finish : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
684 (stdResultBind
685 (family NativeCheckpointFailure)
686 (family NativePhysicalCommands)
687 (family NativePhysicalCommands)
688 (planNativePeerRegionPublish
689 (niPublication slots system layout resume edges)
690 extent
691 owner
692 (nativePeerEdgesFold
693 edges
694 (lambda unrestricted index : Nat .
695 (lambda unrestricted edge : (family NativePeerEdge) .
696 (nativeSocketCloseChecked
697 (nativeLaunchRecipeSlotValue
698 (nativePeerEdgeConnectionSlot index))
699 nativePeerScratchSlot)))
700 (niOutput
701 (niStateAt layout)
702 (niCaptureBytes slots system)
703 (finish niHalt))))
704 (lambda unrestricted published : (family NativePhysicalCommands) .
705 (stdResultBind
706 (family NativeCheckpointFailure)
707 (family NativePhysicalCommands)
708 (family NativePhysicalCommands)
709 (niStart
710 slots
711 system
712 layout
713 owner
714 extent
715 resume
716 (niFinite
717 (niValuesAt layout)
718 slots
719 (nativePeerEdgeSetup
720 owner
721 edges
722 (niEndpoint slots system layout)
723 (prepare (niRoundsWith layout steps step (capture published))))))
724 (lambda unrestricted commands : (family NativePhysicalCommands) .
725 (constructor
726 StdResult
727 StdSuccess
728 (family NativeCheckpointFailure)
729 (family NativePhysicalCommands)
730 (niInitialize slots system layout owner commands))))))))))))))))))
731
732def nativeIndependentArtifact =
733 (lambda unrestricted target : (family NativeHostTarget) .
734 (lambda unrestricted resources : (family NativeResourceContext) .
735 (lambda unrestricted slots : Nat .
736 (lambda unrestricted system : (family IndependentStateSystem slots) .
737 (lambda unrestricted owner : Nat .
738 (lambda unrestricted addresses : (family StdList Bytes) .
739 (lambda unrestricted resume : Nat .
740 (lambda unrestricted epoch : Nat .
741 (lambda unrestricted steps : Nat .
742 (lambda unrestricted available : Nat .
743 (let unrestricted edges =
744 (niEdges slots system owner addresses)
745 in
746 (niWithLayout
747 slots
748 system
749 epoch
750 0
751 (pointwiseProgramTemporaryValues
752 StdU64
753 slots
754 (independentAssignments slots system))
755 available
756 (lambda unrestricted layout : (family NativeIndependentLayout) .
757 (nat-eliminate
758 (lambda unrestricted valid : Nat . Bytes)
759 b""
760 (lambda unrestricted previous : Nat .
761 (lambda unrestricted ignored : Bytes .
762 (eliminate
763 StdResult
764 (lambda unrestricted result : (family StdResult Bytes (family NativePhysicalCommands)) .
765 Bytes)
766 (planNativePointwiseProgram
767 slots
768 (independentAssignments slots system)
769 (niValuesAt layout)
770 (niEndpoint slots system layout)
771 nativePeerScratchSlot
772 niEnd)
773 (branch StdFailure error . b"")
774 (branch
775 StdSuccess
776 step
777 .
778 (eliminate
779 StdResult
780 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
781 Bytes)
782 (niCommandsWith
783 slots
784 system
785 layout
786 owner
787 edges
788 resume
789 steps
790 (niExtent slots system layout edges)
791 (lambda unrestricted tail : (family NativePhysicalCommands) .
792 tail)
793 (nativePhysicalProgramComposeCommandsAppend step)
794 (lambda unrestricted tail : (family NativePhysicalCommands) .
795 tail)
796 (lambda unrestricted tail : (family NativePhysicalCommands) .
797 tail))
798 (branch StdFailure error . b"")
799 (branch
800 StdSuccess
801 commands
802 .
803 (nativeHostTargetResourceArtifact
804 target
805 resources
806 (niProgramFor
807 (nativePeerEdgeSlots edges)
808 (niExtent slots system layout edges)
809 commands))))))))
810 (naturalAnd
811 (niRunAdmitted slots system owner resume epoch steps)
812 (naturalAnd
813 (niEdgesAdmitted slots system owner addresses)
814 (naturalLessOrEqual
815 (niExtent slots system layout edges)
816 available)))))))))))))))))
817
818-- Evaluation restores the joined logical state through the same checkpoint
819-- owner. A target evaluates and captures before the public result is written.
820def niEvaluationCommands =
821 (lambda unrestricted paths : (family NativeRegionPaths) .
822 (lambda unrestricted width : Nat .
823 (lambda unrestricted checkpoint : (family NativeRegionCheckpoint) .
824 (lambda unrestricted base : Nat .
825 (lambda unrestricted extent : Nat .
826 (lambda unrestricted prepare : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
827 (lambda unrestricted evaluate : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
828 (lambda unrestricted capture : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
829 (lambda unrestricted finish : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
830 (planNativeRegionRestore
831 checkpoint
832 (nativeRegionPathArgument (nativeRegionPathFirst paths))
833 (lambda unrestricted index : Nat .
834 (nativeRegionPathArgument
835 (naturalAdd (nativeRegionInputShardBase paths) index)))
836 nativePeerListenerSlot
837 nativePeerScratchSlot
838 extent
839 (constructor
840 StdList
841 StdListCons
842 (family NativeRegionDestination)
843 (constructor
844 NativeRegionDestination
845 NativeRegionDestinationOf
846 0
847 (constructor
848 LogicalInterval
849 LogicalIntervalOf
850 0
851 (nativePointwiseAt 0 width))
852 base)
853 (constructor StdList StdListEmpty (family NativeRegionDestination)))
854 (nativeLaunchRecipeAssertEqual
855 (nativeMemoryLoad (nativeRegionCaptureAt checkpoint))
856 (nativeMemoryLoad (nativePointwiseAt (nativeRegionCaptureAt checkpoint) 1))
857 b"independent-input-position"
858 (niFinite
859 base
860 width
861 (prepare
862 (evaluate
863 (capture (niOutput base nativePointwiseWordBytes (finish niHalt)))))))))))))))))
864
865def nativeIndependentEvaluation =
866 (lambda unrestricted target : (family NativeHostTarget) .
867 (lambda unrestricted resources : (family NativeResourceContext) .
868 (lambda unrestricted slots : Nat .
869 (lambda unrestricted system : (family IndependentStateSystem slots) .
870 (lambda unrestricted epoch : Nat .
871 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 (naturalMultiply (niOwners slots system) (independentPersistentCount slots system)))) .
872 (lambda unrestricted available : Nat .
873 (eliminate
874 StdResult
875 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
876 Bytes)
877 (planNativeRegionCheckpoint
878 (niContext slots system)
879 (niRegions slots system)
880 (niPartitions slots system)
881 epoch
882 0
883 available
884 (niOwners slots system))
885 (branch StdFailure error . b"")
886 (branch
887 StdSuccess
888 checkpoint
889 .
890 (let unrestricted width =
891 (naturalMultiply
892 (niOwners slots system)
893 (independentPersistentCount slots system))
894 in
895 (let unrestricted base =
896 (nativeRegionEnd checkpoint)
897 in
898 (let unrestricted extent =
899 (nativePointwiseExtent width program base)
900 in
901 (nat-eliminate
902 (lambda unrestricted valid : Nat . Bytes)
903 b""
904 (lambda unrestricted previous : Nat .
905 (lambda unrestricted ignored : Bytes .
906 (eliminate
907 StdResult
908 (lambda unrestricted result : (family StdResult Bytes (family NativePhysicalCommands)) .
909 Bytes)
910 (planNativePointwiseProgram
911 width
912 program
913 base
914 extent
915 nativePeerScratchSlot
916 niEnd)
917 (branch StdFailure error . b"")
918 (branch
919 StdSuccess
920 evaluated
921 .
922 (eliminate
923 StdResult
924 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
925 Bytes)
926 (niEvaluationCommands
927 (niPaths slots system)
928 width
929 checkpoint
930 base
931 extent
932 (lambda unrestricted tail : (family NativePhysicalCommands) .
933 tail)
934 (nativePhysicalProgramComposeCommandsAppend evaluated)
935 (lambda unrestricted tail : (family NativePhysicalCommands) .
936 tail)
937 (lambda unrestricted tail : (family NativePhysicalCommands) .
938 tail))
939 (branch StdFailure error . b"")
940 (branch
941 StdSuccess
942 commands
943 .
944 (nativeHostTargetResourceArtifact
945 target
946 resources
947 (niProgramFor nativePeerEndpointSlots extent commands))))))))
948 (naturalAnd
949 (independentStateAdmitted slots system)
950 (naturalAnd
951 (niOwnersAdmitted slots system)
952 (naturalLessOrEqual extent available))))))))))))))))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.