1module Observe.CapturePolicy
2
3import Data.Bytes
4import Observe.Value
5import Std.Natural
6
7-- Profiles select source-declared quantities; they do not infer meaning from
8-- names or values. Content capture needs a separate opt-in even in diagnostics.
9family CaptureProfile : Type 0
10constructor CaptureLifecycleProfile
11constructor CaptureProgressProfile
12constructor CapturePerformanceProfile
13constructor CaptureDiagnosticProfile
14
15end-family
16
17family CaptureClass : Type 0
18constructor CaptureLifecycleClass
19constructor CaptureHealthClass
20constructor CaptureProgressClass
21constructor CapturePerformanceClass
22constructor CaptureDiagnosticClass
23constructor CaptureContentClass
24
25end-family
26
27-- Budgets apply to an encoded drain batch, not to the lifetime of a run or
28-- total process memory. Flush bounds count selected plus excluded opportunities
29-- between declared safe boundaries; they are not acquired wall-clock bounds.
30family CapturePolicy : Type 0
31constructor CapturePolicyValue
32field unrestricted capturePolicyVersionField : Nat
33field unrestricted capturePolicyIdentityField : Bytes
34field unrestricted capturePolicyProfileField : (family CaptureProfile)
35field unrestricted capturePolicyContentField : Nat
36field unrestricted capturePolicyOrdinaryField : Nat
37field unrestricted capturePolicyReservedField : Nat
38field unrestricted capturePolicyBytesField : Nat
39field unrestricted capturePolicyDimensionsField : Nat
40field unrestricted capturePolicyFlushField : Nat
41field unrestricted capturePolicyRequiredField : Nat
42
43end-family
44
45family CaptureSite : Type 0
46constructor CaptureSiteValue
47field unrestricted captureSiteIdentityField : Bytes
48field unrestricted captureSiteNameField : Bytes
49field unrestricted captureSiteKindField : (family CaptureClass)
50field unrestricted captureSiteReservedField : Nat
51field unrestricted captureSiteDimensionsField : Nat
52field unrestricted captureSiteStrideField : Nat
53
54end-family
55
56def captureProfileLevel =
57 (lambda unrestricted profile : (family CaptureProfile) .
58 (eliminate
59 CaptureProfile
60 (lambda unrestricted current : (family CaptureProfile) . Nat)
61 profile
62 (branch CaptureLifecycleProfile . 0)
63 (branch CaptureProgressProfile . 1)
64 (branch CapturePerformanceProfile . 2)
65 (branch CaptureDiagnosticProfile . 3)))
66
67def captureProfileName =
68 (lambda unrestricted profile : (family CaptureProfile) .
69 (eliminate
70 CaptureProfile
71 (lambda unrestricted current : (family CaptureProfile) . Bytes)
72 profile
73 (branch CaptureLifecycleProfile . b"lifecycle")
74 (branch CaptureProgressProfile . b"progress")
75 (branch CapturePerformanceProfile . b"performance")
76 (branch CaptureDiagnosticProfile . b"diagnostic")))
77
78def captureClassLevel =
79 (lambda unrestricted kind : (family CaptureClass) .
80 (eliminate
81 CaptureClass
82 (lambda unrestricted current : (family CaptureClass) . Nat)
83 kind
84 (branch CaptureLifecycleClass . 0)
85 (branch CaptureHealthClass . 0)
86 (branch CaptureProgressClass . 1)
87 (branch CapturePerformanceClass . 2)
88 (branch CaptureDiagnosticClass . 3)
89 (branch CaptureContentClass . 4)))
90
91def captureClassName =
92 (lambda unrestricted kind : (family CaptureClass) .
93 (eliminate
94 CaptureClass
95 (lambda unrestricted current : (family CaptureClass) . Bytes)
96 kind
97 (branch CaptureLifecycleClass . b"lifecycle")
98 (branch CaptureHealthClass . b"health")
99 (branch CaptureProgressClass . b"progress")
100 (branch CapturePerformanceClass . b"performance")
101 (branch CaptureDiagnosticClass . b"diagnostic")
102 (branch CaptureContentClass . b"content")))
103
104def capturePolicyIdentifier =
105 (lambda unrestricted value : (family CapturePolicy) .
106 (eliminate
107 CapturePolicy
108 (lambda unrestricted current : (family CapturePolicy) . Bytes)
109 value
110 (branch
111 CapturePolicyValue
112 version
113 identity
114 profile
115 content
116 ordinary
117 reserved
118 bytes
119 dimensions
120 flush
121 required
122 .
123 identity)))
124
125def capturePolicyProfile =
126 (lambda unrestricted value : (family CapturePolicy) .
127 (eliminate
128 CapturePolicy
129 (lambda unrestricted current : (family CapturePolicy) . (family CaptureProfile))
130 value
131 (branch
132 CapturePolicyValue
133 version
134 identity
135 profile
136 content
137 ordinary
138 reserved
139 bytes
140 dimensions
141 flush
142 required
143 .
144 profile)))
145
146def capturePolicyContentEnabled =
147 (lambda unrestricted value : (family CapturePolicy) .
148 (eliminate
149 CapturePolicy
150 (lambda unrestricted current : (family CapturePolicy) . Nat)
151 value
152 (branch
153 CapturePolicyValue
154 version
155 identity
156 profile
157 content
158 ordinary
159 reserved
160 bytes
161 dimensions
162 flush
163 required
164 .
165 content)))
166
167def capturePolicyOrdinaryCapacity =
168 (lambda unrestricted value : (family CapturePolicy) .
169 (eliminate
170 CapturePolicy
171 (lambda unrestricted current : (family CapturePolicy) . Nat)
172 value
173 (branch
174 CapturePolicyValue
175 version
176 identity
177 profile
178 content
179 ordinary
180 reserved
181 bytes
182 dimensions
183 flush
184 required
185 .
186 ordinary)))
187
188def capturePolicyReservedCapacity =
189 (lambda unrestricted value : (family CapturePolicy) .
190 (eliminate
191 CapturePolicy
192 (lambda unrestricted current : (family CapturePolicy) . Nat)
193 value
194 (branch
195 CapturePolicyValue
196 version
197 identity
198 profile
199 content
200 ordinary
201 reserved
202 bytes
203 dimensions
204 flush
205 required
206 .
207 reserved)))
208
209def capturePolicyByteBudget =
210 (lambda unrestricted value : (family CapturePolicy) .
211 (eliminate
212 CapturePolicy
213 (lambda unrestricted current : (family CapturePolicy) . Nat)
214 value
215 (branch
216 CapturePolicyValue
217 version
218 identity
219 profile
220 content
221 ordinary
222 reserved
223 bytes
224 dimensions
225 flush
226 required
227 .
228 bytes)))
229
230def capturePolicyDimensionLimit =
231 (lambda unrestricted value : (family CapturePolicy) .
232 (eliminate
233 CapturePolicy
234 (lambda unrestricted current : (family CapturePolicy) . Nat)
235 value
236 (branch
237 CapturePolicyValue
238 version
239 identity
240 profile
241 content
242 ordinary
243 reserved
244 bytes
245 dimensions
246 flush
247 required
248 .
249 dimensions)))
250
251def capturePolicyFlushOpportunities =
252 (lambda unrestricted value : (family CapturePolicy) .
253 (eliminate
254 CapturePolicy
255 (lambda unrestricted current : (family CapturePolicy) . Nat)
256 value
257 (branch
258 CapturePolicyValue
259 version
260 identity
261 profile
262 content
263 ordinary
264 reserved
265 bytes
266 dimensions
267 flush
268 required
269 .
270 flush)))
271
272def capturePolicyRequired =
273 (lambda unrestricted value : (family CapturePolicy) .
274 (eliminate
275 CapturePolicy
276 (lambda unrestricted current : (family CapturePolicy) . Nat)
277 value
278 (branch
279 CapturePolicyValue
280 version
281 identity
282 profile
283 content
284 ordinary
285 reserved
286 bytes
287 dimensions
288 flush
289 required
290 .
291 required)))
292
293def captureSiteIdentifier =
294 (lambda unrestricted value : (family CaptureSite) .
295 (eliminate
296 CaptureSite
297 (lambda unrestricted current : (family CaptureSite) . Bytes)
298 value
299 (branch CaptureSiteValue identity name kind reserved dimensions stride . identity)))
300
301def captureSiteName =
302 (lambda unrestricted value : (family CaptureSite) .
303 (eliminate
304 CaptureSite
305 (lambda unrestricted current : (family CaptureSite) . Bytes)
306 value
307 (branch CaptureSiteValue identity name kind reserved dimensions stride . name)))
308
309def captureSiteClass =
310 (lambda unrestricted value : (family CaptureSite) .
311 (eliminate
312 CaptureSite
313 (lambda unrestricted current : (family CaptureSite) . (family CaptureClass))
314 value
315 (branch CaptureSiteValue identity name kind reserved dimensions stride . kind)))
316
317def captureSiteReserved =
318 (lambda unrestricted value : (family CaptureSite) .
319 (eliminate
320 CaptureSite
321 (lambda unrestricted current : (family CaptureSite) . Nat)
322 value
323 (branch CaptureSiteValue identity name kind reserved dimensions stride . reserved)))
324
325def captureSiteDimensions =
326 (lambda unrestricted value : (family CaptureSite) .
327 (eliminate
328 CaptureSite
329 (lambda unrestricted current : (family CaptureSite) . Nat)
330 value
331 (branch CaptureSiteValue identity name kind reserved dimensions stride . dimensions)))
332
333def captureSiteStride =
334 (lambda unrestricted value : (family CaptureSite) .
335 (eliminate
336 CaptureSite
337 (lambda unrestricted current : (family CaptureSite) . Nat)
338 value
339 (branch CaptureSiteValue identity name kind reserved dimensions stride . stride)))
340
341def capturePolicyAdmission =
342 (lambda unrestricted policy : (family CapturePolicy) .
343 (eliminate
344 CapturePolicy
345 (lambda unrestricted current : (family CapturePolicy) . Nat)
346 policy
347 (branch
348 CapturePolicyValue
349 version
350 identity
351 profile
352 content
353 ordinary
354 reserved
355 bytes
356 dimensions
357 flush
358 required
359 .
360 (naturalAnd
361 (naturalEqual version 1)
362 (naturalAnd
363 (aosIsIdentity identity)
364 (naturalAnd
365 (naturalLessOrEqual content 1)
366 (naturalAnd
367 (naturalLessOrEqual required 1)
368 (naturalAnd
369 (naturalLessOrEqual 2 reserved)
370 (naturalAnd
371 (naturalLessOrEqual (naturalAdd ordinary reserved) 1024)
372 (naturalAnd
373 (naturalNonzero bytes)
374 (naturalAnd
375 (naturalLessOrEqual bytes 18446744073709551615)
376 (naturalAnd
377 (naturalLessOrEqual dimensions 18446744073709551615)
378 (naturalAnd
379 (naturalNonzero flush)
380 (naturalAnd
381 (naturalLessOrEqual flush 18446744073709551615)
382 (aosChoose
383 Nat
384 content
385 (naturalEqual (captureProfileLevel profile) 3)
386 1)))))))))))))))
387
388def captureSiteAdmission =
389 (lambda unrestricted policy : (family CapturePolicy) .
390 (lambda unrestricted site : (family CaptureSite) .
391 (eliminate
392 CaptureSite
393 (lambda unrestricted current : (family CaptureSite) . Nat)
394 site
395 (branch
396 CaptureSiteValue
397 identity
398 name
399 kind
400 reserved
401 dimensions
402 stride
403 .
404 (naturalAnd
405 (capturePolicyAdmission policy)
406 (naturalAnd
407 (aosIsIdentity identity)
408 (naturalAnd
409 (naturalNonzero (bytes-length name))
410 (naturalAnd
411 (naturalLessOrEqual (bytes-length name) 256)
412 (naturalAnd
413 (naturalLessOrEqual reserved 1)
414 (naturalAnd
415 (naturalLessOrEqual dimensions (capturePolicyDimensionLimit policy))
416 (naturalAnd
417 (naturalNonzero stride)
418 (naturalAnd
419 (naturalLessOrEqual stride 18446744073709551615)
420 (naturalAnd
421 (aosChoose
422 Nat
423 (bytes-equal (captureClassName kind) b"health")
424 reserved
425 1)
426 (aosChoose
427 Nat
428 reserved
429 (naturalAnd
430 (naturalEqual (captureClassLevel kind) 0)
431 (naturalEqual stride 1))
432 1))))))))))))))
433
434def captureSiteSelected =
435 (lambda unrestricted policy : (family CapturePolicy) .
436 (lambda unrestricted site : (family CaptureSite) .
437 (naturalAnd
438 (captureSiteAdmission policy site)
439 (aosChoose
440 Nat
441 (naturalEqual (captureClassLevel (captureSiteClass site)) 4)
442 (capturePolicyContentEnabled policy)
443 (naturalLessOrEqual
444 (captureClassLevel (captureSiteClass site))
445 (captureProfileLevel (capturePolicyProfile policy)))))))
446
447-- A pending capture is not complete and cannot justify workload continuation.
448-- The runtime returns it at a safe boundary; the owning run policy must drain
449-- and retry or report its declared pause/failure, never turn it into success.
450def captureCanContinue =
451 (lambda unrestricted required : Nat .
452 (lambda unrestricted decision : Nat .
453 (naturalAnd
454 (naturalLessOrEqual required 1)
455 (naturalOr
456 (naturalLessOrEqual decision 1)
457 (naturalAnd (naturalEqual required 0) (naturalEqual decision 2))))))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.