Admission and reservation charge the scratch of the interpreter that will
run the program, i.e. of its maximum repeat depth, never a fixed extent:
a reservation smaller than the allocation would let a nested program map
more than it was admitted for.
97def nativePhysicalMemoryAdmitted =
98 (lambda unrestricted state : Nat .
99 (lambda unrestricted slots : Nat .
100 (lambda unrestricted depth : Nat .
101 (let unrestricted scratch =
102 (nativePhysicalRepeatScratchBytes depth)
103 in
104 (naturalAnd
105 (naturalNonzero state)
106 (naturalAnd
107 (naturalLessOrEqual
108 state
109 (naturalSaturatingSubtract nativePhysicalMemoryWordLimit scratch))
110 (naturalLessOrEqual
111 slots
112 (naturalDivideUnchecked
113 (naturalSaturatingSubtract
114 (naturalSaturatingSubtract nativePhysicalMemoryWordLimit scratch)
115 state)
116 nativePhysicalMemoryWordBytes))))))))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.