Runtime.NativeTelemetrySeal

1module Runtime.NativeTelemetrySeal
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Runtime.TelemetrySeal
6import Std.Foundation
7import Std.List
8import Std.Natural
9
10-- SEALING AN ALPHATEL RECORD AT RUN TIME (docs/observability PRD item 9).
11-- Runtime.NativeTelemetry encodes a record as "ALPHATEL", the body, then
12-- the SHA-256 of the body in 64 lowercase hex characters.  A record whose
13-- body carries a clock reading can only be sealed where the reading is
14-- taken, so this routine does, in the executable, what the encoder does at
15-- build time for the rest of the body:
16--
17--   rdi  the body followed by its SHA-256 padding (0x80, zeros, the bit
18--        length), whole 64-byte blocks, in writable memory
19--   rsi  the number of blocks
20--   rdx  the record: "ALPHATEL" already at +0; the body is copied to +8
21--        and the hex digest written after it
22--   rcx  the body's length in bytes (nonzero)
23--   r8   a struct timespec (seconds, nanoseconds): its nanoseconds since
24--        the clock's epoch are written into the body at `sealMonotonicAt`
25--        first, so the digest covers them
26--   r9   a work area of `sealWorkBytes` bytes
27--
28-- It keeps the System V callee-saved registers it uses in the work area
29-- (the instruction set has no push) and returns.  Every 32-bit quantity is
30-- kept zero-extended in a 64-bit register and truncated by its 32-bit
31-- store; a rotation is a shift of the doubled word.  The digest is checked
32-- against the build-time encoder's by reading a record the executable
33-- wrote (scripts/ci/observability.sh: `alpha observe import alphatel`
34-- verifies every record's digest).
35
36def sealImm32 = x86NativeImmediate32FromNatural
37
38def sealDisp = x86NativeDisplacement32FromNatural
39
40def sealImm8 = (lambda unrestricted n : Nat . (constructor X86NativeImmediate8 X86NativeImmediate8Value (nat-to-byte n)))
41
42def sealRAX = (constructor X86NativeRegister64 X86NativeRAX)
43
44def sealRBX = (constructor X86NativeRegister64 X86NativeRBX)
45
46def sealRCX = (constructor X86NativeRegister64 X86NativeRCX)
47
48def sealRDX = (constructor X86NativeRegister64 X86NativeRDX)
49
50def sealRSI = (constructor X86NativeRegister64 X86NativeRSI)
51
52def sealRDI = (constructor X86NativeRegister64 X86NativeRDI)
53
54def sealRBP = (constructor X86NativeRegister64 X86NativeRBP)
55
56def sealR8 = (constructor X86NativeRegister64 X86NativeR8)
57
58def sealR9 = (constructor X86NativeRegister64 X86NativeR9)
59
60def sealR10 = (constructor X86NativeRegister64 X86NativeR10)
61
62def sealR11 = (constructor X86NativeRegister64 X86NativeR11)
63
64def sealR12 = (constructor X86NativeRegister64 X86NativeR12)
65
66def sealR13 = (constructor X86NativeRegister64 X86NativeR13)
67
68def sealR14 = (constructor X86NativeRegister64 X86NativeR14)
69
70def sealR15 = (constructor X86NativeRegister64 X86NativeR15)
71
72def sealEmit = (lambda unrestricted instruction : (family X86NativeInstruction) . (lambda unrestricted rest : (family X86NativeAssembly) .
73  (constructor X86NativeAssembly X86NativeAssemblyEmit instruction rest)))
74
75def sealLoad32 = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat .
76  (sealEmit (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64 d base (sealDisp at))))))
77
78def sealLoad64 = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat .
79  (sealEmit (constructor X86NativeInstruction X86NativeLoadMemory64 d base (sealDisp at))))))
80
81def sealLoad8 = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat .
82  (sealEmit (constructor X86NativeInstruction X86NativeLoadMemory8ZeroExtend64 d base (sealDisp at))))))
83
84def sealStore32 = (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (lambda unrestricted s : (family X86NativeRegister64) .
85  (sealEmit (constructor X86NativeInstruction X86NativeStoreMemory32 base (sealDisp at) s)))))
86
87def sealStore64 = (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (lambda unrestricted s : (family X86NativeRegister64) .
88  (sealEmit (constructor X86NativeInstruction X86NativeStoreMemory64 base (sealDisp at) s)))))
89
90def sealStore8 = (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted at : Nat . (lambda unrestricted s : (family X86NativeRegister64) .
91  (sealEmit (constructor X86NativeInstruction X86NativeStoreMemory8 base (sealDisp at) s)))))
92
93def sealMov = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) .
94  (sealEmit (constructor X86NativeInstruction X86NativeMoveRegister64 s d))))
95
96def sealAdd = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) .
97  (sealEmit (constructor X86NativeInstruction X86NativeAddRegister64 s d))))
98
99def sealAnd = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) .
100  (sealEmit (constructor X86NativeInstruction X86NativeAndRegister64 s d))))
101
102def sealOr = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) .
103  (sealEmit (constructor X86NativeInstruction X86NativeOrRegister64 s d))))
104
105def sealXor = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted s : (family X86NativeRegister64) .
106  (sealEmit (constructor X86NativeInstruction X86NativeXorRegister64 s d))))
107
108def sealShl = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat .
109  (sealEmit (constructor X86NativeInstruction X86NativeShiftLeftImmediate64 d (sealImm8 n)))))
110
111def sealShr = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat .
112  (sealEmit (constructor X86NativeInstruction X86NativeShiftRightImmediate64 d (sealImm8 n)))))
113
114def sealMovImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat .
115  (sealEmit (constructor X86NativeInstruction X86NativeMoveImmediate32 d (sealImm32 n)))))
116
117def sealAddImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat .
118  (sealEmit (constructor X86NativeInstruction X86NativeAddImmediate64 d (sealImm32 n)))))
119
120def sealAndImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat .
121  (sealEmit (constructor X86NativeInstruction X86NativeAndImmediate64 d (sealImm32 n)))))
122
123def sealCmpImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat .
124  (sealEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 d (sealImm32 n)))))
125
126def sealMulImm = (lambda unrestricted d : (family X86NativeRegister64) . (lambda unrestricted n : Nat .
127  (sealEmit (constructor X86NativeInstruction X86NativeMultiplyImmediate64 d (sealImm32 n)))))
128
129def sealLabel = (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family X86NativeAssembly) .
130  (constructor X86NativeAssembly X86NativeAssemblyLabel name rest)))
131
132def sealJumpIf = (lambda unrestricted condition : (family X86NativeCondition) . (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family X86NativeAssembly) .
133  (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition name rest))))
134
135def sealReturn = (lambda unrestricted rest : (family X86NativeAssembly) . (sealEmit (constructor X86NativeInstruction X86NativeReturn) rest))
136
137def sealEnd : (family X86NativeAssembly) = (constructor X86NativeAssembly X86NativeAssemblyEnd)
138
139def sealBackendJump = (lambda unrestricted condition : (family TelemetrySealCondition) .
140  (eliminate TelemetrySealCondition
141    (lambda unrestricted current : (family TelemetrySealCondition) .
142      (pi unrestricted name : Bytes . (pi unrestricted rest : (family X86NativeAssembly) . (family X86NativeAssembly)))) condition
143    (branch TelemetrySealBelow . (sealJumpIf (constructor X86NativeCondition X86NativeConditionBelow)))
144    (branch TelemetrySealNotZero . (sealJumpIf (constructor X86NativeCondition X86NativeConditionNotZero)))))
145
146def sealX86Backend : (family TelemetrySealBackend (family X86NativeAssembly) (family X86NativeRegister64)) =
147  (constructor TelemetrySealBackend TelemetrySealBackendValue (family X86NativeAssembly) (family X86NativeRegister64)
148    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)
149
150def sealAssembly : (family X86NativeAssembly) =
151  (telemetrySealAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) sealX86Backend)
152
153def nativeTelemetrySealRoutine : Bytes = (compiler-native-encode (family X86NativeAssembly) sealAssembly)