Initialize the owner-controlled policy and counters. Runtime room checks
precede every mutation; accepted counts are the sum of the two used fields.
218def captureInitialControl =
219 (lambda unrestricted ordinaryCapacity : Nat .
220 (lambda unrestricted reservedCapacity : Nat .
221 (lambda unrestricted required : Nat .
222 (aosChoose
223 Bytes
224 (naturalAnd
225 (naturalEqual
226 (aosCaptureAdmission 1 0 0 required ordinaryCapacity reservedCapacity 0 0)
227 0)
228 (naturalLessOrEqual
229 (captureQueueBytes ordinaryCapacity reservedCapacity)
230 captureExtentMaximum))
231 (bytes-append
232 (dataBytesWord64LE (modelWord64FromNaturalTruncated ordinaryCapacity))
233 (bytes-append
234 (dataBytesWord64LE (modelWord64FromNaturalTruncated reservedCapacity))
235 (bytes-append
236 (dataBytesWord64LE 0)
237 (bytes-append
238 (dataBytesWord64LE 0)
239 (bytes-append
240 (dataBytesWord64LE 0)
241 (bytes-append
242 (dataBytesWord64LE 0)
243 (bytes-append
244 (dataBytesWord64LE 0)
245 (dataBytesWord64LE (modelWord64FromNaturalTruncated required)))))))))
246 b""))))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.