Runtime.TelemetryValue

1module Runtime.TelemetryValue
2
3import Data.Bytes
4import Observe.Value
5import Runtime.TelemetryCapture
6import Std.Natural
7
8-- A fixed-width JSON cell contains canonical quoted decimal digits followed
9-- by JSON whitespace OUTSIDE the closing quote. Source integers therefore
10-- stay canonical even as a value grows from one to twenty digits. Reserving
11-- leading zeroes inside the string would violate AOS-JSON-004. These cells
12-- are drain storage, not a new AOS value or acquisition representation.
13def telemetryDecimalDigits : Nat =
14  (bytes-length (naturalDecimalBytesWithin 20 aosU64Maximum))
15
16def telemetryDecimalCellBytes : Nat =
17  (naturalAdd 2 telemetryDecimalDigits)
18
19def telemetryDecimalCell =
20  (lambda unrestricted negative : Nat .
21    (lambda unrestricted magnitude : Nat .
22      (let unrestricted digits =
23        (bytes-append
24          (aosChoose Bytes negative b"-" b"")
25          (naturalDecimalBytesWithin telemetryDecimalDigits magnitude))
26        in
27        (bytes-append
28          b"\""
29          (bytes-append
30            digits
31            (bytes-append
32              b"\""
33              (dataBytesRepeatByte
34                (byte 32)
35                (naturalSaturatingSubtract telemetryDecimalDigits (bytes-length digits)))))))))
36
37def telemetryUnsignedCell =
38  (lambda unrestricted value : Nat .
39    (aosChoose Bytes (naturalLessOrEqual value aosU64Maximum) (telemetryDecimalCell 0 value) b""))
40
41def telemetrySignedCell =
42  (lambda unrestricted negative : Nat .
43    (lambda unrestricted magnitude : Nat .
44      (aosChoose
45        Bytes
46        (naturalAnd
47          (naturalLessOrEqual negative 1)
48          (aosChoose
49            Nat
50            negative
51            (naturalAnd
52              (naturalNonzero magnitude)
53              (naturalLessOrEqual magnitude aosI64MinimumMagnitude))
54            (naturalLessOrEqual magnitude aosI64Maximum)))
55        (telemetryDecimalCell negative magnitude)
56        b"")))
57
58-- Hex cells retain fixed-width bytes: identities use memory order; float
59-- bits use most-significant-byte first. The caller declares which operation
60-- it needs. A numerical value is never inferred from a raw byte sequence.
61def telemetryHexSourceMaximumBytes : Nat =
62  captureValuesBytes
63
64def telemetryHexCellBytes =
65  (lambda unrestricted width : Nat . (naturalAdd 2 (naturalMultiply 2 width)))
66
67def telemetryHexCell =
68  (lambda unrestricted value : Bytes .
69    (aosChoose
70      Bytes
71      (naturalAnd
72        (naturalNonzero (bytes-length value))
73        (naturalLessOrEqual (bytes-length value) telemetryHexSourceMaximumBytes))
74      (bytes-append b"\"" (bytes-append (dataBytesRenderHex value) b"\""))
75      b""))
76
77-- Admission is checked before touching either buffer. Source and destination
78-- disjointness is a caller layout obligation, certified alongside application
79-- and publication storage. Codes: 0 admitted, 4 refused; no durability claim.
80def telemetryHexCellAdmission =
81  (lambda unrestricted width : Nat .
82    (lambda unrestricted reverse : Nat .
83      (lambda unrestricted sourceExtent : Nat .
84        (lambda unrestricted destinationExtent : Nat .
85          (aosChoose
86            Nat
87            (naturalAnd
88              (naturalNonzero width)
89              (naturalAnd
90                (naturalLessOrEqual width telemetryHexSourceMaximumBytes)
91                (naturalAnd
92                  (naturalLessOrEqual reverse 1)
93                  (naturalAnd
94                    (naturalLessOrEqual width sourceExtent)
95                    (naturalLessOrEqual
96                      width
97                      (naturalDivideUnchecked (naturalSaturatingSubtract destinationExtent 2) 2))))))
98            0
99            4)))))
100
101-- Subtract only after retaining the offset bound. This is equivalent to
102-- offset + width <= extent over naturals, without overflowing machine-word
103-- evaluation when a rejected caller supplies a maximal offset or width.
104def telemetryRangeFits =
105  (lambda unrestricted offset : Nat .
106    (lambda unrestricted width : Nat .
107      (lambda unrestricted extent : Nat .
108        (naturalAnd
109          (naturalLessOrEqual offset extent)
110          (naturalLessOrEqual width (naturalSaturatingSubtract extent offset))))))
111
112def telemetryWordCellAdmission =
113  (lambda unrestricted offset : Nat .
114    (lambda unrestricted sourceExtent : Nat .
115      (lambda unrestricted destinationExtent : Nat .
116        (aosChoose
117          Nat
118          (naturalAnd
119            (telemetryRangeFits offset captureWordBytes captureRecordBytes)
120            (naturalAnd
121              (telemetryRangeFits offset captureWordBytes sourceExtent)
122              (naturalLessOrEqual telemetryDecimalCellBytes destinationExtent)))
123          0
124          4))))
125
126def telemetryHexSliceCellAdmission =
127  (lambda unrestricted width : Nat .
128    (lambda unrestricted reverse : Nat .
129      (lambda unrestricted offset : Nat .
130        (lambda unrestricted sourceExtent : Nat .
131          (lambda unrestricted destinationExtent : Nat .
132            (aosChoose
133              Nat
134              (naturalAnd
135                (telemetryRangeFits offset width captureRecordBytes)
136                (telemetryRangeFits offset width sourceExtent))
137              (telemetryHexCellAdmission width reverse width destinationExtent)
138              4))))))