The load segment's memory extent: 4 MiB, or the file's extent when the
file is larger (a host program whose schedule outgrows 4 MiB of records:
the memory must cover the file, and nothing past the file is read)
202def elfLoadSizeAtLeast4M =
203 (lambda unrestricted fileSize : Nat .
204 (nat-eliminate (lambda unrestricted current : Nat . Bytes)
205 elfLoadSize4M
206 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes .
207 (elfModelWord64Bytes (modelWord64FromNaturalTruncated fileSize))))
208 (naturalLess 4194304 fileSize)))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.