1module Checkpoint.NativeRegions
2
3import Checkpoint.Envelope
4import Checkpoint.NativeEnvelope
5import Checkpoint.RegionManifest
6import Representation.Partition
7import Runtime.NativePhysicalProgram
8import Runtime.NativeLaunchRecipeLoad
9import Runtime.NativeMemoryPlan
10import Runtime.ArenaCertificate
11import Model.Word64
12import Data.Bytes
13import Std.Foundation
14import Std.List
15import Std.Natural
16
17-- Fixed-membership POSIX realization. Prepared files are immutable durable
18-- NativeEnvelope publications on the admitted store. The manifest binds their
19-- actual payload digests, not rank/path names. This bounded publisher stages
20-- each shard privately; it is not the hierarchical fleet checkpoint owner.
21-- A store lease keeps referenced files immutable and retained through restore.
22family NativeRegionShard : Type 0
23constructor NativeRegionShardOf
24field unrestricted nativeRegionOrdinalValue : Nat
25field unrestricted nativeRegionIntervalValue : (family LogicalInterval)
26field unrestricted nativeRegionLayoutValue : (family NativeCheckpointLayout)
27
28end-family
29
30family NativeRegionCheckpoint : Type 0
31constructor NativeRegionCheckpointOf
32field unrestricted nativeRegionManifestValue : (family NativeCheckpointLayout)
33field unrestricted nativeRegionShardsValue : (family StdList (family NativeRegionShard))
34field unrestricted nativeRegionEpochValue : Nat
35field unrestricted nativeRegionEndValue : Nat
36
37end-family
38
39family NativeRegionDestination : Type 0
40constructor NativeRegionDestinationOf
41field unrestricted nativeRegionDestinationOrdinal : Nat
42field unrestricted nativeRegionDestinationInterval : (family LogicalInterval)
43field unrestricted nativeRegionDestinationOffset : Nat
44
45end-family
46
47def nativeRegionOrdinal =
48 (lambda unrestricted value : (family NativeRegionShard) .
49 (eliminate
50 NativeRegionShard
51 (lambda unrestricted current : (family NativeRegionShard) . Nat)
52 value
53 (branch
54 NativeRegionShardOf
55 nativeRegionOrdinal
56 nativeRegionInterval
57 nativeRegionLayout
58 .
59 nativeRegionOrdinal)))
60
61def nativeRegionInterval =
62 (lambda unrestricted value : (family NativeRegionShard) .
63 (eliminate
64 NativeRegionShard
65 (lambda unrestricted current : (family NativeRegionShard) . (family LogicalInterval))
66 value
67 (branch
68 NativeRegionShardOf
69 nativeRegionOrdinal
70 nativeRegionInterval
71 nativeRegionLayout
72 .
73 nativeRegionInterval)))
74
75def nativeRegionLayout =
76 (lambda unrestricted value : (family NativeRegionShard) .
77 (eliminate
78 NativeRegionShard
79 (lambda unrestricted current : (family NativeRegionShard) . (family NativeCheckpointLayout))
80 value
81 (branch
82 NativeRegionShardOf
83 nativeRegionOrdinal
84 nativeRegionInterval
85 nativeRegionLayout
86 .
87 nativeRegionLayout)))
88
89def nativeRegionManifest =
90 (lambda unrestricted value : (family NativeRegionCheckpoint) .
91 (eliminate
92 NativeRegionCheckpoint
93 (lambda unrestricted current : (family NativeRegionCheckpoint) .
94 (family NativeCheckpointLayout))
95 value
96 (branch
97 NativeRegionCheckpointOf
98 nativeRegionManifest
99 nativeRegionShards
100 nativeRegionEpoch
101 nativeRegionEnd
102 .
103 nativeRegionManifest)))
104
105def nativeRegionShards =
106 (lambda unrestricted value : (family NativeRegionCheckpoint) .
107 (eliminate
108 NativeRegionCheckpoint
109 (lambda unrestricted current : (family NativeRegionCheckpoint) .
110 (family StdList (family NativeRegionShard)))
111 value
112 (branch
113 NativeRegionCheckpointOf
114 nativeRegionManifest
115 nativeRegionShards
116 nativeRegionEpoch
117 nativeRegionEnd
118 .
119 nativeRegionShards)))
120
121def nativeRegionEpoch =
122 (lambda unrestricted value : (family NativeRegionCheckpoint) .
123 (eliminate
124 NativeRegionCheckpoint
125 (lambda unrestricted current : (family NativeRegionCheckpoint) . Nat)
126 value
127 (branch
128 NativeRegionCheckpointOf
129 nativeRegionManifest
130 nativeRegionShards
131 nativeRegionEpoch
132 nativeRegionEnd
133 .
134 nativeRegionEpoch)))
135
136def nativeRegionEnd =
137 (lambda unrestricted value : (family NativeRegionCheckpoint) .
138 (eliminate
139 NativeRegionCheckpoint
140 (lambda unrestricted current : (family NativeRegionCheckpoint) . Nat)
141 value
142 (branch
143 NativeRegionCheckpointOf
144 nativeRegionManifest
145 nativeRegionShards
146 nativeRegionEpoch
147 nativeRegionEnd
148 .
149 nativeRegionEnd)))
150
151-- Capture words are update, consumed-input cursor, and membership epoch.
152-- The first two are protected by NativeEnvelope's counter agreement checks.
153def nativeRegionCaptureBytes =
154 (naturalMultiply 3 nativeCheckpointWordBytes)
155
156def nativeRegionDescriptorBytes =
157 (naturalMultiply 3 nativeCheckpointWordBytes)
158
159def nativeRegionRecordBytes =
160 (naturalAdd nativeRegionDescriptorBytes checkpointEnvelopeDigestBytes)
161
162def nativeRegionDescriptor =
163 (lambda unrestricted ordinal : Nat .
164 (lambda unrestricted interval : (family LogicalInterval) .
165 (bytes-append
166 (checkpointEnvelopeWord ordinal)
167 (bytes-append
168 (checkpointEnvelopeWord (intervalBegin interval))
169 (checkpointEnvelopeWord (intervalEnd interval))))))
170
171def nativeRegionContract =
172 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
173 (lambda unrestricted schema : Bytes .
174 (lambda unrestricted extent : Nat .
175 (eliminate
176 CheckpointEnvelopeContract
177 (lambda unrestricted current : (family CheckpointEnvelopeContract) .
178 (family CheckpointEnvelopeContract))
179 context
180 (branch
181 CheckpointEnvelopeContractValue
182 original
183 learner
184 data
185 seed
186 payload
187 chunk
188 updates
189 .
190 (constructor
191 CheckpointEnvelopeContract
192 CheckpointEnvelopeContractValue
193 (bytes-builder-build
194 (bytes-builder-append
195 (checkpointManifestSized original)
196 (checkpointManifestSized schema)))
197 learner
198 data
199 seed
200 extent
201 extent
202 updates))))))
203
204def nativeRegionPartitionBytes =
205 (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) .
206 (bytes-builder-build
207 (stdListFold
208 (family CheckpointRegionPartition)
209 BytesBuilder
210 (lambda unrestricted part : (family CheckpointRegionPartition) .
211 (lambda unrestricted rest : BytesBuilder .
212 (bytes-builder-append
213 (bytes-builder-append
214 (bytes-builder-chunk (checkpointEnvelopeWord (checkpointPartitionOrdinal part)))
215 (bytes-builder-append
216 (bytes-builder-chunk
217 (checkpointEnvelopeWord
218 (stdListLength (family LogicalInterval) (checkpointPartitionIntervals part))))
219 (stdListFold
220 (family LogicalInterval)
221 BytesBuilder
222 (lambda unrestricted interval : (family LogicalInterval) .
223 (lambda unrestricted more : BytesBuilder .
224 (bytes-builder-append
225 (bytes-builder-chunk
226 (nativeRegionDescriptor (checkpointPartitionOrdinal part) interval))
227 more)))
228 (bytes-builder-empty)
229 (checkpointPartitionIntervals part))))
230 rest)))
231 (bytes-builder-empty)
232 parts)))
233
234def nativeRegionShardCount =
235 (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) .
236 (stdListFold
237 (family CheckpointRegionPartition)
238 Nat
239 (lambda unrestricted part : (family CheckpointRegionPartition) .
240 (lambda unrestricted rest : Nat .
241 (naturalAdd
242 (stdListLength (family LogicalInterval) (checkpointPartitionIntervals part))
243 rest)))
244 0
245 parts))
246
247def nativeRegionAppend =
248 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
249 (lambda unrestricted logical : Bytes .
250 (lambda unrestricted available : Nat .
251 (lambda unrestricted ordinal : Nat .
252 (lambda unrestricted interval : (family LogicalInterval) .
253 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
254 (eliminate
255 StdResult
256 (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
257 (family
258 StdResult
259 (family NativeCheckpointFailure)
260 (family NativeRegionCheckpoint)))
261 result
262 (branch
263 StdFailure
264 error
265 .
266 (constructor
267 StdResult
268 StdFailure
269 (family NativeCheckpointFailure)
270 (family NativeRegionCheckpoint)
271 error))
272 (branch
273 StdSuccess
274 plan
275 .
276 (eliminate
277 StdResult
278 (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
279 (family
280 StdResult
281 (family NativeCheckpointFailure)
282 (family NativeRegionCheckpoint)))
283 (planNativeCheckpoint
284 (nativeRegionContract
285 context
286 (bytes-append
287 b"ALPHA-REGION-SHARD-1\x00"
288 (bytes-append logical (nativeRegionDescriptor ordinal interval)))
289 (naturalAdd nativeRegionCaptureBytes (intervalExtent interval)))
290 (nativeCheckpointAlign (nativeRegionEnd plan))
291 0
292 nativeCheckpointWordBytes
293 available)
294 (branch
295 StdFailure
296 error
297 .
298 (constructor
299 StdResult
300 StdFailure
301 (family NativeCheckpointFailure)
302 (family NativeRegionCheckpoint)
303 error))
304 (branch
305 StdSuccess
306 layout
307 .
308 (constructor
309 StdResult
310 StdSuccess
311 (family NativeCheckpointFailure)
312 (family NativeRegionCheckpoint)
313 (constructor
314 NativeRegionCheckpoint
315 NativeRegionCheckpointOf
316 (nativeRegionManifest plan)
317 (constructor
318 StdList
319 StdListCons
320 (family NativeRegionShard)
321 (constructor
322 NativeRegionShard
323 NativeRegionShardOf
324 ordinal
325 interval
326 layout)
327 (nativeRegionShards plan))
328 (nativeRegionEpoch plan)
329 (nativeCheckpointEnd layout)))))))))))))
330
331def nativeRegionAppendParts =
332 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
333 (lambda unrestricted logical : Bytes .
334 (lambda unrestricted available : Nat .
335 (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) .
336 (lambda unrestricted initial : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
337 (stdListFold
338 (family CheckpointRegionPartition)
339 (pi unrestricted previous : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
340 (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)))
341 (lambda unrestricted part : (family CheckpointRegionPartition) .
342 (lambda unrestricted continuation : (pi unrestricted previous : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) .
343 (lambda unrestricted previous : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
344 (continuation
345 (stdListFold
346 (family LogicalInterval)
347 (pi unrestricted prior : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
348 (family
349 StdResult
350 (family NativeCheckpointFailure)
351 (family NativeRegionCheckpoint)))
352 (lambda unrestricted interval : (family LogicalInterval) .
353 (lambda unrestricted next : (pi unrestricted prior : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) .
354 (lambda unrestricted prior : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
355 (next
356 (nativeRegionAppend
357 context
358 logical
359 available
360 (checkpointPartitionOrdinal part)
361 interval
362 prior)))))
363 (lambda unrestricted prior : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
364 prior)
365 (checkpointPartitionIntervals part)
366 previous)))))
367 (lambda unrestricted previous : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
368 previous)
369 parts
370 initial))))))
371
372def planNativeRegionCheckpoint =
373 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
374 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
375 (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) .
376 (lambda unrestricted epoch : Nat .
377 (lambda unrestricted base : Nat .
378 (lambda unrestricted available : Nat .
379 (lambda unrestricted fragmentLimit : Nat .
380 (nat-eliminate
381 (lambda unrestricted flag : Nat .
382 (family
383 StdResult
384 (family NativeCheckpointFailure)
385 (family NativeRegionCheckpoint)))
386 (constructor
387 StdResult
388 StdFailure
389 (family NativeCheckpointFailure)
390 (family NativeRegionCheckpoint)
391 (constructor NativeCheckpointFailure NativeCheckpointBounds))
392 (lambda unrestricted previous : Nat .
393 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
394 (let unrestricted logical =
395 (checkpointLogicalSchemaBytes regions)
396 in
397 (eliminate
398 StdResult
399 (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
400 (family
401 StdResult
402 (family NativeCheckpointFailure)
403 (family NativeRegionCheckpoint)))
404 (planNativeCheckpoint
405 (nativeRegionContract
406 context
407 (bytes-append
408 b"ALPHA-REGION-MANIFEST-1\x00"
409 (bytes-append logical (nativeRegionPartitionBytes parts)))
410 (naturalAdd
411 nativeRegionCaptureBytes
412 (naturalMultiply
413 (nativeRegionShardCount parts)
414 nativeRegionRecordBytes)))
415 base
416 0
417 nativeCheckpointWordBytes
418 available)
419 (branch
420 StdFailure
421 error
422 .
423 (constructor
424 StdResult
425 StdFailure
426 (family NativeCheckpointFailure)
427 (family NativeRegionCheckpoint)
428 error))
429 (branch
430 StdSuccess
431 manifest
432 .
433 (eliminate
434 StdResult
435 (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
436 (family
437 StdResult
438 (family NativeCheckpointFailure)
439 (family NativeRegionCheckpoint)))
440 (nativeRegionAppendParts
441 context
442 logical
443 available
444 parts
445 (constructor
446 StdResult
447 StdSuccess
448 (family NativeCheckpointFailure)
449 (family NativeRegionCheckpoint)
450 (constructor
451 NativeRegionCheckpoint
452 NativeRegionCheckpointOf
453 manifest
454 (constructor StdList StdListEmpty (family NativeRegionShard))
455 epoch
456 (nativeCheckpointEnd manifest))))
457 (branch
458 StdFailure
459 error
460 .
461 (constructor
462 StdResult
463 StdFailure
464 (family NativeCheckpointFailure)
465 (family NativeRegionCheckpoint)
466 error))
467 (branch
468 StdSuccess
469 plan
470 .
471 (constructor
472 StdResult
473 StdSuccess
474 (family NativeCheckpointFailure)
475 (family NativeRegionCheckpoint)
476 (constructor
477 NativeRegionCheckpoint
478 NativeRegionCheckpointOf
479 manifest
480 (stdListReverse
481 (family NativeRegionShard)
482 (nativeRegionShards plan))
483 epoch
484 (nativeRegionEnd plan))))))))))
485 (naturalAnd
486 (checkpointPartitionsValid regions parts)
487 (naturalAnd
488 (naturalNonzero epoch)
489 (naturalAnd
490 (checkpointManifestWordFits epoch)
491 (naturalLessOrEqual (nativeRegionShardCount parts) fragmentLimit))))))))))))
492
493def nativeRegionCaptureAt =
494 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
495 (nativeCheckpointPayloadAt (nativeRegionManifest plan)))
496
497def nativeRegionRecordAt =
498 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
499 (lambda unrestricted index : Nat .
500 (naturalAdd
501 (nativeRegionCaptureAt plan)
502 (naturalAdd nativeRegionCaptureBytes (naturalMultiply index nativeRegionRecordBytes)))))
503
504def nativeRegionRequireEpoch =
505 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
506 (lambda unrestricted tail : (family NativePhysicalCommands) .
507 (nativeLaunchRecipeAssertEqual
508 (nativeMemoryLoad
509 (naturalAdd (nativeRegionCaptureAt plan) (naturalMultiply 2 nativeCheckpointWordBytes)))
510 (nativeLaunchRecipeImmediate (nativeRegionEpoch plan))
511 b"checkpoint-membership-epoch"
512 tail)))
513
514def nativeRegionLoadShards =
515 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
516 (lambda unrestricted path : (pi unrestricted index : Nat . (family NativePhysicalOperand)) .
517 (lambda unrestricted descriptor : Nat .
518 (lambda unrestricted scratch : Nat .
519 (lambda unrestricted writing : Nat .
520 (lambda unrestricted tail : (family NativePhysicalCommands) .
521 (stdListFold
522 (family NativeRegionShard)
523 (pi unrestricted index : Nat . (family NativePhysicalCommands))
524 (lambda unrestricted shard : (family NativeRegionShard) .
525 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
526 (lambda unrestricted index : Nat .
527 (let unrestricted layout =
528 (nativeRegionLayout shard)
529 in
530 (let unrestricted record =
531 (nativeRegionRecordAt plan index)
532 in
533 (nativeCheckpointRestore
534 layout
535 (path index)
536 descriptor
537 scratch
538 (nativeMemoryCompareRegions
539 (nativeRegionCaptureAt plan)
540 (nativeCheckpointPayloadAt layout)
541 nativeRegionCaptureBytes
542 scratch
543 b"checkpoint-capture-mismatch"
544 (nat-eliminate
545 (lambda unrestricted flag : Nat . (family NativePhysicalCommands))
546 (nativeMemoryCopyPayload
547 (nativeCheckpointMetadataAt (nativeRegionManifest plan))
548 (nativeRegionDescriptor
549 (nativeRegionOrdinal shard)
550 (nativeRegionInterval shard))
551 (nativeMemoryCompareRegions
552 record
553 (nativeCheckpointMetadataAt (nativeRegionManifest plan))
554 nativeRegionDescriptorBytes
555 scratch
556 b"checkpoint-region-descriptor"
557 (nativeMemoryCompareRegions
558 (naturalAdd record nativeRegionDescriptorBytes)
559 (naturalAdd
560 (nativeCheckpointBase layout)
561 checkpointEnvelopeDigestsAt)
562 checkpointEnvelopeDigestBytes
563 scratch
564 b"checkpoint-prepared-digest"
565 (next (succ index)))))
566 (lambda unrestricted previous : Nat .
567 (lambda unrestricted unused : (family NativePhysicalCommands) .
568 (nativeMemoryCopyPayload
569 record
570 (nativeRegionDescriptor
571 (nativeRegionOrdinal shard)
572 (nativeRegionInterval shard))
573 (nativeMemoryCopyOperands
574 (nativeMemoryState
575 (naturalAdd record nativeRegionDescriptorBytes))
576 (nativeMemoryState
577 (naturalAdd
578 (nativeCheckpointBase layout)
579 checkpointEnvelopeDigestsAt))
580 checkpointEnvelopeDigestBytes
581 scratch
582 b"checkpoint-record-digest"
583 (next (succ index))))))
584 writing))))))))
585 (lambda unrestricted index : Nat . tail)
586 (nativeRegionShards plan)
587 0)))))))
588
589def nativeRegionPublish =
590 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
591 (lambda unrestricted captureAt : Nat .
592 (lambda unrestricted path : (pi unrestricted index : Nat . (family NativePhysicalOperand)) .
593 (lambda unrestricted candidate : (family NativePhysicalOperand) .
594 (lambda unrestricted committed : (family NativePhysicalOperand) .
595 (lambda unrestricted directory : (family NativePhysicalOperand) .
596 (lambda unrestricted descriptor : Nat .
597 (lambda unrestricted scratch : Nat .
598 (lambda unrestricted stages : Nat .
599 (lambda unrestricted tail : (family NativePhysicalCommands) .
600 (nativeMemoryCopyOperands
601 (nativeMemoryState (nativeRegionCaptureAt plan))
602 (nativeMemoryState captureAt)
603 nativeRegionCaptureBytes
604 scratch
605 b"checkpoint-capture-copy"
606 (nativeRegionRequireEpoch
607 plan
608 (nativeRegionLoadShards
609 plan
610 path
611 descriptor
612 scratch
613 1
614 (nativeCheckpointPublish
615 (nativeRegionManifest plan)
616 candidate
617 committed
618 directory
619 descriptor
620 scratch
621 stages
622 tail))))))))))))))
623
624def nativeRegionRestore =
625 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
626 (lambda unrestricted manifestPath : (family NativePhysicalOperand) .
627 (lambda unrestricted path : (pi unrestricted index : Nat . (family NativePhysicalOperand)) .
628 (lambda unrestricted descriptor : Nat .
629 (lambda unrestricted scratch : Nat .
630 (lambda unrestricted tail : (family NativePhysicalCommands) .
631 (nativeCheckpointRestore
632 (nativeRegionManifest plan)
633 manifestPath
634 descriptor
635 scratch
636 (nativeRegionRequireEpoch
637 plan
638 (nativeRegionLoadShards plan path descriptor scratch 0 tail)))))))))
639
640-- Materialization is deliberately separate from validation: the consumer calls
641-- it only in nativeRegionRestore's success continuation, after every referenced
642-- shard is checked. Destination ownership/bounds belong to the host arena plan.
643-- This small realization scans the admitted fragment list for each requested
644-- interval; fragmentLimit bounds its scope. Fleet lowering must replace that
645-- bounded scan with hierarchical routing, not lift the cap silently.
646def nativeRegionCopyInterval =
647 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
648 (lambda unrestricted ordinal : Nat .
649 (lambda unrestricted wanted : (family LogicalInterval) .
650 (lambda unrestricted destination : Nat .
651 (lambda unrestricted scratch : Nat .
652 (lambda unrestricted tail : (family NativePhysicalCommands) .
653 (stdListFold
654 (family NativeRegionShard)
655 (family NativePhysicalCommands)
656 (lambda unrestricted shard : (family NativeRegionShard) .
657 (lambda unrestricted next : (family NativePhysicalCommands) .
658 (let unrestricted begin =
659 (intervalBegin (intervalIntersection wanted (nativeRegionInterval shard)))
660 in
661 (let unrestricted end =
662 (naturalMinimum
663 (intervalEnd wanted)
664 (intervalEnd (nativeRegionInterval shard)))
665 in
666 (nat-eliminate
667 (lambda unrestricted flag : Nat . (family NativePhysicalCommands))
668 next
669 (lambda unrestricted previous : Nat .
670 (lambda unrestricted unused : (family NativePhysicalCommands) .
671 (nativeMemoryCopyOperands
672 (nativeMemoryState
673 (naturalAdd
674 destination
675 (naturalSaturatingSubtract begin (intervalBegin wanted))))
676 (nativeMemoryState
677 (naturalAdd
678 (nativeCheckpointPayloadAt (nativeRegionLayout shard))
679 (naturalAdd
680 nativeRegionCaptureBytes
681 (naturalSaturatingSubtract
682 begin
683 (intervalBegin (nativeRegionInterval shard))))))
684 (naturalSaturatingSubtract end begin)
685 scratch
686 b"checkpoint-repartition-copy"
687 next)))
688 (naturalAnd
689 (naturalEqual ordinal (nativeRegionOrdinal shard))
690 (naturalLess begin end)))))))
691 tail
692 (nativeRegionShards plan))))))))
693
694def nativeRegionResidents =
695 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
696 (constructor
697 ArenaResidents
698 ArenaResidentsNext
699 (constructor
700 ArenaResident
701 ArenaResidentValue
702 b"checkpoint-regions-private-staging"
703 (nativeCheckpointBase (nativeRegionManifest plan))
704 (naturalSaturatingSubtract
705 (nativeRegionEnd plan)
706 (nativeCheckpointBase (nativeRegionManifest plan)))
707 1)
708 (constructor ArenaResidents ArenaResidentsEnd)))
709
710-- Check each requested coordinate against the admitted, non-overlapping saved
711-- partition. The byte sum is sound here because saved coverage was separately
712-- checked; a byte sum alone is never used to admit the source manifest.
713def nativeRegionCoveredBytes =
714 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
715 (lambda unrestricted ordinal : Nat .
716 (lambda unrestricted wanted : (family LogicalInterval) .
717 (stdListFold
718 (family NativeRegionShard)
719 Nat
720 (lambda unrestricted shard : (family NativeRegionShard) .
721 (lambda unrestricted rest : Nat .
722 (naturalAdd
723 rest
724 (naturalSelect
725 (naturalEqual ordinal (nativeRegionOrdinal shard))
726 (intervalExtent (intervalIntersection wanted (nativeRegionInterval shard)))
727 0))))
728 0
729 (nativeRegionShards plan)))))
730
731def nativeRegionDestinationsValid =
732 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
733 (stdListFold
734 (family NativeRegionDestination)
735 Nat
736 (lambda unrestricted destination : (family NativeRegionDestination) .
737 (lambda unrestricted rest : Nat .
738 (eliminate
739 NativeRegionDestination
740 (lambda unrestricted current : (family NativeRegionDestination) . Nat)
741 destination
742 (branch
743 NativeRegionDestinationOf
744 ordinal
745 interval
746 offset
747 .
748 (naturalAnd
749 rest
750 (naturalAnd
751 (naturalLess (intervalBegin interval) (intervalEnd interval))
752 (naturalEqual
753 (nativeRegionCoveredBytes plan ordinal interval)
754 (intervalExtent interval))))))))
755 1))
756
757def nativeRegionDestinationResidents =
758 (lambda unrestricted destinations : (family StdList (family NativeRegionDestination)) .
759 (lambda unrestricted rest : (family ArenaResidents) .
760 (stdListFold
761 (family NativeRegionDestination)
762 (family ArenaResidents)
763 (lambda unrestricted destination : (family NativeRegionDestination) .
764 (lambda unrestricted tail : (family ArenaResidents) .
765 (eliminate
766 NativeRegionDestination
767 (lambda unrestricted current : (family NativeRegionDestination) .
768 (family ArenaResidents))
769 destination
770 (branch
771 NativeRegionDestinationOf
772 ordinal
773 interval
774 offset
775 .
776 (constructor
777 ArenaResidents
778 ArenaResidentsNext
779 (constructor
780 ArenaResident
781 ArenaResidentValue
782 b"restored-logical-fragment"
783 offset
784 (intervalExtent interval)
785 1)
786 tail)))))
787 rest
788 destinations)))
789
790def nativeRegionMaterialize =
791 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
792 (lambda unrestricted destinations : (family StdList (family NativeRegionDestination)) .
793 (lambda unrestricted scratch : Nat .
794 (lambda unrestricted tail : (family NativePhysicalCommands) .
795 (stdListFold
796 (family NativeRegionDestination)
797 (family NativePhysicalCommands)
798 (lambda unrestricted destination : (family NativeRegionDestination) .
799 (lambda unrestricted next : (family NativePhysicalCommands) .
800 (eliminate
801 NativeRegionDestination
802 (lambda unrestricted current : (family NativeRegionDestination) .
803 (family NativePhysicalCommands))
804 destination
805 (branch
806 NativeRegionDestinationOf
807 ordinal
808 interval
809 offset
810 .
811 (nativeRegionCopyInterval plan ordinal interval offset scratch next)))))
812 tail
813 destinations)))))
814
815-- The public restore planner refuses missing coordinates, destination aliases,
816-- staging overlap and out-of-arena writes before emitting any executable.
817-- All file/content checks execute before the first destination copy.
818def planNativeRegionRestore =
819 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
820 (lambda unrestricted manifestPath : (family NativePhysicalOperand) .
821 (lambda unrestricted path : (pi unrestricted index : Nat . (family NativePhysicalOperand)) .
822 (lambda unrestricted descriptor : Nat .
823 (lambda unrestricted scratch : Nat .
824 (lambda unrestricted available : Nat .
825 (lambda unrestricted destinations : (family StdList (family NativeRegionDestination)) .
826 (lambda unrestricted tail : (family NativePhysicalCommands) .
827 (nat-eliminate
828 (lambda unrestricted flag : Nat .
829 (family
830 StdResult
831 (family NativeCheckpointFailure)
832 (family NativePhysicalCommands)))
833 (constructor
834 StdResult
835 StdFailure
836 (family NativeCheckpointFailure)
837 (family NativePhysicalCommands)
838 (constructor NativeCheckpointFailure NativeCheckpointBounds))
839 (lambda unrestricted previous : Nat .
840 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
841 (constructor
842 StdResult
843 StdSuccess
844 (family NativeCheckpointFailure)
845 (family NativePhysicalCommands)
846 (nativeRegionRestore
847 plan
848 manifestPath
849 path
850 descriptor
851 scratch
852 (nativeRegionMaterialize plan destinations scratch tail)))))
853 (naturalAnd
854 (checkpointManifestWordFits available)
855 (naturalAnd
856 (nativeRegionDestinationsValid plan destinations)
857 (arenaCertificate
858 available
859 (nativeRegionDestinationResidents
860 destinations
861 (nativeRegionResidents plan))))))))))))))
862
863-- Serialize one quiescent, admitted source fragment through the same durable
864-- envelope owner used by restore. Source/capture are caller-owned host regions;
865-- they must be disjoint from this layout's private staging. Extents are derived
866-- from the logical shard, never from a peer-provided byte count.
867def nativeRegionPrepareShard =
868 (lambda unrestricted shard : (family NativeRegionShard) .
869 (lambda unrestricted capture : (family NativePhysicalOperand) .
870 (lambda unrestricted source : (family NativePhysicalOperand) .
871 (lambda unrestricted candidate : (family NativePhysicalOperand) .
872 (lambda unrestricted committed : (family NativePhysicalOperand) .
873 (lambda unrestricted directory : (family NativePhysicalOperand) .
874 (lambda unrestricted descriptor : Nat .
875 (lambda unrestricted scratch : Nat .
876 (lambda unrestricted tail : (family NativePhysicalCommands) .
877 (let unrestricted layout =
878 (nativeRegionLayout shard)
879 in
880 (nativeMemoryCopyOperands
881 (nativeMemoryState (nativeCheckpointPayloadAt layout))
882 capture
883 nativeRegionCaptureBytes
884 scratch
885 b"checkpoint-shard-capture"
886 (nativeMemoryCopyOperands
887 (nativeMemoryState
888 (naturalAdd (nativeCheckpointPayloadAt layout) nativeRegionCaptureBytes))
889 source
890 (intervalExtent (nativeRegionInterval shard))
891 scratch
892 b"checkpoint-shard-state"
893 (nativeCheckpointPublish
894 layout
895 candidate
896 committed
897 directory
898 descriptor
899 scratch
900 6
901 tail)))))))))))))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.