1module Runtime.NativeTelemetryPublication
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Data.Bytes
6import Model.Word64
7import Observe.Value
8import Runtime.NativeLaunchRecipeLoad
9import Runtime.NativePhysicalProgram
10import Runtime.NativeTelemetry
11import Runtime.NativeTelemetryCapture
12import Runtime.NativeTelemetryIdentity
13import Runtime.NativeTelemetrySeal
14import Runtime.TelemetryCapture
15import Runtime.TelemetryIdentity
16import Runtime.TelemetryPublication
17import Runtime.TelemetryPublicationRoutine
18import Std.Natural
19import Runtime.NativeWordDigest
20
21-- Single-writer safe-boundary publication. Preparing copies occupied records,
22-- never unused capacity. Acquisition cannot run concurrently with prepare,
23-- sealing or commit. The plan certifies the capture, identity, padded body,
24-- record, zero-timespec and hash work areas together.
25-- Prepare ABI: control, queue, identities, publication arena, queue extent,
26-- publication extent. Commit ABI: control, publication arena, sink descriptor,
27-- sealed record, record length, containing-directory descriptor.
28--
29-- A full write followed by file AND directory fsync permits reclamation. Any
30-- failed/short write or sync poisons this sink and retains the queue/cumulative
31-- counters: appending a retry behind a torn tail would corrupt the journal.
32-- The caller receives a decision and owns its declared optional/required
33-- capture response. Publication never exits the application on its behalf.
34-- This is x86-64 Linux acquisition of filesystem durability, not GPU capture.
35def publicationCompare =
36 (lambda unrestricted left : (family X86NativeRegister64) .
37 (lambda unrestricted right : (family X86NativeRegister64) .
38 (digestEmit (constructor X86NativeInstruction X86NativeCompareRegister64 right left))))
39
40def publicationSubtract =
41 (lambda unrestricted left : (family X86NativeRegister64) .
42 (lambda unrestricted right : (family X86NativeRegister64) .
43 (digestEmit (constructor X86NativeInstruction X86NativeSubtractRegister64 right left))))
44
45def publicationJump =
46 (lambda unrestricted name : Bytes .
47 (lambda unrestricted tail : (family X86NativeAssembly) .
48 (constructor X86NativeAssembly X86NativeAssemblyJump name tail)))
49
50-- System V realization; syscall operations belong to the host adapter.
51def publicationX86JumpIf =
52 (lambda unrestricted condition : (family TelemetryPublicationCondition) .
53 (digestJumpIf
54 (eliminate
55 TelemetryPublicationCondition
56 (lambda unrestricted current : (family TelemetryPublicationCondition) .
57 (family X86NativeCondition))
58 condition
59 (branch TelemetryPublicationZero . (constructor X86NativeCondition X86NativeConditionZero))
60 (branch
61 TelemetryPublicationNotZero
62 .
63 (constructor X86NativeCondition X86NativeConditionNotZero))
64 (branch
65 TelemetryPublicationBelow
66 .
67 (constructor X86NativeCondition X86NativeConditionBelow))
68 (branch
69 TelemetryPublicationAbove
70 .
71 (constructor X86NativeCondition X86NativeConditionAbove)))))
72
73def publicationX86Write =
74 (lambda unrestricted tail : (family X86NativeAssembly) .
75 (digestMovImm digestRAX 1 (digestEmit (constructor X86NativeInstruction X86NativeSystemCall) tail)))
76
77def publicationX86Sync =
78 (lambda unrestricted tail : (family X86NativeAssembly) .
79 (digestMovImm digestRAX 74 (digestEmit (constructor X86NativeInstruction X86NativeSystemCall) tail)))
80
81def publicationX86Backend =
82 (constructor
83 TelemetryPublicationBackend
84 TelemetryPublicationBackendValue
85 (family X86NativeAssembly)
86 (family X86NativeRegister64)
87 digestMovImm
88 digestMov
89 digestLoad64
90 digestStore64
91 digestStore8
92 digestCmpImm
93 publicationCompare
94 publicationSubtract
95 digestOr
96 digestAdd
97 digestAddImm
98 digestMulImm
99 digestShr
100 publicationX86JumpIf
101 publicationJump
102 digestLabel
103 digestReturn
104 publicationX86Write
105 publicationX86Sync
106 digestEnd
107 digestRAX
108 digestRDI
109 digestRSI
110 digestRDX
111 digestRCX
112 digestR8
113 digestR9
114 digestR10
115 digestR11
116 digestR12
117 digestR13
118 digestR14
119 digestR15)
120
121def nativeTelemetryPublicationRoutineFor =
122 (lambda unrestricted kind : (family TelemetryPublicationRoutineKind) .
123 (compiler-native-encode
124 (family X86NativeAssembly)
125 (telemetryPublicationAssemblyFor
126 (family X86NativeAssembly)
127 (family X86NativeRegister64)
128 publicationX86Backend
129 kind)))
130
131-- A scalar snapshot fits in any admitted larger body bound. The typed drain
132-- can replace the copied scalar payload before sealing; this routine itself
133-- still prepares version-two scalar bytes and never claims typed admission.
134def nativeTelemetryPublicationPrepareRoutineForBody =
135 (lambda unrestricted ordinaryCapacity : Nat .
136 (lambda unrestricted reservedCapacity : Nat .
137 (lambda unrestricted bodyBytes : Nat .
138 (aosChoose
139 Bytes
140 (naturalAnd
141 (naturalLessOrEqual
142 (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity)
143 bodyBytes)
144 (naturalLessOrEqual (publicationRecordBytes bodyBytes) publicationMaximumFrameBytes))
145 (nativeTelemetryPublicationRoutineFor
146 (constructor
147 TelemetryPublicationRoutineKind
148 TelemetryPublicationPrepareRoutine
149 ordinaryCapacity
150 reservedCapacity
151 bodyBytes))
152 b""))))
153
154def nativeTelemetryPublicationPrepareRoutine =
155 (lambda unrestricted ordinaryCapacity : Nat .
156 (lambda unrestricted reservedCapacity : Nat .
157 (nativeTelemetryPublicationPrepareRoutineForBody
158 ordinaryCapacity
159 reservedCapacity
160 (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity))))
161
162-- Replaces version/length/padding in a prepared snapshot. The shared
163-- algorithm checks the exact arena before access and clears accessible
164-- readiness on refusal. This byte mechanism does not validate JSON meaning.
165def nativeTelemetryPublicationTypedPaddingRoutineForBody =
166 (lambda unrestricted bodyBytes : Nat .
167 (aosChoose
168 Bytes
169 (naturalAnd
170 (naturalLessOrEqual publicationPayloadRecordsAt bodyBytes)
171 (naturalLessOrEqual (publicationRecordBytes bodyBytes) publicationMaximumFrameBytes))
172 (nativeTelemetryPublicationRoutineFor
173 (constructor
174 TelemetryPublicationRoutineKind
175 TelemetryPublicationTypedPaddingRoutine
176 bodyBytes))
177 b""))
178
179def nativeTelemetryPublicationCommitRoutine : Bytes =
180 (nativeTelemetryPublicationRoutineFor
181 (constructor TelemetryPublicationRoutineKind TelemetryPublicationCommitRoutine))
182
183-- All external operands are declared host descriptors. The containing-directory
184-- descriptor must be the directory used to open the sink, not an unrelated
185-- descriptor whose fsync merely happens to succeed.
186def publicationStateAddress =
187 (lambda unrestricted applicationBytes : Nat .
188 (lambda unrestricted ordinaryCapacity : Nat .
189 (lambda unrestricted reservedCapacity : Nat .
190 (lambda unrestricted relative : Nat .
191 (constructor
192 NativePhysicalOperand
193 NativePhysicalStateAddress
194 (modelWord64FromNaturalTruncated
195 (naturalAdd
196 (publicationBase applicationBytes ordinaryCapacity reservedCapacity)
197 relative)))))))
198
199def publicationStateLoad =
200 (lambda unrestricted applicationBytes : Nat .
201 (lambda unrestricted ordinaryCapacity : Nat .
202 (lambda unrestricted reservedCapacity : Nat .
203 (lambda unrestricted relative : Nat .
204 (constructor
205 NativePhysicalOperand
206 NativePhysicalStateLoad64
207 (modelWord64FromNaturalTruncated
208 (naturalAdd
209 (publicationBase applicationBytes ordinaryCapacity reservedCapacity)
210 relative)))))))
211
212def publicationCopyPayload =
213 (lambda unrestricted applicationBytes : Nat .
214 (lambda unrestricted ordinaryCapacity : Nat .
215 (lambda unrestricted reservedCapacity : Nat .
216 (lambda unrestricted relative : Nat .
217 (lambda unrestricted payload : Bytes .
218 (lambda unrestricted identity : Bytes .
219 (nativeLaunchRecipeCommand
220 (constructor
221 NativePhysicalOperation
222 NativePhysicalCopyPayloadToState
223 (modelWord64FromNaturalTruncated
224 (naturalAdd
225 (publicationBase applicationBytes ordinaryCapacity reservedCapacity)
226 relative))
227 (modelWord64FromNaturalTruncated (bytes-length payload))
228 payload)
229 identity)))))))
230
231def publicationSealAndCommitCommandsForBody =
232 (lambda unrestricted applicationBytes : Nat .
233 (lambda unrestricted ordinaryCapacity : Nat .
234 (lambda unrestricted reservedCapacity : Nat .
235 (lambda unrestricted bodyBytes : Nat .
236 (lambda unrestricted sink : (family NativePhysicalOperand) .
237 (lambda unrestricted directory : (family NativePhysicalOperand) .
238 (lambda unrestricted resultSlot : Nat .
239 (lambda unrestricted identity : Bytes .
240 (lambda unrestricted tail : (family NativePhysicalCommands) .
241 (nativeLaunchRecipeCommand
242 (constructor
243 NativePhysicalOperation
244 NativePhysicalRepeatBeginCounted
245 (publicationStateLoad
246 applicationBytes
247 ordinaryCapacity
248 reservedCapacity
249 publicationReadyAt))
250 identity
251 (nativeLaunchRecipeCommand
252 (constructor
253 NativePhysicalOperation
254 NativePhysicalMachineRoutine
255 nativeTelemetrySealRoutine
256 (constructor
257 NativePhysicalArguments
258 NativePhysicalArgumentsValue
259 (publicationStateAddress
260 applicationBytes
261 ordinaryCapacity
262 reservedCapacity
263 publicationBodyAt)
264 (publicationStateLoad
265 applicationBytes
266 ordinaryCapacity
267 reservedCapacity
268 publicationBlockCountAt)
269 (publicationStateAddress
270 applicationBytes
271 ordinaryCapacity
272 reservedCapacity
273 (publicationRecordAtForBody bodyBytes))
274 (publicationStateLoad
275 applicationBytes
276 ordinaryCapacity
277 reservedCapacity
278 publicationBodyLengthAt)
279 (publicationStateAddress
280 applicationBytes
281 ordinaryCapacity
282 reservedCapacity
283 (publicationZeroClockAtForBody bodyBytes))
284 (publicationStateAddress
285 applicationBytes
286 ordinaryCapacity
287 reservedCapacity
288 (publicationSealWorkAtForBody bodyBytes)))
289 (constructor NativePhysicalResultBinding NativePhysicalDiscardResult))
290 identity
291 (nativeLaunchRecipeCommand
292 (constructor
293 NativePhysicalOperation
294 NativePhysicalMachineRoutine
295 nativeTelemetryPublicationCommitRoutine
296 (constructor
297 NativePhysicalArguments
298 NativePhysicalArgumentsValue
299 (constructor
300 NativePhysicalOperand
301 NativePhysicalStateAddress
302 (modelWord64FromNaturalTruncated
303 (captureControlAt applicationBytes)))
304 (publicationStateAddress
305 applicationBytes
306 ordinaryCapacity
307 reservedCapacity
308 0)
309 sink
310 (publicationStateAddress
311 applicationBytes
312 ordinaryCapacity
313 reservedCapacity
314 (publicationRecordAtForBody bodyBytes))
315 (publicationStateLoad
316 applicationBytes
317 ordinaryCapacity
318 reservedCapacity
319 publicationRecordLengthAt)
320 directory)
321 (nativeLaunchRecipeStore resultSlot))
322 identity
323 (nativeLaunchRecipeCommand
324 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
325 identity
326 tail)))))))))))))
327
328def publicationSealAndCommitCommands =
329 (lambda unrestricted applicationBytes : Nat .
330 (lambda unrestricted ordinaryCapacity : Nat .
331 (lambda unrestricted reservedCapacity : Nat .
332 (publicationSealAndCommitCommandsForBody
333 applicationBytes
334 ordinaryCapacity
335 reservedCapacity
336 (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity)))))
337
338def nativeTelemetryPublicationPrepareCommandsForBody =
339 (lambda unrestricted applicationBytes : Nat .
340 (lambda unrestricted ordinaryCapacity : Nat .
341 (lambda unrestricted reservedCapacity : Nat .
342 (lambda unrestricted bodyBytes : Nat .
343 (lambda unrestricted terminal : Nat .
344 (lambda unrestricted resultSlot : Nat .
345 (lambda unrestricted identity : Bytes .
346 (lambda unrestricted tail : (family NativePhysicalCommands) .
347 (publicationCopyPayload
348 applicationBytes
349 ordinaryCapacity
350 reservedCapacity
351 publicationBodyAt
352 publicationBodyPrefix
353 identity
354 (publicationCopyPayload
355 applicationBytes
356 ordinaryCapacity
357 reservedCapacity
358 (publicationRecordAtForBody bodyBytes)
359 nativeTelemetryMagic
360 identity
361 (publicationCopyPayload
362 applicationBytes
363 ordinaryCapacity
364 reservedCapacity
365 (publicationZeroClockAtForBody bodyBytes)
366 (dataBytesRepeatByte (byte 0) publicationZeroClockBytes)
367 identity
368 (nativeLaunchRecipeCommand
369 (constructor
370 NativePhysicalOperation
371 NativePhysicalStoreWord64
372 (publicationStateAddress
373 applicationBytes
374 ordinaryCapacity
375 reservedCapacity
376 publicationReadyAt)
377 (nativeLaunchRecipeImmediate 0))
378 identity
379 (nativeLaunchRecipeCommand
380 (constructor
381 NativePhysicalOperation
382 NativePhysicalStoreWord64
383 (publicationStateAddress
384 applicationBytes
385 ordinaryCapacity
386 reservedCapacity
387 publicationTerminalRequestAt)
388 (nativeLaunchRecipeImmediate terminal))
389 identity
390 (nativeLaunchRecipeCommand
391 (constructor
392 NativePhysicalOperation
393 NativePhysicalMachineRoutine
394 (aosChoose
395 Bytes
396 (naturalAnd
397 (naturalAnd
398 (publicationStorageCertificateForBody
399 applicationBytes
400 ordinaryCapacity
401 reservedCapacity
402 bodyBytes)
403 (naturalEqual
404 captureControlBytes
405 (bytes-length
406 (nativeTelemetryEncodeCounters publicationEmptyCounters))))
407 (naturalLessOrEqual terminal 1))
408 (nativeTelemetryPublicationPrepareRoutineForBody
409 ordinaryCapacity
410 reservedCapacity
411 bodyBytes)
412 b"")
413 (constructor
414 NativePhysicalArguments
415 NativePhysicalArgumentsValue
416 (constructor
417 NativePhysicalOperand
418 NativePhysicalStateAddress
419 (modelWord64FromNaturalTruncated
420 (captureControlAt applicationBytes)))
421 (constructor
422 NativePhysicalOperand
423 NativePhysicalStateAddress
424 (modelWord64FromNaturalTruncated
425 (captureQueueAt applicationBytes)))
426 (constructor
427 NativePhysicalOperand
428 NativePhysicalStateAddress
429 (modelWord64FromNaturalTruncated
430 (captureIdentityAt
431 applicationBytes
432 ordinaryCapacity
433 reservedCapacity)))
434 (publicationStateAddress
435 applicationBytes
436 ordinaryCapacity
437 reservedCapacity
438 0)
439 (nativeLaunchRecipeImmediate
440 (captureQueueBytes ordinaryCapacity reservedCapacity))
441 (nativeLaunchRecipeImmediate
442 (publicationArenaBytesForBody bodyBytes)))
443 (nativeLaunchRecipeStore resultSlot))
444 identity
445 tail))))))))))))))
446
447def nativeTelemetryPublicationCommandsForBody =
448 (lambda unrestricted applicationBytes : Nat .
449 (lambda unrestricted ordinaryCapacity : Nat .
450 (lambda unrestricted reservedCapacity : Nat .
451 (lambda unrestricted bodyBytes : Nat .
452 (lambda unrestricted terminal : Nat .
453 (lambda unrestricted sink : (family NativePhysicalOperand) .
454 (lambda unrestricted directory : (family NativePhysicalOperand) .
455 (lambda unrestricted resultSlot : Nat .
456 (lambda unrestricted identity : Bytes .
457 (lambda unrestricted tail : (family NativePhysicalCommands) .
458 (nativeTelemetryPublicationPrepareCommandsForBody
459 applicationBytes
460 ordinaryCapacity
461 reservedCapacity
462 bodyBytes
463 terminal
464 resultSlot
465 identity
466 (publicationSealAndCommitCommandsForBody
467 applicationBytes
468 ordinaryCapacity
469 reservedCapacity
470 bodyBytes
471 sink
472 directory
473 resultSlot
474 identity
475 tail))))))))))))
476
477def nativeTelemetryPublicationCommands =
478 (lambda unrestricted applicationBytes : Nat .
479 (lambda unrestricted ordinaryCapacity : Nat .
480 (lambda unrestricted reservedCapacity : Nat .
481 (nativeTelemetryPublicationCommandsForBody
482 applicationBytes
483 ordinaryCapacity
484 reservedCapacity
485 (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity)))))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.