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.
154def nativeMemoryMappedBytes =
155 (lambda unrestricted quantum : Nat .
156 (lambda unrestricted bytes : Nat .
157 (eliminate
158 StdBool
159 (lambda unrestricted flag : (family StdBool) .
160 (family StdResult (family NativePhysicalMemoryFailure) Nat))
161 (stdBoolFromNatural
162 (naturalAnd
163 (naturalNonzero quantum)
164 (naturalAnd
165 (naturalLessOrEqual quantum nativePhysicalMemoryWordLimit)
166 (naturalAnd
167 (naturalNonzero bytes)
168 (naturalLessOrEqual bytes nativePhysicalMemoryWordLimit)))))
169 (branch
170 StdTrue
171 .
172 (let unrestricted pages =
173 (naturalAdd (naturalDivideUnchecked (naturalSaturatingSubtract bytes 1) quantum) 1)
174 in
175 (eliminate
176 StdBool
177 (lambda unrestricted flag : (family StdBool) .
178 (family StdResult (family NativePhysicalMemoryFailure) Nat))
179 (stdBoolFromNatural
180 (naturalLessOrEqual
181 pages
182 (naturalDivideUnchecked nativePhysicalMemoryWordLimit quantum)))
183 (branch
184 StdTrue
185 .
186 (constructor
187 StdResult
188 StdSuccess
189 (family NativePhysicalMemoryFailure)
190 Nat
191 (naturalMultiply pages quantum)))
192 (branch
193 StdFalse
194 .
195 (constructor
196 StdResult
197 StdFailure
198 (family NativePhysicalMemoryFailure)
199 Nat
200 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow))))))
201 (branch
202 StdFalse
203 .
204 (constructor
205 StdResult
206 StdFailure
207 (family NativePhysicalMemoryFailure)
208 Nat
209 (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.