Admission compares a derived extent with available capacity; the executable
allocates exactly frameEnd. Base alignment makes the shared relative layout
independent of an earlier role's placement. Subtraction avoids base overflow.
223def frameLayoutFits =
224 (lambda unrestricted available : Nat .
225 (lambda unrestricted layout : (family RegionFrameLayout) .
226 (naturalAnd
227 (naturalLessOrEqual available regionFrameWordLimit)
228 (naturalAnd
229 (naturalIsZero (naturalModuloUnchecked (frameBase layout) digestWorkAlignment))
230 (naturalAnd
231 (naturalLessOrEqual (frameBase layout) available)
232 (naturalLessOrEqual
233 (frameStorageBytes layout)
234 (naturalSaturatingSubtract available (frameBase layout))))))))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.