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.
713def nativeRegionCoveredBytes =
714 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
715 (lambda unrestricted ordinal : Nat .
716 (lambda unrestricted wanted : (family LogicalInterval) .
717 (stdListFold
718 (family NativeRegionShard)
719 Nat
720 (lambda unrestricted shard : (family NativeRegionShard) .
721 (lambda unrestricted rest : Nat .
722 (naturalAdd
723 rest
724 (naturalSelect
725 (naturalEqual ordinal (nativeRegionOrdinal shard))
726 (intervalExtent (intervalIntersection wanted (nativeRegionInterval shard)))
727 0))))
728 0
729 (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.