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