Read an assigned run/attempt/producer from a caller-owned descriptor at its
current position. The descriptor remains caller-owned. Exactly one bounded
read of the binding and one EOF probe are permitted: short/error/extended
inputs fail by name, without an entropy retry or a fresh-identity fallback.
The EOF probe uses the first byte of the as-yet-uninitialized epoch region;
epoch renewal overwrites that region only after framing and nonzero assigned
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)))))))))))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.