module Runtime.NativeTelemetrySeal import Compiler.MachineX86Native import Compiler.MachineX86NativeAssembly import Runtime.TelemetrySeal import Std.Foundation import Std.List import Std.Natural -- SEALING AN ALPHATEL RECORD AT RUN TIME (docs/observability PRD item 9). -- Runtime.NativeTelemetry encodes a record as "ALPHATEL", the body, then -- the SHA-256 of the body in 64 lowercase hex characters. A record whose -- body carries a clock reading can only be sealed where the reading is -- taken, so this routine does, in the executable, what the encoder does at -- build time for the rest of the body: -- -- rdi the body followed by its SHA-256 padding (0x80, zeros, the bit -- length), whole 64-byte blocks, in writable memory -- rsi the number of blocks -- rdx the record: "ALPHATEL" already at +0; the body is copied to +8 -- and the hex digest written after it -- rcx the body's length in bytes (nonzero) -- r8 a struct timespec (seconds, nanoseconds): its nanoseconds since -- the clock's epoch are written into the body at `sealMonotonicAt` -- first, so the digest covers them -- r9 a work area of `sealWorkBytes` bytes -- -- It keeps the System V callee-saved registers it uses in the work area -- (the instruction set has no push) and returns. Every 32-bit quantity is -- kept zero-extended in a 64-bit register and truncated by its 32-bit -- store; a rotation is a shift of the doubled word. The digest is checked -- against the build-time encoder's by reading a record the executable -- wrote (scripts/ci/observability.sh: `alpha observe import alphatel` -- verifies every record's digest). def sealImm32 = x86NativeImmediate32FromNatural def sealDisp = x86NativeDisplacement32FromNatural def sealImm8 = (lambda unrestricted n : Nat . (constructor X86NativeImmediate8 X86NativeImmediate8Value (nat-to-byte n))) def sealRAX = (constructor X86NativeRegister64 X86NativeRAX) def sealRBX = (constructor X86NativeRegister64 X86NativeRBX) def sealRCX = (constructor X86NativeRegister64 X86NativeRCX) def sealRDX = (constructor X86NativeRegister64 X86NativeRDX) def sealRSI = (constructor X86NativeRegister64 X86NativeRSI) def sealRDI = (constructor X86NativeRegister64 X86NativeRDI) def sealRBP = (constructor X86NativeRegister64 X86NativeRBP) def sealR8 = (constructor X86NativeRegister64 X86NativeR8) def sealR9 = (constructor X86NativeRegister64 X86NativeR9) def sealR10 = (constructor X86NativeRegister64 X86NativeR10) def sealR11 = (constructor X86NativeRegister64 X86NativeR11) def sealR12 = (constructor X86NativeRegister64 X86NativeR12) def sealR13 = (constructor X86NativeRegister64 X86NativeR13) def sealR14 = (constructor X86NativeRegister64 X86NativeR14) def sealR15 = (constructor X86NativeRegister64 X86NativeR15) def sealEmit = (lambda unrestricted instruction : (family X86NativeInstruction) . (lambda unrestricted rest : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyEmit instruction rest))) def sealLoad32 = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (sealEmit (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64 d base (sealDisp at)))))) def sealLoad64 = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (sealEmit (constructor X86NativeInstruction X86NativeLoadMemory64 d base (sealDisp at)))))) def sealLoad8 = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (sealEmit (constructor X86NativeInstruction X86NativeLoadMemory8ZeroExtend64 d base (sealDisp at)))))) def sealStore32 = (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (lambda unrestricted s : (family X86NativeRegister64) . (sealEmit (constructor X86NativeInstruction X86NativeStoreMemory32 base (sealDisp at) s))))) def sealStore64 = (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (lambda unrestricted s : (family X86NativeRegister64) . (sealEmit (constructor X86NativeInstruction X86NativeStoreMemory64 base (sealDisp at) s))))) def sealStore8 = (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (lambda unrestricted s : (family X86NativeRegister64) . (sealEmit (constructor X86NativeInstruction X86NativeStoreMemory8 base (sealDisp at) s))))) def sealMov = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (sealEmit (constructor X86NativeInstruction X86NativeMoveRegister64 s d)))) def sealAdd = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (sealEmit (constructor X86NativeInstruction X86NativeAddRegister64 s d)))) def sealAnd = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (sealEmit (constructor X86NativeInstruction X86NativeAndRegister64 s d)))) def sealOr = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (sealEmit (constructor X86NativeInstruction X86NativeOrRegister64 s d)))) def sealXor = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) . (sealEmit (constructor X86NativeInstruction X86NativeXorRegister64 s d)))) def sealShl = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (sealEmit (constructor X86NativeInstruction X86NativeShiftLeftImmediate64 d (sealImm8 n))))) def sealShr = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (sealEmit (constructor X86NativeInstruction X86NativeShiftRightImmediate64 d (sealImm8 n))))) def sealMovImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (sealEmit (constructor X86NativeInstruction X86NativeMoveImmediate32 d (sealImm32 n))))) def sealAddImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (sealEmit (constructor X86NativeInstruction X86NativeAddImmediate64 d (sealImm32 n))))) def sealAndImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (sealEmit (constructor X86NativeInstruction X86NativeAndImmediate64 d (sealImm32 n))))) def sealCmpImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (sealEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 d (sealImm32 n))))) def sealMulImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat . (sealEmit (constructor X86NativeInstruction X86NativeMultiplyImmediate64 d (sealImm32 n))))) def sealLabel = (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyLabel name rest))) def sealJumpIf = (lambda unrestricted condition : (family X86NativeCondition) . (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family X86NativeAssembly) . (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition name rest)))) def sealReturn = (lambda unrestricted rest : (family X86NativeAssembly) . (sealEmit (constructor X86NativeInstruction X86NativeReturn) rest)) def sealEnd : (family X86NativeAssembly) = (constructor X86NativeAssembly X86NativeAssemblyEnd) def sealBackendJump = (lambda unrestricted condition : (family TelemetrySealCondition) . (eliminate TelemetrySealCondition (lambda unrestricted current : (family TelemetrySealCondition) . (pi unrestricted name : Bytes . (pi unrestricted rest : (family X86NativeAssembly) . (family X86NativeAssembly)))) condition (branch TelemetrySealBelow . (sealJumpIf (constructor X86NativeCondition X86NativeConditionBelow))) (branch TelemetrySealNotZero . (sealJumpIf (constructor X86NativeCondition X86NativeConditionNotZero))))) def sealX86Backend : (family TelemetrySealBackend (family X86NativeAssembly) (family X86NativeRegister64)) = (constructor TelemetrySealBackend TelemetrySealBackendValue (family X86NativeAssembly) (family X86NativeRegister64) sealLoad32 sealLoad64 sealLoad8 sealStore32 sealStore64 sealStore8 sealMov sealAdd sealAnd sealOr sealXor sealShl sealShr sealMovImm sealAddImm sealAndImm sealCmpImm sealMulImm sealLabel sealBackendJump sealReturn sealEnd sealRAX sealRBX sealRCX sealRDX sealRSI sealRDI sealRBP sealR8 sealR9 sealR10 sealR11 sealR12 sealR13 sealR14 sealR15) def sealAssembly : (family X86NativeAssembly) = (telemetrySealAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) sealX86Backend) def nativeTelemetrySealRoutine : Bytes = (compiler-native-encode (family X86NativeAssembly) sealAssembly)