Runtime.NativeTelemetryCapture

1module Runtime.NativeTelemetryCapture
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Model.Word64
6import Runtime.NativeLaunchRecipeLoad
7import Runtime.NativePhysicalProgram
8import Observe.Value
9import Runtime.TelemetryCapture
10import Runtime.TelemetryCaptureRoutine
11import Std.Natural
12
13-- System V: control, queue, eight values, selected, reserved, queue extent.
14-- Single producer, no concurrent drain. All acquisition uses caller-saved
15-- registers and performs no syscall, hashing, formatting, or allocation.
16-- Control policy is immutable to the application by the arena certificate.
17-- A pending return leaves the queue/control unchanged. The caller must retain
18-- the pending values and choose retry/pause/failure at its declared boundary;
19-- this acquisition primitive cannot silently change application semantics.
20-- Extent and overflow checks precede mutations. Return codes match
21-- Observe.Capture; a queued return never claims persistence.
22def captureRAX =
23  (constructor X86NativeRegister64 X86NativeRAX)
24
25def captureRCX =
26  (constructor X86NativeRegister64 X86NativeRCX)
27
28def captureRDX =
29  (constructor X86NativeRegister64 X86NativeRDX)
30
31def captureRSI =
32  (constructor X86NativeRegister64 X86NativeRSI)
33
34def captureRDI =
35  (constructor X86NativeRegister64 X86NativeRDI)
36
37def captureR8 =
38  (constructor X86NativeRegister64 X86NativeR8)
39
40def captureR9 =
41  (constructor X86NativeRegister64 X86NativeR9)
42
43def captureR10 =
44  (constructor X86NativeRegister64 X86NativeR10)
45
46def captureR11 =
47  (constructor X86NativeRegister64 X86NativeR11)
48
49def captureEmit =
50  (lambda unrestricted instruction : (family X86NativeInstruction) .
51    (lambda unrestricted tail : (family X86NativeAssembly) .
52      (constructor X86NativeAssembly X86NativeAssemblyEmit instruction tail)))
53
54def captureLabel =
55  (lambda unrestricted name : Bytes .
56    (lambda unrestricted tail : (family X86NativeAssembly) .
57      (constructor X86NativeAssembly X86NativeAssemblyLabel name tail)))
58
59def captureJump =
60  (lambda unrestricted name : Bytes .
61    (lambda unrestricted tail : (family X86NativeAssembly) .
62      (constructor X86NativeAssembly X86NativeAssemblyJump name tail)))
63
64def captureJumpIf =
65  (lambda unrestricted condition : (family X86NativeCondition) .
66    (lambda unrestricted name : Bytes .
67      (lambda unrestricted tail : (family X86NativeAssembly) .
68        (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition name tail))))
69
70def captureLoad =
71  (lambda unrestricted destination : (family X86NativeRegister64) .
72    (lambda unrestricted base : (family X86NativeRegister64) .
73      (lambda unrestricted offset : Nat .
74        (captureEmit
75          (constructor
76            X86NativeInstruction
77            X86NativeLoadMemory64
78            destination
79            base
80            (x86NativeDisplacement32FromNatural offset))))))
81
82def captureStore =
83  (lambda unrestricted base : (family X86NativeRegister64) .
84    (lambda unrestricted offset : Nat .
85      (lambda unrestricted source : (family X86NativeRegister64) .
86        (captureEmit
87          (constructor
88            X86NativeInstruction
89            X86NativeStoreMemory64
90            base
91            (x86NativeDisplacement32FromNatural offset)
92            source)))))
93
94def captureMove =
95  (lambda unrestricted destination : (family X86NativeRegister64) .
96    (lambda unrestricted source : (family X86NativeRegister64) .
97      (captureEmit (constructor X86NativeInstruction X86NativeMoveRegister64 source destination))))
98
99def captureAdd =
100  (lambda unrestricted destination : (family X86NativeRegister64) .
101    (lambda unrestricted source : (family X86NativeRegister64) .
102      (captureEmit (constructor X86NativeInstruction X86NativeAddRegister64 source destination))))
103
104def captureCompare =
105  (lambda unrestricted left : (family X86NativeRegister64) .
106    (lambda unrestricted right : (family X86NativeRegister64) .
107      (captureEmit (constructor X86NativeInstruction X86NativeCompareRegister64 right left))))
108
109def captureCompareImmediate =
110  (lambda unrestricted register : (family X86NativeRegister64) .
111    (lambda unrestricted value : Nat .
112      (captureEmit
113        (constructor
114          X86NativeInstruction
115          X86NativeCompareImmediate64
116          register
117          (x86NativeImmediate32FromNatural value)))))
118
119def captureSet =
120  (lambda unrestricted register : (family X86NativeRegister64) .
121    (lambda unrestricted value : Nat .
122      (captureEmit
123        (constructor
124          X86NativeInstruction
125          X86NativeMoveImmediate32
126          register
127          (x86NativeImmediate32FromNatural value)))))
128
129def captureIncrement =
130  (lambda unrestricted register : (family X86NativeRegister64) .
131    (captureEmit
132      (constructor
133        X86NativeInstruction
134        X86NativeAddImmediate64
135        register
136        (x86NativeImmediate32FromNatural 1))))
137
138def captureReturnCode =
139  (lambda unrestricted code : Nat .
140    (lambda unrestricted tail : (family X86NativeAssembly) .
141      (captureSet
142        captureRAX
143        code
144        (captureEmit (constructor X86NativeInstruction X86NativeReturn) tail))))
145
146-- CMP r64, imm32 sign-extends all ones to the unsigned 64-bit maximum.
147-- This is an ISA encoding operand, not a pasted application quantity.
148def captureMaximumCounterImmediate : Nat =
149  0xffffffff
150
151def captureCompareMaximum =
152  (lambda unrestricted register : (family X86NativeRegister64) .
153    (captureCompareImmediate register captureMaximumCounterImmediate))
154
155def captureScale =
156  (lambda unrestricted register : (family X86NativeRegister64) .
157    (lambda unrestricted stride : Nat .
158      (captureEmit
159        (constructor
160          X86NativeInstruction
161          X86NativeMultiplyImmediate64
162          register
163          (x86NativeImmediate32FromNatural stride)))))
164
165def captureProduct =
166  (captureEmit (constructor X86NativeInstruction X86NativeMultiplyRegister64Unsigned captureR10))
167
168def captureBackendJumpIf =
169  (lambda unrestricted condition : (family TelemetryCaptureCondition) .
170    (captureJumpIf
171      (eliminate
172        TelemetryCaptureCondition
173        (lambda unrestricted current : (family TelemetryCaptureCondition) .
174          (family X86NativeCondition))
175        condition
176        (branch TelemetryCaptureZero . (constructor X86NativeCondition X86NativeConditionZero))
177        (branch
178          TelemetryCaptureNotZero
179          .
180          (constructor X86NativeCondition X86NativeConditionNotZero))
181        (branch TelemetryCaptureBelow . (constructor X86NativeCondition X86NativeConditionBelow))
182        (branch TelemetryCaptureAbove . (constructor X86NativeCondition X86NativeConditionAbove)))))
183
184def captureX86Backend =
185  (constructor
186    TelemetryCaptureBackend
187    TelemetryCaptureBackendValue
188    (family X86NativeAssembly)
189    (family X86NativeRegister64)
190    captureLoad
191    captureStore
192    captureMove
193    captureAdd
194    captureCompare
195    captureCompareImmediate
196    captureCompareMaximum
197    captureSet
198    captureIncrement
199    captureScale
200    captureProduct
201    captureReturnCode
202    captureLabel
203    captureJump
204    captureBackendJumpIf
205    (constructor X86NativeAssembly X86NativeAssemblyEnd)
206    captureRAX
207    captureRCX
208    captureRDX
209    captureRSI
210    captureRDI
211    captureR8
212    captureR9
213    captureR10
214    captureR11)
215
216def captureAssemblyPart0 =
217  (telemetryCaptureAssemblyFor
218    (family X86NativeAssembly)
219    (family X86NativeRegister64)
220    captureX86Backend)
221
222def nativeTelemetryCaptureRoutine : Bytes =
223  (eliminate
224    X86NativeAssemblyResult
225    (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
226    (x86NativeAssemble captureAssemblyPart0)
227    (branch X86NativeAssemblyEncoded code . code)
228    (branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
229    (branch X86NativeAssemblyEncodeOffsetOverflow . b"")
230    (branch X86NativeAssemblyMissingLabel name . b"")
231    (branch X86NativeAssemblyDisplacementOutOfRange name . b""))
232
233-- This constructor binds every pointer/extent to the same certified plan.
234-- Invalid placements lower to an unavailable routine and fail artifact build;
235-- unsupported host targets must refuse this x86 realization, never copy it.
236def nativeTelemetryCaptureSelectedCommand =
237  (lambda unrestricted applicationBytes : Nat .
238    (lambda unrestricted ordinaryCapacity : Nat .
239      (lambda unrestricted reservedCapacity : Nat .
240        (lambda unrestricted selected : (family NativePhysicalOperand) .
241          (lambda unrestricted reserved : Nat .
242            (lambda unrestricted resultSlot : Nat .
243              (lambda unrestricted identity : Bytes .
244                (lambda unrestricted tail : (family NativePhysicalCommands) .
245                  (nativeLaunchRecipeCommand
246                    (constructor
247                      NativePhysicalOperation
248                      NativePhysicalMachineRoutine
249                      (aosChoose
250                        Bytes
251                        (captureArenaCertificate applicationBytes ordinaryCapacity reservedCapacity)
252                        nativeTelemetryCaptureRoutine
253                        b"")
254                      (constructor
255                        NativePhysicalArguments
256                        NativePhysicalArgumentsValue
257                        (constructor
258                          NativePhysicalOperand
259                          NativePhysicalStateAddress
260                          (modelWord64FromNaturalTruncated (captureControlAt applicationBytes)))
261                        (constructor
262                          NativePhysicalOperand
263                          NativePhysicalStateAddress
264                          (modelWord64FromNaturalTruncated (captureQueueAt applicationBytes)))
265                        (constructor
266                          NativePhysicalOperand
267                          NativePhysicalStateAddress
268                          (modelWord64FromNaturalTruncated
269                            (captureValuesScratchAt
270                              applicationBytes
271                              ordinaryCapacity
272                              reservedCapacity)))
273                        selected
274                        (nativeLaunchRecipeImmediate reserved)
275                        (nativeLaunchRecipeImmediate
276                          (captureQueueBytes ordinaryCapacity reservedCapacity)))
277                      (nativeLaunchRecipeStore resultSlot))
278                    identity
279                    tail)))))))))
280
281def nativeTelemetryCaptureCommand =
282  (lambda unrestricted applicationBytes : Nat .
283    (lambda unrestricted ordinaryCapacity : Nat .
284      (lambda unrestricted reservedCapacity : Nat .
285        (lambda unrestricted selected : Nat .
286          (nativeTelemetryCaptureSelectedCommand
287            applicationBytes
288            ordinaryCapacity
289            reservedCapacity
290            (nativeLaunchRecipeImmediate selected))))))