1module Data.SHA256Compress
2
3import Data.SHA256
4import Data.SHA256Constants
5import Data.SHA256Core
6import Data.SHA256Schedule
7import Data.SHA256ScheduleExpand
8import Model.Config
9import Model.Word32
10import Std.Natural
11
12family SHA256CompressionRoundState : Type 0
13constructor SHA256CompressionRoundStateValue
14field unrestricted sha256CompressionWorkingState : (family SHA256State)
15field unrestricted sha256CompressionRoundIndex : Nat
16field unrestricted sha256CompressionRotateCount : Nat
17field unrestricted sha256CompressionShiftCount : Nat
18field unrestricted sha256CompressionBooleanCount : Nat
19field unrestricted sha256CompressionAddCount : Nat
20
21end-family
22
23family SHA256CompressionRoundsResult : Type 0
24constructor SHA256CompressionRoundsSucceeded
25field unrestricted sha256CompressionRoundsState : (family SHA256CompressionRoundState)
26constructor SHA256CompressionRoundsFailed
27field unrestricted sha256CompressionRoundsError : (family SHA256ErrorCode)
28field unrestricted sha256CompressionRoundsFailureIndex : Nat
29
30end-family
31
32family SHA256CompressionTelemetry : Type 0
33constructor SHA256CompressionTelemetryValue
34field unrestricted sha256CompressionTelemetryDecodedWords : Nat
35field unrestricted sha256CompressionTelemetryExpandedWords : Nat
36field unrestricted sha256CompressionTelemetryRounds : Nat
37field unrestricted sha256CompressionTelemetryLookups : Nat
38field unrestricted sha256CompressionTelemetrySigmas : Nat
39field unrestricted sha256CompressionTelemetryRotates : Nat
40field unrestricted sha256CompressionTelemetryShifts : Nat
41field unrestricted sha256CompressionTelemetryBooleans : Nat
42field unrestricted sha256CompressionTelemetryAdds : Nat
43
44end-family
45
46family SHA256CompressionResult : Type 0
47constructor SHA256CompressionSucceeded
48field unrestricted sha256CompressionResultState : (family SHA256State)
49field unrestricted sha256CompressionResultTelemetry : (family SHA256CompressionTelemetry)
50constructor SHA256CompressionFailed
51field unrestricted sha256CompressionError : (family SHA256ErrorCode)
52field unrestricted sha256CompressionFailureIndex : Nat
53
54end-family
55
56def sha256StateAdd =
57 (lambda unrestricted left : (family SHA256State) .
58 (lambda unrestricted right : (family SHA256State) .
59 (eliminate
60 SHA256State
61 (lambda unrestricted current : (family SHA256State) . (family SHA256State))
62 left
63 (branch
64 SHA256StateValue
65 l0
66 l1
67 l2
68 l3
69 l4
70 l5
71 l6
72 l7
73 .
74 (eliminate
75 SHA256State
76 (lambda unrestricted current : (family SHA256State) . (family SHA256State))
77 right
78 (branch
79 SHA256StateValue
80 r0
81 r1
82 r2
83 r3
84 r4
85 r5
86 r6
87 r7
88 .
89 (constructor
90 SHA256State
91 SHA256StateValue
92 (modelWord32Add l0 r0)
93 (modelWord32Add l1 r1)
94 (modelWord32Add l2 r2)
95 (modelWord32Add l3 r3)
96 (modelWord32Add l4 r4)
97 (modelWord32Add l5 r5)
98 (modelWord32Add l6 r6)
99 (modelWord32Add l7 r7))))))))
100
101def sha256CompressionRounds =
102 (lambda unrestricted schedule : (family SHA256Schedule) .
103 (eliminate
104 SHA256Schedule
105 (lambda unrestricted current : (family SHA256Schedule) .
106 (pi unrestricted constants : (family SHA256Schedule) .
107 (pi unrestricted roundState : (family SHA256CompressionRoundState) .
108 (family SHA256CompressionRoundsResult))))
109 schedule
110 (branch
111 SHA256ScheduleEnd
112 .
113 (lambda unrestricted constants : (family SHA256Schedule) .
114 (lambda unrestricted roundState : (family SHA256CompressionRoundState) .
115 (eliminate
116 SHA256Schedule
117 (lambda unrestricted current : (family SHA256Schedule) .
118 (family SHA256CompressionRoundsResult))
119 constants
120 (branch
121 SHA256ScheduleEnd
122 .
123 (eliminate
124 SHA256CompressionRoundState
125 (lambda unrestricted current : (family SHA256CompressionRoundState) .
126 (family SHA256CompressionRoundsResult))
127 roundState
128 (branch
129 SHA256CompressionRoundStateValue
130 state
131 index
132 rotates
133 shifts
134 booleans
135 adds
136 .
137 (nat-eliminate
138 (lambda unrestricted validCount : Nat .
139 (family SHA256CompressionRoundsResult))
140 (constructor
141 SHA256CompressionRoundsResult
142 SHA256CompressionRoundsFailed
143 (constructor SHA256ErrorCode SHA256RoundCountInvalid)
144 index)
145 (lambda unrestricted predecessor : Nat .
146 (lambda unrestricted induction : (family SHA256CompressionRoundsResult) .
147 (constructor
148 SHA256CompressionRoundsResult
149 SHA256CompressionRoundsSucceeded
150 roundState)))
151 (naturalEqual index sha256NaturalSixtyFour)))))
152 (branch
153 SHA256ScheduleNext
154 constant
155 tail
156 induction
157 .
158 (eliminate
159 SHA256CompressionRoundState
160 (lambda unrestricted current : (family SHA256CompressionRoundState) .
161 (family SHA256CompressionRoundsResult))
162 roundState
163 (branch
164 SHA256CompressionRoundStateValue
165 state
166 index
167 rotates
168 shifts
169 booleans
170 adds
171 .
172 (constructor
173 SHA256CompressionRoundsResult
174 SHA256CompressionRoundsFailed
175 (constructor SHA256ErrorCode SHA256RoundCountInvalid)
176 index))))))))
177 (branch
178 SHA256ScheduleNext
179 scheduleWord
180 scheduleTail
181 induction
182 .
183 (lambda unrestricted constants : (family SHA256Schedule) .
184 (lambda unrestricted roundState : (family SHA256CompressionRoundState) .
185 (eliminate
186 SHA256Schedule
187 (lambda unrestricted current : (family SHA256Schedule) .
188 (family SHA256CompressionRoundsResult))
189 constants
190 (branch
191 SHA256ScheduleEnd
192 .
193 (eliminate
194 SHA256CompressionRoundState
195 (lambda unrestricted current : (family SHA256CompressionRoundState) .
196 (family SHA256CompressionRoundsResult))
197 roundState
198 (branch
199 SHA256CompressionRoundStateValue
200 state
201 index
202 rotates
203 shifts
204 booleans
205 adds
206 .
207 (constructor
208 SHA256CompressionRoundsResult
209 SHA256CompressionRoundsFailed
210 (constructor SHA256ErrorCode SHA256RoundCountInvalid)
211 index))))
212 (branch
213 SHA256ScheduleNext
214 constant
215 constantTail
216 constantInduction
217 .
218 (eliminate
219 SHA256CompressionRoundState
220 (lambda unrestricted current : (family SHA256CompressionRoundState) .
221 (family SHA256CompressionRoundsResult))
222 roundState
223 (branch
224 SHA256CompressionRoundStateValue
225 state
226 index
227 rotates
228 shifts
229 booleans
230 adds
231 .
232 (induction
233 constantTail
234 (constructor
235 SHA256CompressionRoundState
236 SHA256CompressionRoundStateValue
237 (sha256RoundState constant scheduleWord state)
238 (succ index)
239 (naturalAdd (byte-to-nat (byte 6)) rotates)
240 shifts
241 (naturalAdd (byte-to-nat (byte 2)) booleans)
242 (naturalAdd (byte-to-nat (byte 7)) adds))))))))))))
243
244def sha256CompressExpandedSchedule =
245 (lambda unrestricted initialState : (family SHA256State) .
246 (lambda unrestricted expandedSchedule : (family SHA256Schedule) .
247 (lambda unrestricted expansionTelemetry : (family SHA256ScheduleExpansionTelemetry) .
248 (eliminate
249 SHA256CompressionRoundsResult
250 (lambda unrestricted current : (family SHA256CompressionRoundsResult) .
251 (family SHA256CompressionResult))
252 (sha256CompressionRounds
253 expandedSchedule
254 sha256RoundConstants
255 (constructor
256 SHA256CompressionRoundState
257 SHA256CompressionRoundStateValue
258 initialState
259 zero
260 zero
261 zero
262 zero
263 zero))
264 (branch
265 SHA256CompressionRoundsSucceeded
266 roundState
267 .
268 (eliminate
269 SHA256CompressionRoundState
270 (lambda unrestricted current : (family SHA256CompressionRoundState) .
271 (family SHA256CompressionResult))
272 roundState
273 (branch
274 SHA256CompressionRoundStateValue
275 workingState
276 rounds
277 rotates
278 shifts
279 booleans
280 adds
281 .
282 (eliminate
283 SHA256ScheduleExpansionTelemetry
284 (lambda unrestricted current : (family SHA256ScheduleExpansionTelemetry) .
285 (family SHA256CompressionResult))
286 expansionTelemetry
287 (branch
288 SHA256ScheduleExpansionTelemetryValue
289 generated
290 lookups
291 sigmas
292 expansionRotates
293 expansionShifts
294 expansionAdds
295 .
296 (constructor
297 SHA256CompressionResult
298 SHA256CompressionSucceeded
299 (sha256StateAdd initialState workingState)
300 (constructor
301 SHA256CompressionTelemetry
302 SHA256CompressionTelemetryValue
303 sha256NaturalSixteen
304 generated
305 rounds
306 lookups
307 sigmas
308 (naturalAdd expansionRotates rotates)
309 (naturalAdd expansionShifts shifts)
310 booleans
311 (naturalAdd (byte-to-nat (byte 8)) (naturalAdd expansionAdds adds)))))))))
312 (branch
313 SHA256CompressionRoundsFailed
314 error
315 failedIndex
316 .
317 (constructor SHA256CompressionResult SHA256CompressionFailed error failedIndex))))))
318
319def sha256CompressBlock =
320 (lambda unrestricted initialState : (family SHA256State) .
321 (lambda unrestricted block : Bytes .
322 (eliminate
323 SHA256BlockDecodeResult
324 (lambda unrestricted current : (family SHA256BlockDecodeResult) .
325 (family SHA256CompressionResult))
326 (sha256DecodeBlockWords block)
327 (branch
328 SHA256BlockDecodeSucceeded
329 initialSchedule
330 decodedCount
331 .
332 (eliminate
333 SHA256ScheduleExpansionResult
334 (lambda unrestricted current : (family SHA256ScheduleExpansionResult) .
335 (family SHA256CompressionResult))
336 (sha256ExpandSchedule initialSchedule)
337 (branch
338 SHA256ScheduleExpansionSucceeded
339 expandedSchedule
340 telemetry
341 .
342 (sha256CompressExpandedSchedule initialState expandedSchedule telemetry))
343 (branch
344 SHA256ScheduleExpansionFailed
345 error
346 failedIndex
347 .
348 (constructor SHA256CompressionResult SHA256CompressionFailed error failedIndex))))
349 (branch
350 SHA256BlockDecodeFailed
351 error
352 failedOrdinal
353 .
354 (constructor SHA256CompressionResult SHA256CompressionFailed error failedOrdinal)))))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.