Memory capture is not persistence. Result codes: 0 excluded, 1 queued,
2 selected but dropped, 3 pending at a declared safe boundary, 4 refused.
Exclusions have no sequence. Optional loss does have a sequence, so AOS
coverage can distinguish unselected quantities from selected records lost.
Reserved health/terminal records never consume ordinary event capacity and
never drop: an exhausted reserve requires a safe-boundary decision.
12def aosCaptureAdmission =
13 (lambda unrestricted version : Nat .
14 (lambda unrestricted selected : Nat .
15 (lambda unrestricted reserved : Nat .
16 (lambda unrestricted required : Nat .
17 (lambda unrestricted ordinaryCapacity : Nat .
18 (lambda unrestricted reservedCapacity : Nat .
19 (lambda unrestricted ordinaryUsed : Nat .
20 (lambda unrestricted reservedUsed : Nat .
21 (aosChoose
22 Nat
23 (naturalAnd
24 (naturalEqual version 1)
25 (naturalAnd
26 (naturalLessOrEqual selected 1)
27 (naturalAnd
28 (naturalLessOrEqual reserved 1)
29 (naturalAnd
30 (naturalLessOrEqual required 1)
31 (naturalAnd
32 (naturalLessOrEqual 2 reservedCapacity)
33 (naturalAnd
34 (naturalLessOrEqual ordinaryUsed ordinaryCapacity)
35 (naturalLessOrEqual reservedUsed reservedCapacity)))))))
36 (aosChoose
37 Nat
38 (naturalIsZero selected)
39 (aosChoose Nat (naturalIsZero reserved) 0 4)
40 (aosChoose
41 Nat
42 (naturalIsZero reserved)
43 (aosChoose
44 Nat
45 (naturalLess ordinaryUsed ordinaryCapacity)
46 1
47 (aosChoose Nat (naturalIsZero required) 2 3))
48 (aosChoose Nat (naturalLess reservedUsed reservedCapacity) 1 3)))
49 4)))))))))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.