1module Runtime.NativeIndependentTree
2
3import Learning.IndependentState
4import Component.Pointwise
5import Checkpoint.Envelope
6import Checkpoint.NativeEnvelope
7import Checkpoint.NativeRegions
8import Checkpoint.NativePeerPublication
9import Checkpoint.NativeTreePublication
10import Checkpoint.RegionManifest
11import Compiler.Planning.RegionFrame
12import Representation.ParticipantTree
13import Representation.Partition
14import Runtime.NativeIndependentState
15import Runtime.NativePointwisePlan
16import Runtime.NativePhysicalProgram
17import Runtime.NativePhysicalProgramComposer
18import Runtime.NativeHostTarget
19import Runtime.NativeResourcePlan
20import Runtime.NativeLaunchRecipeLoad
21import Runtime.NativeMemoryPlan
22import Runtime.NativeSocketPlan
23import Runtime.NativePeerEndpoint
24import Runtime.NativePeerTree
25import Runtime.NativeRegionFrame
26import Runtime.NativeWordArithmetic
27import Runtime.RegionTransfer
28import Runtime.ArenaCertificate
29import Learning.Transition
30import Data.Bytes
31import Model.Word64
32import Std.Foundation
33import Std.List
34import Std.Natural
35import Std.Word
36
37-- The independent-state learner over a bounded-fan-out hierarchy instead of a
38-- star: owners 0..n-1 sit at the roles of Representation.ParticipantTree,
39-- each establishes only its parent and child edges
40-- (Runtime.NativePeerTree), trains its own state, and publishes through
41-- Checkpoint.NativeTreePublication: own shard and group manifest locally,
42-- one commitment up, release down. No owner receives another owner's state,
43-- and an owner's arena and edges are bounded by the fan-out and height, not
44-- by n. Resume reads only the root-to-owner manifest path and the owner's
45-- own shard. The local equation, numerics and checkpoint identity of the
46-- state itself are the star realization's (Runtime.NativeIndependentState).
47family NativeIndependentTreeLayout : Type 0
48constructor NativeIndependentTreeLayoutOf
49-- template frames, planned for the edge of role 1; every edge's frames share
50-- this storage (Runtime.NativeIndependentState.niFrameAt)
51field unrestricted independentTreeCommitment : (family RegionFrameLayout)
52field unrestricted independentTreeRelease : (family RegionFrameLayout)
53field unrestricted independentTreeCheckpoint : (family NativeTreeCheckpoint)
54field unrestricted independentTreeScratchWords : Nat
55-- the system identity's digest, computed once per artifact
56field unrestricted independentTreeDigest : Bytes
57
58end-family
59
60def nitCommitment =
61 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
62 (eliminate
63 NativeIndependentTreeLayout
64 (lambda unrestricted current : (family NativeIndependentTreeLayout) .
65 (family RegionFrameLayout))
66 layout
67 (branch
68 NativeIndependentTreeLayoutOf
69 commitment
70 release
71 checkpoint
72 scratch
73 digest
74 .
75 commitment)))
76
77def nitRelease =
78 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
79 (eliminate
80 NativeIndependentTreeLayout
81 (lambda unrestricted current : (family NativeIndependentTreeLayout) .
82 (family RegionFrameLayout))
83 layout
84 (branch NativeIndependentTreeLayoutOf commitment release checkpoint scratch digest . release)))
85
86def nitCheckpoint =
87 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
88 (eliminate
89 NativeIndependentTreeLayout
90 (lambda unrestricted current : (family NativeIndependentTreeLayout) .
91 (family NativeTreeCheckpoint))
92 layout
93 (branch
94 NativeIndependentTreeLayoutOf
95 commitment
96 release
97 checkpoint
98 scratch
99 digest
100 .
101 checkpoint)))
102
103def nitScratchWords =
104 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
105 (eliminate
106 NativeIndependentTreeLayout
107 (lambda unrestricted current : (family NativeIndependentTreeLayout) . Nat)
108 layout
109 (branch NativeIndependentTreeLayoutOf commitment release checkpoint scratch digest . scratch)))
110
111def nitDigest =
112 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
113 (eliminate
114 NativeIndependentTreeLayout
115 (lambda unrestricted current : (family NativeIndependentTreeLayout) . Bytes)
116 layout
117 (branch NativeIndependentTreeLayoutOf commitment release checkpoint scratch digest . digest)))
118
119def nitStateAt =
120 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
121 (nativeCheckpointAlign (nativeTreeEnd (nitCheckpoint layout))))
122
123def nitValuesAt =
124 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
125 (naturalAdd (nitStateAt layout) nativeRegionCaptureBytes))
126
127def nitEndpoint =
128 (lambda unrestricted slots : Nat .
129 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
130 (nativePointwiseAt (nitValuesAt layout) (naturalAdd slots (nitScratchWords layout)))))
131
132def nitExtent =
133 (lambda unrestricted slots : Nat .
134 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
135 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
136 (nativePeerEdgesEnd (nitEndpoint slots layout) edges))))
137
138-- A role holds one interval of the one logical region: its own state words.
139def nitOwnOf =
140 (lambda unrestricted slots : Nat .
141 (lambda unrestricted system : (family IndependentStateSystem slots) .
142 (lambda unrestricted role : Nat .
143 (constructor
144 StdList
145 StdListCons
146 (family CheckpointRegionPartition)
147 (constructor
148 CheckpointRegionPartition
149 CheckpointRegionPartitionOf
150 0
151 (constructor
152 StdList
153 StdListCons
154 (family LogicalInterval)
155 (niInterval slots system role)
156 (constructor StdList StdListEmpty (family LogicalInterval))))
157 (constructor StdList StdListEmpty (family CheckpointRegionPartition))))))
158
159-- The tree protocol is a different publication from the star's, so its
160-- checkpoint identity differs even for the same system and owners.
161def nitContext =
162 (lambda unrestricted slots : Nat .
163 (lambda unrestricted system : (family IndependentStateSystem slots) .
164 (constructor
165 CheckpointEnvelopeContract
166 CheckpointEnvelopeContractValue
167 (bytes-append
168 b"independent-tree-state-f64-finite-rne-separate-v1;"
169 (independentStateIdentity slots system))
170 b"typed-sequential-local-transitions"
171 b"immutable-local-inputs;one-input-round-per-update"
172 b"declared-initial-state;no-randomness"
173 1
174 1
175 1)))
176
177def nitParent =
178 (lambda unrestricted fanout : Nat .
179 (lambda unrestricted count : Nat .
180 (lambda unrestricted role : Nat .
181 (participantTreeParentOf (participantTreeNode fanout count role)))))
182
183-- The frames of the edge between `child` and its parent.
184def nitCommitmentFor =
185 (lambda unrestricted slots : Nat .
186 (lambda unrestricted system : (family IndependentStateSystem slots) .
187 (lambda unrestricted fanout : Nat .
188 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
189 (lambda unrestricted child : Nat .
190 (niFrameAt
191 (niIdentity
192 slots
193 system
194 (nitDigest layout)
195 2
196 child
197 (nitParent fanout (niOwners slots system) child))
198 nativeTreeCommitmentBytes
199 (nitCommitment layout)))))))
200
201def nitReleaseFor =
202 (lambda unrestricted slots : Nat .
203 (lambda unrestricted system : (family IndependentStateSystem slots) .
204 (lambda unrestricted fanout : Nat .
205 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
206 (lambda unrestricted child : Nat .
207 (niFrameAt
208 (niIdentity
209 slots
210 system
211 (nitDigest layout)
212 3
213 (nitParent fanout (niOwners slots system) child)
214 child)
215 nativePointwiseWordBytes
216 (nitRelease layout)))))))
217
218def nitWithLayout =
219 (lambda unrestricted slots : Nat .
220 (lambda unrestricted system : (family IndependentStateSystem slots) .
221 (lambda unrestricted fanout : Nat .
222 (lambda unrestricted role : Nat .
223 (lambda unrestricted epoch : Nat .
224 (lambda unrestricted base : Nat .
225 (lambda unrestricted scratchWords : Nat .
226 (lambda unrestricted available : Nat .
227 (lambda unrestricted emit : (pi unrestricted layout : (family NativeIndependentTreeLayout) . Bytes) .
228 (let unrestricted digest =
229 (niIdentityDigest slots system)
230 in
231 (eliminate
232 StdResult
233 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
234 Bytes)
235 (planRegionFrameLayout
236 (niIdentity slots system digest 2 1 0)
237 nativeTreeCommitmentBytes
238 512
239 base
240 available)
241 (branch StdFailure error . b"")
242 (branch
243 StdSuccess
244 commitment
245 .
246 (eliminate
247 StdResult
248 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
249 Bytes)
250 (planRegionFrameLayout
251 (niIdentity slots system digest 3 0 1)
252 nativePointwiseWordBytes
253 512
254 (frameAlign (frameEnd commitment))
255 available)
256 (branch StdFailure error . b"")
257 (branch
258 StdSuccess
259 release
260 .
261 (eliminate
262 StdResult
263 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)) .
264 Bytes)
265 (planNativeTreeCheckpoint
266 (nitContext slots system)
267 (niRegions slots system)
268 fanout
269 (niOwners slots system)
270 role
271 (nitOwnOf slots system)
272 epoch
273 (frameAlign (frameEnd release))
274 available)
275 (branch StdFailure error . b"")
276 (branch
277 StdSuccess
278 checkpoint
279 .
280 (emit
281 (constructor
282 NativeIndependentTreeLayout
283 NativeIndependentTreeLayoutOf
284 commitment
285 release
286 checkpoint
287 scratchWords
288 digest))))))))))))))))))
289
290-- argv for n owners (positions after the program name): 1 the previous root
291-- manifest; 1 + r the previous group manifest of role r >= 1; n + 1 + r the
292-- previous shard of role r; 2n + 1 + 2r and 2n + 2 + 2r the candidate and
293-- committed group manifest of role r (role 0's is the published root);
294-- 4n + 1 + 2r and 4n + 2 + 2r role r's candidate and committed shard; 6n + 1
295-- the generation directory. Every owner receives the same argv and reads
296-- only its own entries and its ancestors'.
297def nitPaths =
298 (lambda unrestricted owners : Nat .
299 (lambda unrestricted role : Nat .
300 (let unrestricted groups =
301 (succ (naturalMultiply 2 owners))
302 in
303 (let unrestricted shards =
304 (succ (naturalMultiply 4 owners))
305 in
306 (constructor
307 NativeTreePaths
308 NativeTreePathsOf
309 (lambda unrestricted at : Nat . (succ at))
310 (lambda unrestricted index : Nat . (succ (naturalAdd owners role)))
311 (naturalAdd groups (naturalMultiply 2 role))
312 (succ (naturalAdd groups (naturalMultiply 2 role)))
313 (lambda unrestricted index : Nat . (naturalAdd shards (naturalMultiply 2 role)))
314 (lambda unrestricted index : Nat . (succ (naturalAdd shards (naturalMultiply 2 role))))
315 (succ (naturalMultiply 6 owners)))))))
316
317-- Fresh: version, cursor 0 and the plan's epoch. Resume: the verified path
318-- restore, the restored prefix, then epoch + 1 (a new membership epoch).
319def nitStart =
320 (lambda unrestricted slots : Nat .
321 (lambda unrestricted system : (family IndependentStateSystem slots) .
322 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
323 (lambda unrestricted fanout : Nat .
324 (lambda unrestricted role : Nat .
325 (lambda unrestricted resume : Nat .
326 (lambda unrestricted tail : (family NativePhysicalCommands) .
327 (let unrestricted stateAt =
328 (nitStateAt layout)
329 in
330 (nat-eliminate
331 (lambda unrestricted mode : Nat . (family NativePhysicalCommands))
332 (nativeMemoryStoreWord64
333 b"independent-version"
334 stateAt
335 (nativeLaunchRecipeImmediate 0)
336 (nativeMemoryStoreWord64
337 b"independent-cursor"
338 (nativePointwiseAt stateAt 1)
339 (nativeLaunchRecipeImmediate 0)
340 (nativeMemoryStoreWord64
341 b"independent-epoch"
342 (nativePointwiseAt stateAt 2)
343 (nativeLaunchRecipeImmediate (nativeTreeEpoch (nitCheckpoint layout)))
344 tail)))
345 (lambda unrestricted previous : Nat .
346 (lambda unrestricted ignored : (family NativePhysicalCommands) .
347 (nativeTreeRestore
348 (nitCheckpoint layout)
349 fanout
350 (niOwners slots system)
351 role
352 (nitOwnOf slots system)
353 (nitPaths (niOwners slots system) role)
354 (lambda unrestricted shard : (family NativeRegionShard) .
355 (nitValuesAt layout))
356 (nativeMemoryCopyOperands
357 (nativeMemoryState stateAt)
358 (nativeMemoryState (nativeTreeRestoredCaptureAt (nitCheckpoint layout)))
359 nativeRegionCaptureBytes
360 nativePeerScratchSlot
361 b"independent-restore-capture"
362 (nativeLaunchRecipeAssertEqual
363 (nativeMemoryLoad stateAt)
364 (nativeMemoryLoad (nativePointwiseAt stateAt 1))
365 b"independent-input-position"
366 (nativeCheckedWordAdd
367 (nativeMemoryState (nativePointwiseAt stateAt 2))
368 (nativeMemoryLoad (nativePointwiseAt stateAt 2))
369 (nativeLaunchRecipeImmediate 1)
370 nativePeerScratchSlot
371 b"independent-epoch-overflow"
372 tail))))))
373 resume)))))))))
374
375-- The publication plan of this generation: the planned layouts with the
376-- new membership epoch after a resume.
377def nitPublicationPlan =
378 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
379 (lambda unrestricted resume : Nat .
380 (nativeTreeCheckpointAdvanced (nitCheckpoint layout) resume)))
381
382def nitCommands =
383 (lambda unrestricted slots : Nat .
384 (lambda unrestricted system : (family IndependentStateSystem slots) .
385 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
386 (lambda unrestricted fanout : Nat .
387 (lambda unrestricted role : Nat .
388 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
389 (lambda unrestricted resume : Nat .
390 (lambda unrestricted steps : Nat .
391 (lambda unrestricted step : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
392 (let unrestricted owners =
393 (niOwners slots system)
394 in
395 (let unrestricted stateAt =
396 (nitStateAt layout)
397 in
398 (niInitializeAt
399 slots
400 system
401 (nitValuesAt layout)
402 role
403 (nitStart
404 slots
405 system
406 layout
407 fanout
408 role
409 resume
410 (niFinite
411 (nitValuesAt layout)
412 slots
413 (nativePeerEdgeSetup
414 role
415 edges
416 (nitEndpoint slots layout)
417 (niRoundsAt
418 stateAt
419 steps
420 step
421 (nativeTreePublish
422 (nitPublicationPlan layout resume)
423 fanout
424 owners
425 role
426 edges
427 (nitCommitmentFor slots system fanout layout)
428 (nitReleaseFor slots system fanout layout)
429 stateAt
430 nativeRegionCaptureBytes
431 (lambda unrestricted shard : (family NativeRegionShard) .
432 nativeRegionCaptureBytes)
433 (nitPaths owners role)
434 (nativePeerEdgesFold
435 edges
436 (lambda unrestricted index : Nat .
437 (lambda unrestricted edge : (family NativePeerEdge) .
438 (nativeSocketCloseChecked
439 (nativeLaunchRecipeSlotValue
440 (nativePeerEdgeConnectionSlot index))
441 nativePeerScratchSlot)))
442 (niOutput stateAt (niCaptureBytes slots system) niHalt)))))))))))))))))))
443
444-- Every edge's frames share the template's storage exactly, and the plan,
445-- frames, state and endpoint state fit the declared arena.
446def nitFramesAdmitted =
447 (lambda unrestricted slots : Nat .
448 (lambda unrestricted system : (family IndependentStateSystem slots) .
449 (lambda unrestricted fanout : Nat .
450 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
451 (stdListFold
452 Nat
453 Nat
454 (lambda unrestricted index : Nat .
455 (lambda unrestricted rest : Nat .
456 (naturalAnd
457 rest
458 (naturalAnd
459 (naturalEqual
460 (frameEnd (nitCommitmentFor slots system fanout layout (succ index)))
461 (frameEnd (nitCommitment layout)))
462 (naturalEqual
463 (frameEnd (nitReleaseFor slots system fanout layout (succ index)))
464 (frameEnd (nitRelease layout)))))))
465 1
466 (stdListNaturalsBelow (naturalPredecessor (niOwners slots system))))))))
467
468def nitRunAdmitted =
469 (lambda unrestricted slots : Nat .
470 (lambda unrestricted system : (family IndependentStateSystem slots) .
471 (lambda unrestricted fanout : Nat .
472 (lambda unrestricted role : Nat .
473 (lambda unrestricted addresses : (family StdList Bytes) .
474 (lambda unrestricted resume : Nat .
475 (lambda unrestricted epoch : Nat .
476 (lambda unrestricted steps : Nat .
477 (naturalAnd
478 (niOwnersAdmitted slots system)
479 (naturalAnd
480 (nativePeerTreeListedAdmitted fanout (niOwners slots system) role addresses)
481 (naturalAnd
482 (naturalLessOrEqual resume 1)
483 (naturalAnd
484 (naturalNonzero epoch)
485 (naturalAnd
486 (naturalBelowTwoPower 64 (naturalAdd epoch resume))
487 (naturalBelowTwoPower 64 steps))))))))))))))
488
489def nativeIndependentTreeArtifact =
490 (lambda unrestricted target : (family NativeHostTarget) .
491 (lambda unrestricted resources : (family NativeResourceContext) .
492 (lambda unrestricted slots : Nat .
493 (lambda unrestricted system : (family IndependentStateSystem slots) .
494 (lambda unrestricted fanout : Nat .
495 (lambda unrestricted role : Nat .
496 (lambda unrestricted addresses : (family StdList Bytes) .
497 (lambda unrestricted resume : Nat .
498 (lambda unrestricted epoch : Nat .
499 (lambda unrestricted steps : Nat .
500 (lambda unrestricted available : Nat .
501 (let unrestricted edges =
502 (nativePeerTreeEdgesListed fanout (niOwners slots system) role addresses)
503 in
504 (nitWithLayout
505 slots
506 system
507 fanout
508 role
509 epoch
510 0
511 (pointwiseProgramTemporaryValues
512 StdU64
513 slots
514 (independentAssignments slots system))
515 available
516 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
517 (let unrestricted extent =
518 (nitExtent slots layout edges)
519 in
520 (nat-eliminate
521 (lambda unrestricted valid : Nat . Bytes)
522 b""
523 (lambda unrestricted previous : Nat .
524 (lambda unrestricted ignored : Bytes .
525 (eliminate
526 StdResult
527 (lambda unrestricted result : (family StdResult Bytes (family NativePhysicalCommands)) .
528 Bytes)
529 (planNativePointwiseProgram
530 slots
531 (independentAssignments slots system)
532 (nitValuesAt layout)
533 (nitEndpoint slots layout)
534 nativePeerScratchSlot
535 niEnd)
536 (branch StdFailure error . b"")
537 (branch
538 StdSuccess
539 step
540 .
541 (nativeHostTargetResourceArtifact
542 target
543 resources
544 (niProgramFor
545 (nativePeerEdgeSlots edges)
546 extent
547 (nitCommands
548 slots
549 system
550 layout
551 fanout
552 role
553 edges
554 resume
555 steps
556 (nativePhysicalProgramComposeCommandsAppend step))))))))
557 (naturalAnd
558 (nitRunAdmitted
559 slots
560 system
561 fanout
562 role
563 addresses
564 resume
565 epoch
566 steps)
567 (naturalAnd
568 (nitFramesAdmitted slots system fanout layout)
569 (naturalAnd
570 (naturalLessOrEqual extent available)
571 (arenaCertificate
572 extent
573 (constructor
574 ArenaResidents
575 ArenaResidentsNext
576 (constructor
577 ArenaResident
578 ArenaResidentValue
579 b"tree-commitment-frame"
580 (frameBase (nitCommitment layout))
581 (naturalSaturatingSubtract
582 (frameEnd (nitCommitment layout))
583 (frameBase (nitCommitment layout)))
584 1)
585 (constructor
586 ArenaResidents
587 ArenaResidentsNext
588 (constructor
589 ArenaResident
590 ArenaResidentValue
591 b"tree-release-frame"
592 (frameBase (nitRelease layout))
593 (naturalSaturatingSubtract
594 (frameEnd (nitRelease layout))
595 (frameBase (nitRelease layout)))
596 1)
597 (constructor
598 ArenaResidents
599 ArenaResidentsNext
600 (constructor
601 ArenaResident
602 ArenaResidentValue
603 b"tree-owner-state-and-endpoints"
604 (nitStateAt layout)
605 (naturalSaturatingSubtract extent (nitStateAt layout))
606 nativeCheckpointWordBytes)
607 (nativeTreeResidents (nitCheckpoint layout)))))))))))))))))))))))))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.