1module Data.SHA256Padding
2
3import Data.Bytes
4import Data.SHA256
5import Data.SHA256Schedule
6import Model.Parameter
7import Model.Word64
8import Std.Byte
9import Std.Natural
10
11family SHA256ContextValidationTelemetry : Type 0
12constructor SHA256ContextValidationTelemetryValue
13field unrestricted sha256ValidationTotalBytes : (family ModelWord64)
14field unrestricted sha256ValidationPendingBytes : Nat
15field unrestricted sha256ValidationTotalRemainder : Nat
16field unrestricted sha256ValidationWithinLengthLimit : Nat
17
18end-family
19
20family SHA256ContextValidationResult : Type 0
21constructor SHA256ContextValidated
22field unrestricted sha256ValidatedContext : (family SHA256Context)
23field unrestricted sha256ValidationTelemetry : (family SHA256ContextValidationTelemetry)
24constructor SHA256ContextValidationFailed
25field unrestricted sha256ValidationError : (family SHA256ErrorCode)
26field unrestricted sha256FailedValidationTelemetry : (family SHA256ContextValidationTelemetry)
27
28end-family
29
30family SHA256ContextPaddingTelemetry : Type 0
31constructor SHA256ContextPaddingTelemetryValue
32field unrestricted sha256ContextPaddingTotalBytes : (family ModelWord64)
33field unrestricted sha256ContextPaddingPendingBytes : Nat
34field unrestricted sha256ContextPaddingBitLength : (family ModelWord64)
35field unrestricted sha256ContextPaddingZeroBytes : Nat
36field unrestricted sha256ContextPaddingFinalBytes : Nat
37field unrestricted sha256ContextPaddingBlockCount : Nat
38
39end-family
40
41family SHA256ContextPaddingResult : Type 0
42constructor SHA256ContextPaddingSucceeded
43field unrestricted sha256ContextPaddingSuffix : Bytes
44field unrestricted sha256ContextPaddingTelemetry : (family SHA256ContextPaddingTelemetry)
45constructor SHA256ContextPaddingFailed
46field unrestricted sha256ContextPaddingError : (family SHA256ErrorCode)
47field unrestricted sha256ContextPaddingFailureStage : Nat
48field unrestricted sha256ContextPaddingValidationTelemetry : (family SHA256ContextValidationTelemetry)
49
50end-family
51
52family SHA256LengthEncodingState : Type 0
53constructor SHA256LengthEncodingStateValue
54field unrestricted sha256LengthEncodingRemaining : Nat
55field unrestricted sha256LengthEncodingBytes : Bytes
56field unrestricted sha256LengthEncodingByteCount : Nat
57
58end-family
59
60family SHA256LengthEncodingResult : Type 0
61constructor SHA256LengthEncodingSucceeded
62field unrestricted sha256EncodedBitLength : Bytes
63field unrestricted sha256BitLengthValue : Nat
64constructor SHA256LengthEncodingFailed
65field unrestricted sha256LengthEncodingError : (family SHA256ErrorCode)
66field unrestricted sha256LengthEncodingRemainingValue : Nat
67
68end-family
69
70family SHA256PaddingTelemetry : Type 0
71constructor SHA256PaddingTelemetryValue
72field unrestricted sha256PaddingOriginalBytes : Nat
73field unrestricted sha256PaddingBitLength : Nat
74field unrestricted sha256PaddingZeroBytes : Nat
75field unrestricted sha256PaddingTotalBytes : Nat
76field unrestricted sha256PaddingBlockCount : Nat
77
78end-family
79
80family SHA256PaddingResult : Type 0
81constructor SHA256PaddingSucceeded
82field unrestricted sha256PaddedMessage : Bytes
83field unrestricted sha256PaddingTelemetry : (family SHA256PaddingTelemetry)
84constructor SHA256PaddingFailed
85field unrestricted sha256PaddingError : (family SHA256ErrorCode)
86
87end-family
88
89def sha256PaddingNaturalEight =
90 (byte-to-nat (byte 8))
91
92def sha256PaddingNaturalFiftySix =
93 (byte-to-nat (byte 56))
94
95def sha256PaddingNaturalOneHundredTwenty =
96 (byte-to-nat (byte 120))
97
98def sha256PaddingNaturalOneHundredTwentyEight =
99 (byte-to-nat (byte 128))
100
101def sha256Word64ModuloBlockBytes =
102 (lambda unrestricted value : (family ModelWord64) .
103 (eliminate
104 ModelWord64
105 (lambda unrestricted current : (family ModelWord64) . Nat)
106 value
107 (branch
108 ModelWord64Value
109 b0
110 b1
111 b2
112 b3
113 b4
114 b5
115 b6
116 b7
117 .
118 (naturalModuloUnchecked (byte-to-nat b0) sha256NaturalSixtyFour))))
119
120def sha256Word64WithinInputLimit =
121 (lambda unrestricted value : (family ModelWord64) .
122 (naturalOr
123 (modelWord64LessThan value sha256MaximumInputBytes)
124 (modelWord64Equal value sha256MaximumInputBytes)))
125
126def sha256ValidateContext =
127 (lambda unrestricted context : (family SHA256Context) .
128 (eliminate
129 SHA256Context
130 (lambda unrestricted current : (family SHA256Context) .
131 (family SHA256ContextValidationResult))
132 context
133 (branch
134 SHA256ContextValue
135 state
136 totalBytes
137 pending
138 .
139 (app
140 (lambda unrestricted pendingBytes : Nat .
141 (app
142 (lambda unrestricted totalRemainder : Nat .
143 (app
144 (lambda unrestricted withinLimit : Nat .
145 (app
146 (lambda unrestricted telemetry : (family SHA256ContextValidationTelemetry) .
147 (nat-eliminate
148 (lambda unrestricted pendingValid : Nat .
149 (family SHA256ContextValidationResult))
150 (constructor
151 SHA256ContextValidationResult
152 SHA256ContextValidationFailed
153 (constructor SHA256ErrorCode SHA256PendingBlockTooLarge)
154 telemetry)
155 (lambda unrestricted pendingPredecessor : Nat .
156 (lambda unrestricted pendingInduction : (family SHA256ContextValidationResult) .
157 (nat-eliminate
158 (lambda unrestricted lengthValid : Nat .
159 (family SHA256ContextValidationResult))
160 (constructor
161 SHA256ContextValidationResult
162 SHA256ContextValidationFailed
163 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
164 telemetry)
165 (lambda unrestricted lengthPredecessor : Nat .
166 (lambda unrestricted lengthInduction : (family SHA256ContextValidationResult) .
167 (nat-eliminate
168 (lambda unrestricted congruent : Nat .
169 (family SHA256ContextValidationResult))
170 (constructor
171 SHA256ContextValidationResult
172 SHA256ContextValidationFailed
173 (constructor SHA256ErrorCode SHA256ContextLengthMismatch)
174 telemetry)
175 (lambda unrestricted congruentPredecessor : Nat .
176 (lambda unrestricted congruentInduction : (family SHA256ContextValidationResult) .
177 (constructor
178 SHA256ContextValidationResult
179 SHA256ContextValidated
180 context
181 telemetry)))
182 (naturalEqual pendingBytes totalRemainder))))
183 withinLimit)))
184 (naturalLess pendingBytes sha256NaturalSixtyFour)))
185 (constructor
186 SHA256ContextValidationTelemetry
187 SHA256ContextValidationTelemetryValue
188 totalBytes
189 pendingBytes
190 totalRemainder
191 withinLimit)))
192 (sha256Word64WithinInputLimit totalBytes)))
193 (sha256Word64ModuloBlockBytes totalBytes)))
194 (bytes-length pending)))))
195
196def sha256ZeroBytes =
197 (lambda unrestricted count : Nat .
198 (nat-eliminate
199 (lambda unrestricted current : Nat . Bytes)
200 b""
201 (lambda unrestricted predecessor : Nat .
202 (lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction)))
203 count))
204
205def sha256LengthEncodingStep =
206 (lambda unrestricted state : (family SHA256LengthEncodingState) .
207 (eliminate
208 SHA256LengthEncodingState
209 (lambda unrestricted current : (family SHA256LengthEncodingState) .
210 (family SHA256LengthEncodingState))
211 state
212 (branch
213 SHA256LengthEncodingStateValue
214 remaining
215 encoded
216 count
217 .
218 (constructor
219 SHA256LengthEncodingState
220 SHA256LengthEncodingStateValue
221 (naturalDivideUnchecked remaining byteNaturalTwoHundredFiftySix)
222 (bytes-cons
223 (nat-to-byte (naturalModuloUnchecked remaining byteNaturalTwoHundredFiftySix))
224 encoded)
225 (succ count)))))
226
227def sha256EncodeBitLength =
228 (lambda unrestricted bitLength : Nat .
229 (eliminate
230 SHA256LengthEncodingState
231 (lambda unrestricted current : (family SHA256LengthEncodingState) .
232 (family SHA256LengthEncodingResult))
233 (app
234 (nat-eliminate
235 (lambda unrestricted current : Nat .
236 (pi unrestricted state : (family SHA256LengthEncodingState) .
237 (family SHA256LengthEncodingState)))
238 (lambda unrestricted state : (family SHA256LengthEncodingState) . state)
239 (lambda unrestricted predecessor : Nat .
240 (lambda unrestricted induction : (pi unrestricted state : (family SHA256LengthEncodingState) . (family SHA256LengthEncodingState)) .
241 (lambda unrestricted state : (family SHA256LengthEncodingState) .
242 (induction (sha256LengthEncodingStep state)))))
243 sha256PaddingNaturalEight)
244 (constructor
245 SHA256LengthEncodingState
246 SHA256LengthEncodingStateValue
247 bitLength
248 b""
249 zero))
250 (branch
251 SHA256LengthEncodingStateValue
252 remaining
253 encoded
254 count
255 .
256 (nat-eliminate
257 (lambda unrestricted remainingZero : Nat . (family SHA256LengthEncodingResult))
258 (constructor
259 SHA256LengthEncodingResult
260 SHA256LengthEncodingFailed
261 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
262 remaining)
263 (lambda unrestricted predecessor : Nat .
264 (lambda unrestricted induction : (family SHA256LengthEncodingResult) .
265 (nat-eliminate
266 (lambda unrestricted validBytes : Nat . (family SHA256LengthEncodingResult))
267 (constructor
268 SHA256LengthEncodingResult
269 SHA256LengthEncodingFailed
270 (constructor SHA256ErrorCode SHA256DigestLengthInvalid)
271 remaining)
272 (lambda unrestricted bytePredecessor : Nat .
273 (lambda unrestricted byteInduction : (family SHA256LengthEncodingResult) .
274 (constructor
275 SHA256LengthEncodingResult
276 SHA256LengthEncodingSucceeded
277 encoded
278 bitLength)))
279 (naturalEqual (bytes-length encoded) sha256PaddingNaturalEight))))
280 (naturalIsZero remaining)))))
281
282def sha256PaddingZeroCount =
283 (lambda unrestricted originalBytes : Nat .
284 (app
285 (lambda unrestricted markerExtent : Nat .
286 (app
287 (lambda unrestricted remainder : Nat .
288 (naturalSelect
289 (naturalLessOrEqual remainder sha256PaddingNaturalFiftySix)
290 (naturalSaturatingSubtract sha256PaddingNaturalFiftySix remainder)
291 (naturalSaturatingSubtract sha256PaddingNaturalOneHundredTwenty remainder)))
292 (naturalModuloUnchecked markerExtent sha256NaturalSixtyFour)))
293 (succ originalBytes)))
294
295-- Part of `sha256PadContext`, lifted out to keep it inside the §28.3 size and
296-- nesting limits; the parameters are the locals it still needs.
297def sha256PadContextPart1 =
298 (lambda unrestricted validationTelemetry : (family SHA256ContextValidationTelemetry) .
299 (lambda unrestricted totalBytes : (family ModelWord64) .
300 (lambda unrestricted bitLength : (family ModelWord64) .
301 (lambda unrestricted pendingBytes : Nat .
302 (lambda unrestricted zeroBytes : Nat .
303 (lambda unrestricted lengthBytes : Bytes .
304 (lambda unrestricted suffix : Bytes .
305 (app
306 (lambda unrestricted finalBytes : Nat .
307 (app
308 (lambda unrestricted blockCount : Nat .
309 (nat-eliminate
310 (lambda unrestricted encodedLengthValid : Nat .
311 (family SHA256ContextPaddingResult))
312 (constructor
313 SHA256ContextPaddingResult
314 SHA256ContextPaddingFailed
315 (constructor SHA256ErrorCode SHA256LengthEncodingInvalid)
316 (succ (succ zero))
317 validationTelemetry)
318 (lambda unrestricted encodedPredecessor : Nat .
319 (lambda unrestricted encodedInduction : (family SHA256ContextPaddingResult) .
320 (nat-eliminate
321 (lambda unrestricted finalLengthValid : Nat .
322 (family SHA256ContextPaddingResult))
323 (constructor
324 SHA256ContextPaddingResult
325 SHA256ContextPaddingFailed
326 (constructor SHA256ErrorCode SHA256PaddingLengthInvalid)
327 (succ (succ (succ zero)))
328 validationTelemetry)
329 (lambda unrestricted finalPredecessor : Nat .
330 (lambda unrestricted finalInduction : (family SHA256ContextPaddingResult) .
331 (constructor
332 SHA256ContextPaddingResult
333 SHA256ContextPaddingSucceeded
334 suffix
335 (constructor
336 SHA256ContextPaddingTelemetry
337 SHA256ContextPaddingTelemetryValue
338 totalBytes
339 pendingBytes
340 bitLength
341 zeroBytes
342 finalBytes
343 blockCount))))
344 (naturalOr
345 (naturalEqual finalBytes sha256NaturalSixtyFour)
346 (naturalEqual
347 finalBytes
348 sha256PaddingNaturalOneHundredTwentyEight)))))
349 (naturalEqual (bytes-length lengthBytes) sha256PaddingNaturalEight)))
350 (naturalDivideUnchecked finalBytes sha256NaturalSixtyFour)))
351 (bytes-length suffix)))))))))
352
353def sha256PadContext =
354 (lambda unrestricted context : (family SHA256Context) .
355 (eliminate
356 SHA256ContextValidationResult
357 (lambda unrestricted current : (family SHA256ContextValidationResult) .
358 (family SHA256ContextPaddingResult))
359 (sha256ValidateContext context)
360 (branch
361 SHA256ContextValidated
362 validated
363 validationTelemetry
364 .
365 (eliminate
366 SHA256Context
367 (lambda unrestricted current : (family SHA256Context) .
368 (family SHA256ContextPaddingResult))
369 validated
370 (branch
371 SHA256ContextValue
372 state
373 totalBytes
374 pending
375 .
376 (eliminate
377 ModelWord64MultiplyCheckedResult
378 (lambda unrestricted current : (family ModelWord64MultiplyCheckedResult) .
379 (family SHA256ContextPaddingResult))
380 (modelWord64MultiplyChecked totalBytes sha256Word64Eight)
381 (branch
382 ModelWord64MultiplySucceeded
383 bitLength
384 .
385 (app
386 (lambda unrestricted pendingBytes : Nat .
387 (app
388 (lambda unrestricted zeroBytes : Nat .
389 (app
390 (lambda unrestricted lengthBytes : Bytes .
391 (sha256PadContextPart1
392 validationTelemetry
393 totalBytes
394 bitLength
395 pendingBytes
396 zeroBytes
397 lengthBytes
398 (bytes-append
399 pending
400 (bytes-cons
401 (byte 128)
402 (bytes-append (sha256ZeroBytes zeroBytes) lengthBytes)))))
403 (dataBytesWord64BE bitLength)))
404 (sha256PaddingZeroCount pendingBytes)))
405 (bytes-length pending)))
406 (branch
407 ModelWord64MultiplyOverflow
408 .
409 (constructor
410 SHA256ContextPaddingResult
411 SHA256ContextPaddingFailed
412 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
413 (succ zero)
414 validationTelemetry))))))
415 (branch
416 SHA256ContextValidationFailed
417 error
418 telemetry
419 .
420 (constructor SHA256ContextPaddingResult SHA256ContextPaddingFailed error zero telemetry))))
421
422def sha256PadMessage =
423 (lambda unrestricted input : Bytes .
424 (app
425 (lambda unrestricted originalBytes : Nat .
426 (app
427 (lambda unrestricted bitLength : Nat .
428 (eliminate
429 SHA256LengthEncodingResult
430 (lambda unrestricted current : (family SHA256LengthEncodingResult) .
431 (family SHA256PaddingResult))
432 (sha256EncodeBitLength bitLength)
433 (branch
434 SHA256LengthEncodingSucceeded
435 lengthBytes
436 encodedBitLength
437 .
438 (app
439 (lambda unrestricted zeroCount : Nat .
440 (app
441 (lambda unrestricted padded : Bytes .
442 (app
443 (lambda unrestricted totalBytes : Nat .
444 (nat-eliminate
445 (lambda unrestricted aligned : Nat . (family SHA256PaddingResult))
446 (constructor
447 SHA256PaddingResult
448 SHA256PaddingFailed
449 (constructor SHA256ErrorCode SHA256BlockLengthInvalid))
450 (lambda unrestricted predecessor : Nat .
451 (lambda unrestricted induction : (family SHA256PaddingResult) .
452 (constructor
453 SHA256PaddingResult
454 SHA256PaddingSucceeded
455 padded
456 (constructor
457 SHA256PaddingTelemetry
458 SHA256PaddingTelemetryValue
459 originalBytes
460 encodedBitLength
461 zeroCount
462 totalBytes
463 (naturalDivideUnchecked totalBytes sha256NaturalSixtyFour)))))
464 (naturalIsZero
465 (naturalModuloUnchecked totalBytes sha256NaturalSixtyFour))))
466 (bytes-length padded)))
467 (bytes-append
468 input
469 (bytes-cons
470 (byte 128)
471 (bytes-append (sha256ZeroBytes zeroCount) lengthBytes)))))
472 (sha256PaddingZeroCount originalBytes)))
473 (branch
474 SHA256LengthEncodingFailed
475 error
476 remaining
477 .
478 (constructor SHA256PaddingResult SHA256PaddingFailed error))))
479 (naturalMultiply originalBytes sha256PaddingNaturalEight)))
480 (bytes-length input)))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.