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)))))))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.