Runtime.TelemetrySeal

1module Runtime.TelemetrySeal
2
3import Std.Foundation
4import Std.List
5import Std.Natural
6
7-- One SHA-256/ALPHATEL algorithm, specialized to a host instruction emitter.
8-- The emitter owns register assignment, instruction selection and branch
9-- flags. Loads/stores are little-endian and permit unaligned access; 8/32-bit
10-- loads zero-extend. Word operations wrap at 64 bits, shifts are logical, and
11-- 8/32-bit stores truncate. AddImm sign-extends its 32-bit operand and sets
12-- zero status; CmpImm supplies unsigned comparison status. Label and move
13-- operations preserve that status. These obligations are tested on each host.
14--
15-- Registers are logical roles inherited from the original implementation:
16-- RDI/RSI/RDX/RCX/R8/R9 carry the six arguments; the remaining names denote
17-- scratch values. The emitter chooses physical registers and preserves its
18-- calling convention. The fixed work-area slots are part of this algorithm,
19-- not per-system addresses. Callers supply writable, nonoverlapping bounded
20-- buffers, a positive block count and body length, and valid SHA padding.
21family TelemetrySealCondition : Type 0
22constructor TelemetrySealBelow
23constructor TelemetrySealNotZero
24end-family
25
26family TelemetrySealBackend : Type 0
27parameter erased sealBackendAssembly : Type 0
28parameter erased sealBackendRegister : Type 0
29constructor TelemetrySealBackendValue
30field unrestricted backendSealLoad32 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly))))
31field unrestricted backendSealLoad64 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly))))
32field unrestricted backendSealLoad8 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly))))
33field unrestricted backendSealStore32 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendRegister . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly))))
34field unrestricted backendSealStore64 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendRegister . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly))))
35field unrestricted backendSealStore8 : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendRegister . (pi unrestricted a3 : sealBackendAssembly . sealBackendAssembly))))
36field unrestricted backendSealMov : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
37field unrestricted backendSealAdd : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
38field unrestricted backendSealAnd : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
39field unrestricted backendSealOr : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
40field unrestricted backendSealXor : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : sealBackendRegister . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
41field unrestricted backendSealShl : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
42field unrestricted backendSealShr : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
43field unrestricted backendSealMovImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
44field unrestricted backendSealAddImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
45field unrestricted backendSealAndImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
46field unrestricted backendSealCmpImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
47field unrestricted backendSealMulImm : (pi unrestricted a0 : sealBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
48field unrestricted backendSealLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : sealBackendAssembly . sealBackendAssembly))
49field unrestricted backendSealJumpIf : (pi unrestricted a0 : (family TelemetrySealCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : sealBackendAssembly . sealBackendAssembly)))
50field unrestricted backendSealReturn : (pi unrestricted a0 : sealBackendAssembly . sealBackendAssembly)
51field unrestricted backendSealEnd : sealBackendAssembly
52field unrestricted backendSealRAX : sealBackendRegister
53field unrestricted backendSealRBX : sealBackendRegister
54field unrestricted backendSealRCX : sealBackendRegister
55field unrestricted backendSealRDX : sealBackendRegister
56field unrestricted backendSealRSI : sealBackendRegister
57field unrestricted backendSealRDI : sealBackendRegister
58field unrestricted backendSealRBP : sealBackendRegister
59field unrestricted backendSealR8 : sealBackendRegister
60field unrestricted backendSealR9 : sealBackendRegister
61field unrestricted backendSealR10 : sealBackendRegister
62field unrestricted backendSealR11 : sealBackendRegister
63field unrestricted backendSealR12 : sealBackendRegister
64field unrestricted backendSealR13 : sealBackendRegister
65field unrestricted backendSealR14 : sealBackendRegister
66field unrestricted backendSealR15 : sealBackendRegister
67end-family
68
69def sealMonotonicAt : Nat = 13
70
71def sealWorkBytes : Nat = 640
72
73def sealW = (lambda unrestricted t : Nat . (naturalMultiply 4 t))
74
75def sealK = (lambda unrestricted t : Nat . (naturalAdd 256 (naturalMultiply 4 t)))
76
77def sealVar = (lambda unrestricted slot : Nat . (naturalAdd 512 (naturalMultiply 4 slot)))
78
79def sealH = (lambda unrestricted i : Nat . (naturalAdd 544 (naturalMultiply 4 i)))
80
81def sealSaved = (lambda unrestricted i : Nat . (naturalAdd 576 (naturalMultiply 8 i)))
82
83def sealRoundConstants : (family StdList Nat) =
84  (constructor StdList StdListCons Nat 0x428a2f98 (constructor StdList StdListCons Nat 0x71374491 (constructor StdList StdListCons Nat 0xb5c0fbcf (constructor StdList StdListCons Nat 0xe9b5dba5
85  (constructor StdList StdListCons Nat 0x3956c25b (constructor StdList StdListCons Nat 0x59f111f1 (constructor StdList StdListCons Nat 0x923f82a4 (constructor StdList StdListCons Nat 0xab1c5ed5
86  (constructor StdList StdListCons Nat 0xd807aa98 (constructor StdList StdListCons Nat 0x12835b01 (constructor StdList StdListCons Nat 0x243185be (constructor StdList StdListCons Nat 0x550c7dc3
87  (constructor StdList StdListCons Nat 0x72be5d74 (constructor StdList StdListCons Nat 0x80deb1fe (constructor StdList StdListCons Nat 0x9bdc06a7 (constructor StdList StdListCons Nat 0xc19bf174
88  (constructor StdList StdListCons Nat 0xe49b69c1 (constructor StdList StdListCons Nat 0xefbe4786 (constructor StdList StdListCons Nat 0x0fc19dc6 (constructor StdList StdListCons Nat 0x240ca1cc
89  (constructor StdList StdListCons Nat 0x2de92c6f (constructor StdList StdListCons Nat 0x4a7484aa (constructor StdList StdListCons Nat 0x5cb0a9dc (constructor StdList StdListCons Nat 0x76f988da
90  (constructor StdList StdListCons Nat 0x983e5152 (constructor StdList StdListCons Nat 0xa831c66d (constructor StdList StdListCons Nat 0xb00327c8 (constructor StdList StdListCons Nat 0xbf597fc7
91  (constructor StdList StdListCons Nat 0xc6e00bf3 (constructor StdList StdListCons Nat 0xd5a79147 (constructor StdList StdListCons Nat 0x06ca6351 (constructor StdList StdListCons Nat 0x14292967
92  (constructor StdList StdListCons Nat 0x27b70a85 (constructor StdList StdListCons Nat 0x2e1b2138 (constructor StdList StdListCons Nat 0x4d2c6dfc (constructor StdList StdListCons Nat 0x53380d13
93  (constructor StdList StdListCons Nat 0x650a7354 (constructor StdList StdListCons Nat 0x766a0abb (constructor StdList StdListCons Nat 0x81c2c92e (constructor StdList StdListCons Nat 0x92722c85
94  (constructor StdList StdListCons Nat 0xa2bfe8a1 (constructor StdList StdListCons Nat 0xa81a664b (constructor StdList StdListCons Nat 0xc24b8b70 (constructor StdList StdListCons Nat 0xc76c51a3
95  (constructor StdList StdListCons Nat 0xd192e819 (constructor StdList StdListCons Nat 0xd6990624 (constructor StdList StdListCons Nat 0xf40e3585 (constructor StdList StdListCons Nat 0x106aa070
96  (constructor StdList StdListCons Nat 0x19a4c116 (constructor StdList StdListCons Nat 0x1e376c08 (constructor StdList StdListCons Nat 0x2748774c (constructor StdList StdListCons Nat 0x34b0bcb5
97  (constructor StdList StdListCons Nat 0x391c0cb3 (constructor StdList StdListCons Nat 0x4ed8aa4a (constructor StdList StdListCons Nat 0x5b9cca4f (constructor StdList StdListCons Nat 0x682e6ff3
98  (constructor StdList StdListCons Nat 0x748f82ee (constructor StdList StdListCons Nat 0x78a5636f (constructor StdList StdListCons Nat 0x84c87814 (constructor StdList StdListCons Nat 0x8cc70208
99  (constructor StdList StdListCons Nat 0x90befffa (constructor StdList StdListCons Nat 0xa4506ceb (constructor StdList StdListCons Nat 0xbef9a3f7 (constructor StdList StdListCons Nat 0xc67178f2
100  (constructor StdList StdListEmpty Nat)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
101
102def sealInitialHash : (family StdList Nat) =
103  (constructor StdList StdListCons Nat 0x6a09e667 (constructor StdList StdListCons Nat 0xbb67ae85 (constructor StdList StdListCons Nat 0x3c6ef372 (constructor StdList StdListCons Nat 0xa54ff53a
104  (constructor StdList StdListCons Nat 0x510e527f (constructor StdList StdListCons Nat 0x9b05688c (constructor StdList StdListCons Nat 0x1f83d9ab (constructor StdList StdListCons Nat 0x5be0cd19
105  (constructor StdList StdListEmpty Nat)))))))))
106
107def sealAt =
108  (lambda unrestricted values : (family StdList Nat) . (lambda unrestricted p : Nat .
109    (eliminate StdOption (lambda unrestricted current : (family StdOption Nat) . Nat) (stdListIndex Nat values p)
110      (branch StdNone . 0)
111      (branch StdSome value . value))))
112
113def sealSlot = (lambda unrestricted v : Nat . (lambda unrestricted t : Nat .
114  (sealVar (naturalModuloUnchecked (naturalSaturatingSubtract (naturalAdd v 64) t) 8))))
115
116def telemetrySealAssemblyFor =
117  (lambda erased A : Type 0 . (lambda erased R : Type 0 .
118    (lambda unrestricted backend : (family TelemetrySealBackend A R) .
119      (eliminate TelemetrySealBackend (lambda unrestricted current : (family TelemetrySealBackend A R) . A) backend
120        (branch TelemetrySealBackendValue
121          sealLoad32 sealLoad64 sealLoad8 sealStore32 sealStore64 sealStore8 sealMov sealAdd sealAnd sealOr sealXor sealShl sealShr sealMovImm sealAddImm sealAndImm sealCmpImm sealMulImm sealLabel sealJumpIf sealReturn sealEnd sealRAX sealRBX sealRCX sealRDX sealRSI sealRDI sealRBP sealR8 sealR9 sealR10 sealR11 sealR12 sealR13 sealR14 sealR15 .
122          (let unrestricted sealFor = (lambda unrestricted count : Nat .
123    (lambda unrestricted body : (pi unrestricted index : Nat . (pi unrestricted rest : A . A)) .
124      (lambda unrestricted tail : A .
125        (nat-eliminate
126          (lambda unrestricted current : Nat . A)
127          tail
128          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : A .
129            (body (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) predecessor) induction)))
130          count))))
131            in           (let unrestricted sealRotate = (lambda unrestricted d : R . (lambda unrestricted s : R . (lambda unrestricted n : Nat .
132  (lambda unrestricted rest : A .
133    (sealMov d s (sealShl d 32 (sealOr d s (sealShr d n rest))))))))
134            in           (let unrestricted sealSigma = (lambda unrestricted d : R . (lambda unrestricted t : R . (lambda unrestricted s : R .
135  (lambda unrestricted x : Nat . (lambda unrestricted y : Nat . (lambda unrestricted z : Nat . (lambda unrestricted shift : Nat .
136  (lambda unrestricted rest : A .
137    (sealRotate d s x (sealRotate t s y (sealXor d t
138      (nat-eliminate (lambda unrestricted current : Nat . A)
139        (sealRotate t s z (sealXor d t rest))
140        (lambda unrestricted p : Nat . (lambda unrestricted i : A . (sealMov t s (sealShr t z (sealXor d t rest)))))
141        shift))))))))))))
142            in           (let unrestricted sealConstant = (lambda unrestricted at : Nat . (lambda unrestricted value : Nat . (lambda unrestricted rest : A .
143  (sealMovImm sealRAX value (sealStore32 sealR9 at sealRAX rest)))))
144            in           (let unrestricted sealMessageWord = (lambda unrestricted i : Nat . (lambda unrestricted rest : A .
145  (sealLoad8 sealRAX sealRDI (naturalMultiply 4 i)
146    (sealShl sealRAX 8 (sealLoad8 sealRBX sealRDI (naturalAdd 1 (naturalMultiply 4 i)) (sealOr sealRAX sealRBX
147    (sealShl sealRAX 8 (sealLoad8 sealRBX sealRDI (naturalAdd 2 (naturalMultiply 4 i)) (sealOr sealRAX sealRBX
148    (sealShl sealRAX 8 (sealLoad8 sealRBX sealRDI (naturalAdd 3 (naturalMultiply 4 i)) (sealOr sealRAX sealRBX
149      (sealStore32 sealR9 (sealW i) sealRAX rest)))))))))))))
150            in           (let unrestricted sealScheduleWord = (lambda unrestricted k : Nat . (lambda unrestricted rest : A .
151  (let unrestricted t = (naturalAdd 16 k)
152    in (sealLoad32 sealRAX sealR9 (sealW (naturalSaturatingSubtract t 15))
153        (sealSigma sealRBX sealR10 sealRAX 7 18 3 1
154        (sealLoad32 sealRAX sealR9 (sealW (naturalSaturatingSubtract t 2))
155        (sealSigma sealR11 sealR10 sealRAX 17 19 10 1
156        (sealAdd sealRBX sealR11
157        (sealLoad32 sealR10 sealR9 (sealW (naturalSaturatingSubtract t 16)) (sealAdd sealRBX sealR10
158        (sealLoad32 sealR10 sealR9 (sealW (naturalSaturatingSubtract t 7)) (sealAdd sealRBX sealR10
159          (sealStore32 sealR9 (sealW t) sealRBX rest)))))))))))))
160            in           (let unrestricted sealRound = (lambda unrestricted t : Nat . (lambda unrestricted rest : A .
161  -- t1 = h + S1(e) + ch(e, f, g) + K[t] + W[t], in rbx
162  (sealLoad32 sealRAX sealR9 (sealSlot 4 t)
163  (sealSigma sealRBX sealR10 sealRAX 6 11 25 0
164  (sealLoad32 sealR11 sealR9 (sealSlot 5 t) (sealMov sealR10 sealRAX (sealAnd sealR10 sealR11
165  (sealLoad32 sealR12 sealR9 (sealSlot 6 t) (sealMov sealR11 sealRAX (sealAnd sealR11 sealR12 (sealXor sealR11 sealR12
166  (sealXor sealR10 sealR11 (sealAdd sealRBX sealR10
167  (sealLoad32 sealR10 sealR9 (sealSlot 7 t) (sealAdd sealRBX sealR10
168  (sealLoad32 sealR10 sealR9 (sealK t) (sealAdd sealRBX sealR10
169  (sealLoad32 sealR10 sealR9 (sealW t) (sealAdd sealRBX sealR10
170  -- t2 = S0(a) + maj(a, b, c), in r10
171  (sealLoad32 sealRAX sealR9 (sealSlot 0 t)
172  (sealSigma sealR10 sealR11 sealRAX 2 13 22 0
173  (sealLoad32 sealR11 sealR9 (sealSlot 1 t) (sealLoad32 sealR12 sealR9 (sealSlot 2 t)
174  (sealMov sealR13 sealRAX (sealAnd sealR13 sealR11 (sealMov sealR14 sealRAX (sealAnd sealR14 sealR12 (sealXor sealR13 sealR14
175  (sealAnd sealR11 sealR12 (sealXor sealR13 sealR11 (sealAdd sealR10 sealR13
176  -- d + t1 is the next e (d's slot), t1 + t2 the next a (h's slot)
177  (sealLoad32 sealR11 sealR9 (sealSlot 3 t) (sealAdd sealR11 sealRBX (sealStore32 sealR9 (sealSlot 3 t) sealR11
178  (sealAdd sealRBX sealR10 (sealStore32 sealR9 (sealSlot 7 t) sealRBX rest))))))))))))))))))))))))))))))))))))
179            in           (let unrestricted sealLoadVariable = (lambda unrestricted i : Nat . (lambda unrestricted rest : A .
180  (sealLoad32 sealRAX sealR9 (sealH i) (sealStore32 sealR9 (sealVar i) sealRAX rest))))
181            in           (let unrestricted sealAccumulate = (lambda unrestricted i : Nat . (lambda unrestricted rest : A .
182  (sealLoad32 sealRAX sealR9 (sealH i) (sealLoad32 sealRBX sealR9 (sealVar i) (sealAdd sealRAX sealRBX (sealStore32 sealR9 (sealH i) sealRAX rest))))))
183            in           (let unrestricted sealHexDigit = (lambda unrestricted q : Nat . (lambda unrestricted rest : A .
184  (let unrestricted skip = (bytes-cons (nat-to-byte q) b"seal-hex-digit")
185    in (sealLoad32 sealRAX sealR9 (sealH (naturalDivideUnchecked q 8))
186        (sealShr sealRAX (naturalMultiply 4 (naturalSaturatingSubtract 7 (naturalModuloUnchecked q 8)))
187        (sealAndImm sealRAX 15
188        (sealCmpImm sealRAX 10
189        (sealJumpIf (constructor TelemetrySealCondition TelemetrySealBelow) skip
190        (sealAddImm sealRAX 39
191        (sealLabel skip
192        (sealAddImm sealRAX 48
193          (sealStore8 sealRDX q sealRAX rest))))))))))))
194            in           (let unrestricted sealSaveRegisters = (lambda unrestricted rest : A .
195  (sealStore64 sealR9 (sealSaved 0) sealRBX (sealStore64 sealR9 (sealSaved 1) sealR12 (sealStore64 sealR9 (sealSaved 2) sealR13
196    (sealStore64 sealR9 (sealSaved 3) sealR14 (sealStore64 sealR9 (sealSaved 4) sealR15 rest))))))
197            in           (let unrestricted sealRestoreRegisters = (lambda unrestricted rest : A .
198  (sealLoad64 sealRBX sealR9 (sealSaved 0) (sealLoad64 sealR12 sealR9 (sealSaved 1) (sealLoad64 sealR13 sealR9 (sealSaved 2)
199    (sealLoad64 sealR14 sealR9 (sealSaved 3) (sealLoad64 sealR15 sealR9 (sealSaved 4) rest))))))
200            in (sealSaveRegisters
201  -- the clock reading into the body: seconds * 1e9 + nanoseconds
202  (sealLoad64 sealRAX sealR8 0 (sealMulImm sealRAX 1000000000 (sealLoad64 sealRBX sealR8 8 (sealAdd sealRAX sealRBX
203  (sealStore64 sealRDI sealMonotonicAt sealRAX
204  -- the constants, the initial hash; r15 keeps the body's start
205  (sealFor 64 (lambda unrestricted t : Nat . (sealConstant (sealK t) (sealAt sealRoundConstants t)))
206  (sealFor 8 (lambda unrestricted i : Nat . (sealConstant (sealH i) (sealAt sealInitialHash i)))
207  (sealMov sealR15 sealRDI
208  (sealLabel b"seal-block"
209    (sealFor 16 sealMessageWord
210    (sealFor 48 sealScheduleWord
211    (sealFor 8 sealLoadVariable
212    (sealFor 64 sealRound
213    (sealFor 8 sealAccumulate
214    (sealAddImm sealRDI 64
215    (sealAddImm sealRSI 0xFFFFFFFF
216    (sealJumpIf (constructor TelemetrySealCondition TelemetrySealNotZero) b"seal-block"
217  -- the body into the record after "ALPHATEL", rdx left after it
218  (sealAddImm sealRDX 8
219  (sealLabel b"seal-copy"
220    (sealLoad8 sealRAX sealR15 0 (sealStore8 sealRDX 0 sealRAX (sealAddImm sealR15 1 (sealAddImm sealRDX 1
221    (sealAddImm sealRCX 0xFFFFFFFF
222    (sealJumpIf (constructor TelemetrySealCondition TelemetrySealNotZero) b"seal-copy"
223  -- the digest's 64 hex digits
224  (sealFor 64 sealHexDigit
225  (sealRestoreRegisters
226  (sealReturn sealEnd))))))))))))))))))))))))))))))))))))))))))))))