Mapping granularity is a platform/deployment fact, never guessed from a
neighboring host. This accepts a positive declared quantum; its provenance
and agreement with the actual OS mapping remain the target's responsibility.
192def nativeMemoryMappedBytes =
193 (lambda unrestricted quantum : Nat .
194 (lambda unrestricted bytes : Nat .
195 (eliminate
196 StdBool
197 (lambda unrestricted flag : (family StdBool) .
198 (family StdResult (family NativePhysicalMemoryFailure) Nat))
199 (stdBoolFromNatural
200 (naturalAnd
201 (naturalNonzero quantum)
202 (naturalAnd
203 (naturalLessOrEqual quantum nativePhysicalMemoryWordLimit)
204 (naturalAnd
205 (naturalNonzero bytes)
206 (naturalLessOrEqual bytes nativePhysicalMemoryWordLimit)))))
207 (branch
208 StdTrue
209 .
210 (let unrestricted pages =
211 (naturalAdd (naturalDivideUnchecked (naturalSaturatingSubtract bytes 1) quantum) 1)
212 in
213 (eliminate
214 StdBool
215 (lambda unrestricted flag : (family StdBool) .
216 (family StdResult (family NativePhysicalMemoryFailure) Nat))
217 (stdBoolFromNatural
218 (naturalLessOrEqual
219 pages
220 (naturalDivideUnchecked nativePhysicalMemoryWordLimit quantum)))
221 (branch
222 StdTrue
223 .
224 (constructor
225 StdResult
226 StdSuccess
227 (family NativePhysicalMemoryFailure)
228 Nat
229 (naturalMultiply pages quantum)))
230 (branch
231 StdFalse
232 .
233 (constructor
234 StdResult
235 StdFailure
236 (family NativePhysicalMemoryFailure)
237 Nat
238 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow))))))
239 (branch
240 StdFalse
241 .
242 (constructor
243 StdResult
244 StdFailure
245 (family NativePhysicalMemoryFailure)
246 Nat
247 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryPageInvalid))))))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.