module Runtime.NativeTelemetryIdentity import Compiler.MachineX86Native import Compiler.MachineX86NativeAssembly import Model.Word64 import Observe.Value import Runtime.NativeLaunchRecipeLoad import Runtime.NativePhysicalProgram import Runtime.TelemetryCapture import Runtime.TelemetryIdentity import Runtime.TelemetryIdentityRoutine import Std.Natural family NativeTelemetryIdentitySource : Type 0 constructor NativeTelemetryFreshIdentity constructor NativeTelemetryAssignedFile field unrestricted nativeTelemetryAssignedPath : (family NativePhysicalOperand) end-family def nativeTelemetryIdentitySourceAdmission = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted applicationSlots : Nat . (lambda unrestricted source : (family NativeTelemetryIdentitySource) . (eliminate NativeTelemetryIdentitySource (lambda unrestricted current : (family NativeTelemetryIdentitySource) . Nat) source (branch NativeTelemetryFreshIdentity . 1) (branch NativeTelemetryAssignedFile path . -- Initialization precedes application steps. Only an incoming argv -- path exists at this point; application state/results are future -- values and may not be read as an already-initialized pathname. (eliminate NativePhysicalOperand (lambda unrestricted current : (family NativePhysicalOperand) . Nat) path (branch NativePhysicalImmediate value . 0) (branch NativePhysicalResultValue slot . 0) (branch NativePhysicalResultAddress slot offset . 0) (branch NativePhysicalStateAddress offset . 0) (branch NativePhysicalStateLoad64 offset . 0) (branch NativePhysicalPayloadAddress offset . 0) (branch NativePhysicalPayloadLoad64 offset . 0) (branch NativePhysicalProcessArgument index . 1) (branch NativePhysicalLoopAffine base stride . 0))))))) -- Linux x86-64 System V: RDI destination, RSI byte extent, RDX contract -- version. Only caller-saved registers are used. Initialize once at process -- birth, before the first event; rotating a spool must not call this again. -- -- One getrandom(GRND_NONBLOCK) call; failure, interruption, short reads or -- zero identities refuse publication. No PID, timestamp, deterministic seed -- or userspace fallback supplies an identity. Failed entropy may have touched -- destination bytes: they have no authority unless the result is zero. -- https://man7.org/linux/man-pages/man2/getrandom.2.html -- Syscall 318: Linux arch/x86/entry/syscalls/syscall_64.tbl, verified against -- /usr/include/x86_64-linux-gnu/asm/unistd_64.h. Other targets must lower their -- own entropy acquisition. Both emitters specialize TelemetryIdentityRoutine. def identityRAX = (constructor X86NativeRegister64 X86NativeRAX) def identityRCX = (constructor X86NativeRegister64 X86NativeRCX) def identityRDX = (constructor X86NativeRegister64 X86NativeRDX) def identityRSI = (constructor X86NativeRegister64 X86NativeRSI) def identityRDI = (constructor X86NativeRegister64 X86NativeRDI) def identityR8 = (constructor X86NativeRegister64 X86NativeR8) def identityEmit = (lambda unrestricted instruction : (family X86NativeInstruction) . (lambda unrestricted tail : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyEmit instruction tail))) def identityLabel = (lambda unrestricted name : Bytes . (lambda unrestricted tail : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyLabel name tail))) def identityJumpIf = (lambda unrestricted condition : (family X86NativeCondition) . (lambda unrestricted name : Bytes . (lambda unrestricted tail : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition name tail)))) def identitySet = (lambda unrestricted register : (family X86NativeRegister64) . (lambda unrestricted value : Nat . (identityEmit (constructor X86NativeInstruction X86NativeMoveImmediate32 register (x86NativeImmediate32FromNatural value))))) def identityCompare = (lambda unrestricted register : (family X86NativeRegister64) . (lambda unrestricted value : Nat . (identityEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 register (x86NativeImmediate32FromNatural value))))) def identityReturn = (lambda unrestricted code : Nat . (lambda unrestricted tail : (family X86NativeAssembly) . (identitySet identityRAX code (identityEmit (constructor X86NativeInstruction X86NativeReturn) tail)))) def identityLoad = (lambda unrestricted register : (family X86NativeRegister64) . (lambda unrestricted offset : Nat . (identityEmit (constructor X86NativeInstruction X86NativeLoadMemory64 register identityRDI (x86NativeDisplacement32FromNatural offset))))) def identityMove = (lambda unrestricted destination : (family X86NativeRegister64) . (lambda unrestricted source : (family X86NativeRegister64) . (identityEmit (constructor X86NativeInstruction X86NativeMoveRegister64 source destination)))) def identityOr = (lambda unrestricted destination : (family X86NativeRegister64) . (lambda unrestricted source : (family X86NativeRegister64) . (identityEmit (constructor X86NativeInstruction X86NativeOrRegister64 source destination)))) def identityAddImmediate = (lambda unrestricted destination : (family X86NativeRegister64) . (lambda unrestricted value : Nat . (identityEmit (constructor X86NativeInstruction X86NativeAddImmediate64 destination (x86NativeImmediate32FromNatural value))))) def identityAcquireEntropy = (lambda unrestricted tail : (family X86NativeAssembly) . (identitySet identityRAX 318 (identityEmit (constructor X86NativeInstruction X86NativeSystemCall) tail))) def identityBackendJumpIf = (lambda unrestricted condition : (family TelemetryIdentityCondition) . (identityJumpIf (eliminate TelemetryIdentityCondition (lambda unrestricted current : (family TelemetryIdentityCondition) . (family X86NativeCondition)) condition (branch TelemetryIdentityZero . (constructor X86NativeCondition X86NativeConditionZero)) (branch TelemetryIdentityNotZero . (constructor X86NativeCondition X86NativeConditionNotZero)) (branch TelemetryIdentityBelow . (constructor X86NativeCondition X86NativeConditionBelow))))) def identityX86Backend = (constructor TelemetryIdentityBackend TelemetryIdentityBackendValue (family X86NativeAssembly) (family X86NativeRegister64) identityLoad identityOr identityCompare identityMove identitySet identityAddImmediate identityReturn identityLabel identityBackendJumpIf identityAcquireEntropy (constructor X86NativeAssembly X86NativeAssemblyEnd) identityRAX identityRCX identityRDX identityRSI identityRDI identityR8) def identityValidateAssembly = (telemetryIdentityAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) identityX86Backend (constructor TelemetryIdentityRoutineKind TelemetryIdentityValidate)) def identityReceiptAssembly = (telemetryIdentityAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) identityX86Backend (constructor TelemetryIdentityRoutineKind TelemetryIdentityReceipt)) def identityCreateAssembly = (telemetryIdentityAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) identityX86Backend (constructor TelemetryIdentityRoutineKind TelemetryIdentityCreate)) def identityEpochAssembly = (telemetryIdentityAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) identityX86Backend (constructor TelemetryIdentityRoutineKind TelemetryIdentityRenewEpoch)) def identityAssemble = (lambda unrestricted assembly : (family X86NativeAssembly) . (eliminate X86NativeAssemblyResult (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes) (x86NativeAssemble assembly) (branch X86NativeAssemblyEncoded code . code) (branch X86NativeAssemblyEncodeDuplicateLabel name . b"") (branch X86NativeAssemblyEncodeOffsetOverflow . b"") (branch X86NativeAssemblyMissingLabel name . b"") (branch X86NativeAssemblyDisplacementOutOfRange name . b""))) def nativeTelemetryIdentityRoutine : Bytes = (identityAssemble identityCreateAssembly) def nativeTelemetryEpochRoutine : Bytes = (identityAssemble identityEpochAssembly) -- Validation is independently reusable for a journal's decoded binary IDs; -- it does not establish entropy provenance or authorize process-ID reuse. def nativeTelemetryIdentityValidateRoutine : Bytes = (identityAssemble identityValidateAssembly) def nativeTelemetryIdentityReceiptRoutine : Bytes = (identityAssemble identityReceiptAssembly) def nativeTelemetryIdentityCommandFor = (lambda unrestricted routine : Bytes . (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (aosChoose Bytes (captureWithIdentityArenaCertificate applicationBytes ordinaryCapacity reservedCapacity) routine b"") (nativeLaunchRecipeArguments (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity))) (nativeLaunchRecipeImmediate telemetryIdentitySetBytes) (nativeLaunchRecipeImmediate 1) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail)))))))) def nativeTelemetryIdentityCommand = (nativeTelemetryIdentityCommandFor nativeTelemetryIdentityRoutine) def nativeTelemetryEpochCommand = (nativeTelemetryIdentityCommandFor nativeTelemetryEpochRoutine) -- 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. def nativeTelemetryReadAssignedIdentity = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted descriptor : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted identityAt = (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity) in (let unrestricted readBinding = (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalSystemCall (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeArguments descriptor (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated identityAt)) (nativeLaunchRecipeImmediate telemetryIdentityBindingBytes) (nativeLaunchRecipeImmediate 0)) b"" (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue resultSlot) (nativeLaunchRecipeImmediate telemetryIdentityBindingBytes) b"telemetry:identity-binding-read" (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalSystemCall (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeArguments descriptor (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated (naturalAdd identityAt telemetryIdentityBindingBytes))) (nativeLaunchRecipeImmediate 1) (nativeLaunchRecipeImmediate 0)) b"" (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue resultSlot) (nativeLaunchRecipeImmediate 0) b"telemetry:identity-binding-trailing" (nativeTelemetryEpochCommand applicationBytes ordinaryCapacity reservedCapacity resultSlot identity tail))))) in (aosChoose (family NativePhysicalCommands) (captureWithIdentityArenaCertificate applicationBytes ordinaryCapacity reservedCapacity) readBinding (nativeTelemetryIdentityCommandFor b"" applicationBytes ordinaryCapacity reservedCapacity resultSlot identity tail))))))))))) -- Source-policy initialization owns this temporary descriptor. CLOEXEC, -- NOFOLLOW and NONBLOCK keep the admitted file read bounded and prevent a -- symlink from replacing the assignment. AArch64 translates NOFOLLOW through -- its existing host syscall adapter. Errors stop before any journal is opened. def nativeTelemetryInitializeIdentityFrom = (lambda unrestricted source : (family NativeTelemetryIdentitySource) . (lambda unrestricted descriptorSlot : Nat . (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NativeTelemetryIdentitySource (lambda unrestricted current : (family NativeTelemetryIdentitySource) . (family NativePhysicalCommands)) source (branch NativeTelemetryFreshIdentity . (nativeTelemetryIdentityCommand applicationBytes ordinaryCapacity reservedCapacity resultSlot identity tail)) (branch NativeTelemetryAssignedFile path . (aosChoose (family NativePhysicalCommands) (naturalIsZero (naturalEqual descriptorSlot resultSlot)) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalSystemCall (nativeLaunchRecipeImmediate 257) (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 18446744073709551516) path (nativeLaunchRecipeImmediate (naturalAdd (naturalPowerOfTwo 19) (naturalAdd (naturalPowerOfTwo 17) (naturalPowerOfTwo 11)))) (nativeLaunchRecipeImmediate 0)) b"" (nativeLaunchRecipeStore descriptorSlot)) identity (nativeTelemetryReadAssignedIdentity applicationBytes ordinaryCapacity reservedCapacity (nativeLaunchRecipeSlotValue descriptorSlot) resultSlot identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue resultSlot) (nativeLaunchRecipeImmediate 0) b"telemetry:identity-binding-invalid" (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalSystemCall (nativeLaunchRecipeImmediate 3) (nativeLaunchRecipeArguments (nativeLaunchRecipeSlotValue descriptorSlot) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) b"" (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue resultSlot) (nativeLaunchRecipeImmediate 0) b"telemetry:identity-binding-close" tail))))) (nativeTelemetryIdentityCommandFor b"" applicationBytes ordinaryCapacity reservedCapacity resultSlot identity tail))))))))))))