1module Checkpoint.NativeEnvelope
2
3import Checkpoint.Envelope
4import Runtime.NativeFilePlan
5import Runtime.NativeMemoryPlan
6import Runtime.NativeMemoryRoutine
7import Runtime.NativePhysicalProgram
8import Runtime.NativeLaunchRecipeLoad
9import Runtime.NativeWordDigest
10import Runtime.WordDigest
11import Runtime.ArenaCertificate
12import Model.Word64
13import Data.Bytes
14import Data.SHA256
15import Data.SHA256Padding
16import Std.Foundation
17import Std.Natural
18
19-- A bounded in-memory realization of the shared checkpoint envelope. It is
20-- suitable for a replicated state or an admitted shard, not a fleet gather.
21-- Logical updates/invocations occupy explicit, distinct words in the hashed
22-- payload. Header counters are checked against them before restore exposes any
23-- state. No peer/file-provided extent controls allocation or pointer arithmetic.
24family NativeCheckpointLayout : Type 0
25constructor NativeCheckpointLayoutOf
26field unrestricted nativeCheckpointLayoutContract : (family CheckpointEnvelopeContract)
27field unrestricted nativeCheckpointLayoutBase : Nat
28field unrestricted nativeCheckpointLayoutUpdates : Nat
29field unrestricted nativeCheckpointLayoutInvocations : Nat
30field unrestricted nativeCheckpointLayoutFullPadding : Bytes
31field unrestricted nativeCheckpointLayoutTailPadding : Bytes
32field unrestricted nativeCheckpointLayoutHeader : Bytes
33
34end-family
35
36family NativeCheckpointFailure : Type 0
37constructor NativeCheckpointBounds
38
39end-family
40
41def nativeCheckpointContract =
42 (lambda unrestricted layout : (family NativeCheckpointLayout) .
43 (eliminate
44 NativeCheckpointLayout
45 (lambda unrestricted current : (family NativeCheckpointLayout) .
46 (family CheckpointEnvelopeContract))
47 layout
48 (branch
49 NativeCheckpointLayoutOf
50 contract
51 base
52 updates
53 invocations
54 fullPadding
55 tailPadding
56 header
57 .
58 contract)))
59
60def nativeCheckpointBase =
61 (lambda unrestricted layout : (family NativeCheckpointLayout) .
62 (eliminate
63 NativeCheckpointLayout
64 (lambda unrestricted current : (family NativeCheckpointLayout) . Nat)
65 layout
66 (branch
67 NativeCheckpointLayoutOf
68 contract
69 base
70 updates
71 invocations
72 fullPadding
73 tailPadding
74 header
75 .
76 base)))
77
78def nativeCheckpointUpdatesOffset =
79 (lambda unrestricted layout : (family NativeCheckpointLayout) .
80 (eliminate
81 NativeCheckpointLayout
82 (lambda unrestricted current : (family NativeCheckpointLayout) . Nat)
83 layout
84 (branch
85 NativeCheckpointLayoutOf
86 contract
87 base
88 updates
89 invocations
90 fullPadding
91 tailPadding
92 header
93 .
94 updates)))
95
96def nativeCheckpointInvocationsOffset =
97 (lambda unrestricted layout : (family NativeCheckpointLayout) .
98 (eliminate
99 NativeCheckpointLayout
100 (lambda unrestricted current : (family NativeCheckpointLayout) . Nat)
101 layout
102 (branch
103 NativeCheckpointLayoutOf
104 contract
105 base
106 updates
107 invocations
108 fullPadding
109 tailPadding
110 header
111 .
112 invocations)))
113
114def nativeCheckpointFullPadding =
115 (lambda unrestricted layout : (family NativeCheckpointLayout) .
116 (eliminate
117 NativeCheckpointLayout
118 (lambda unrestricted current : (family NativeCheckpointLayout) . Bytes)
119 layout
120 (branch
121 NativeCheckpointLayoutOf
122 contract
123 base
124 updates
125 invocations
126 fullPadding
127 tailPadding
128 header
129 .
130 fullPadding)))
131
132def nativeCheckpointTailPadding =
133 (lambda unrestricted layout : (family NativeCheckpointLayout) .
134 (eliminate
135 NativeCheckpointLayout
136 (lambda unrestricted current : (family NativeCheckpointLayout) . Bytes)
137 layout
138 (branch
139 NativeCheckpointLayoutOf
140 contract
141 base
142 updates
143 invocations
144 fullPadding
145 tailPadding
146 header
147 .
148 tailPadding)))
149
150def nativeCheckpointWordBytes =
151 (bytes-length (checkpointEnvelopeWord 0))
152
153-- Header identities are immutable for a planned layout. Keep their derived
154-- bytes in that layout so preparation, validation and command inspection
155-- share the SHA computations. A suspended constructor field leaves bounds
156-- admission cheap when no executable consumes the header. This is the same
157-- canonical envelope, not a saved hash or a second digest implementation.
158def nativeCheckpointHeaderFor =
159 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
160 (bytes-append
161 (checkpointEnvelopeFixed contract)
162 (bytes-append
163 (dataBytesRepeatByte (byte 0) (naturalMultiply 2 nativeCheckpointWordBytes))
164 (bytes-append
165 (checkpointEnvelopeIdentityDigests contract)
166 (dataBytesRepeatByte
167 (byte 0)
168 (naturalSaturatingSubtract
169 (checkpointEnvelopeHeaderBytes contract)
170 checkpointEnvelopeDigestsAt))))))
171
172def nativeCheckpointHeader =
173 (lambda unrestricted layout : (family NativeCheckpointLayout) .
174 (eliminate
175 NativeCheckpointLayout
176 (lambda unrestricted current : (family NativeCheckpointLayout) . Bytes)
177 layout
178 (branch
179 NativeCheckpointLayoutOf
180 contract
181 base
182 updates
183 invocations
184 fullPadding
185 tailPadding
186 header
187 .
188 header)))
189
190def nativeCheckpointAlign =
191 (lambda unrestricted n : Nat .
192 (naturalMultiply
193 digestWorkAlignment
194 (naturalDivideUnchecked
195 (naturalAdd n (naturalSaturatingSubtract digestWorkAlignment 1))
196 digestWorkAlignment)))
197
198def nativeCheckpointFileBytes =
199 (lambda unrestricted layout : (family NativeCheckpointLayout) .
200 (checkpointEnvelopeFileBytes (nativeCheckpointContract layout)))
201
202def nativeCheckpointHeaderBytes =
203 (lambda unrestricted layout : (family NativeCheckpointLayout) .
204 (checkpointEnvelopeHeaderBytes (nativeCheckpointContract layout)))
205
206def nativeCheckpointPayloadAt =
207 (lambda unrestricted layout : (family NativeCheckpointLayout) .
208 (naturalAdd (nativeCheckpointBase layout) (nativeCheckpointHeaderBytes layout)))
209
210def nativeCheckpointUpdatesAt =
211 (lambda unrestricted layout : (family NativeCheckpointLayout) .
212 (naturalAdd (nativeCheckpointPayloadAt layout) (nativeCheckpointUpdatesOffset layout)))
213
214def nativeCheckpointInvocationsAt =
215 (lambda unrestricted layout : (family NativeCheckpointLayout) .
216 (naturalAdd (nativeCheckpointPayloadAt layout) (nativeCheckpointInvocationsOffset layout)))
217
218def nativeCheckpointReadbackAt =
219 (lambda unrestricted layout : (family NativeCheckpointLayout) .
220 (naturalAdd (nativeCheckpointBase layout) (nativeCheckpointFileBytes layout)))
221
222def nativeCheckpointProbeAt =
223 (lambda unrestricted layout : (family NativeCheckpointLayout) .
224 (naturalAdd (nativeCheckpointReadbackAt layout) (nativeCheckpointFileBytes layout)))
225
226def nativeCheckpointChunkAt =
227 (lambda unrestricted layout : (family NativeCheckpointLayout) .
228 (nativeCheckpointAlign (succ (nativeCheckpointProbeAt layout))))
229
230def nativeCheckpointChunkBytes =
231 (lambda unrestricted layout : (family NativeCheckpointLayout) .
232 (naturalAdd
233 (checkpointEnvelopeContractChunk (nativeCheckpointContract layout))
234 (bytes-length (nativeCheckpointFullPadding layout))))
235
236def nativeCheckpointMetadataAt =
237 (lambda unrestricted layout : (family NativeCheckpointLayout) .
238 (naturalAdd (nativeCheckpointChunkAt layout) (nativeCheckpointChunkBytes layout)))
239
240def nativeCheckpointDigestAt =
241 (lambda unrestricted layout : (family NativeCheckpointLayout) .
242 (naturalAdd (nativeCheckpointMetadataAt layout) (nativeCheckpointHeaderBytes layout)))
243
244def nativeCheckpointWorkAt =
245 (lambda unrestricted layout : (family NativeCheckpointLayout) .
246 (nativeCheckpointAlign
247 (naturalAdd (nativeCheckpointDigestAt layout) checkpointEnvelopeDigestBytes)))
248
249def nativeCheckpointSourcePointerAt =
250 (lambda unrestricted layout : (family NativeCheckpointLayout) .
251 (naturalAdd (nativeCheckpointWorkAt layout) digestWorkBytes))
252
253def nativeCheckpointDigestPointerAt =
254 (lambda unrestricted layout : (family NativeCheckpointLayout) .
255 (naturalAdd (nativeCheckpointSourcePointerAt layout) nativeCheckpointWordBytes))
256
257def nativeCheckpointEnd =
258 (lambda unrestricted layout : (family NativeCheckpointLayout) .
259 (naturalAdd (nativeCheckpointDigestPointerAt layout) nativeCheckpointWordBytes))
260
261def planNativeCheckpointNonempty =
262 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
263 (lambda unrestricted base : Nat .
264 (lambda unrestricted updates : Nat .
265 (lambda unrestricted invocations : Nat .
266 (lambda unrestricted available : Nat .
267 (nat-eliminate
268 (lambda unrestricted admitted : Nat .
269 (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)))
270 (constructor
271 StdResult
272 StdFailure
273 (family NativeCheckpointFailure)
274 (family NativeCheckpointLayout)
275 (constructor NativeCheckpointFailure NativeCheckpointBounds))
276 (lambda unrestricted previous : Nat .
277 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
278 (eliminate
279 StdResult
280 (lambda unrestricted r : (family StdResult (family SHA256ErrorCode) Bytes) .
281 (family
282 StdResult
283 (family NativeCheckpointFailure)
284 (family NativeCheckpointLayout)))
285 (sha256PaddingSuffix (checkpointEnvelopeContractChunk contract))
286 (branch
287 StdFailure
288 error
289 .
290 (constructor
291 StdResult
292 StdFailure
293 (family NativeCheckpointFailure)
294 (family NativeCheckpointLayout)
295 (constructor NativeCheckpointFailure NativeCheckpointBounds)))
296 (branch
297 StdSuccess
298 fullPadding
299 .
300 (eliminate
301 StdResult
302 (lambda unrestricted r : (family StdResult (family SHA256ErrorCode) Bytes) .
303 (family
304 StdResult
305 (family NativeCheckpointFailure)
306 (family NativeCheckpointLayout)))
307 (sha256PaddingSuffix (checkpointEnvelopeTailBytes contract))
308 (branch
309 StdFailure
310 error
311 .
312 (constructor
313 StdResult
314 StdFailure
315 (family NativeCheckpointFailure)
316 (family NativeCheckpointLayout)
317 (constructor NativeCheckpointFailure NativeCheckpointBounds)))
318 (branch
319 StdSuccess
320 tailPadding
321 .
322 (let unrestricted layout =
323 (constructor
324 NativeCheckpointLayout
325 NativeCheckpointLayoutOf
326 contract
327 base
328 updates
329 invocations
330 fullPadding
331 tailPadding
332 (nativeCheckpointHeaderFor contract))
333 in
334 (nat-eliminate
335 (lambda unrestricted fits : Nat .
336 (family
337 StdResult
338 (family NativeCheckpointFailure)
339 (family NativeCheckpointLayout)))
340 (constructor
341 StdResult
342 StdFailure
343 (family NativeCheckpointFailure)
344 (family NativeCheckpointLayout)
345 (constructor NativeCheckpointFailure NativeCheckpointBounds))
346 (lambda unrestricted previousFit : Nat .
347 (lambda unrestricted ignoredFit : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
348 (constructor
349 StdResult
350 StdSuccess
351 (family NativeCheckpointFailure)
352 (family NativeCheckpointLayout)
353 layout)))
354 (naturalAnd
355 (naturalLessOrEqual (nativeCheckpointEnd layout) available)
356 (naturalLessOrEqual
357 (nativeCheckpointEnd layout)
358 18446744073709551615))))))))))
359 (naturalAnd
360 (naturalEqual (naturalModuloUnchecked base digestWorkAlignment) 0)
361 (naturalAnd
362 (naturalLessOrEqual 1 (checkpointEnvelopeContractChunk contract))
363 (naturalAnd
364 (naturalLessOrEqual
365 (checkpointEnvelopeContractChunk contract)
366 (checkpointEnvelopeContractPayload contract))
367 (naturalAnd
368 (naturalLessOrEqual (checkpointEnvelopeFileBytes contract) 2147479552)
369 (naturalAnd
370 (naturalLessOrEqual
371 nativeCheckpointWordBytes
372 (checkpointEnvelopeContractPayload contract))
373 (naturalAnd
374 (naturalLessOrEqual
375 updates
376 (naturalSaturatingSubtract
377 (checkpointEnvelopeContractPayload contract)
378 nativeCheckpointWordBytes))
379 (naturalAnd
380 (naturalLessOrEqual
381 invocations
382 (naturalSaturatingSubtract
383 (checkpointEnvelopeContractPayload contract)
384 nativeCheckpointWordBytes))
385 (naturalAnd
386 (naturalEqual
387 (naturalModuloUnchecked updates nativeCheckpointWordBytes)
388 0)
389 (naturalAnd
390 (naturalEqual
391 (naturalModuloUnchecked invocations nativeCheckpointWordBytes)
392 0)
393 (naturalEqual (naturalEqual updates invocations) 0))))))))))))))))
394
395-- Avoid evaluating chunk division even in strict artifact realization when
396-- the proposed contract has a zero chunk width.
397def planNativeCheckpoint =
398 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
399 (lambda unrestricted base : Nat .
400 (lambda unrestricted updates : Nat .
401 (lambda unrestricted invocations : Nat .
402 (lambda unrestricted available : Nat .
403 (nat-eliminate
404 (lambda unrestricted valid : Nat .
405 (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)))
406 (constructor
407 StdResult
408 StdFailure
409 (family NativeCheckpointFailure)
410 (family NativeCheckpointLayout)
411 (constructor NativeCheckpointFailure NativeCheckpointBounds))
412 (lambda unrestricted previous : Nat .
413 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
414 (planNativeCheckpointNonempty contract base updates invocations available)))
415 (naturalNonzero (checkpointEnvelopeContractChunk contract))))))))
416
417def nativeCheckpointStore =
418 (lambda unrestricted at : Nat .
419 (lambda unrestricted value : (family NativePhysicalOperand) .
420 (nativeLaunchRecipeCommand
421 (constructor NativePhysicalOperation NativePhysicalStoreWord64 (nativeMemoryState at) value)
422 b"checkpoint-state")))
423
424def nativeCheckpointAffine =
425 (lambda unrestricted base : Nat .
426 (lambda unrestricted stride : Nat .
427 (constructor
428 NativePhysicalOperand
429 NativePhysicalLoopAffine
430 (modelWord64FromNaturalTruncated base)
431 (modelWord64FromNaturalTruncated stride))))
432
433def nativeCheckpointPointer =
434 (lambda unrestricted at : Nat .
435 (lambda unrestricted base : Nat .
436 (lambda unrestricted stride : Nat .
437 (lambda unrestricted tail : (family NativePhysicalCommands) .
438 (nativeLaunchRecipeCommand
439 (constructor
440 NativePhysicalOperation
441 NativePhysicalAddWord64
442 (nativeMemoryState at)
443 (nativeMemoryState base)
444 (nativeCheckpointAffine 0 stride))
445 b"checkpoint-chunk-pointer"
446 tail)))))
447
448-- Each chunk is copied into a separate padded arena, so hashing cannot
449-- overwrite following payload bytes or an expected digest. Loop-affine offsets
450-- derive from the admitted file schema. This fragment is used outside learning
451-- repeats, since the current native program admits non-nested bounded loops.
452def nativeCheckpointHashChunk =
453 (lambda unrestricted layout : (family NativeCheckpointLayout) .
454 (lambda unrestricted extent : Nat .
455 (lambda unrestricted padding : Bytes .
456 (lambda unrestricted generate : Nat .
457 (lambda unrestricted slot : Nat .
458 (lambda unrestricted tail : (family NativePhysicalCommands) .
459 (nativeMemoryCopyOperands
460 (nativeMemoryState (nativeCheckpointChunkAt layout))
461 (nativeMemoryLoad (nativeCheckpointSourcePointerAt layout))
462 extent
463 slot
464 b"checkpoint-chunk-copy"
465 (nativeMemoryCopyPayload
466 (naturalAdd (nativeCheckpointChunkAt layout) extent)
467 padding
468 (nativeLaunchRecipeCommand
469 (constructor
470 NativePhysicalOperation
471 NativePhysicalMachineRoutine
472 nativeWordDigestRoutine
473 (constructor
474 NativePhysicalArguments
475 NativePhysicalArgumentsValue
476 (nativeMemoryState (nativeCheckpointChunkAt layout))
477 (nativeLaunchRecipeImmediate
478 (naturalDivideUnchecked
479 (naturalAdd extent (bytes-length padding))
480 digestBlockBytes))
481 (nativeMemoryState (nativeCheckpointDigestAt layout))
482 (nativeLaunchRecipeImmediate 0)
483 (nativeLaunchRecipeImmediate 0)
484 (nativeMemoryState (nativeCheckpointWorkAt layout)))
485 (nativeLaunchRecipeStore slot))
486 b"checkpoint-hash"
487 (nativeLaunchRecipeAssertEqual
488 (nativeLaunchRecipeSlotValue slot)
489 (nativeLaunchRecipeImmediate checkpointEnvelopeDigestBytes)
490 b"checkpoint-hash-count"
491 (nat-eliminate
492 (lambda unrestricted mode : Nat . (family NativePhysicalCommands))
493 (nativeMemoryCompareOperands
494 (nativeMemoryState (nativeCheckpointDigestAt layout))
495 (nativeMemoryLoad (nativeCheckpointDigestPointerAt layout))
496 checkpointEnvelopeDigestBytes
497 slot
498 b"checkpoint-chunk"
499 tail)
500 (lambda unrestricted previous : Nat .
501 (lambda unrestricted ignored : (family NativePhysicalCommands) .
502 (nativeMemoryCopyOperands
503 (nativeMemoryLoad (nativeCheckpointDigestPointerAt layout))
504 (nativeMemoryState (nativeCheckpointDigestAt layout))
505 checkpointEnvelopeDigestBytes
506 slot
507 b"checkpoint-digest-copy"
508 tail)))
509 generate)))))))))))
510
511def nativeCheckpointDigests =
512 (lambda unrestricted layout : (family NativeCheckpointLayout) .
513 (lambda unrestricted generate : Nat .
514 (lambda unrestricted slot : Nat .
515 (lambda unrestricted tail : (family NativePhysicalCommands) .
516 (let unrestricted contract =
517 (nativeCheckpointContract layout)
518 in
519 (let unrestricted full =
520 (checkpointEnvelopeFullChunks contract)
521 in
522 (let unrestricted chunk =
523 (checkpointEnvelopeContractChunk contract)
524 in
525 (let unrestricted last =
526 (checkpointEnvelopeTailBytes contract)
527 in
528 (nativeLaunchRecipeCommand
529 (constructor
530 NativePhysicalOperation
531 NativePhysicalRepeatBeginCounted
532 (nativeLaunchRecipeImmediate full))
533 b"checkpoint-chunks"
534 (nativeCheckpointPointer
535 (nativeCheckpointSourcePointerAt layout)
536 (nativeCheckpointPayloadAt layout)
537 chunk
538 (nativeCheckpointPointer
539 (nativeCheckpointDigestPointerAt layout)
540 (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeDigestsAt)
541 checkpointEnvelopeDigestBytes
542 (nativeCheckpointHashChunk
543 layout
544 chunk
545 (nativeCheckpointFullPadding layout)
546 generate
547 slot
548 (nativeLaunchRecipeCommand
549 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
550 b"checkpoint-chunks-end"
551 (nativeFileWhen
552 (naturalNonzero last)
553 (lambda unrestricted after : (family NativePhysicalCommands) .
554 (nativeCheckpointStore
555 (nativeCheckpointSourcePointerAt layout)
556 (nativeMemoryState
557 (naturalAdd
558 (nativeCheckpointPayloadAt layout)
559 (naturalMultiply full chunk)))
560 (nativeCheckpointStore
561 (nativeCheckpointDigestPointerAt layout)
562 (nativeMemoryState
563 (naturalAdd
564 (naturalAdd
565 (nativeCheckpointBase layout)
566 checkpointEnvelopeDigestsAt)
567 (naturalMultiply full checkpointEnvelopeDigestBytes)))
568 (nativeCheckpointHashChunk
569 layout
570 last
571 (nativeCheckpointTailPadding layout)
572 generate
573 slot
574 after))))
575 tail))))))))))))))
576
577def nativeCheckpointRequireCounters =
578 (lambda unrestricted layout : (family NativeCheckpointLayout) .
579 (lambda unrestricted tail : (family NativePhysicalCommands) .
580 (nativeLaunchRecipeAssertEqual
581 (nativeMemoryLoad (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeUpdatesAt))
582 (nativeMemoryLoad (nativeCheckpointUpdatesAt layout))
583 b"checkpoint-update-counter"
584 (nativeLaunchRecipeAssertEqual
585 (nativeMemoryLoad
586 (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeInvocationsAt))
587 (nativeMemoryLoad (nativeCheckpointInvocationsAt layout))
588 b"checkpoint-invocation-counter"
589 tail))))
590
591def nativeCheckpointPrepare =
592 (lambda unrestricted layout : (family NativeCheckpointLayout) .
593 (lambda unrestricted slot : Nat .
594 (lambda unrestricted tail : (family NativePhysicalCommands) .
595 (nativeMemoryCopyPayload
596 (nativeCheckpointBase layout)
597 (nativeCheckpointHeader layout)
598 (nativeCheckpointStore
599 (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeUpdatesAt)
600 (nativeMemoryLoad (nativeCheckpointUpdatesAt layout))
601 (nativeCheckpointStore
602 (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeInvocationsAt)
603 (nativeMemoryLoad (nativeCheckpointInvocationsAt layout))
604 (nativeCheckpointDigests layout 1 slot tail)))))))
605
606-- Canonical zero padding is part of version one's envelope, not an extension
607-- area whose arbitrary bytes may survive integrity checks unnoticed.
608def nativeCheckpointRequirePadding =
609 (lambda unrestricted layout : (family NativeCheckpointLayout) .
610 (lambda unrestricted slot : Nat .
611 (lambda unrestricted tail : (family NativePhysicalCommands) .
612 (let unrestricted start =
613 (naturalAdd
614 checkpointEnvelopeDigestsAt
615 (naturalMultiply
616 checkpointEnvelopeDigestBytes
617 (checkpointEnvelopeChunkCount (nativeCheckpointContract layout))))
618 in
619 (nativeMemoryCompareRegions
620 (naturalAdd (nativeCheckpointBase layout) start)
621 (naturalAdd (nativeCheckpointMetadataAt layout) start)
622 (naturalSaturatingSubtract (nativeCheckpointHeaderBytes layout) start)
623 slot
624 b"checkpoint-padding"
625 tail)))))
626
627def nativeCheckpointValidate =
628 (lambda unrestricted layout : (family NativeCheckpointLayout) .
629 (lambda unrestricted slot : Nat .
630 (lambda unrestricted tail : (family NativePhysicalCommands) .
631 (nativeMemoryCopyPayload
632 (nativeCheckpointMetadataAt layout)
633 (nativeCheckpointHeader layout)
634 (nativeMemoryCompareRegions
635 (nativeCheckpointBase layout)
636 (nativeCheckpointMetadataAt layout)
637 checkpointEnvelopeFixedBytes
638 slot
639 b"checkpoint-layout"
640 (nativeMemoryCompareRegions
641 (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeSchemaAt)
642 (naturalAdd (nativeCheckpointMetadataAt layout) checkpointEnvelopeSchemaAt)
643 (naturalSaturatingSubtract checkpointEnvelopeDigestsAt checkpointEnvelopeSchemaAt)
644 slot
645 b"checkpoint-identity"
646 (nativeCheckpointRequirePadding
647 layout
648 slot
649 (nativeCheckpointDigests
650 layout
651 0
652 slot
653 (nativeCheckpointRequireCounters layout tail)))))))))
654
655def nativeCheckpointRestore =
656 (lambda unrestricted layout : (family NativeCheckpointLayout) .
657 (lambda unrestricted path : (family NativePhysicalOperand) .
658 (lambda unrestricted descriptor : Nat .
659 (lambda unrestricted slot : Nat .
660 (lambda unrestricted tail : (family NativePhysicalCommands) .
661 (nativeFileOpen
662 path
663 nativeFileReadFlags
664 descriptor
665 slot
666 b"checkpoint-open"
667 (nativeFileRead
668 (nativeLaunchRecipeSlotValue descriptor)
669 (nativeMemoryState (nativeCheckpointBase layout))
670 (nativeCheckpointFileBytes layout)
671 (nativeLaunchRecipeImmediate 0)
672 slot
673 b"checkpoint-read"
674 (nativeFileRequireEOF
675 (nativeLaunchRecipeSlotValue descriptor)
676 (nativeMemoryState (nativeCheckpointProbeAt layout))
677 (nativeCheckpointFileBytes layout)
678 slot
679 (nativeFileClose
680 (nativeLaunchRecipeSlotValue descriptor)
681 slot
682 b"checkpoint-read-close"
683 (nativeCheckpointValidate layout slot tail))))))))))
684
685def nativeCheckpointPublish =
686 (lambda unrestricted layout : (family NativeCheckpointLayout) .
687 (lambda unrestricted candidate : (family NativePhysicalOperand) .
688 (lambda unrestricted committed : (family NativePhysicalOperand) .
689 (lambda unrestricted directory : (family NativePhysicalOperand) .
690 (lambda unrestricted descriptor : Nat .
691 (lambda unrestricted slot : Nat .
692 (lambda unrestricted stages : Nat .
693 (lambda unrestricted tail : (family NativePhysicalCommands) .
694 (nativeCheckpointPrepare
695 layout
696 slot
697 (nativeFileOpen
698 candidate
699 nativeFileCandidateFlags
700 descriptor
701 slot
702 b"checkpoint-candidate-open"
703 (nativeFileWrite
704 (nativeLaunchRecipeSlotValue descriptor)
705 (nativeMemoryState (nativeCheckpointBase layout))
706 (nativeCheckpointFileBytes layout)
707 (nativeLaunchRecipeImmediate 0)
708 slot
709 b"checkpoint-write"
710 (nativeFileRead
711 (nativeLaunchRecipeSlotValue descriptor)
712 (nativeMemoryState (nativeCheckpointReadbackAt layout))
713 (nativeCheckpointFileBytes layout)
714 (nativeLaunchRecipeImmediate 0)
715 slot
716 b"checkpoint-readback"
717 (nativeFileRequireEOF
718 (nativeLaunchRecipeSlotValue descriptor)
719 (nativeMemoryState (nativeCheckpointProbeAt layout))
720 (nativeCheckpointFileBytes layout)
721 slot
722 (nativeMemoryCompareRegions
723 (nativeCheckpointBase layout)
724 (nativeCheckpointReadbackAt layout)
725 (nativeCheckpointFileBytes layout)
726 slot
727 b"checkpoint-readback-mismatch"
728 (nativeFileCommitStages
729 stages
730 0
731 descriptor
732 slot
733 candidate
734 committed
735 directory
736 tail)))))))))))))))
737
738def nativeCheckpointResidents =
739 (lambda unrestricted layout : (family NativeCheckpointLayout) .
740 (constructor
741 ArenaResidents
742 ArenaResidentsNext
743 (constructor
744 ArenaResident
745 ArenaResidentValue
746 b"checkpoint-file"
747 (nativeCheckpointBase layout)
748 (nativeCheckpointFileBytes layout)
749 1)
750 (constructor
751 ArenaResidents
752 ArenaResidentsNext
753 (constructor
754 ArenaResident
755 ArenaResidentValue
756 b"checkpoint-readback"
757 (nativeCheckpointReadbackAt layout)
758 (succ (nativeCheckpointFileBytes layout))
759 1)
760 (constructor
761 ArenaResidents
762 ArenaResidentsNext
763 (constructor
764 ArenaResident
765 ArenaResidentValue
766 b"checkpoint-chunk"
767 (nativeCheckpointChunkAt layout)
768 (nativeCheckpointChunkBytes layout)
769 1)
770 (constructor
771 ArenaResidents
772 ArenaResidentsNext
773 (constructor
774 ArenaResident
775 ArenaResidentValue
776 b"checkpoint-metadata"
777 (nativeCheckpointMetadataAt layout)
778 (nativeCheckpointHeaderBytes layout)
779 1)
780 (constructor
781 ArenaResidents
782 ArenaResidentsNext
783 (constructor
784 ArenaResident
785 ArenaResidentValue
786 b"checkpoint-digest"
787 (nativeCheckpointDigestAt layout)
788 checkpointEnvelopeDigestBytes
789 1)
790 (constructor
791 ArenaResidents
792 ArenaResidentsNext
793 (constructor
794 ArenaResident
795 ArenaResidentValue
796 b"checkpoint-hash-work"
797 (nativeCheckpointWorkAt layout)
798 digestWorkBytes
799 1)
800 (constructor
801 ArenaResidents
802 ArenaResidentsNext
803 (constructor
804 ArenaResident
805 ArenaResidentValue
806 b"checkpoint-pointers"
807 (nativeCheckpointSourcePointerAt layout)
808 (naturalMultiply 2 nativeCheckpointWordBytes)
809 1)
810 (constructor ArenaResidents ArenaResidentsEnd)))))))))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.