1module Runtime.NativeTelemetryRecord
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Data.Bytes
6import Model.Parameter
7import Model.Word64
8import Observe.Value
9import Runtime.NativeLaunchRecipeLoad
10import Runtime.NativePhysicalProgram
11import Runtime.NativeTelemetry
12import Runtime.NativeTelemetrySeal
13import Runtime.NativeTelemetryValue
14import Runtime.TelemetryCapture
15import Runtime.TelemetryIdentity
16import Runtime.TelemetryRecord
17import Runtime.TelemetryRecordRoutine
18import Runtime.TelemetryValue
19import Std.Natural
20import Runtime.NativeWordDigest
21
22-- System V realization of the shared read-only admission algorithm. Keep
23-- register roles and encodings stable while both targets share the semantics.
24def recordX86Backend =
25 (constructor
26 TelemetryRecordBackend
27 TelemetryRecordBackendValue
28 (family X86NativeAssembly)
29 (family X86NativeRegister64)
30 digestLoad64
31 digestOr
32 digestCmpImm
33 (digestJumpIf (constructor X86NativeCondition X86NativeConditionZero))
34 (digestJumpIf (constructor X86NativeCondition X86NativeConditionBelow))
35 digestMovImm
36 digestLabel
37 digestReturn
38 digestEnd
39 digestRAX
40 digestR10
41 digestRDI
42 digestRSI
43 digestRCX
44 digestR8
45 digestR9)
46
47def recordAdmissionAssembly =
48 (lambda unrestricted parts : (family TelemetryRecordParts) .
49 (telemetryRecordAssemblyFor
50 (family X86NativeAssembly)
51 (family X86NativeRegister64)
52 recordX86Backend
53 (constructor TelemetryRecordRoutineKind TelemetryRecordAdmissionRoutine parts)))
54
55def recordAdmissionRoutine =
56 (lambda unrestricted parts : (family TelemetryRecordParts) .
57 (compiler-native-encode (family X86NativeAssembly) (recordAdmissionAssembly parts)))
58
59def nativeTelemetryRecordAdmissionRoutine =
60 (lambda unrestricted program : (family TelemetryRecordPlan) .
61 (eliminate
62 TelemetryRecordPlan
63 (lambda unrestricted current : (family TelemetryRecordPlan) . Bytes)
64 program
65 (branch TelemetryRecordReady parts template . (recordAdmissionRoutine parts))
66 (branch TelemetryRecordRefused reason . b"")))
67
68-- Reads only the caller's private rendering status, never an application value.
69def recordStatusRoutine : Bytes =
70 (compiler-native-encode
71 (family X86NativeAssembly)
72 (telemetryRecordAssemblyFor
73 (family X86NativeAssembly)
74 (family X86NativeRegister64)
75 recordX86Backend
76 (constructor TelemetryRecordRoutineKind TelemetryRecordStatusRoutine)))
77
78def recordState =
79 (lambda unrestricted offset : Nat .
80 (constructor
81 NativePhysicalOperand
82 NativePhysicalStateAddress
83 (modelWord64FromNaturalTruncated offset)))
84
85def recordCellCommand =
86 (lambda unrestricted routine : Bytes .
87 (lambda unrestricted source : (family NativePhysicalOperand) .
88 (lambda unrestricted destination : Nat .
89 (lambda unrestricted sourceExtent : Nat .
90 (lambda unrestricted destinationExtent : Nat .
91 (lambda unrestricted identity : Bytes .
92 (nativeLaunchRecipeCommand
93 (constructor
94 NativePhysicalOperation
95 NativePhysicalMachineRoutine
96 routine
97 (constructor
98 NativePhysicalArguments
99 NativePhysicalArgumentsValue
100 source
101 (recordState destination)
102 (nativeLaunchRecipeImmediate sourceExtent)
103 (nativeLaunchRecipeImmediate destinationExtent)
104 (nativeLaunchRecipeImmediate 0)
105 (nativeLaunchRecipeImmediate 0))
106 (constructor NativePhysicalResultBinding NativePhysicalDiscardResult))
107 identity)))))))
108
109-- Offsets are accumulated from the very pieces copied into the output. No
110-- caller has a second field-offset table. Admitted field shapes/constant
111-- extents make formatting total for all captured machine words. References
112-- were validated before this stage and cannot change during the drain.
113def recordPatchCommands =
114 (lambda unrestricted parts : (family TelemetryRecordParts) .
115 (lambda unrestricted source : (family NativePhysicalOperand) .
116 (lambda unrestricted identities : (family NativePhysicalOperand) .
117 (lambda unrestricted identity : Bytes .
118 (eliminate
119 TelemetryRecordParts
120 (lambda unrestricted current : (family TelemetryRecordParts) .
121 (pi unrestricted at : Nat .
122 (pi unrestricted commands : (family NativePhysicalCommands) .
123 (family NativePhysicalCommands))))
124 parts
125 (branch
126 TelemetryRecordEnd
127 .
128 (lambda unrestricted at : Nat .
129 (lambda unrestricted commands : (family NativePhysicalCommands) . commands)))
130 (branch
131 TelemetryRecordLiteral
132 bytes
133 tail
134 induction
135 .
136 (lambda unrestricted at : Nat .
137 (lambda unrestricted commands : (family NativePhysicalCommands) .
138 (induction (naturalAdd at (bytes-length bytes)) commands))))
139 (branch
140 TelemetryRecordDecimal
141 signed
142 offset
143 tail
144 induction
145 .
146 (lambda unrestricted at : Nat .
147 (lambda unrestricted commands : (family NativePhysicalCommands) .
148 (recordCellCommand
149 (nativeTelemetryDecimalWordCellRoutine signed offset)
150 source
151 at
152 captureRecordBytes
153 telemetryDecimalCellBytes
154 identity
155 (induction (naturalAdd at telemetryDecimalCellBytes) commands)))))
156 (branch
157 TelemetryRecordHex
158 sourceKind
159 offset
160 width
161 reverse
162 nonzero
163 tail
164 induction
165 .
166 (lambda unrestricted at : Nat .
167 (lambda unrestricted commands : (family NativePhysicalCommands) .
168 (recordCellCommand
169 (nativeTelemetryHexSliceCellRoutine width reverse offset)
170 (aosChoose (family NativePhysicalOperand) sourceKind identities source)
171 at
172 (aosChoose Nat sourceKind telemetryIdentitySetBytes captureRecordBytes)
173 (telemetryHexCellBytes width)
174 identity
175 (induction (naturalAdd at (telemetryHexCellBytes width)) commands))))))))))
176
177-- A declaration derives its entire envelope, including identity and sequence
178-- cells. On refusal, status is four and prior event bytes remain unchanged;
179-- callers must not publish those stale bytes. Success is zero, not a durable
180-- acknowledgement. The arena's status word and event region have one owner.
181def recordRenderCommands =
182 (lambda unrestricted parts : (family TelemetryRecordParts) .
183 (lambda unrestricted bytes : Bytes .
184 (lambda unrestricted source : (family NativePhysicalOperand) .
185 (lambda unrestricted identities : (family NativePhysicalOperand) .
186 (lambda unrestricted arenaAt : Nat .
187 (lambda unrestricted resultSlot : Nat .
188 (lambda unrestricted identity : Bytes .
189 (lambda unrestricted tail : (family NativePhysicalCommands) .
190 (let unrestricted destination =
191 (naturalAdd arenaAt telemetryRecordAt)
192 in
193 (nativeLaunchRecipeCommand
194 (constructor
195 NativePhysicalOperation
196 NativePhysicalStoreWord64
197 (recordState arenaAt)
198 (nativeLaunchRecipeImmediate 4))
199 identity
200 (nativeLaunchRecipeCommand
201 (constructor
202 NativePhysicalOperation
203 NativePhysicalMachineRoutine
204 (recordAdmissionRoutine parts)
205 (constructor
206 NativePhysicalArguments
207 NativePhysicalArgumentsValue
208 source
209 identities
210 (recordState destination)
211 (nativeLaunchRecipeImmediate captureRecordBytes)
212 (nativeLaunchRecipeImmediate telemetryIdentitySetBytes)
213 (nativeLaunchRecipeImmediate (bytes-length bytes)))
214 (nativeLaunchRecipeStore resultSlot))
215 identity
216 (nativeLaunchRecipeCommand
217 (constructor
218 NativePhysicalOperation
219 NativePhysicalRepeatBeginCounted
220 (nativeLaunchRecipeSlotValue resultSlot))
221 identity
222 (nativeLaunchRecipeCommand
223 (constructor
224 NativePhysicalOperation
225 NativePhysicalCopyPayloadToState
226 (modelWord64FromNaturalTruncated destination)
227 (modelWord64FromNaturalTruncated (bytes-length bytes))
228 bytes)
229 identity
230 (recordPatchCommands
231 parts
232 source
233 identities
234 identity
235 destination
236 (nativeLaunchRecipeCommand
237 (constructor
238 NativePhysicalOperation
239 NativePhysicalStoreWord64
240 (recordState arenaAt)
241 (nativeLaunchRecipeImmediate 0))
242 identity
243 (nativeLaunchRecipeCommand
244 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
245 identity
246 (nativeLaunchRecipeCommand
247 (constructor
248 NativePhysicalOperation
249 NativePhysicalMachineRoutine
250 recordStatusRoutine
251 (nativeLaunchRecipeArguments
252 (recordState arenaAt)
253 (nativeLaunchRecipeImmediate 0)
254 (nativeLaunchRecipeImmediate 0)
255 (nativeLaunchRecipeImmediate 0))
256 (nativeLaunchRecipeStore resultSlot))
257 identity
258 tail)))))))))))))))))
259
260def nativeTelemetryRecordCommands =
261 (lambda unrestricted program : (family TelemetryRecordPlan) .
262 (lambda unrestricted source : (family NativePhysicalOperand) .
263 (lambda unrestricted identities : (family NativePhysicalOperand) .
264 (lambda unrestricted arenaAt : Nat .
265 (lambda unrestricted resultSlot : Nat .
266 (lambda unrestricted identity : Bytes .
267 (lambda unrestricted tail : (family NativePhysicalCommands) .
268 (eliminate
269 TelemetryRecordPlan
270 (lambda unrestricted current : (family TelemetryRecordPlan) .
271 (family NativePhysicalCommands))
272 program
273 (branch
274 TelemetryRecordReady
275 parts
276 template
277 .
278 (recordRenderCommands
279 parts
280 template
281 source
282 identities
283 arenaAt
284 resultSlot
285 identity
286 tail))
287 (branch
288 TelemetryRecordRefused
289 reason
290 .
291 (nativeLaunchRecipeCommand
292 (constructor
293 NativePhysicalOperation
294 NativePhysicalMachineRoutine
295 b""
296 (nativeLaunchRecipeArguments
297 source
298 identities
299 (recordState arenaAt)
300 (nativeLaunchRecipeImmediate 0))
301 (nativeLaunchRecipeStore resultSlot))
302 identity
303 tail))))))))))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.