Materialization is deliberately separate from validation: the consumer calls
it only in nativeRegionRestore's success continuation, after every referenced
shard is checked. Destination ownership/bounds belong to the host arena plan.
This small realization scans the admitted fragment list for each requested
interval; fragmentLimit bounds its scope. Fleet lowering must replace that
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))))))))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.