1module Data.SHA256Digest
2
3import Data.Bytes
4import Data.SHA256
5import Data.SHA256Compress
6import Data.SHA256Padding
7import Data.SHA256Schedule
8import Model.Parameter
9import Model.Word64
10import Std.Foundation
11import Std.Natural
12
13family SHA256DigestTelemetry : Type 0
14constructor SHA256DigestTelemetryValue
15field unrestricted sha256DigestTelemetryInputBytes : Nat
16field unrestricted sha256DigestTelemetryPaddedBytes : Nat
17field unrestricted sha256DigestTelemetryBlocks : Nat
18field unrestricted sha256DigestTelemetryDecodedWords : Nat
19field unrestricted sha256DigestTelemetryExpandedWords : Nat
20field unrestricted sha256DigestTelemetryRounds : Nat
21field unrestricted sha256DigestTelemetryLookups : Nat
22field unrestricted sha256DigestTelemetrySigmas : Nat
23field unrestricted sha256DigestTelemetryRotates : Nat
24field unrestricted sha256DigestTelemetryShifts : Nat
25field unrestricted sha256DigestTelemetryBooleans : Nat
26field unrestricted sha256DigestTelemetryAdds : Nat
27
28end-family
29
30family SHA256DigestBlockRunResult : Type 0
31constructor SHA256DigestBlocksSucceeded
32field unrestricted sha256DigestBlockState : (family SHA256State)
33field unrestricted sha256DigestBlockTelemetry : (family SHA256DigestTelemetry)
34constructor SHA256DigestBlocksFailed
35field unrestricted sha256DigestBlockError : (family SHA256ErrorCode)
36field unrestricted sha256DigestBlockFailureOrdinal : Nat
37field unrestricted sha256DigestBlockFailureInternalIndex : Nat
38field unrestricted sha256DigestBlockTelemetryBeforeFailure : (family SHA256DigestTelemetry)
39
40end-family
41
42family SHA256DigestGroupResult : Type 0
43constructor SHA256DigestGroupSucceeded
44field unrestricted sha256DigestGroupState : (family SHA256State)
45field unrestricted sha256DigestGroupRemaining : Bytes
46field unrestricted sha256DigestGroupTelemetry : (family SHA256DigestTelemetry)
47constructor SHA256DigestGroupFailed
48field unrestricted sha256DigestGroupError : (family SHA256ErrorCode)
49field unrestricted sha256DigestGroupFailureOrdinal : Nat
50field unrestricted sha256DigestGroupFailureInternalIndex : Nat
51field unrestricted sha256DigestGroupTelemetryBeforeFailure : (family SHA256DigestTelemetry)
52
53end-family
54
55family SHA256DigestExecutionResult : Type 0
56constructor SHA256DigestExecutionSucceeded
57field unrestricted sha256DigestExecutionDigest : (family SHA256Digest)
58field unrestricted sha256DigestExecutionTelemetry : (family SHA256DigestTelemetry)
59constructor SHA256DigestExecutionFailed
60field unrestricted sha256DigestExecutionError : (family SHA256ErrorCode)
61field unrestricted sha256DigestExecutionFailureOrdinal : Nat
62field unrestricted sha256DigestExecutionTelemetryBeforeFailure : (family SHA256DigestTelemetry)
63
64end-family
65
66family SHA256HexResult : Type 0
67constructor SHA256HexSucceeded
68field unrestricted sha256HexBytes : Bytes
69field unrestricted sha256HexTelemetry : (family SHA256DigestTelemetry)
70constructor SHA256HexFailed
71field unrestricted sha256HexError : (family SHA256ErrorCode)
72field unrestricted sha256HexFailureOrdinal : Nat
73field unrestricted sha256HexTelemetryBeforeFailure : (family SHA256DigestTelemetry)
74
75end-family
76
77family SHA256NaturalWord64Result : Type 0
78constructor SHA256NaturalWord64Succeeded
79field unrestricted sha256NaturalWord64Value : (family ModelWord64)
80constructor SHA256NaturalWord64Failed
81field unrestricted sha256NaturalWord64Error : (family SHA256ErrorCode)
82
83end-family
84
85family SHA256UpdateTelemetry : Type 0
86constructor SHA256UpdateTelemetryValue
87field unrestricted sha256UpdateInputBytes : Nat
88field unrestricted sha256UpdateTotalBytesBefore : (family ModelWord64)
89field unrestricted sha256UpdatePendingBytesBefore : Nat
90field unrestricted sha256UpdateCombinedBytes : Nat
91field unrestricted sha256UpdateCompressedBytes : Nat
92field unrestricted sha256UpdateCompressedBlocks : Nat
93field unrestricted sha256UpdatePendingBytesAfter : Nat
94field unrestricted sha256UpdateTotalBytesAfter : (family ModelWord64)
95field unrestricted sha256UpdateCompressionTelemetry : (family SHA256DigestTelemetry)
96
97end-family
98
99family SHA256ContextUpdateResult : Type 0
100constructor SHA256ContextUpdateSucceeded
101field unrestricted sha256UpdatedContext : (family SHA256Context)
102field unrestricted sha256UpdateTelemetry : (family SHA256UpdateTelemetry)
103constructor SHA256ContextUpdateFailed
104field unrestricted sha256UpdateError : (family SHA256ErrorCode)
105field unrestricted sha256UpdateFailureOrdinal : Nat
106field unrestricted sha256UpdateFailureInternalIndex : Nat
107field unrestricted sha256UpdateTelemetryBeforeFailure : (family SHA256DigestTelemetry)
108
109end-family
110
111family SHA256FinalizeTelemetry : Type 0
112constructor SHA256FinalizeTelemetryValue
113field unrestricted sha256FinalizeTotalBytes : (family ModelWord64)
114field unrestricted sha256FinalizePendingBytes : Nat
115field unrestricted sha256FinalizeBitLength : (family ModelWord64)
116field unrestricted sha256FinalizeZeroBytes : Nat
117field unrestricted sha256FinalizeCompressedBytes : Nat
118field unrestricted sha256FinalizeCompressedBlocks : Nat
119field unrestricted sha256FinalizeDigestBytes : Nat
120field unrestricted sha256FinalizeCompressionTelemetry : (family SHA256DigestTelemetry)
121
122end-family
123
124family SHA256ContextFinalizeResult : Type 0
125constructor SHA256ContextFinalizeSucceeded
126field unrestricted sha256FinalizedDigest : (family SHA256Digest)
127field unrestricted sha256FinalizeTelemetry : (family SHA256FinalizeTelemetry)
128constructor SHA256ContextFinalizeFailed
129field unrestricted sha256FinalizeError : (family SHA256ErrorCode)
130field unrestricted sha256FinalizeFailureOrdinal : Nat
131field unrestricted sha256FinalizeFailureInternalIndex : Nat
132field unrestricted sha256FinalizeTelemetryBeforeFailure : (family SHA256DigestTelemetry)
133
134end-family
135
136family SHA256DigestIdentity : Type 0
137constructor SHA256DigestIdentityValue
138field unrestricted sha256DigestIdentityBinary : (family SHA256Digest)
139
140end-family
141
142family SHA256DigestIdentityResult : Type 0
143constructor SHA256DigestIdentitySucceeded
144field unrestricted sha256ValidatedDigestIdentity : (family SHA256DigestIdentity)
145constructor SHA256DigestIdentityFailed
146field unrestricted sha256DigestIdentityError : (family SHA256ErrorCode)
147
148end-family
149
150-- A first-order split of a byte string into a taken prefix and the rest, used to
151-- slice fixed-size blocks without a function-valued fold or bytes-eliminate.
152family SHA256BytesSplit : Type 0
153constructor SHA256BytesSplitValue
154field unrestricted sha256BytesSplitTaken : Bytes
155field unrestricted sha256BytesSplitRest : Bytes
156
157end-family
158
159-- Field projection for `sha256DigestTelemetryAdds`, generated from the declaration: the family
160-- has one constructor, so this is the unique total projection.
161def sha256DigestTelemetryAdds =
162 (lambda unrestricted value : (family SHA256DigestTelemetry) .
163 (eliminate
164 SHA256DigestTelemetry
165 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
166 value
167 (branch
168 SHA256DigestTelemetryValue
169 sha256DigestTelemetryInputBytes
170 sha256DigestTelemetryPaddedBytes
171 sha256DigestTelemetryBlocks
172 sha256DigestTelemetryDecodedWords
173 sha256DigestTelemetryExpandedWords
174 sha256DigestTelemetryRounds
175 sha256DigestTelemetryLookups
176 sha256DigestTelemetrySigmas
177 sha256DigestTelemetryRotates
178 sha256DigestTelemetryShifts
179 sha256DigestTelemetryBooleans
180 sha256DigestTelemetryAdds
181 .
182 sha256DigestTelemetryAdds)))
183
184-- Field projection for `sha256DigestTelemetryBooleans`, generated from the declaration: the family
185-- has one constructor, so this is the unique total projection.
186def sha256DigestTelemetryBooleans =
187 (lambda unrestricted value : (family SHA256DigestTelemetry) .
188 (eliminate
189 SHA256DigestTelemetry
190 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
191 value
192 (branch
193 SHA256DigestTelemetryValue
194 sha256DigestTelemetryInputBytes
195 sha256DigestTelemetryPaddedBytes
196 sha256DigestTelemetryBlocks
197 sha256DigestTelemetryDecodedWords
198 sha256DigestTelemetryExpandedWords
199 sha256DigestTelemetryRounds
200 sha256DigestTelemetryLookups
201 sha256DigestTelemetrySigmas
202 sha256DigestTelemetryRotates
203 sha256DigestTelemetryShifts
204 sha256DigestTelemetryBooleans
205 sha256DigestTelemetryAdds
206 .
207 sha256DigestTelemetryBooleans)))
208
209-- Field projection for `sha256DigestTelemetryDecodedWords`, generated from the declaration: the family
210-- has one constructor, so this is the unique total projection.
211def sha256DigestTelemetryDecodedWords =
212 (lambda unrestricted value : (family SHA256DigestTelemetry) .
213 (eliminate
214 SHA256DigestTelemetry
215 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
216 value
217 (branch
218 SHA256DigestTelemetryValue
219 sha256DigestTelemetryInputBytes
220 sha256DigestTelemetryPaddedBytes
221 sha256DigestTelemetryBlocks
222 sha256DigestTelemetryDecodedWords
223 sha256DigestTelemetryExpandedWords
224 sha256DigestTelemetryRounds
225 sha256DigestTelemetryLookups
226 sha256DigestTelemetrySigmas
227 sha256DigestTelemetryRotates
228 sha256DigestTelemetryShifts
229 sha256DigestTelemetryBooleans
230 sha256DigestTelemetryAdds
231 .
232 sha256DigestTelemetryDecodedWords)))
233
234-- Field projection for `sha256DigestTelemetryExpandedWords`, generated from the declaration: the family
235-- has one constructor, so this is the unique total projection.
236def sha256DigestTelemetryExpandedWords =
237 (lambda unrestricted value : (family SHA256DigestTelemetry) .
238 (eliminate
239 SHA256DigestTelemetry
240 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
241 value
242 (branch
243 SHA256DigestTelemetryValue
244 sha256DigestTelemetryInputBytes
245 sha256DigestTelemetryPaddedBytes
246 sha256DigestTelemetryBlocks
247 sha256DigestTelemetryDecodedWords
248 sha256DigestTelemetryExpandedWords
249 sha256DigestTelemetryRounds
250 sha256DigestTelemetryLookups
251 sha256DigestTelemetrySigmas
252 sha256DigestTelemetryRotates
253 sha256DigestTelemetryShifts
254 sha256DigestTelemetryBooleans
255 sha256DigestTelemetryAdds
256 .
257 sha256DigestTelemetryExpandedWords)))
258
259-- Field projection for `sha256DigestTelemetryInputBytes`, generated from the declaration: the family
260-- has one constructor, so this is the unique total projection.
261def sha256DigestTelemetryInputBytes =
262 (lambda unrestricted value : (family SHA256DigestTelemetry) .
263 (eliminate
264 SHA256DigestTelemetry
265 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
266 value
267 (branch
268 SHA256DigestTelemetryValue
269 sha256DigestTelemetryInputBytes
270 sha256DigestTelemetryPaddedBytes
271 sha256DigestTelemetryBlocks
272 sha256DigestTelemetryDecodedWords
273 sha256DigestTelemetryExpandedWords
274 sha256DigestTelemetryRounds
275 sha256DigestTelemetryLookups
276 sha256DigestTelemetrySigmas
277 sha256DigestTelemetryRotates
278 sha256DigestTelemetryShifts
279 sha256DigestTelemetryBooleans
280 sha256DigestTelemetryAdds
281 .
282 sha256DigestTelemetryInputBytes)))
283
284-- Field projection for `sha256DigestTelemetryLookups`, generated from the declaration: the family
285-- has one constructor, so this is the unique total projection.
286def sha256DigestTelemetryLookups =
287 (lambda unrestricted value : (family SHA256DigestTelemetry) .
288 (eliminate
289 SHA256DigestTelemetry
290 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
291 value
292 (branch
293 SHA256DigestTelemetryValue
294 sha256DigestTelemetryInputBytes
295 sha256DigestTelemetryPaddedBytes
296 sha256DigestTelemetryBlocks
297 sha256DigestTelemetryDecodedWords
298 sha256DigestTelemetryExpandedWords
299 sha256DigestTelemetryRounds
300 sha256DigestTelemetryLookups
301 sha256DigestTelemetrySigmas
302 sha256DigestTelemetryRotates
303 sha256DigestTelemetryShifts
304 sha256DigestTelemetryBooleans
305 sha256DigestTelemetryAdds
306 .
307 sha256DigestTelemetryLookups)))
308
309-- Field projection for `sha256DigestTelemetryPaddedBytes`, generated from the declaration: the family
310-- has one constructor, so this is the unique total projection.
311def sha256DigestTelemetryPaddedBytes =
312 (lambda unrestricted value : (family SHA256DigestTelemetry) .
313 (eliminate
314 SHA256DigestTelemetry
315 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
316 value
317 (branch
318 SHA256DigestTelemetryValue
319 sha256DigestTelemetryInputBytes
320 sha256DigestTelemetryPaddedBytes
321 sha256DigestTelemetryBlocks
322 sha256DigestTelemetryDecodedWords
323 sha256DigestTelemetryExpandedWords
324 sha256DigestTelemetryRounds
325 sha256DigestTelemetryLookups
326 sha256DigestTelemetrySigmas
327 sha256DigestTelemetryRotates
328 sha256DigestTelemetryShifts
329 sha256DigestTelemetryBooleans
330 sha256DigestTelemetryAdds
331 .
332 sha256DigestTelemetryPaddedBytes)))
333
334-- Field projection for `sha256DigestTelemetryRotates`, generated from the declaration: the family
335-- has one constructor, so this is the unique total projection.
336def sha256DigestTelemetryRotates =
337 (lambda unrestricted value : (family SHA256DigestTelemetry) .
338 (eliminate
339 SHA256DigestTelemetry
340 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
341 value
342 (branch
343 SHA256DigestTelemetryValue
344 sha256DigestTelemetryInputBytes
345 sha256DigestTelemetryPaddedBytes
346 sha256DigestTelemetryBlocks
347 sha256DigestTelemetryDecodedWords
348 sha256DigestTelemetryExpandedWords
349 sha256DigestTelemetryRounds
350 sha256DigestTelemetryLookups
351 sha256DigestTelemetrySigmas
352 sha256DigestTelemetryRotates
353 sha256DigestTelemetryShifts
354 sha256DigestTelemetryBooleans
355 sha256DigestTelemetryAdds
356 .
357 sha256DigestTelemetryRotates)))
358
359-- Field projection for `sha256DigestTelemetryRounds`, generated from the declaration: the family
360-- has one constructor, so this is the unique total projection.
361def sha256DigestTelemetryRounds =
362 (lambda unrestricted value : (family SHA256DigestTelemetry) .
363 (eliminate
364 SHA256DigestTelemetry
365 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
366 value
367 (branch
368 SHA256DigestTelemetryValue
369 sha256DigestTelemetryInputBytes
370 sha256DigestTelemetryPaddedBytes
371 sha256DigestTelemetryBlocks
372 sha256DigestTelemetryDecodedWords
373 sha256DigestTelemetryExpandedWords
374 sha256DigestTelemetryRounds
375 sha256DigestTelemetryLookups
376 sha256DigestTelemetrySigmas
377 sha256DigestTelemetryRotates
378 sha256DigestTelemetryShifts
379 sha256DigestTelemetryBooleans
380 sha256DigestTelemetryAdds
381 .
382 sha256DigestTelemetryRounds)))
383
384-- Field projection for `sha256DigestTelemetryShifts`, generated from the declaration: the family
385-- has one constructor, so this is the unique total projection.
386def sha256DigestTelemetryShifts =
387 (lambda unrestricted value : (family SHA256DigestTelemetry) .
388 (eliminate
389 SHA256DigestTelemetry
390 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
391 value
392 (branch
393 SHA256DigestTelemetryValue
394 sha256DigestTelemetryInputBytes
395 sha256DigestTelemetryPaddedBytes
396 sha256DigestTelemetryBlocks
397 sha256DigestTelemetryDecodedWords
398 sha256DigestTelemetryExpandedWords
399 sha256DigestTelemetryRounds
400 sha256DigestTelemetryLookups
401 sha256DigestTelemetrySigmas
402 sha256DigestTelemetryRotates
403 sha256DigestTelemetryShifts
404 sha256DigestTelemetryBooleans
405 sha256DigestTelemetryAdds
406 .
407 sha256DigestTelemetryShifts)))
408
409-- Field projection for `sha256DigestTelemetrySigmas`, generated from the declaration: the family
410-- has one constructor, so this is the unique total projection.
411def sha256DigestTelemetrySigmas =
412 (lambda unrestricted value : (family SHA256DigestTelemetry) .
413 (eliminate
414 SHA256DigestTelemetry
415 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
416 value
417 (branch
418 SHA256DigestTelemetryValue
419 sha256DigestTelemetryInputBytes
420 sha256DigestTelemetryPaddedBytes
421 sha256DigestTelemetryBlocks
422 sha256DigestTelemetryDecodedWords
423 sha256DigestTelemetryExpandedWords
424 sha256DigestTelemetryRounds
425 sha256DigestTelemetryLookups
426 sha256DigestTelemetrySigmas
427 sha256DigestTelemetryRotates
428 sha256DigestTelemetryShifts
429 sha256DigestTelemetryBooleans
430 sha256DigestTelemetryAdds
431 .
432 sha256DigestTelemetrySigmas)))
433
434-- Field projection (fields do not create definitions).
435def sha256DigestTelemetryBlocks =
436 (lambda unrestricted value : (family SHA256DigestTelemetry) .
437 (eliminate
438 SHA256DigestTelemetry
439 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
440 value
441 (branch
442 SHA256DigestTelemetryValue
443 sha256DigestTelemetryInputBytes
444 sha256DigestTelemetryPaddedBytes
445 sha256DigestTelemetryBlocksField
446 sha256DigestTelemetryDecodedWords
447 sha256DigestTelemetryExpandedWords
448 sha256DigestTelemetryRounds
449 sha256DigestTelemetryLookups
450 sha256DigestTelemetrySigmas
451 sha256DigestTelemetryRotates
452 sha256DigestTelemetryShifts
453 sha256DigestTelemetryBooleans
454 sha256DigestTelemetryAdds
455 .
456 sha256DigestTelemetryBlocksField)))
457
458def sha256DigestTelemetryInitial =
459 (lambda unrestricted inputBytes : Nat .
460 (lambda unrestricted paddedBytes : Nat .
461 (constructor
462 SHA256DigestTelemetry
463 SHA256DigestTelemetryValue
464 inputBytes
465 paddedBytes
466 zero
467 zero
468 zero
469 zero
470 zero
471 zero
472 zero
473 zero
474 zero
475 zero)))
476
477-- The per-block counts come FIRST: `naturalAdd` folds over its first argument,
478-- so adding the running total the other way round made every block cost the
479-- total so far (quadratic; D17 measurement: 27 min for 240 KB).
480def sha256DigestTelemetryAddCompression =
481 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
482 (lambda unrestricted compression : (family SHA256CompressionTelemetry) .
483 (eliminate
484 SHA256DigestTelemetry
485 (lambda unrestricted current : (family SHA256DigestTelemetry) .
486 (family SHA256DigestTelemetry))
487 telemetry
488 (branch
489 SHA256DigestTelemetryValue
490 inputBytes
491 paddedBytes
492 blocks
493 decoded
494 expanded
495 rounds
496 lookups
497 sigmas
498 rotates
499 shifts
500 booleans
501 adds
502 .
503 (eliminate
504 SHA256CompressionTelemetry
505 (lambda unrestricted current : (family SHA256CompressionTelemetry) .
506 (family SHA256DigestTelemetry))
507 compression
508 (branch
509 SHA256CompressionTelemetryValue
510 nextDecoded
511 nextExpanded
512 nextRounds
513 nextLookups
514 nextSigmas
515 nextRotates
516 nextShifts
517 nextBooleans
518 nextAdds
519 .
520 (constructor
521 SHA256DigestTelemetry
522 SHA256DigestTelemetryValue
523 inputBytes
524 paddedBytes
525 (succ blocks)
526 (naturalAdd nextDecoded decoded)
527 (naturalAdd nextExpanded expanded)
528 (naturalAdd nextRounds rounds)
529 (naturalAdd nextLookups lookups)
530 (naturalAdd nextSigmas sigmas)
531 (naturalAdd nextRotates rotates)
532 (naturalAdd nextShifts shifts)
533 (naturalAdd nextBooleans booleans)
534 (naturalAdd nextAdds adds))))))))
535
536def sha256DigestTelemetryCombine =
537 (lambda unrestricted inputBytes : Nat .
538 (lambda unrestricted paddedBytes : Nat .
539 (lambda unrestricted left : (family SHA256DigestTelemetry) .
540 (lambda unrestricted right : (family SHA256DigestTelemetry) .
541 (eliminate
542 SHA256DigestTelemetry
543 (lambda unrestricted current : (family SHA256DigestTelemetry) .
544 (family SHA256DigestTelemetry))
545 left
546 (branch
547 SHA256DigestTelemetryValue
548 leftInput
549 leftPadded
550 leftBlocks
551 leftDecoded
552 leftExpanded
553 leftRounds
554 leftLookups
555 leftSigmas
556 leftRotates
557 leftShifts
558 leftBooleans
559 leftAdds
560 .
561 (eliminate
562 SHA256DigestTelemetry
563 (lambda unrestricted current : (family SHA256DigestTelemetry) .
564 (family SHA256DigestTelemetry))
565 right
566 (branch
567 SHA256DigestTelemetryValue
568 rightInput
569 rightPadded
570 rightBlocks
571 rightDecoded
572 rightExpanded
573 rightRounds
574 rightLookups
575 rightSigmas
576 rightRotates
577 rightShifts
578 rightBooleans
579 rightAdds
580 .
581 (constructor
582 SHA256DigestTelemetry
583 SHA256DigestTelemetryValue
584 inputBytes
585 paddedBytes
586 (naturalAdd leftBlocks rightBlocks)
587 (naturalAdd leftDecoded rightDecoded)
588 (naturalAdd leftExpanded rightExpanded)
589 (naturalAdd leftRounds rightRounds)
590 (naturalAdd leftLookups rightLookups)
591 (naturalAdd leftSigmas rightSigmas)
592 (naturalAdd leftRotates rightRotates)
593 (naturalAdd leftShifts rightShifts)
594 (naturalAdd leftBooleans rightBooleans)
595 (naturalAdd leftAdds rightAdds))))))))))
596
597def sha256DigestTelemetryBlockCount =
598 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
599 (eliminate
600 SHA256DigestTelemetry
601 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
602 telemetry
603 (branch
604 SHA256DigestTelemetryValue
605 input
606 padded
607 blocks
608 decoded
609 expanded
610 rounds
611 lookups
612 sigmas
613 rotates
614 shifts
615 booleans
616 adds
617 .
618 blocks)))
619
620def sha256DigestTelemetryPaddedCount =
621 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
622 (eliminate
623 SHA256DigestTelemetry
624 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
625 telemetry
626 (branch
627 SHA256DigestTelemetryValue
628 input
629 padded
630 blocks
631 decoded
632 expanded
633 rounds
634 lookups
635 sigmas
636 rotates
637 shifts
638 booleans
639 adds
640 .
641 padded)))
642
643-- First-order prefix take.
644--
645-- The previous definition folded a FUNCTION accumulator (`pi input . Bytes`) and,
646-- worse, used `bytes-eliminate` inside the step. The VM's bytes recursor EAGERLY
647-- evaluates the tail's recursive result before the branch (which ignores it)
648-- runs, so composing it under the fuel fold re-walked every suffix at every
649-- level -- an exponential that made even `take 64` of a 64-byte LITERAL cost
650-- minutes and gigabytes, which then fed a non-literal block into decode/expand
651-- and blew those up in turn. This version folds a FIRST-ORDER value accumulator
652-- (taken prefix + remaining bytes) built only from the O(1) native primitives
653-- bytes-head / bytes-tail / bytes-cons / bytes-append, so a take over a literal
654-- stays a literal and costs O(fuel^2) bounded work. For the 64-aligned blocks the
655-- digest driver slices, the bytes produced are identical, so the digest is
656-- preserved exactly.
657def sha256DigestTakeWithFuel =
658 (lambda unrestricted fuel : Nat .
659 (lambda unrestricted input : Bytes .
660 (eliminate
661 SHA256BytesSplit
662 (lambda unrestricted current : (family SHA256BytesSplit) . Bytes)
663 (nat-eliminate
664 (lambda unrestricted current : Nat . (family SHA256BytesSplit))
665 (constructor SHA256BytesSplit SHA256BytesSplitValue b"" input)
666 (lambda unrestricted predecessor : Nat .
667 (lambda unrestricted induction : (family SHA256BytesSplit) .
668 (eliminate
669 SHA256BytesSplit
670 (lambda unrestricted current : (family SHA256BytesSplit) .
671 (family SHA256BytesSplit))
672 induction
673 (branch
674 SHA256BytesSplitValue
675 taken
676 rest
677 .
678 (constructor
679 SHA256BytesSplit
680 SHA256BytesSplitValue
681 (bytes-append taken (bytes-cons (bytes-head rest) b""))
682 (bytes-tail rest))))))
683 fuel)
684 (branch SHA256BytesSplitValue taken rest . taken))))
685
686-- First-order drop: peel `fuel` bytes with the native O(1) bytes-tail instead of
687-- the higher-order `bytes-eliminate` fold (same exponential as take above). On a
688-- literal the result stays a literal.
689def sha256DigestDropWithFuel =
690 (lambda unrestricted fuel : Nat .
691 (lambda unrestricted input : Bytes .
692 (nat-eliminate
693 (lambda unrestricted current : Nat . Bytes)
694 input
695 (lambda unrestricted predecessor : Nat .
696 (lambda unrestricted induction : Bytes . (bytes-tail induction)))
697 fuel)))
698
699-- D18: the block loop runs as an outer fold over GROUPS of blocks with an
700-- inner fold over one group, so the garbage of a group is reclaimed when the
701-- group ends instead of the whole message's garbage staying resident (the
702-- flat loop held 8.7 GB for a 240 KB message).
703def sha256DigestBlocksPerGroup : Nat =
704 32
705
706-- Compress `count` blocks off the front of `input`, returning the state and
707-- what is left (no length check: the caller sizes the groups).
708def sha256DigestRunBlockGroup =
709 (lambda unrestricted count : Nat .
710 (nat-eliminate
711 (lambda unrestricted current : Nat .
712 (pi unrestricted state : (family SHA256State) .
713 (pi unrestricted input : Bytes .
714 (pi unrestricted telemetry : (family SHA256DigestTelemetry) .
715 (family SHA256DigestGroupResult)))))
716 (lambda unrestricted state : (family SHA256State) .
717 (lambda unrestricted input : Bytes .
718 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
719 (constructor SHA256DigestGroupResult SHA256DigestGroupSucceeded state input telemetry))))
720 (lambda unrestricted predecessor : Nat .
721 (lambda unrestricted induction : (pi unrestricted state : (family SHA256State) . (pi unrestricted input : Bytes . (pi unrestricted telemetry : (family SHA256DigestTelemetry) . (family SHA256DigestGroupResult)))) .
722 (lambda unrestricted state : (family SHA256State) .
723 (lambda unrestricted input : Bytes .
724 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
725 (eliminate
726 SHA256CompressionResult
727 (lambda unrestricted current : (family SHA256CompressionResult) .
728 (family SHA256DigestGroupResult))
729 (sha256CompressBlock
730 state
731 (sha256DigestTakeWithFuel sha256NaturalSixtyFour input))
732 (branch
733 SHA256CompressionSucceeded
734 nextState
735 compressionTelemetry
736 .
737 (induction
738 nextState
739 (sha256DigestDropWithFuel sha256NaturalSixtyFour input)
740 (sha256DigestTelemetryAddCompression telemetry compressionTelemetry)))
741 (branch
742 SHA256CompressionFailed
743 error
744 failedIndex
745 .
746 (constructor
747 SHA256DigestGroupResult
748 SHA256DigestGroupFailed
749 error
750 (sha256DigestTelemetryBlockCount telemetry)
751 failedIndex
752 telemetry))))))))
753 count))
754
755-- `groups` full groups, then the remainder group of `rest` blocks.
756def sha256DigestRunBlockGroups =
757 (lambda unrestricted groups : Nat .
758 (lambda unrestricted rest : Nat .
759 (nat-eliminate
760 (lambda unrestricted current : Nat .
761 (pi unrestricted state : (family SHA256State) .
762 (pi unrestricted input : Bytes .
763 (pi unrestricted telemetry : (family SHA256DigestTelemetry) .
764 (family SHA256DigestGroupResult)))))
765 (sha256DigestRunBlockGroup rest)
766 (lambda unrestricted predecessor : Nat .
767 (lambda unrestricted induction : (pi unrestricted state : (family SHA256State) . (pi unrestricted input : Bytes . (pi unrestricted telemetry : (family SHA256DigestTelemetry) . (family SHA256DigestGroupResult)))) .
768 (lambda unrestricted state : (family SHA256State) .
769 (lambda unrestricted input : Bytes .
770 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
771 (eliminate
772 SHA256DigestGroupResult
773 (lambda unrestricted current : (family SHA256DigestGroupResult) .
774 (family SHA256DigestGroupResult))
775 (sha256DigestRunBlockGroup sha256DigestBlocksPerGroup state input telemetry)
776 (branch
777 SHA256DigestGroupSucceeded
778 nextState
779 remaining
780 nextTelemetry
781 .
782 (induction nextState remaining nextTelemetry))
783 (branch
784 SHA256DigestGroupFailed
785 error
786 ordinal
787 internalIndex
788 before
789 .
790 (constructor
791 SHA256DigestGroupResult
792 SHA256DigestGroupFailed
793 error
794 ordinal
795 internalIndex
796 before))))))))
797 groups)))
798
799-- The public shape is unchanged: exactly `blockCount` blocks must consume the
800-- whole input, or the run fails with SHA256BlockLengthInvalid.
801def sha256DigestRunBlocks =
802 (lambda unrestricted blockCount : Nat .
803 (lambda unrestricted state : (family SHA256State) .
804 (lambda unrestricted input : Bytes .
805 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
806 (eliminate
807 SHA256DigestGroupResult
808 (lambda unrestricted current : (family SHA256DigestGroupResult) .
809 (family SHA256DigestBlockRunResult))
810 (sha256DigestRunBlockGroups
811 (naturalDivideUnchecked blockCount sha256DigestBlocksPerGroup)
812 (naturalModuloUnchecked blockCount sha256DigestBlocksPerGroup)
813 state
814 input
815 telemetry)
816 (branch
817 SHA256DigestGroupSucceeded
818 finalState
819 remaining
820 finalTelemetry
821 .
822 (nat-eliminate
823 (lambda unrestricted empty : Nat . (family SHA256DigestBlockRunResult))
824 (constructor
825 SHA256DigestBlockRunResult
826 SHA256DigestBlocksFailed
827 (constructor SHA256ErrorCode SHA256BlockLengthInvalid)
828 (sha256DigestTelemetryBlockCount finalTelemetry)
829 zero
830 finalTelemetry)
831 (lambda unrestricted predecessor : Nat .
832 (lambda unrestricted induction : (family SHA256DigestBlockRunResult) .
833 (constructor
834 SHA256DigestBlockRunResult
835 SHA256DigestBlocksSucceeded
836 finalState
837 finalTelemetry)))
838 (naturalIsZero (bytes-length remaining))))
839 (branch
840 SHA256DigestGroupFailed
841 error
842 ordinal
843 internalIndex
844 before
845 .
846 (constructor
847 SHA256DigestBlockRunResult
848 SHA256DigestBlocksFailed
849 error
850 ordinal
851 internalIndex
852 before)))))))
853
854def sha256DigestStateBytes =
855 (lambda unrestricted state : (family SHA256State) .
856 (eliminate
857 SHA256State
858 (lambda unrestricted current : (family SHA256State) . Bytes)
859 state
860 (branch
861 SHA256StateValue
862 w0
863 w1
864 w2
865 w3
866 w4
867 w5
868 w6
869 w7
870 .
871 (bytes-builder-build
872 (bytes-builder-append
873 (bytes-builder-chunk (dataBytesWord32BE w0))
874 (bytes-builder-append
875 (bytes-builder-chunk (dataBytesWord32BE w1))
876 (bytes-builder-append
877 (bytes-builder-chunk (dataBytesWord32BE w2))
878 (bytes-builder-append
879 (bytes-builder-chunk (dataBytesWord32BE w3))
880 (bytes-builder-append
881 (bytes-builder-chunk (dataBytesWord32BE w4))
882 (bytes-builder-append
883 (bytes-builder-chunk (dataBytesWord32BE w5))
884 (bytes-builder-append
885 (bytes-builder-chunk (dataBytesWord32BE w6))
886 (bytes-builder-chunk (dataBytesWord32BE w7)))))))))))))
887
888def sha256NaturalToWord64 =
889 (lambda unrestricted value : Nat .
890 (eliminate
891 SHA256LengthEncodingResult
892 (lambda unrestricted current : (family SHA256LengthEncodingResult) .
893 (family SHA256NaturalWord64Result))
894 (sha256EncodeBitLength value)
895 (branch
896 SHA256LengthEncodingSucceeded
897 encoded
898 encodedValue
899 .
900 (eliminate
901 DataBytesWord64DecodeResult
902 (lambda unrestricted current : (family DataBytesWord64DecodeResult) .
903 (family SHA256NaturalWord64Result))
904 (dataBytesReadWord64BE encoded)
905 (branch
906 DataBytesWord64Decoded
907 word
908 remaining
909 .
910 (nat-eliminate
911 (lambda unrestricted empty : Nat . (family SHA256NaturalWord64Result))
912 (constructor
913 SHA256NaturalWord64Result
914 SHA256NaturalWord64Failed
915 (constructor SHA256ErrorCode SHA256LengthEncodingInvalid))
916 (lambda unrestricted predecessor : Nat .
917 (lambda unrestricted induction : (family SHA256NaturalWord64Result) .
918 (constructor SHA256NaturalWord64Result SHA256NaturalWord64Succeeded word)))
919 (naturalIsZero (bytes-length remaining))))
920 (branch
921 DataBytesWord64DecodeFailed
922 decodeError
923 .
924 (constructor
925 SHA256NaturalWord64Result
926 SHA256NaturalWord64Failed
927 (constructor SHA256ErrorCode SHA256LengthEncodingInvalid)))))
928 (branch
929 SHA256LengthEncodingFailed
930 error
931 remaining
932 .
933 (constructor SHA256NaturalWord64Result SHA256NaturalWord64Failed error))))
934
935-- Part of `sha256Update`, lifted out to keep it inside the §28.3 size and
936-- nesting limits; the parameters are the locals it still needs.
937def sha256UpdatePart1 =
938 (lambda unrestricted state : (family SHA256State) .
939 (lambda unrestricted totalBytes : (family ModelWord64) .
940 (lambda unrestricted inputBytes : Nat .
941 (lambda unrestricted nextTotalBytes : (family ModelWord64) .
942 (lambda unrestricted pendingBefore : Nat .
943 (lambda unrestricted combined : Bytes .
944 (lambda unrestricted combinedBytes : Nat .
945 (lambda unrestricted compressedBytes : Nat .
946 (lambda unrestricted compressedBlocks : Nat .
947 (app
948 (lambda unrestricted compressed : Bytes .
949 (app
950 (lambda unrestricted nextPending : Bytes .
951 (app
952 (lambda unrestricted operations : (family SHA256DigestTelemetry) .
953 (eliminate
954 SHA256DigestBlockRunResult
955 (lambda unrestricted current : (family SHA256DigestBlockRunResult) .
956 (family SHA256ContextUpdateResult))
957 (sha256DigestRunBlocks
958 compressedBlocks
959 state
960 compressed
961 operations)
962 (branch
963 SHA256DigestBlocksSucceeded
964 nextState
965 nextOperations
966 .
967 (app
968 (lambda unrestricted nextContext : (family SHA256Context) .
969 (eliminate
970 SHA256ContextValidationResult
971 (lambda unrestricted current : (family SHA256ContextValidationResult) .
972 (family SHA256ContextUpdateResult))
973 (sha256ValidateContext nextContext)
974 (branch
975 SHA256ContextValidated
976 checkedContext
977 checkedTelemetry
978 .
979 (constructor
980 SHA256ContextUpdateResult
981 SHA256ContextUpdateSucceeded
982 checkedContext
983 (constructor
984 SHA256UpdateTelemetry
985 SHA256UpdateTelemetryValue
986 inputBytes
987 totalBytes
988 pendingBefore
989 combinedBytes
990 compressedBytes
991 compressedBlocks
992 (bytes-length nextPending)
993 nextTotalBytes
994 nextOperations)))
995 (branch
996 SHA256ContextValidationFailed
997 nextError
998 nextValidation
999 .
1000 (constructor
1001 SHA256ContextUpdateResult
1002 SHA256ContextUpdateFailed
1003 nextError
1004 compressedBlocks
1005 zero
1006 nextOperations))))
1007 (constructor
1008 SHA256Context
1009 SHA256ContextValue
1010 nextState
1011 nextTotalBytes
1012 nextPending)))
1013 (branch
1014 SHA256DigestBlocksFailed
1015 blockError
1016 blockOrdinal
1017 internalIndex
1018 partialTelemetry
1019 .
1020 (constructor
1021 SHA256ContextUpdateResult
1022 SHA256ContextUpdateFailed
1023 blockError
1024 blockOrdinal
1025 internalIndex
1026 partialTelemetry))))
1027 (sha256DigestTelemetryInitial inputBytes compressedBytes)))
1028 (sha256DigestDropWithFuel compressedBytes combined)))
1029 (sha256DigestTakeWithFuel compressedBytes combined)))))))))))
1030
1031-- Part of `sha256Update`, lifted out to keep it inside the §28.3 size and
1032-- nesting limits; the parameters are the locals it still needs.
1033def sha256UpdatePart2 =
1034 (lambda unrestricted input : Bytes .
1035 (lambda unrestricted state : (family SHA256State) .
1036 (lambda unrestricted totalBytes : (family ModelWord64) .
1037 (lambda unrestricted pending : Bytes .
1038 (lambda unrestricted inputBytes : Nat .
1039 (lambda unrestricted nextTotalBytes : (family ModelWord64) .
1040 (lambda unrestricted pendingBefore : Nat .
1041 (app
1042 (lambda unrestricted combined : Bytes .
1043 (app
1044 (lambda unrestricted combinedBytes : Nat .
1045 (app
1046 (lambda unrestricted compressedBytes : Nat .
1047 (sha256UpdatePart1
1048 state
1049 totalBytes
1050 inputBytes
1051 nextTotalBytes
1052 pendingBefore
1053 combined
1054 combinedBytes
1055 compressedBytes
1056 (naturalDivideUnchecked compressedBytes sha256NaturalSixtyFour)))
1057 (naturalSaturatingSubtract
1058 combinedBytes
1059 (naturalModuloUnchecked combinedBytes sha256NaturalSixtyFour))))
1060 (bytes-length combined)))
1061 (bytes-append pending input)))))))))
1062
1063def sha256Update =
1064 (lambda unrestricted context : (family SHA256Context) .
1065 (lambda unrestricted input : Bytes .
1066 (eliminate
1067 SHA256ContextValidationResult
1068 (lambda unrestricted current : (family SHA256ContextValidationResult) .
1069 (family SHA256ContextUpdateResult))
1070 (sha256ValidateContext context)
1071 (branch
1072 SHA256ContextValidated
1073 validated
1074 validationTelemetry
1075 .
1076 (eliminate
1077 SHA256Context
1078 (lambda unrestricted current : (family SHA256Context) .
1079 (family SHA256ContextUpdateResult))
1080 validated
1081 (branch
1082 SHA256ContextValue
1083 state
1084 totalBytes
1085 pending
1086 .
1087 (app
1088 (lambda unrestricted inputBytes : Nat .
1089 (eliminate
1090 SHA256NaturalWord64Result
1091 (lambda unrestricted current : (family SHA256NaturalWord64Result) .
1092 (family SHA256ContextUpdateResult))
1093 (sha256NaturalToWord64 inputBytes)
1094 (branch
1095 SHA256NaturalWord64Succeeded
1096 inputWord64
1097 .
1098 (eliminate
1099 ModelWord64CheckedResult
1100 (lambda unrestricted current : (family ModelWord64CheckedResult) .
1101 (family SHA256ContextUpdateResult))
1102 (modelWord64AddChecked totalBytes inputWord64)
1103 (branch
1104 ModelWord64CheckedSucceeded
1105 nextTotalBytes
1106 .
1107 (nat-eliminate
1108 (lambda unrestricted withinLimit : Nat .
1109 (family SHA256ContextUpdateResult))
1110 (constructor
1111 SHA256ContextUpdateResult
1112 SHA256ContextUpdateFailed
1113 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
1114 zero
1115 zero
1116 (sha256DigestTelemetryInitial inputBytes zero))
1117 (lambda unrestricted limitPredecessor : Nat .
1118 (lambda unrestricted limitInduction : (family SHA256ContextUpdateResult) .
1119 (sha256UpdatePart2
1120 input
1121 state
1122 totalBytes
1123 pending
1124 inputBytes
1125 nextTotalBytes
1126 (bytes-length pending))))
1127 (sha256Word64WithinInputLimit nextTotalBytes)))
1128 (branch
1129 ModelWord64CheckedFailed
1130 arithmeticError
1131 .
1132 (constructor
1133 SHA256ContextUpdateResult
1134 SHA256ContextUpdateFailed
1135 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
1136 zero
1137 zero
1138 (sha256DigestTelemetryInitial inputBytes zero)))))
1139 (branch
1140 SHA256NaturalWord64Failed
1141 error
1142 .
1143 (constructor
1144 SHA256ContextUpdateResult
1145 SHA256ContextUpdateFailed
1146 error
1147 zero
1148 zero
1149 (sha256DigestTelemetryInitial inputBytes zero)))))
1150 (bytes-length input)))))
1151 (branch
1152 SHA256ContextValidationFailed
1153 error
1154 validationTelemetry
1155 .
1156 (constructor
1157 SHA256ContextUpdateResult
1158 SHA256ContextUpdateFailed
1159 error
1160 zero
1161 zero
1162 (sha256DigestTelemetryInitial (bytes-length input) zero))))))
1163
1164def sha256Finalize =
1165 (lambda unrestricted context : (family SHA256Context) .
1166 (eliminate
1167 SHA256Context
1168 (lambda unrestricted current : (family SHA256Context) . (family SHA256ContextFinalizeResult))
1169 context
1170 (branch
1171 SHA256ContextValue
1172 state
1173 totalBytes
1174 pending
1175 .
1176 (eliminate
1177 SHA256ContextPaddingResult
1178 (lambda unrestricted current : (family SHA256ContextPaddingResult) .
1179 (family SHA256ContextFinalizeResult))
1180 (sha256PadContext context)
1181 (branch
1182 SHA256ContextPaddingSucceeded
1183 suffix
1184 paddingTelemetry
1185 .
1186 (eliminate
1187 SHA256ContextPaddingTelemetry
1188 (lambda unrestricted current : (family SHA256ContextPaddingTelemetry) .
1189 (family SHA256ContextFinalizeResult))
1190 paddingTelemetry
1191 (branch
1192 SHA256ContextPaddingTelemetryValue
1193 checkedTotal
1194 pendingBytes
1195 bitLength
1196 zeroBytes
1197 finalBytes
1198 blockCount
1199 .
1200 (app
1201 (lambda unrestricted operations : (family SHA256DigestTelemetry) .
1202 (eliminate
1203 SHA256DigestBlockRunResult
1204 (lambda unrestricted current : (family SHA256DigestBlockRunResult) .
1205 (family SHA256ContextFinalizeResult))
1206 (sha256DigestRunBlocks blockCount state suffix operations)
1207 (branch
1208 SHA256DigestBlocksSucceeded
1209 finalState
1210 finalOperations
1211 .
1212 (app
1213 (lambda unrestricted digestBytes : Bytes .
1214 (eliminate
1215 SHA256Result
1216 (lambda unrestricted current : (family SHA256Result) .
1217 (family SHA256ContextFinalizeResult))
1218 (sha256DigestFromBytes digestBytes)
1219 (branch
1220 SHA256Succeeded
1221 digest
1222 .
1223 (constructor
1224 SHA256ContextFinalizeResult
1225 SHA256ContextFinalizeSucceeded
1226 digest
1227 (constructor
1228 SHA256FinalizeTelemetry
1229 SHA256FinalizeTelemetryValue
1230 checkedTotal
1231 pendingBytes
1232 bitLength
1233 zeroBytes
1234 finalBytes
1235 blockCount
1236 (bytes-length digestBytes)
1237 finalOperations)))
1238 (branch
1239 SHA256Failed
1240 error
1241 .
1242 (constructor
1243 SHA256ContextFinalizeResult
1244 SHA256ContextFinalizeFailed
1245 error
1246 blockCount
1247 zero
1248 finalOperations))))
1249 (sha256DigestStateBytes finalState)))
1250 (branch
1251 SHA256DigestBlocksFailed
1252 blockError
1253 blockOrdinal
1254 internalIndex
1255 partialTelemetry
1256 .
1257 (constructor
1258 SHA256ContextFinalizeResult
1259 SHA256ContextFinalizeFailed
1260 blockError
1261 blockOrdinal
1262 internalIndex
1263 partialTelemetry))))
1264 (sha256DigestTelemetryInitial pendingBytes finalBytes)))))
1265 (branch
1266 SHA256ContextPaddingFailed
1267 error
1268 stage
1269 validationTelemetry
1270 .
1271 (constructor
1272 SHA256ContextFinalizeResult
1273 SHA256ContextFinalizeFailed
1274 error
1275 stage
1276 zero
1277 (sha256DigestTelemetryInitial (bytes-length pending) zero)))))))
1278
1279def sha256DigestExecute =
1280 (lambda unrestricted input : Bytes .
1281 (eliminate
1282 SHA256ContextUpdateResult
1283 (lambda unrestricted current : (family SHA256ContextUpdateResult) .
1284 (family SHA256DigestExecutionResult))
1285 (sha256Update sha256InitialContext input)
1286 (branch
1287 SHA256ContextUpdateSucceeded
1288 context
1289 updateTelemetry
1290 .
1291 (eliminate
1292 SHA256UpdateTelemetry
1293 (lambda unrestricted current : (family SHA256UpdateTelemetry) .
1294 (family SHA256DigestExecutionResult))
1295 updateTelemetry
1296 (branch
1297 SHA256UpdateTelemetryValue
1298 inputBytes
1299 totalBefore
1300 pendingBefore
1301 combinedBytes
1302 compressedBytes
1303 compressedBlocks
1304 pendingAfter
1305 totalAfter
1306 updateOperations
1307 .
1308 (eliminate
1309 SHA256ContextFinalizeResult
1310 (lambda unrestricted current : (family SHA256ContextFinalizeResult) .
1311 (family SHA256DigestExecutionResult))
1312 (sha256Finalize context)
1313 (branch
1314 SHA256ContextFinalizeSucceeded
1315 digest
1316 finalizeTelemetry
1317 .
1318 (eliminate
1319 SHA256FinalizeTelemetry
1320 (lambda unrestricted current : (family SHA256FinalizeTelemetry) .
1321 (family SHA256DigestExecutionResult))
1322 finalizeTelemetry
1323 (branch
1324 SHA256FinalizeTelemetryValue
1325 finalTotal
1326 finalPending
1327 bitLength
1328 zeroBytes
1329 finalBytes
1330 finalBlocks
1331 digestBytes
1332 finalOperations
1333 .
1334 (constructor
1335 SHA256DigestExecutionResult
1336 SHA256DigestExecutionSucceeded
1337 digest
1338 (sha256DigestTelemetryCombine
1339 inputBytes
1340 (naturalAdd compressedBytes finalBytes)
1341 updateOperations
1342 finalOperations)))))
1343 (branch
1344 SHA256ContextFinalizeFailed
1345 error
1346 ordinal
1347 internalIndex
1348 finalOperations
1349 .
1350 (constructor
1351 SHA256DigestExecutionResult
1352 SHA256DigestExecutionFailed
1353 error
1354 ordinal
1355 (sha256DigestTelemetryCombine
1356 inputBytes
1357 (naturalAdd compressedBytes (sha256DigestTelemetryPaddedCount finalOperations))
1358 updateOperations
1359 finalOperations)))))))
1360 (branch
1361 SHA256ContextUpdateFailed
1362 error
1363 ordinal
1364 internalIndex
1365 telemetry
1366 .
1367 (constructor
1368 SHA256DigestExecutionResult
1369 SHA256DigestExecutionFailed
1370 error
1371 ordinal
1372 telemetry))))
1373
1374-- Canonical SHA-256 identity text is exactly 64 lowercase ASCII hex bytes.
1375-- Uppercase is deliberately rejected so one digest has one display spelling.
1376def sha256DigestHexByteInRange =
1377 (lambda unrestricted value : Byte .
1378 (lambda unrestricted lower : Byte .
1379 (lambda unrestricted upper : Byte .
1380 (naturalAnd
1381 (naturalLessOrEqual (byte-to-nat lower) (byte-to-nat value))
1382 (nat-less-than (byte-to-nat value) (byte-to-nat upper))))))
1383
1384-- Returns 0..15 for lowercase hexadecimal and 16 for every invalid byte.
1385def sha256DigestLowerHexNibble =
1386 (lambda unrestricted value : Byte .
1387 (nat-eliminate
1388 (lambda unrestricted decimal : Nat . Nat)
1389 (nat-eliminate
1390 (lambda unrestricted lower : Nat . Nat)
1391 (byte-to-nat (byte 16))
1392 (lambda unrestricted predecessor : Nat .
1393 (lambda unrestricted induction : Nat .
1394 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 87)))))
1395 (sha256DigestHexByteInRange value (byte 97) (byte 103)))
1396 (lambda unrestricted predecessor : Nat .
1397 (lambda unrestricted induction : Nat .
1398 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48)))))
1399 (sha256DigestHexByteInRange value (byte 48) (byte 58))))
1400
1401-- Decode exactly `pairs` pairs. The public caller first proves a 64-byte
1402-- source length, so the two heads in every one of the 32 steps are in range.
1403def sha256DigestDecodeHexPairs =
1404 (lambda unrestricted pairs : Nat .
1405 (nat-eliminate
1406 (lambda unrestricted current : Nat .
1407 (pi unrestricted input : Bytes . (family StdResult (family SHA256ErrorCode) Bytes)))
1408 (lambda unrestricted input : Bytes .
1409 (constructor StdResult StdSuccess (family SHA256ErrorCode) Bytes b""))
1410 (lambda unrestricted predecessor : Nat .
1411 (lambda unrestricted induction : (pi unrestricted input : Bytes . (family StdResult (family SHA256ErrorCode) Bytes)) .
1412 (lambda unrestricted input : Bytes .
1413 (app
1414 (lambda unrestricted high : Nat .
1415 (app
1416 (lambda unrestricted low : Nat .
1417 (nat-eliminate
1418 (lambda unrestricted invalid : Nat .
1419 (family StdResult (family SHA256ErrorCode) Bytes))
1420 (eliminate
1421 StdResult
1422 (lambda unrestricted current : (family StdResult (family SHA256ErrorCode) Bytes) .
1423 (family StdResult (family SHA256ErrorCode) Bytes))
1424 (induction (bytes-tail (bytes-tail input)))
1425 (branch
1426 StdFailure
1427 error
1428 .
1429 (constructor StdResult StdFailure (family SHA256ErrorCode) Bytes error))
1430 (branch
1431 StdSuccess
1432 decodedTail
1433 .
1434 (constructor
1435 StdResult
1436 StdSuccess
1437 (family SHA256ErrorCode)
1438 Bytes
1439 (bytes-cons
1440 (nat-to-byte (naturalAdd (naturalMultiply high 16) low))
1441 decodedTail))))
1442 (lambda unrestricted invalidPredecessor : Nat .
1443 (lambda unrestricted invalidInduction : (family StdResult (family SHA256ErrorCode) Bytes) .
1444 (constructor
1445 StdResult
1446 StdFailure
1447 (family SHA256ErrorCode)
1448 Bytes
1449 (constructor SHA256ErrorCode SHA256DigestHexInvalid))))
1450 (naturalOr
1451 (naturalIsZero (nat-less-than high 16))
1452 (naturalIsZero (nat-less-than low 16)))))
1453 (sha256DigestLowerHexNibble (bytes-head (bytes-tail input)))))
1454 (sha256DigestLowerHexNibble (bytes-head input))))))
1455 pairs))
1456
1457def sha256DigestFromHex : (pi unrestricted input : Bytes . (family SHA256Result)) =
1458 (lambda unrestricted input : Bytes .
1459 (nat-eliminate
1460 (lambda unrestricted validLength : Nat . (family SHA256Result))
1461 (constructor
1462 SHA256Result
1463 SHA256Failed
1464 (constructor SHA256ErrorCode SHA256DigestLengthInvalid))
1465 (lambda unrestricted predecessor : Nat .
1466 (lambda unrestricted induction : (family SHA256Result) .
1467 (eliminate
1468 StdResult
1469 (lambda unrestricted current : (family StdResult (family SHA256ErrorCode) Bytes) .
1470 (family SHA256Result))
1471 (sha256DigestDecodeHexPairs (byte-to-nat (byte 32)) input)
1472 (branch StdFailure error . (constructor SHA256Result SHA256Failed error))
1473 (branch StdSuccess decoded . (sha256DigestFromBytes decoded)))))
1474 (naturalEqual (bytes-length input) (byte-to-nat (byte 64)))))
1475
1476def sha256DigestToHex =
1477 (lambda unrestricted digest : (family SHA256Digest) .
1478 (dataBytesRenderHex (sha256DigestToBytes digest)))
1479
1480def sha256DigestIdentity =
1481 (lambda unrestricted digest : (family SHA256Digest) .
1482 (constructor
1483 SHA256DigestIdentityResult
1484 SHA256DigestIdentitySucceeded
1485 (constructor SHA256DigestIdentity SHA256DigestIdentityValue digest)))
1486
1487-- A checked identity owns only the 32-byte digest. Canonical lowercase
1488-- hexadecimal is derived, so no constructor can pair valid binary bytes with
1489-- unrelated display text.
1490def sha256DigestIdentityBinary =
1491 (lambda unrestricted identity : (family SHA256DigestIdentity) .
1492 (eliminate
1493 SHA256DigestIdentity
1494 (lambda unrestricted current : (family SHA256DigestIdentity) . (family SHA256Digest))
1495 identity
1496 (branch SHA256DigestIdentityValue binary . binary)))
1497
1498def sha256DigestIdentityHex =
1499 (lambda unrestricted identity : (family SHA256DigestIdentity) .
1500 (sha256DigestToHex (sha256DigestIdentityBinary identity)))
1501
1502def sha256DigestIdentityEqual =
1503 (lambda unrestricted left : (family SHA256DigestIdentity) .
1504 (lambda unrestricted right : (family SHA256DigestIdentity) .
1505 (sha256DigestEqual
1506 (sha256DigestIdentityBinary left)
1507 (sha256DigestIdentityBinary right))))
1508
1509-- Text is admitted exactly once: parsing rejects non-canonical spellings,
1510-- then sha256DigestIdentity re-renders the checked binary value. The result
1511-- therefore cannot contain a 64-byte string that merely looks digest-like.
1512def sha256DigestIdentityFromHex =
1513 (lambda unrestricted input : Bytes .
1514 (eliminate
1515 SHA256Result
1516 (lambda unrestricted current : (family SHA256Result) . (family SHA256DigestIdentityResult))
1517 (sha256DigestFromHex input)
1518 (branch SHA256Succeeded digest . (sha256DigestIdentity digest))
1519 (branch
1520 SHA256Failed
1521 error
1522 .
1523 (constructor SHA256DigestIdentityResult SHA256DigestIdentityFailed error))))
1524
1525def sha256Bytes =
1526 (lambda unrestricted input : Bytes .
1527 (eliminate
1528 SHA256DigestExecutionResult
1529 (lambda unrestricted current : (family SHA256DigestExecutionResult) . (family SHA256Result))
1530 (sha256DigestExecute input)
1531 (branch
1532 SHA256DigestExecutionSucceeded
1533 digest
1534 telemetry
1535 .
1536 (constructor SHA256Result SHA256Succeeded digest))
1537 (branch
1538 SHA256DigestExecutionFailed
1539 error
1540 ordinal
1541 telemetry
1542 .
1543 (constructor SHA256Result SHA256Failed error))))
1544
1545def sha256Hex =
1546 (lambda unrestricted input : Bytes .
1547 (eliminate
1548 SHA256DigestExecutionResult
1549 (lambda unrestricted current : (family SHA256DigestExecutionResult) .
1550 (family SHA256HexResult))
1551 (sha256DigestExecute input)
1552 (branch
1553 SHA256DigestExecutionSucceeded
1554 digest
1555 telemetry
1556 .
1557 (eliminate
1558 SHA256DigestIdentityResult
1559 (lambda unrestricted current : (family SHA256DigestIdentityResult) .
1560 (family SHA256HexResult))
1561 (sha256DigestIdentity digest)
1562 (branch
1563 SHA256DigestIdentitySucceeded
1564 identity
1565 .
1566 (eliminate
1567 SHA256DigestIdentity
1568 (lambda unrestricted current : (family SHA256DigestIdentity) .
1569 (family SHA256HexResult))
1570 identity
1571 (branch
1572 SHA256DigestIdentityValue
1573 binary
1574 .
1575 (constructor
1576 SHA256HexResult
1577 SHA256HexSucceeded
1578 (sha256DigestToHex binary)
1579 telemetry))))
1580 (branch
1581 SHA256DigestIdentityFailed
1582 error
1583 .
1584 (constructor
1585 SHA256HexResult
1586 SHA256HexFailed
1587 error
1588 (sha256DigestTelemetryBlockCount telemetry)
1589 telemetry))))
1590 (branch
1591 SHA256DigestExecutionFailed
1592 error
1593 ordinal
1594 telemetry
1595 .
1596 (constructor SHA256HexResult SHA256HexFailed error ordinal telemetry))))
1597
1598def sha256HexBytesOrEmpty =
1599 (lambda unrestricted result : (family SHA256HexResult) .
1600 (eliminate
1601 SHA256HexResult
1602 (lambda unrestricted current : (family SHA256HexResult) . Bytes)
1603 result
1604 (branch SHA256HexSucceeded hexBytes telemetry . hexBytes)
1605 (branch SHA256HexFailed error ordinal telemetry . b"")))
1606
1607-- Bytes -> Bytes raw digest: the 32 digest bytes of the input, or empty
1608-- bytes on the failure path. Downstream 32-length gates keep empty
1609-- fail-closed (the raw counterpart of sha256Digest below).
1610def sha256RawDigestOrEmpty =
1611 (lambda unrestricted material : Bytes .
1612 (eliminate
1613 SHA256Result
1614 (lambda unrestricted current : (family SHA256Result) . Bytes)
1615 (sha256Bytes material)
1616 (branch
1617 SHA256Succeeded
1618 digest
1619 .
1620 (eliminate
1621 SHA256Digest
1622 (lambda unrestricted current : (family SHA256Digest) . Bytes)
1623 digest
1624 (branch SHA256DigestValue raw proof . raw)))
1625 (branch SHA256Failed error . b"")))
1626
1627-- Bytes -> Bytes convenience digest: the 64-hex identity of the input,
1628-- or empty bytes on the (length-guarded) failure path. Downstream
1629-- 64-length/equality gates keep empty fail-closed.
1630def sha256Digest =
1631 (lambda unrestricted material : Bytes . (sha256HexBytesOrEmpty (sha256Hex material)))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.