1module Runtime.TelemetryRecordRoutine
2
3import Observe.Value
4import Runtime.TelemetryCapture
5import Runtime.TelemetryIdentity
6import Runtime.TelemetryRecord
7import Std.Natural
8
9-- Read-only admission for a closed record recipe. Extents are checked before
10-- any source read; all four bound identities and required 128-bit references
11-- must be nonzero. A caller supplies live disjoint buffers, keeps the source
12-- and identities stable through rendering, and checks the returned status.
13-- Success here grants rendering, never publication or durable acknowledgement.
14-- Word loads and OR operate on exact 64-bit words; extent comparisons are
15-- unsigned. Emitters preserve the host interpreter's persistent registers.
16family TelemetryRecordRoutineKind : Type 0
17constructor TelemetryRecordAdmissionRoutine
18field unrestricted recordAdmissionParts : (family TelemetryRecordParts)
19constructor TelemetryRecordStatusRoutine
20
21end-family
22
23family TelemetryRecordBackend : Type 0
24parameter erased A : Type 0
25parameter erased R : Type 0
26constructor TelemetryRecordBackendValue
27field unrestricted backendRecordLoad64 : (pi unrestricted destination : R . (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted tail : A . A))))
28field unrestricted backendRecordOr : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
29field unrestricted backendRecordCompareImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
30field unrestricted backendRecordJumpZero : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
31field unrestricted backendRecordJumpBelow : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
32field unrestricted backendRecordSet : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
33field unrestricted backendRecordLabel : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
34field unrestricted backendRecordReturn : (pi unrestricted tail : A . A)
35field unrestricted backendRecordEnd : A
36field unrestricted backendRecordResult : R
37field unrestricted backendRecordScratch : R
38field unrestricted backendRecordSource : R
39field unrestricted backendRecordIdentities : R
40field unrestricted backendRecordSourceExtent : R
41field unrestricted backendRecordIdentityExtent : R
42field unrestricted backendRecordOutputExtent : R
43
44end-family
45
46def telemetryRecordAssemblyFor =
47 (lambda erased A : Type 0 .
48 (lambda erased R : Type 0 .
49 (lambda unrestricted backend : (family TelemetryRecordBackend A R) .
50 (lambda unrestricted kind : (family TelemetryRecordRoutineKind) .
51 (eliminate
52 TelemetryRecordBackend
53 (lambda unrestricted current : (family TelemetryRecordBackend A R) . A)
54 backend
55 (branch
56 TelemetryRecordBackendValue
57 recordLoad64
58 recordOr
59 recordCompareImmediate
60 recordJumpZero
61 recordJumpBelow
62 recordSet
63 recordLabel
64 recordReturn
65 recordEnd
66 recordResult
67 recordScratch
68 recordSource
69 recordIdentities
70 recordSourceExtent
71 recordIdentityExtent
72 recordOutputExtent
73 .
74 (let unrestricted recordCheckNonzero =
75 (lambda unrestricted base : R .
76 (lambda unrestricted offset : Nat .
77 (lambda unrestricted tail : A .
78 (recordLoad64
79 recordResult
80 base
81 offset
82 (recordLoad64
83 recordScratch
84 base
85 (naturalAdd offset captureWordBytes)
86 (recordOr
87 recordResult
88 recordScratch
89 (recordCompareImmediate
90 recordResult
91 0
92 (recordJumpZero b"record-refused" tail))))))))
93 in
94 (let unrestricted recordCheckParts =
95 (lambda unrestricted parts : (family TelemetryRecordParts) .
96 (eliminate
97 TelemetryRecordParts
98 (lambda unrestricted current : (family TelemetryRecordParts) . A)
99 parts
100 (branch
101 TelemetryRecordEnd
102 .
103 (recordSet
104 recordResult
105 1
106 (recordReturn
107 (recordLabel
108 b"record-refused"
109 (recordSet recordResult 0 (recordReturn recordEnd))))))
110 (branch TelemetryRecordLiteral bytes tail induction . induction)
111 (branch TelemetryRecordDecimal signed offset tail induction . induction)
112 (branch
113 TelemetryRecordHex
114 source
115 offset
116 width
117 reverse
118 nonzero
119 tail
120 induction
121 .
122 (aosChoose
123 A
124 nonzero
125 (recordCheckNonzero
126 (aosChoose R source recordIdentities recordSource)
127 offset
128 induction)
129 induction))))
130 in
131 (let unrestricted recordAdmissionAssembly =
132 (lambda unrestricted parts : (family TelemetryRecordParts) .
133 (recordCompareImmediate
134 recordSourceExtent
135 captureRecordBytes
136 (recordJumpBelow
137 b"record-refused"
138 (recordCompareImmediate
139 recordIdentityExtent
140 telemetryIdentitySetBytes
141 (recordJumpBelow
142 b"record-refused"
143 (recordCompareImmediate
144 recordOutputExtent
145 (bytes-length (telemetryRecordPartBytes parts))
146 (recordJumpBelow
147 b"record-refused"
148 (nat-eliminate
149 (lambda unrestricted current : Nat . A)
150 (recordCheckParts parts)
151 (lambda unrestricted index : Nat .
152 (lambda unrestricted induction : A .
153 (recordCheckNonzero
154 recordIdentities
155 (telemetryIdentityOffset index)
156 induction)))
157 (succ telemetryProducerEpochIndex)))))))))
158 in
159 (eliminate
160 TelemetryRecordRoutineKind
161 (lambda unrestricted current : (family TelemetryRecordRoutineKind) . A)
162 kind
163 (branch
164 TelemetryRecordAdmissionRoutine
165 parts
166 .
167 (recordAdmissionAssembly parts))
168 (branch
169 TelemetryRecordStatusRoutine
170 .
171 (recordLoad64 recordResult recordSource 0 (recordReturn recordEnd)))))))))))))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.