1module Runtime.NativeTelemetryIdentity
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Model.Word64
6import Observe.Value
7import Runtime.NativeLaunchRecipeLoad
8import Runtime.NativePhysicalProgram
9import Runtime.TelemetryCapture
10import Runtime.TelemetryIdentity
11import Runtime.TelemetryIdentityRoutine
12import Std.Natural
13
14family NativeTelemetryIdentitySource : Type 0
15constructor NativeTelemetryFreshIdentity
16constructor NativeTelemetryAssignedFile
17field unrestricted nativeTelemetryAssignedPath : (family NativePhysicalOperand)
18
19end-family
20
21def nativeTelemetryIdentitySourceAdmission =
22 (lambda unrestricted applicationBytes : Nat .
23 (lambda unrestricted applicationSlots : Nat .
24 (lambda unrestricted source : (family NativeTelemetryIdentitySource) .
25 (eliminate
26 NativeTelemetryIdentitySource
27 (lambda unrestricted current : (family NativeTelemetryIdentitySource) . Nat)
28 source
29 (branch NativeTelemetryFreshIdentity . 1)
30 (branch NativeTelemetryAssignedFile path .
31 -- Initialization precedes application steps. Only an incoming argv
32 -- path exists at this point; application state/results are future
33 -- values and may not be read as an already-initialized pathname.
34 (eliminate
35 NativePhysicalOperand
36 (lambda unrestricted current : (family NativePhysicalOperand) . Nat)
37 path
38 (branch NativePhysicalImmediate value . 0)
39 (branch NativePhysicalResultValue slot . 0)
40 (branch NativePhysicalResultAddress slot offset . 0)
41 (branch NativePhysicalStateAddress offset . 0)
42 (branch NativePhysicalStateLoad64 offset . 0)
43 (branch NativePhysicalPayloadAddress offset . 0)
44 (branch NativePhysicalPayloadLoad64 offset . 0)
45 (branch NativePhysicalProcessArgument index . 1)
46 (branch NativePhysicalLoopAffine base stride . 0)))))))
47
48-- Linux x86-64 System V: RDI destination, RSI byte extent, RDX contract
49-- version. Only caller-saved registers are used. Initialize once at process
50-- birth, before the first event; rotating a spool must not call this again.
51--
52-- One getrandom(GRND_NONBLOCK) call; failure, interruption, short reads or
53-- zero identities refuse publication. No PID, timestamp, deterministic seed
54-- or userspace fallback supplies an identity. Failed entropy may have touched
55-- destination bytes: they have no authority unless the result is zero.
56-- https://man7.org/linux/man-pages/man2/getrandom.2.html
57-- Syscall 318: Linux arch/x86/entry/syscalls/syscall_64.tbl, verified against
58-- /usr/include/x86_64-linux-gnu/asm/unistd_64.h. Other targets must lower their
59-- own entropy acquisition. Both emitters specialize TelemetryIdentityRoutine.
60def identityRAX =
61 (constructor X86NativeRegister64 X86NativeRAX)
62
63def identityRCX =
64 (constructor X86NativeRegister64 X86NativeRCX)
65
66def identityRDX =
67 (constructor X86NativeRegister64 X86NativeRDX)
68
69def identityRSI =
70 (constructor X86NativeRegister64 X86NativeRSI)
71
72def identityRDI =
73 (constructor X86NativeRegister64 X86NativeRDI)
74
75def identityR8 =
76 (constructor X86NativeRegister64 X86NativeR8)
77
78def identityEmit =
79 (lambda unrestricted instruction : (family X86NativeInstruction) .
80 (lambda unrestricted tail : (family X86NativeAssembly) .
81 (constructor X86NativeAssembly X86NativeAssemblyEmit instruction tail)))
82
83def identityLabel =
84 (lambda unrestricted name : Bytes .
85 (lambda unrestricted tail : (family X86NativeAssembly) .
86 (constructor X86NativeAssembly X86NativeAssemblyLabel name tail)))
87
88def identityJumpIf =
89 (lambda unrestricted condition : (family X86NativeCondition) .
90 (lambda unrestricted name : Bytes .
91 (lambda unrestricted tail : (family X86NativeAssembly) .
92 (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition name tail))))
93
94def identitySet =
95 (lambda unrestricted register : (family X86NativeRegister64) .
96 (lambda unrestricted value : Nat .
97 (identityEmit
98 (constructor
99 X86NativeInstruction
100 X86NativeMoveImmediate32
101 register
102 (x86NativeImmediate32FromNatural value)))))
103
104def identityCompare =
105 (lambda unrestricted register : (family X86NativeRegister64) .
106 (lambda unrestricted value : Nat .
107 (identityEmit
108 (constructor
109 X86NativeInstruction
110 X86NativeCompareImmediate64
111 register
112 (x86NativeImmediate32FromNatural value)))))
113
114def identityReturn =
115 (lambda unrestricted code : Nat .
116 (lambda unrestricted tail : (family X86NativeAssembly) .
117 (identitySet
118 identityRAX
119 code
120 (identityEmit (constructor X86NativeInstruction X86NativeReturn) tail))))
121
122def identityLoad =
123 (lambda unrestricted register : (family X86NativeRegister64) .
124 (lambda unrestricted offset : Nat .
125 (identityEmit
126 (constructor
127 X86NativeInstruction
128 X86NativeLoadMemory64
129 register
130 identityRDI
131 (x86NativeDisplacement32FromNatural offset)))))
132
133def identityMove =
134 (lambda unrestricted destination : (family X86NativeRegister64) .
135 (lambda unrestricted source : (family X86NativeRegister64) .
136 (identityEmit (constructor X86NativeInstruction X86NativeMoveRegister64 source destination))))
137
138def identityOr =
139 (lambda unrestricted destination : (family X86NativeRegister64) .
140 (lambda unrestricted source : (family X86NativeRegister64) .
141 (identityEmit (constructor X86NativeInstruction X86NativeOrRegister64 source destination))))
142
143def identityAddImmediate =
144 (lambda unrestricted destination : (family X86NativeRegister64) .
145 (lambda unrestricted value : Nat .
146 (identityEmit
147 (constructor
148 X86NativeInstruction
149 X86NativeAddImmediate64
150 destination
151 (x86NativeImmediate32FromNatural value)))))
152
153def identityAcquireEntropy =
154 (lambda unrestricted tail : (family X86NativeAssembly) .
155 (identitySet
156 identityRAX
157 318
158 (identityEmit (constructor X86NativeInstruction X86NativeSystemCall) tail)))
159
160def identityBackendJumpIf =
161 (lambda unrestricted condition : (family TelemetryIdentityCondition) .
162 (identityJumpIf
163 (eliminate
164 TelemetryIdentityCondition
165 (lambda unrestricted current : (family TelemetryIdentityCondition) .
166 (family X86NativeCondition))
167 condition
168 (branch TelemetryIdentityZero . (constructor X86NativeCondition X86NativeConditionZero))
169 (branch
170 TelemetryIdentityNotZero
171 .
172 (constructor X86NativeCondition X86NativeConditionNotZero))
173 (branch TelemetryIdentityBelow . (constructor X86NativeCondition X86NativeConditionBelow)))))
174
175def identityX86Backend =
176 (constructor
177 TelemetryIdentityBackend
178 TelemetryIdentityBackendValue
179 (family X86NativeAssembly)
180 (family X86NativeRegister64)
181 identityLoad
182 identityOr
183 identityCompare
184 identityMove
185 identitySet
186 identityAddImmediate
187 identityReturn
188 identityLabel
189 identityBackendJumpIf
190 identityAcquireEntropy
191 (constructor X86NativeAssembly X86NativeAssemblyEnd)
192 identityRAX
193 identityRCX
194 identityRDX
195 identityRSI
196 identityRDI
197 identityR8)
198
199def identityValidateAssembly =
200 (telemetryIdentityAssemblyFor
201 (family X86NativeAssembly)
202 (family X86NativeRegister64)
203 identityX86Backend
204 (constructor TelemetryIdentityRoutineKind TelemetryIdentityValidate))
205
206def identityReceiptAssembly =
207 (telemetryIdentityAssemblyFor
208 (family X86NativeAssembly)
209 (family X86NativeRegister64)
210 identityX86Backend
211 (constructor TelemetryIdentityRoutineKind TelemetryIdentityReceipt))
212
213def identityCreateAssembly =
214 (telemetryIdentityAssemblyFor
215 (family X86NativeAssembly)
216 (family X86NativeRegister64)
217 identityX86Backend
218 (constructor TelemetryIdentityRoutineKind TelemetryIdentityCreate))
219
220def identityEpochAssembly =
221 (telemetryIdentityAssemblyFor
222 (family X86NativeAssembly)
223 (family X86NativeRegister64)
224 identityX86Backend
225 (constructor TelemetryIdentityRoutineKind TelemetryIdentityRenewEpoch))
226
227def identityAssemble =
228 (lambda unrestricted assembly : (family X86NativeAssembly) .
229 (eliminate
230 X86NativeAssemblyResult
231 (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
232 (x86NativeAssemble assembly)
233 (branch X86NativeAssemblyEncoded code . code)
234 (branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
235 (branch X86NativeAssemblyEncodeOffsetOverflow . b"")
236 (branch X86NativeAssemblyMissingLabel name . b"")
237 (branch X86NativeAssemblyDisplacementOutOfRange name . b"")))
238
239def nativeTelemetryIdentityRoutine : Bytes =
240 (identityAssemble identityCreateAssembly)
241
242def nativeTelemetryEpochRoutine : Bytes =
243 (identityAssemble identityEpochAssembly)
244
245-- Validation is independently reusable for a journal's decoded binary IDs;
246-- it does not establish entropy provenance or authorize process-ID reuse.
247def nativeTelemetryIdentityValidateRoutine : Bytes =
248 (identityAssemble identityValidateAssembly)
249
250def nativeTelemetryIdentityReceiptRoutine : Bytes =
251 (identityAssemble identityReceiptAssembly)
252
253def nativeTelemetryIdentityCommandFor =
254 (lambda unrestricted routine : Bytes .
255 (lambda unrestricted applicationBytes : Nat .
256 (lambda unrestricted ordinaryCapacity : Nat .
257 (lambda unrestricted reservedCapacity : Nat .
258 (lambda unrestricted resultSlot : Nat .
259 (lambda unrestricted identity : Bytes .
260 (lambda unrestricted tail : (family NativePhysicalCommands) .
261 (nativeLaunchRecipeCommand
262 (constructor
263 NativePhysicalOperation
264 NativePhysicalMachineRoutine
265 (aosChoose
266 Bytes
267 (captureWithIdentityArenaCertificate
268 applicationBytes
269 ordinaryCapacity
270 reservedCapacity)
271 routine
272 b"")
273 (nativeLaunchRecipeArguments
274 (constructor
275 NativePhysicalOperand
276 NativePhysicalStateAddress
277 (modelWord64FromNaturalTruncated
278 (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity)))
279 (nativeLaunchRecipeImmediate telemetryIdentitySetBytes)
280 (nativeLaunchRecipeImmediate 1)
281 (nativeLaunchRecipeImmediate 0))
282 (nativeLaunchRecipeStore resultSlot))
283 identity
284 tail))))))))
285
286def nativeTelemetryIdentityCommand =
287 (nativeTelemetryIdentityCommandFor nativeTelemetryIdentityRoutine)
288
289def nativeTelemetryEpochCommand =
290 (nativeTelemetryIdentityCommandFor nativeTelemetryEpochRoutine)
291
292-- Read an assigned run/attempt/producer from a caller-owned descriptor at its
293-- current position. The descriptor remains caller-owned. Exactly one bounded
294-- read of the binding and one EOF probe are permitted: short/error/extended
295-- inputs fail by name, without an entropy retry or a fresh-identity fallback.
296-- The EOF probe uses the first byte of the as-yet-uninitialized epoch region;
297-- epoch renewal overwrites that region only after framing and nonzero assigned
298-- role validation succeed. No application address is used as identity storage.
299def nativeTelemetryReadAssignedIdentity =
300 (lambda unrestricted applicationBytes : Nat .
301 (lambda unrestricted ordinaryCapacity : Nat .
302 (lambda unrestricted reservedCapacity : Nat .
303 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
304 (lambda unrestricted resultSlot : Nat .
305 (lambda unrestricted identity : Bytes .
306 (lambda unrestricted tail : (family NativePhysicalCommands) .
307 (let unrestricted identityAt =
308 (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity)
309 in
310 (let unrestricted readBinding =
311 (nativeLaunchRecipeCommand
312 (constructor
313 NativePhysicalOperation
314 NativePhysicalSystemCall
315 (nativeLaunchRecipeImmediate 0)
316 (nativeLaunchRecipeArguments
317 descriptor
318 (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated identityAt))
319 (nativeLaunchRecipeImmediate telemetryIdentityBindingBytes)
320 (nativeLaunchRecipeImmediate 0))
321 b""
322 (nativeLaunchRecipeStore resultSlot))
323 identity
324 (nativeLaunchRecipeAssertEqual
325 (nativeLaunchRecipeSlotValue resultSlot)
326 (nativeLaunchRecipeImmediate telemetryIdentityBindingBytes)
327 b"telemetry:identity-binding-read"
328 (nativeLaunchRecipeCommand
329 (constructor
330 NativePhysicalOperation
331 NativePhysicalSystemCall
332 (nativeLaunchRecipeImmediate 0)
333 (nativeLaunchRecipeArguments
334 descriptor
335 (constructor
336 NativePhysicalOperand
337 NativePhysicalStateAddress
338 (modelWord64FromNaturalTruncated
339 (naturalAdd identityAt telemetryIdentityBindingBytes)))
340 (nativeLaunchRecipeImmediate 1)
341 (nativeLaunchRecipeImmediate 0))
342 b""
343 (nativeLaunchRecipeStore resultSlot))
344 identity
345 (nativeLaunchRecipeAssertEqual
346 (nativeLaunchRecipeSlotValue resultSlot)
347 (nativeLaunchRecipeImmediate 0)
348 b"telemetry:identity-binding-trailing"
349 (nativeTelemetryEpochCommand
350 applicationBytes ordinaryCapacity reservedCapacity resultSlot identity tail)))))
351 in
352 (aosChoose
353 (family NativePhysicalCommands)
354 (captureWithIdentityArenaCertificate applicationBytes ordinaryCapacity reservedCapacity)
355 readBinding
356 (nativeTelemetryIdentityCommandFor
357 b"" applicationBytes ordinaryCapacity reservedCapacity resultSlot identity tail)))))))))))
358
359-- Source-policy initialization owns this temporary descriptor. CLOEXEC,
360-- NOFOLLOW and NONBLOCK keep the admitted file read bounded and prevent a
361-- symlink from replacing the assignment. AArch64 translates NOFOLLOW through
362-- its existing host syscall adapter. Errors stop before any journal is opened.
363def nativeTelemetryInitializeIdentityFrom =
364 (lambda unrestricted source : (family NativeTelemetryIdentitySource) .
365 (lambda unrestricted descriptorSlot : Nat .
366 (lambda unrestricted applicationBytes : Nat .
367 (lambda unrestricted ordinaryCapacity : Nat .
368 (lambda unrestricted reservedCapacity : Nat .
369 (lambda unrestricted resultSlot : Nat .
370 (lambda unrestricted identity : Bytes .
371 (lambda unrestricted tail : (family NativePhysicalCommands) .
372 (eliminate
373 NativeTelemetryIdentitySource
374 (lambda unrestricted current : (family NativeTelemetryIdentitySource) . (family NativePhysicalCommands))
375 source
376 (branch NativeTelemetryFreshIdentity .
377 (nativeTelemetryIdentityCommand applicationBytes ordinaryCapacity reservedCapacity resultSlot identity tail))
378 (branch NativeTelemetryAssignedFile path .
379 (aosChoose
380 (family NativePhysicalCommands)
381 (naturalIsZero (naturalEqual descriptorSlot resultSlot))
382 (nativeLaunchRecipeCommand
383 (constructor
384 NativePhysicalOperation NativePhysicalSystemCall
385 (nativeLaunchRecipeImmediate 257)
386 (nativeLaunchRecipeArguments
387 (nativeLaunchRecipeImmediate 18446744073709551516)
388 path
389 (nativeLaunchRecipeImmediate
390 (naturalAdd (naturalPowerOfTwo 19) (naturalAdd (naturalPowerOfTwo 17) (naturalPowerOfTwo 11))))
391 (nativeLaunchRecipeImmediate 0))
392 b"" (nativeLaunchRecipeStore descriptorSlot))
393 identity
394 (nativeTelemetryReadAssignedIdentity
395 applicationBytes ordinaryCapacity reservedCapacity
396 (nativeLaunchRecipeSlotValue descriptorSlot) resultSlot identity
397 (nativeLaunchRecipeAssertEqual
398 (nativeLaunchRecipeSlotValue resultSlot) (nativeLaunchRecipeImmediate 0)
399 b"telemetry:identity-binding-invalid"
400 (nativeLaunchRecipeCommand
401 (constructor
402 NativePhysicalOperation NativePhysicalSystemCall
403 (nativeLaunchRecipeImmediate 3)
404 (nativeLaunchRecipeArguments
405 (nativeLaunchRecipeSlotValue descriptorSlot)
406 (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0))
407 b"" (nativeLaunchRecipeStore resultSlot))
408 identity
409 (nativeLaunchRecipeAssertEqual
410 (nativeLaunchRecipeSlotValue resultSlot) (nativeLaunchRecipeImmediate 0)
411 b"telemetry:identity-binding-close" tail)))))
412 (nativeTelemetryIdentityCommandFor b"" applicationBytes ordinaryCapacity reservedCapacity resultSlot identity 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.