1module Data.SHA256ScheduleExpand
2
3import Data.SHA256
4import Data.SHA256Core
5import Data.SHA256Schedule
6import Model.Config
7import Model.Word32
8import Model.Word32Logic
9import Std.Natural
10
11family SHA256ScheduleDependenciesResult : Type 0
12constructor SHA256ScheduleDependenciesSucceeded
13field unrestricted sha256ScheduleWordMinus2 : (family ModelWord32)
14field unrestricted sha256ScheduleWordMinus7 : (family ModelWord32)
15field unrestricted sha256ScheduleWordMinus15 : (family ModelWord32)
16field unrestricted sha256ScheduleWordMinus16 : (family ModelWord32)
17constructor SHA256ScheduleDependenciesFailed
18field unrestricted sha256ScheduleDependenciesError : (family SHA256ErrorCode)
19field unrestricted sha256ScheduleDependenciesFailureIndex : Nat
20
21end-family
22
23family SHA256ScheduleExpansionState : Type 0
24constructor SHA256ScheduleExpansionStateValue
25field unrestricted sha256ExpansionSchedule : (family SHA256Schedule)
26field unrestricted sha256ExpansionNextIndex : Nat
27field unrestricted sha256ExpansionGeneratedWords : Nat
28field unrestricted sha256ExpansionLookupCount : Nat
29field unrestricted sha256ExpansionSigmaCount : Nat
30field unrestricted sha256ExpansionRotateCount : Nat
31field unrestricted sha256ExpansionShiftCount : Nat
32field unrestricted sha256ExpansionAddCount : Nat
33
34end-family
35
36family SHA256ScheduleExpansionStepResult : Type 0
37constructor SHA256ScheduleExpansionStepSucceeded
38field unrestricted sha256ExpansionStepState : (family SHA256ScheduleExpansionState)
39constructor SHA256ScheduleExpansionStepFailed
40field unrestricted sha256ExpansionStepError : (family SHA256ErrorCode)
41field unrestricted sha256ExpansionStepFailureIndex : Nat
42
43end-family
44
45family SHA256ScheduleExpansionTelemetry : Type 0
46constructor SHA256ScheduleExpansionTelemetryValue
47field unrestricted sha256ExpansionTelemetryGeneratedWords : Nat
48field unrestricted sha256ExpansionTelemetryLookupCount : Nat
49field unrestricted sha256ExpansionTelemetrySigmaCount : Nat
50field unrestricted sha256ExpansionTelemetryRotateCount : Nat
51field unrestricted sha256ExpansionTelemetryShiftCount : Nat
52field unrestricted sha256ExpansionTelemetryAddCount : Nat
53
54end-family
55
56family SHA256ScheduleExpansionResult : Type 0
57constructor SHA256ScheduleExpansionSucceeded
58field unrestricted sha256ExpandedSchedule : (family SHA256Schedule)
59field unrestricted sha256ExpansionTelemetry : (family SHA256ScheduleExpansionTelemetry)
60constructor SHA256ScheduleExpansionFailed
61field unrestricted sha256ExpansionError : (family SHA256ErrorCode)
62field unrestricted sha256ExpansionFailureIndex : Nat
63
64end-family
65
66def sha256NaturalTwo =
67 (byte-to-nat (byte 2))
68
69def sha256NaturalSeven =
70 (byte-to-nat (byte 7))
71
72def sha256NaturalFifteen =
73 (byte-to-nat (byte 15))
74
75def sha256NaturalFortyEight =
76 (byte-to-nat (byte 48))
77
78def sha256LookupScheduleDependencies =
79 (lambda unrestricted schedule : (family SHA256Schedule) .
80 (lambda unrestricted index : Nat .
81 (eliminate
82 SHA256ScheduleLookupResult
83 (lambda unrestricted current : (family SHA256ScheduleLookupResult) .
84 (family SHA256ScheduleDependenciesResult))
85 (sha256ScheduleLookup schedule (naturalSaturatingSubtract index sha256NaturalTwo))
86 (branch
87 SHA256ScheduleLookupSucceeded
88 wordMinus2
89 .
90 (eliminate
91 SHA256ScheduleLookupResult
92 (lambda unrestricted current : (family SHA256ScheduleLookupResult) .
93 (family SHA256ScheduleDependenciesResult))
94 (sha256ScheduleLookup schedule (naturalSaturatingSubtract index sha256NaturalSeven))
95 (branch
96 SHA256ScheduleLookupSucceeded
97 wordMinus7
98 .
99 (eliminate
100 SHA256ScheduleLookupResult
101 (lambda unrestricted current : (family SHA256ScheduleLookupResult) .
102 (family SHA256ScheduleDependenciesResult))
103 (sha256ScheduleLookup
104 schedule
105 (naturalSaturatingSubtract index sha256NaturalFifteen))
106 (branch
107 SHA256ScheduleLookupSucceeded
108 wordMinus15
109 .
110 (eliminate
111 SHA256ScheduleLookupResult
112 (lambda unrestricted current : (family SHA256ScheduleLookupResult) .
113 (family SHA256ScheduleDependenciesResult))
114 (sha256ScheduleLookup
115 schedule
116 (naturalSaturatingSubtract index sha256NaturalSixteen))
117 (branch
118 SHA256ScheduleLookupSucceeded
119 wordMinus16
120 .
121 (constructor
122 SHA256ScheduleDependenciesResult
123 SHA256ScheduleDependenciesSucceeded
124 wordMinus2
125 wordMinus7
126 wordMinus15
127 wordMinus16))
128 (branch
129 SHA256ScheduleLookupFailed
130 error
131 failedIndex
132 .
133 (constructor
134 SHA256ScheduleDependenciesResult
135 SHA256ScheduleDependenciesFailed
136 error
137 failedIndex))))
138 (branch
139 SHA256ScheduleLookupFailed
140 error
141 failedIndex
142 .
143 (constructor
144 SHA256ScheduleDependenciesResult
145 SHA256ScheduleDependenciesFailed
146 error
147 failedIndex))))
148 (branch
149 SHA256ScheduleLookupFailed
150 error
151 failedIndex
152 .
153 (constructor
154 SHA256ScheduleDependenciesResult
155 SHA256ScheduleDependenciesFailed
156 error
157 failedIndex))))
158 (branch
159 SHA256ScheduleLookupFailed
160 error
161 failedIndex
162 .
163 (constructor
164 SHA256ScheduleDependenciesResult
165 SHA256ScheduleDependenciesFailed
166 error
167 failedIndex)))))
168
169def sha256ExpandScheduleStep =
170 (lambda unrestricted state : (family SHA256ScheduleExpansionState) .
171 (eliminate
172 SHA256ScheduleExpansionState
173 (lambda unrestricted current : (family SHA256ScheduleExpansionState) .
174 (family SHA256ScheduleExpansionStepResult))
175 state
176 (branch
177 SHA256ScheduleExpansionStateValue
178 schedule
179 nextIndex
180 generated
181 lookups
182 sigmas
183 rotates
184 shifts
185 adds
186 .
187 (eliminate
188 SHA256ScheduleDependenciesResult
189 (lambda unrestricted current : (family SHA256ScheduleDependenciesResult) .
190 (family SHA256ScheduleExpansionStepResult))
191 (sha256LookupScheduleDependencies schedule nextIndex)
192 (branch
193 SHA256ScheduleDependenciesSucceeded
194 wordMinus2
195 wordMinus7
196 wordMinus15
197 wordMinus16
198 .
199 (app
200 (lambda unrestricted generatedWord : (family ModelWord32) .
201 (constructor
202 SHA256ScheduleExpansionStepResult
203 SHA256ScheduleExpansionStepSucceeded
204 (constructor
205 SHA256ScheduleExpansionState
206 SHA256ScheduleExpansionStateValue
207 (sha256ScheduleAppend schedule generatedWord)
208 (succ nextIndex)
209 (succ generated)
210 (naturalAdd lookups sha256NaturalFour)
211 (naturalAdd sigmas sha256NaturalTwo)
212 (naturalAdd rotates sha256NaturalFour)
213 (naturalAdd shifts sha256NaturalTwo)
214 (naturalAdd adds (byte-to-nat (byte 3))))))
215 (modelWord32AddFour
216 (sha256SmallSigma1 wordMinus2)
217 wordMinus7
218 (sha256SmallSigma0 wordMinus15)
219 wordMinus16)))
220 (branch
221 SHA256ScheduleDependenciesFailed
222 error
223 failedIndex
224 .
225 (constructor
226 SHA256ScheduleExpansionStepResult
227 SHA256ScheduleExpansionStepFailed
228 error
229 failedIndex))))))
230
231-- Run `fuel` expansion steps, FIRST-ORDER.
232--
233-- The previous definition folded with a FUNCTION accumulator
234-- (`pi state . Result`) and recursed by applying the induction hypothesis to the
235-- next state. Because the VM normalizes a fold's function part before the
236-- concrete state is supplied, it symbolically unrolled all 48 iterations of a
237-- large step body (four schedule lookups + sigma arithmetic each) into one giant
238-- term and only then evaluated it -- ~O(fuel^2 * body) work that kept expansion
239-- slow even after the lookup itself was made linear.
240--
241-- This version folds with a first-order accumulator: the step-result VALUE
242-- (`Succeeded state | Failed`). Each iteration runs exactly one `expandStep` on
243-- the concrete accumulated state (or threads a failure through), so the whole
244-- expansion is O(fuel) over concrete values with no symbolic term building. The
245-- computed words -- and therefore the digest -- are unchanged.
246def sha256ExpandScheduleWithFuel =
247 (lambda unrestricted fuel : Nat .
248 (lambda unrestricted initialState : (family SHA256ScheduleExpansionState) .
249 (eliminate
250 SHA256ScheduleExpansionStepResult
251 (lambda unrestricted current : (family SHA256ScheduleExpansionStepResult) .
252 (family SHA256ScheduleExpansionResult))
253 (nat-eliminate
254 (lambda unrestricted current : Nat . (family SHA256ScheduleExpansionStepResult))
255 (constructor
256 SHA256ScheduleExpansionStepResult
257 SHA256ScheduleExpansionStepSucceeded
258 initialState)
259 (lambda unrestricted predecessor : Nat .
260 (lambda unrestricted induction : (family SHA256ScheduleExpansionStepResult) .
261 (eliminate
262 SHA256ScheduleExpansionStepResult
263 (lambda unrestricted current : (family SHA256ScheduleExpansionStepResult) .
264 (family SHA256ScheduleExpansionStepResult))
265 induction
266 (branch
267 SHA256ScheduleExpansionStepSucceeded
268 state
269 .
270 (sha256ExpandScheduleStep state))
271 (branch SHA256ScheduleExpansionStepFailed error failedIndex . induction))))
272 fuel)
273 (branch
274 SHA256ScheduleExpansionStepSucceeded
275 state
276 .
277 (eliminate
278 SHA256ScheduleExpansionState
279 (lambda unrestricted current : (family SHA256ScheduleExpansionState) .
280 (family SHA256ScheduleExpansionResult))
281 state
282 (branch
283 SHA256ScheduleExpansionStateValue
284 schedule
285 nextIndex
286 generated
287 lookups
288 sigmas
289 rotates
290 shifts
291 adds
292 .
293 (constructor
294 SHA256ScheduleExpansionResult
295 SHA256ScheduleExpansionSucceeded
296 schedule
297 (constructor
298 SHA256ScheduleExpansionTelemetry
299 SHA256ScheduleExpansionTelemetryValue
300 generated
301 lookups
302 sigmas
303 rotates
304 shifts
305 adds)))))
306 (branch
307 SHA256ScheduleExpansionStepFailed
308 error
309 failedIndex
310 .
311 (constructor
312 SHA256ScheduleExpansionResult
313 SHA256ScheduleExpansionFailed
314 error
315 failedIndex)))))
316
317def sha256ValidateExpandedSchedule =
318 (lambda unrestricted result : (family SHA256ScheduleExpansionResult) .
319 (eliminate
320 SHA256ScheduleExpansionResult
321 (lambda unrestricted current : (family SHA256ScheduleExpansionResult) .
322 (family SHA256ScheduleExpansionResult))
323 result
324 (branch
325 SHA256ScheduleExpansionSucceeded
326 schedule
327 telemetry
328 .
329 (nat-eliminate
330 (lambda unrestricted validLength : Nat . (family SHA256ScheduleExpansionResult))
331 (constructor
332 SHA256ScheduleExpansionResult
333 SHA256ScheduleExpansionFailed
334 (constructor SHA256ErrorCode SHA256ScheduleLengthInvalid)
335 (sha256ScheduleLength schedule))
336 (lambda unrestricted predecessor : Nat .
337 (lambda unrestricted induction : (family SHA256ScheduleExpansionResult) .
338 (constructor
339 SHA256ScheduleExpansionResult
340 SHA256ScheduleExpansionSucceeded
341 schedule
342 telemetry)))
343 (naturalEqual (sha256ScheduleLength schedule) sha256NaturalSixtyFour)))
344 (branch
345 SHA256ScheduleExpansionFailed
346 error
347 failedIndex
348 .
349 (constructor SHA256ScheduleExpansionResult SHA256ScheduleExpansionFailed error failedIndex))))
350
351def sha256ExpandSchedule =
352 (lambda unrestricted initialSchedule : (family SHA256Schedule) .
353 (nat-eliminate
354 (lambda unrestricted validInitialLength : Nat . (family SHA256ScheduleExpansionResult))
355 (constructor
356 SHA256ScheduleExpansionResult
357 SHA256ScheduleExpansionFailed
358 (constructor SHA256ErrorCode SHA256ScheduleLengthInvalid)
359 (sha256ScheduleLength initialSchedule))
360 (lambda unrestricted predecessor : Nat .
361 (lambda unrestricted induction : (family SHA256ScheduleExpansionResult) .
362 (sha256ValidateExpandedSchedule
363 (sha256ExpandScheduleWithFuel
364 sha256NaturalFortyEight
365 (constructor
366 SHA256ScheduleExpansionState
367 SHA256ScheduleExpansionStateValue
368 initialSchedule
369 sha256NaturalSixteen
370 zero
371 zero
372 zero
373 zero
374 zero
375 zero)))))
376 (naturalEqual (sha256ScheduleLength initialSchedule) sha256NaturalSixteen)))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.