module Checkpoint.NativeRegions import Checkpoint.Envelope import Checkpoint.NativeEnvelope import Checkpoint.RegionManifest import Representation.Partition import Runtime.NativePhysicalProgram import Runtime.NativeLaunchRecipeLoad import Runtime.NativeMemoryPlan import Runtime.ArenaCertificate import Model.Word64 import Data.Bytes import Std.Foundation import Std.List import Std.Natural -- Fixed-membership POSIX realization. Prepared files are immutable durable -- NativeEnvelope publications on the admitted store. The manifest binds their -- actual payload digests, not rank/path names. This bounded publisher stages -- each shard privately; it is not the hierarchical fleet checkpoint owner. -- A store lease keeps referenced files immutable and retained through restore. family NativeRegionShard : Type 0 constructor NativeRegionShardOf field unrestricted nativeRegionOrdinalValue : Nat field unrestricted nativeRegionIntervalValue : (family LogicalInterval) field unrestricted nativeRegionLayoutValue : (family NativeCheckpointLayout) end-family family NativeRegionCheckpoint : Type 0 constructor NativeRegionCheckpointOf field unrestricted nativeRegionManifestValue : (family NativeCheckpointLayout) field unrestricted nativeRegionShardsValue : (family StdList (family NativeRegionShard)) field unrestricted nativeRegionEpochValue : Nat field unrestricted nativeRegionEndValue : Nat end-family family NativeRegionDestination : Type 0 constructor NativeRegionDestinationOf field unrestricted nativeRegionDestinationOrdinal : Nat field unrestricted nativeRegionDestinationInterval : (family LogicalInterval) field unrestricted nativeRegionDestinationOffset : Nat end-family def nativeRegionOrdinal = (lambda unrestricted value : (family NativeRegionShard) . (eliminate NativeRegionShard (lambda unrestricted current : (family NativeRegionShard) . Nat) value (branch NativeRegionShardOf nativeRegionOrdinal nativeRegionInterval nativeRegionLayout . nativeRegionOrdinal))) def nativeRegionInterval = (lambda unrestricted value : (family NativeRegionShard) . (eliminate NativeRegionShard (lambda unrestricted current : (family NativeRegionShard) . (family LogicalInterval)) value (branch NativeRegionShardOf nativeRegionOrdinal nativeRegionInterval nativeRegionLayout . nativeRegionInterval))) def nativeRegionLayout = (lambda unrestricted value : (family NativeRegionShard) . (eliminate NativeRegionShard (lambda unrestricted current : (family NativeRegionShard) . (family NativeCheckpointLayout)) value (branch NativeRegionShardOf nativeRegionOrdinal nativeRegionInterval nativeRegionLayout . nativeRegionLayout))) def nativeRegionManifest = (lambda unrestricted value : (family NativeRegionCheckpoint) . (eliminate NativeRegionCheckpoint (lambda unrestricted current : (family NativeRegionCheckpoint) . (family NativeCheckpointLayout)) value (branch NativeRegionCheckpointOf nativeRegionManifest nativeRegionShards nativeRegionEpoch nativeRegionEnd . nativeRegionManifest))) def nativeRegionShards = (lambda unrestricted value : (family NativeRegionCheckpoint) . (eliminate NativeRegionCheckpoint (lambda unrestricted current : (family NativeRegionCheckpoint) . (family StdList (family NativeRegionShard))) value (branch NativeRegionCheckpointOf nativeRegionManifest nativeRegionShards nativeRegionEpoch nativeRegionEnd . nativeRegionShards))) def nativeRegionEpoch = (lambda unrestricted value : (family NativeRegionCheckpoint) . (eliminate NativeRegionCheckpoint (lambda unrestricted current : (family NativeRegionCheckpoint) . Nat) value (branch NativeRegionCheckpointOf nativeRegionManifest nativeRegionShards nativeRegionEpoch nativeRegionEnd . nativeRegionEpoch))) def nativeRegionEnd = (lambda unrestricted value : (family NativeRegionCheckpoint) . (eliminate NativeRegionCheckpoint (lambda unrestricted current : (family NativeRegionCheckpoint) . Nat) value (branch NativeRegionCheckpointOf nativeRegionManifest nativeRegionShards nativeRegionEpoch nativeRegionEnd . nativeRegionEnd))) -- Capture words are update, consumed-input cursor, and membership epoch. -- The first two are protected by NativeEnvelope's counter agreement checks. def nativeRegionCaptureBytes = (naturalMultiply 3 nativeCheckpointWordBytes) def nativeRegionDescriptorBytes = (naturalMultiply 3 nativeCheckpointWordBytes) def nativeRegionRecordBytes = (naturalAdd nativeRegionDescriptorBytes checkpointEnvelopeDigestBytes) def nativeRegionDescriptor = (lambda unrestricted ordinal : Nat . (lambda unrestricted interval : (family LogicalInterval) . (bytes-append (checkpointEnvelopeWord ordinal) (bytes-append (checkpointEnvelopeWord (intervalBegin interval)) (checkpointEnvelopeWord (intervalEnd interval)))))) def nativeRegionContract = (lambda unrestricted context : (family CheckpointEnvelopeContract) . (lambda unrestricted schema : Bytes . (lambda unrestricted extent : Nat . (eliminate CheckpointEnvelopeContract (lambda unrestricted current : (family CheckpointEnvelopeContract) . (family CheckpointEnvelopeContract)) context (branch CheckpointEnvelopeContractValue original learner data seed payload chunk updates . (constructor CheckpointEnvelopeContract CheckpointEnvelopeContractValue (bytes-builder-build (bytes-builder-append (checkpointManifestSized original) (checkpointManifestSized schema))) learner data seed extent extent updates)))))) def nativeRegionPartitionBytes = (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) . (bytes-builder-build (stdListFold (family CheckpointRegionPartition) BytesBuilder (lambda unrestricted part : (family CheckpointRegionPartition) . (lambda unrestricted rest : BytesBuilder . (bytes-builder-append (bytes-builder-append (bytes-builder-chunk (checkpointEnvelopeWord (checkpointPartitionOrdinal part))) (bytes-builder-append (bytes-builder-chunk (checkpointEnvelopeWord (stdListLength (family LogicalInterval) (checkpointPartitionIntervals part)))) (stdListFold (family LogicalInterval) BytesBuilder (lambda unrestricted interval : (family LogicalInterval) . (lambda unrestricted more : BytesBuilder . (bytes-builder-append (bytes-builder-chunk (nativeRegionDescriptor (checkpointPartitionOrdinal part) interval)) more))) (bytes-builder-empty) (checkpointPartitionIntervals part)))) rest))) (bytes-builder-empty) parts))) def nativeRegionShardCount = (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) . (stdListFold (family CheckpointRegionPartition) Nat (lambda unrestricted part : (family CheckpointRegionPartition) . (lambda unrestricted rest : Nat . (naturalAdd (stdListLength (family LogicalInterval) (checkpointPartitionIntervals part)) rest))) 0 parts)) def nativeRegionAppend = (lambda unrestricted context : (family CheckpointEnvelopeContract) . (lambda unrestricted logical : Bytes . (lambda unrestricted available : Nat . (lambda unrestricted ordinal : Nat . (lambda unrestricted interval : (family LogicalInterval) . (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (eliminate StdResult (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) result (branch StdFailure error . (constructor StdResult StdFailure (family NativeCheckpointFailure) (family NativeRegionCheckpoint) error)) (branch StdSuccess plan . (eliminate StdResult (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) (planNativeCheckpoint (nativeRegionContract context (bytes-append b"ALPHA-REGION-SHARD-1\x00" (bytes-append logical (nativeRegionDescriptor ordinal interval))) (naturalAdd nativeRegionCaptureBytes (intervalExtent interval))) (nativeCheckpointAlign (nativeRegionEnd plan)) 0 nativeCheckpointWordBytes available) (branch StdFailure error . (constructor StdResult StdFailure (family NativeCheckpointFailure) (family NativeRegionCheckpoint) error)) (branch StdSuccess layout . (constructor StdResult StdSuccess (family NativeCheckpointFailure) (family NativeRegionCheckpoint) (constructor NativeRegionCheckpoint NativeRegionCheckpointOf (nativeRegionManifest plan) (constructor StdList StdListCons (family NativeRegionShard) (constructor NativeRegionShard NativeRegionShardOf ordinal interval layout) (nativeRegionShards plan)) (nativeRegionEpoch plan) (nativeCheckpointEnd layout))))))))))))) def nativeRegionAppendParts = (lambda unrestricted context : (family CheckpointEnvelopeContract) . (lambda unrestricted logical : Bytes . (lambda unrestricted available : Nat . (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) . (lambda unrestricted initial : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (stdListFold (family CheckpointRegionPartition) (pi unrestricted previous : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) (lambda unrestricted part : (family CheckpointRegionPartition) . (lambda unrestricted continuation : (pi unrestricted previous : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) . (lambda unrestricted previous : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (continuation (stdListFold (family LogicalInterval) (pi unrestricted prior : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) (lambda unrestricted interval : (family LogicalInterval) . (lambda unrestricted next : (pi unrestricted prior : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) . (lambda unrestricted prior : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (next (nativeRegionAppend context logical available (checkpointPartitionOrdinal part) interval prior))))) (lambda unrestricted prior : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . prior) (checkpointPartitionIntervals part) previous))))) (lambda unrestricted previous : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . previous) parts initial)))))) def planNativeRegionCheckpoint = (lambda unrestricted context : (family CheckpointEnvelopeContract) . (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) . (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) . (lambda unrestricted epoch : Nat . (lambda unrestricted base : Nat . (lambda unrestricted available : Nat . (lambda unrestricted fragmentLimit : Nat . (nat-eliminate (lambda unrestricted flag : Nat . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) (constructor StdResult StdFailure (family NativeCheckpointFailure) (family NativeRegionCheckpoint) (constructor NativeCheckpointFailure NativeCheckpointBounds)) (lambda unrestricted previous : Nat . (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (let unrestricted logical = (checkpointLogicalSchemaBytes regions) in (eliminate StdResult (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) (planNativeCheckpoint (nativeRegionContract context (bytes-append b"ALPHA-REGION-MANIFEST-1\x00" (bytes-append logical (nativeRegionPartitionBytes parts))) (naturalAdd nativeRegionCaptureBytes (naturalMultiply (nativeRegionShardCount parts) nativeRegionRecordBytes))) base 0 nativeCheckpointWordBytes available) (branch StdFailure error . (constructor StdResult StdFailure (family NativeCheckpointFailure) (family NativeRegionCheckpoint) error)) (branch StdSuccess manifest . (eliminate StdResult (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) . (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint))) (nativeRegionAppendParts context logical available parts (constructor StdResult StdSuccess (family NativeCheckpointFailure) (family NativeRegionCheckpoint) (constructor NativeRegionCheckpoint NativeRegionCheckpointOf manifest (constructor StdList StdListEmpty (family NativeRegionShard)) epoch (nativeCheckpointEnd manifest)))) (branch StdFailure error . (constructor StdResult StdFailure (family NativeCheckpointFailure) (family NativeRegionCheckpoint) error)) (branch StdSuccess plan . (constructor StdResult StdSuccess (family NativeCheckpointFailure) (family NativeRegionCheckpoint) (constructor NativeRegionCheckpoint NativeRegionCheckpointOf manifest (stdListReverse (family NativeRegionShard) (nativeRegionShards plan)) epoch (nativeRegionEnd plan)))))))))) (naturalAnd (checkpointPartitionsValid regions parts) (naturalAnd (naturalNonzero epoch) (naturalAnd (checkpointManifestWordFits epoch) (naturalLessOrEqual (nativeRegionShardCount parts) fragmentLimit)))))))))))) def nativeRegionCaptureAt = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (nativeCheckpointPayloadAt (nativeRegionManifest plan))) def nativeRegionRecordAt = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (lambda unrestricted index : Nat . (naturalAdd (nativeRegionCaptureAt plan) (naturalAdd nativeRegionCaptureBytes (naturalMultiply index nativeRegionRecordBytes))))) def nativeRegionRequireEpoch = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeAssertEqual (nativeMemoryLoad (naturalAdd (nativeRegionCaptureAt plan) (naturalMultiply 2 nativeCheckpointWordBytes))) (nativeLaunchRecipeImmediate (nativeRegionEpoch plan)) b"checkpoint-membership-epoch" tail))) def nativeRegionLoadShards = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (lambda unrestricted path : (pi unrestricted index : Nat . (family NativePhysicalOperand)) . (lambda unrestricted descriptor : Nat . (lambda unrestricted scratch : Nat . (lambda unrestricted writing : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (stdListFold (family NativeRegionShard) (pi unrestricted index : Nat . (family NativePhysicalCommands)) (lambda unrestricted shard : (family NativeRegionShard) . (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) . (lambda unrestricted index : Nat . (let unrestricted layout = (nativeRegionLayout shard) in (let unrestricted record = (nativeRegionRecordAt plan index) in (nativeCheckpointRestore layout (path index) descriptor scratch (nativeMemoryCompareRegions (nativeRegionCaptureAt plan) (nativeCheckpointPayloadAt layout) nativeRegionCaptureBytes scratch b"checkpoint-capture-mismatch" (nat-eliminate (lambda unrestricted flag : Nat . (family NativePhysicalCommands)) (nativeMemoryCopyPayload (nativeCheckpointMetadataAt (nativeRegionManifest plan)) (nativeRegionDescriptor (nativeRegionOrdinal shard) (nativeRegionInterval shard)) (nativeMemoryCompareRegions record (nativeCheckpointMetadataAt (nativeRegionManifest plan)) nativeRegionDescriptorBytes scratch b"checkpoint-region-descriptor" (nativeMemoryCompareRegions (naturalAdd record nativeRegionDescriptorBytes) (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeDigestsAt) checkpointEnvelopeDigestBytes scratch b"checkpoint-prepared-digest" (next (succ index))))) (lambda unrestricted previous : Nat . (lambda unrestricted unused : (family NativePhysicalCommands) . (nativeMemoryCopyPayload record (nativeRegionDescriptor (nativeRegionOrdinal shard) (nativeRegionInterval shard)) (nativeMemoryCopyOperands (nativeMemoryState (naturalAdd record nativeRegionDescriptorBytes)) (nativeMemoryState (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeDigestsAt)) checkpointEnvelopeDigestBytes scratch b"checkpoint-record-digest" (next (succ index)))))) writing)))))))) (lambda unrestricted index : Nat . tail) (nativeRegionShards plan) 0))))))) def nativeRegionPublish = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (lambda unrestricted captureAt : Nat . (lambda unrestricted path : (pi unrestricted index : Nat . (family NativePhysicalOperand)) . (lambda unrestricted candidate : (family NativePhysicalOperand) . (lambda unrestricted committed : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted descriptor : Nat . (lambda unrestricted scratch : Nat . (lambda unrestricted stages : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeMemoryCopyOperands (nativeMemoryState (nativeRegionCaptureAt plan)) (nativeMemoryState captureAt) nativeRegionCaptureBytes scratch b"checkpoint-capture-copy" (nativeRegionRequireEpoch plan (nativeRegionLoadShards plan path descriptor scratch 1 (nativeCheckpointPublish (nativeRegionManifest plan) candidate committed directory descriptor scratch stages tail)))))))))))))) def nativeRegionRestore = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (lambda unrestricted manifestPath : (family NativePhysicalOperand) . (lambda unrestricted path : (pi unrestricted index : Nat . (family NativePhysicalOperand)) . (lambda unrestricted descriptor : Nat . (lambda unrestricted scratch : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeCheckpointRestore (nativeRegionManifest plan) manifestPath descriptor scratch (nativeRegionRequireEpoch plan (nativeRegionLoadShards plan path descriptor scratch 0 tail))))))))) -- 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. def nativeRegionCopyInterval = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (lambda unrestricted ordinal : Nat . (lambda unrestricted wanted : (family LogicalInterval) . (lambda unrestricted destination : Nat . (lambda unrestricted scratch : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (stdListFold (family NativeRegionShard) (family NativePhysicalCommands) (lambda unrestricted shard : (family NativeRegionShard) . (lambda unrestricted next : (family NativePhysicalCommands) . (let unrestricted begin = (intervalBegin (intervalIntersection wanted (nativeRegionInterval shard))) in (let unrestricted end = (naturalMinimum (intervalEnd wanted) (intervalEnd (nativeRegionInterval shard))) in (nat-eliminate (lambda unrestricted flag : Nat . (family NativePhysicalCommands)) next (lambda unrestricted previous : Nat . (lambda unrestricted unused : (family NativePhysicalCommands) . (nativeMemoryCopyOperands (nativeMemoryState (naturalAdd destination (naturalSaturatingSubtract begin (intervalBegin wanted)))) (nativeMemoryState (naturalAdd (nativeCheckpointPayloadAt (nativeRegionLayout shard)) (naturalAdd nativeRegionCaptureBytes (naturalSaturatingSubtract begin (intervalBegin (nativeRegionInterval shard)))))) (naturalSaturatingSubtract end begin) scratch b"checkpoint-repartition-copy" next))) (naturalAnd (naturalEqual ordinal (nativeRegionOrdinal shard)) (naturalLess begin end))))))) tail (nativeRegionShards plan)))))))) def nativeRegionResidents = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"checkpoint-regions-private-staging" (nativeCheckpointBase (nativeRegionManifest plan)) (naturalSaturatingSubtract (nativeRegionEnd plan) (nativeCheckpointBase (nativeRegionManifest plan))) 1) (constructor ArenaResidents ArenaResidentsEnd))) -- Check each requested coordinate against the admitted, non-overlapping saved -- partition. The byte sum is sound here because saved coverage was separately -- checked; a byte sum alone is never used to admit the source manifest. def nativeRegionCoveredBytes = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (lambda unrestricted ordinal : Nat . (lambda unrestricted wanted : (family LogicalInterval) . (stdListFold (family NativeRegionShard) Nat (lambda unrestricted shard : (family NativeRegionShard) . (lambda unrestricted rest : Nat . (naturalAdd rest (naturalSelect (naturalEqual ordinal (nativeRegionOrdinal shard)) (intervalExtent (intervalIntersection wanted (nativeRegionInterval shard))) 0)))) 0 (nativeRegionShards plan))))) def nativeRegionDestinationsValid = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (stdListFold (family NativeRegionDestination) Nat (lambda unrestricted destination : (family NativeRegionDestination) . (lambda unrestricted rest : Nat . (eliminate NativeRegionDestination (lambda unrestricted current : (family NativeRegionDestination) . Nat) destination (branch NativeRegionDestinationOf ordinal interval offset . (naturalAnd rest (naturalAnd (naturalLess (intervalBegin interval) (intervalEnd interval)) (naturalEqual (nativeRegionCoveredBytes plan ordinal interval) (intervalExtent interval)))))))) 1)) def nativeRegionDestinationResidents = (lambda unrestricted destinations : (family StdList (family NativeRegionDestination)) . (lambda unrestricted rest : (family ArenaResidents) . (stdListFold (family NativeRegionDestination) (family ArenaResidents) (lambda unrestricted destination : (family NativeRegionDestination) . (lambda unrestricted tail : (family ArenaResidents) . (eliminate NativeRegionDestination (lambda unrestricted current : (family NativeRegionDestination) . (family ArenaResidents)) destination (branch NativeRegionDestinationOf ordinal interval offset . (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"restored-logical-fragment" offset (intervalExtent interval) 1) tail))))) rest destinations))) def nativeRegionMaterialize = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (lambda unrestricted destinations : (family StdList (family NativeRegionDestination)) . (lambda unrestricted scratch : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (stdListFold (family NativeRegionDestination) (family NativePhysicalCommands) (lambda unrestricted destination : (family NativeRegionDestination) . (lambda unrestricted next : (family NativePhysicalCommands) . (eliminate NativeRegionDestination (lambda unrestricted current : (family NativeRegionDestination) . (family NativePhysicalCommands)) destination (branch NativeRegionDestinationOf ordinal interval offset . (nativeRegionCopyInterval plan ordinal interval offset scratch next))))) tail destinations))))) -- The public restore planner refuses missing coordinates, destination aliases, -- staging overlap and out-of-arena writes before emitting any executable. -- All file/content checks execute before the first destination copy. def planNativeRegionRestore = (lambda unrestricted plan : (family NativeRegionCheckpoint) . (lambda unrestricted manifestPath : (family NativePhysicalOperand) . (lambda unrestricted path : (pi unrestricted index : Nat . (family NativePhysicalOperand)) . (lambda unrestricted descriptor : Nat . (lambda unrestricted scratch : Nat . (lambda unrestricted available : Nat . (lambda unrestricted destinations : (family StdList (family NativeRegionDestination)) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted flag : Nat . (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands))) (constructor StdResult StdFailure (family NativeCheckpointFailure) (family NativePhysicalCommands) (constructor NativeCheckpointFailure NativeCheckpointBounds)) (lambda unrestricted previous : Nat . (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) . (constructor StdResult StdSuccess (family NativeCheckpointFailure) (family NativePhysicalCommands) (nativeRegionRestore plan manifestPath path descriptor scratch (nativeRegionMaterialize plan destinations scratch tail))))) (naturalAnd (checkpointManifestWordFits available) (naturalAnd (nativeRegionDestinationsValid plan destinations) (arenaCertificate available (nativeRegionDestinationResidents destinations (nativeRegionResidents plan)))))))))))))) -- Serialize one quiescent, admitted source fragment through the same durable -- envelope owner used by restore. Source/capture are caller-owned host regions; -- they must be disjoint from this layout's private staging. Extents are derived -- from the logical shard, never from a peer-provided byte count. def nativeRegionPrepareShard = (lambda unrestricted shard : (family NativeRegionShard) . (lambda unrestricted capture : (family NativePhysicalOperand) . (lambda unrestricted source : (family NativePhysicalOperand) . (lambda unrestricted candidate : (family NativePhysicalOperand) . (lambda unrestricted committed : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted descriptor : Nat . (lambda unrestricted scratch : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted layout = (nativeRegionLayout shard) in (nativeMemoryCopyOperands (nativeMemoryState (nativeCheckpointPayloadAt layout)) capture nativeRegionCaptureBytes scratch b"checkpoint-shard-capture" (nativeMemoryCopyOperands (nativeMemoryState (naturalAdd (nativeCheckpointPayloadAt layout) nativeRegionCaptureBytes)) source (intervalExtent (nativeRegionInterval shard)) scratch b"checkpoint-shard-state" (nativeCheckpointPublish layout candidate committed directory descriptor scratch 6 tail)))))))))))))