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))))))))))))))))))))))))))))))))))))))))))))))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.