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