Runtime.TelemetryCapture

1module Runtime.TelemetryCapture
2
3import Data.Bytes
4import Model.Parameter
5import Model.Word64
6import Observe.Capture
7import Observe.Value
8import Runtime.ArenaCertificate
9import Runtime.NativeTelemetry
10import Std.Natural
11
12-- A fixed-shape acquisition buffer for the existing native scalar record.
13-- This is capture storage, not a wire encoding or durability acknowledgement.
14-- Sequence precedes the native counters; formatting/sealing belongs to drain.
15-- The field list owns all offsets. No caller carries a layout-specific number.
16def captureWordBytes : Nat =
17  (bytes-length (nativeTelemetryWord64Bytes nativeTelemetryZeroWord64))
18
19def captureValuesBytes : Nat =
20  (bytes-length
21    (nativeTelemetryEncodeCounters
22      (constructor NativeTelemetryCounters NativeTelemetryCountersValue 0 0 0 0 0 0 0 0)))
23
24def captureValueWords : Nat =
25  (naturalDivideUnchecked captureValuesBytes captureWordBytes)
26
27def captureSequenceAt : Nat =
28  0
29
30def captureValuesAt : Nat =
31  captureWordBytes
32
33def captureRecordBytes : Nat =
34  (naturalAdd captureWordBytes captureValuesBytes)
35
36def captureOrdinaryCapacityIndex : Nat =
37  0
38
39def captureOrdinaryCapacityAt : Nat =
40  (naturalMultiply captureOrdinaryCapacityIndex captureWordBytes)
41
42def captureReservedCapacityIndex : Nat =
43  (succ captureOrdinaryCapacityIndex)
44
45def captureReservedCapacityAt : Nat =
46  (naturalMultiply captureReservedCapacityIndex captureWordBytes)
47
48def captureOrdinaryUsedIndex : Nat =
49  (succ captureReservedCapacityIndex)
50
51def captureOrdinaryUsedAt : Nat =
52  (naturalMultiply captureOrdinaryUsedIndex captureWordBytes)
53
54def captureReservedUsedIndex : Nat =
55  (succ captureOrdinaryUsedIndex)
56
57def captureReservedUsedAt : Nat =
58  (naturalMultiply captureReservedUsedIndex captureWordBytes)
59
60def captureNextSequenceIndex : Nat =
61  (succ captureReservedUsedIndex)
62
63def captureNextSequenceAt : Nat =
64  (naturalMultiply captureNextSequenceIndex captureWordBytes)
65
66def captureDroppedIndex : Nat =
67  (succ captureNextSequenceIndex)
68
69def captureDroppedAt : Nat =
70  (naturalMultiply captureDroppedIndex captureWordBytes)
71
72def captureExcludedIndex : Nat =
73  (succ captureDroppedIndex)
74
75def captureExcludedAt : Nat =
76  (naturalMultiply captureExcludedIndex captureWordBytes)
77
78def captureRequiredIndex : Nat =
79  (succ captureExcludedIndex)
80
81def captureRequiredAt : Nat =
82  (naturalMultiply captureRequiredIndex captureWordBytes)
83
84def captureControlBytes : Nat =
85  (naturalMultiply (succ captureRequiredIndex) captureWordBytes)
86
87def captureAlign =
88  (lambda unrestricted n : Nat .
89    (naturalMultiply
90      (naturalDivideUnchecked
91        (naturalAdd n (naturalSaturatingSubtract captureWordBytes 1))
92        captureWordBytes)
93      captureWordBytes))
94
95def captureControlAt =
96  captureAlign
97
98def captureQueueAt =
99  (lambda unrestricted applicationBytes : Nat .
100    (naturalAdd (captureControlAt applicationBytes) captureControlBytes))
101
102def captureQueueBytes =
103  (lambda unrestricted ordinaryCapacity : Nat .
104    (lambda unrestricted reservedCapacity : Nat .
105      (naturalMultiply (naturalAdd ordinaryCapacity reservedCapacity) captureRecordBytes)))
106
107def captureValuesScratchAt =
108  (lambda unrestricted applicationBytes : Nat .
109    (lambda unrestricted ordinaryCapacity : Nat .
110      (lambda unrestricted reservedCapacity : Nat .
111        (naturalAdd
112          (captureQueueAt applicationBytes)
113          (captureQueueBytes ordinaryCapacity reservedCapacity)))))
114
115def captureArenaBytes =
116  (lambda unrestricted applicationBytes : Nat .
117    (lambda unrestricted ordinaryCapacity : Nat .
118      (lambda unrestricted reservedCapacity : Nat .
119        (naturalAdd
120          (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity)
121          captureValuesBytes))))
122
123-- A general program may have no application arena. The capture arena
124-- must not invent an empty resident merely to certify that valid shape.
125def captureArenaResidents =
126  (lambda unrestricted applicationBytes : Nat .
127    (lambda unrestricted ordinaryCapacity : Nat .
128      (lambda unrestricted reservedCapacity : Nat .
129        (aosChoose
130          (family ArenaResidents)
131          (naturalIsZero applicationBytes)
132          (constructor
133            ArenaResidents
134            ArenaResidentsNext
135            (constructor
136              ArenaResident
137              ArenaResidentValue
138              b"capture-control"
139              (captureControlAt applicationBytes)
140              captureControlBytes
141              captureWordBytes)
142            (constructor
143              ArenaResidents
144              ArenaResidentsNext
145              (constructor
146                ArenaResident
147                ArenaResidentValue
148                b"capture-queue"
149                (captureQueueAt applicationBytes)
150                (captureQueueBytes ordinaryCapacity reservedCapacity)
151                captureWordBytes)
152              (constructor
153                ArenaResidents
154                ArenaResidentsNext
155                (constructor
156                  ArenaResident
157                  ArenaResidentValue
158                  b"capture-values"
159                  (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity)
160                  captureValuesBytes
161                  captureWordBytes)
162                (constructor ArenaResidents ArenaResidentsEnd))))
163          (constructor
164            ArenaResidents
165            ArenaResidentsNext
166            (constructor ArenaResident ArenaResidentValue b"application" 0 applicationBytes 1)
167            (constructor
168              ArenaResidents
169              ArenaResidentsNext
170              (constructor
171                ArenaResident
172                ArenaResidentValue
173                b"capture-control"
174                (captureControlAt applicationBytes)
175                captureControlBytes
176                captureWordBytes)
177              (constructor
178                ArenaResidents
179                ArenaResidentsNext
180                (constructor
181                  ArenaResident
182                  ArenaResidentValue
183                  b"capture-queue"
184                  (captureQueueAt applicationBytes)
185                  (captureQueueBytes ordinaryCapacity reservedCapacity)
186                  captureWordBytes)
187                (constructor
188                  ArenaResidents
189                  ArenaResidentsNext
190                  (constructor
191                    ArenaResident
192                    ArenaResidentValue
193                    b"capture-values"
194                    (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity)
195                    captureValuesBytes
196                    captureWordBytes)
197                  (constructor ArenaResidents ArenaResidentsEnd)))))))))
198
199def captureExtentMaximum : Nat =
200  18446744073709551615
201
202def captureArenaCertificate =
203  (lambda unrestricted applicationBytes : Nat .
204    (lambda unrestricted ordinaryCapacity : Nat .
205      (lambda unrestricted reservedCapacity : Nat .
206        (naturalAnd
207          (naturalLessOrEqual
208            (captureArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
209            captureExtentMaximum)
210          (naturalAnd
211            (naturalLessOrEqual 2 reservedCapacity)
212            (arenaCertificate
213              (captureArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
214              (captureArenaResidents applicationBytes ordinaryCapacity reservedCapacity)))))))
215
216-- Initialize the owner-controlled policy and counters. Runtime room checks
217-- 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""))))