Observe.Capture

1module Observe.Capture
2
3import Observe.Value
4import Std.Natural
5
6-- Memory capture is not persistence. Result codes: 0 excluded, 1 queued,
7-- 2 selected but dropped, 3 pending at a declared safe boundary, 4 refused.
8-- Exclusions have no sequence. Optional loss does have a sequence, so AOS
9-- coverage can distinguish unselected quantities from selected records lost.
10-- Reserved health/terminal records never consume ordinary event capacity and
11-- 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)))))))))
50
51-- Exact room flags come from the bounded runtime counters. Refuse before any
52-- mutation if a required counter would wrap; never record an invented zero.
53def aosCaptureCounterAdmission =
54  (lambda unrestricted decision : Nat .
55    (lambda unrestricted sequenceRoom : Nat .
56      (lambda unrestricted droppedRoom : Nat .
57        (lambda unrestricted excludedRoom : Nat .
58          (aosChoose
59            Nat
60            (naturalAnd
61              (naturalLessOrEqual decision 4)
62              (naturalAnd
63                (naturalLessOrEqual sequenceRoom 1)
64                (naturalAnd (naturalLessOrEqual droppedRoom 1) (naturalLessOrEqual excludedRoom 1))))
65            (aosChoose
66              Nat
67              (naturalEqual decision 0)
68              (aosChoose Nat excludedRoom 0 4)
69              (aosChoose
70                Nat
71                (naturalEqual decision 1)
72                (aosChoose Nat sequenceRoom 1 4)
73                (aosChoose
74                  Nat
75                  (naturalEqual decision 2)
76                  (aosChoose Nat (naturalAnd sequenceRoom droppedRoom) 2 4)
77                  decision)))
78            4)))))