1module Runtime.WordDigest
2
3import Data.SHA256
4import Data.SHA256Constants
5import Model.Config
6import Model.Word32
7import Std.Foundation
8import Std.List
9import Std.Natural
10
11-- One SHA-256 block-compression algorithm, specialized to a host instruction emitter.
12-- The emitter owns register assignment, instruction selection and branch
13-- flags. Loads/stores are little-endian and permit unaligned access; 8/32-bit
14-- loads zero-extend. Word operations wrap at 64 bits, shifts are logical, and
15-- 8/32-bit stores truncate. AddImm sign-extends its 32-bit operand and sets
16-- zero status; CmpImm supplies unsigned, zero and signed-negative status. Label and move
17-- operations preserve that status. These obligations are tested on each host.
18--
19-- Registers are logical roles inherited from the original implementation:
20-- RDI/RSI/RDX/RCX/R8/R9 carry the six arguments; the remaining names denote
21-- scratch values. The emitter chooses physical registers and preserves its
22-- calling convention. The fixed work-area slots are part of this algorithm,
23-- not per-system addresses. Callers supply writable, nonoverlapping bounded
24-- buffers, a positive block count and body length, and valid SHA padding.
25family WordDigestCondition : Type 0
26constructor WordDigestBelow
27constructor WordDigestNotZero
28constructor WordDigestZero
29constructor WordDigestNegative
30
31end-family
32
33family WordDigestBackend : Type 0
34parameter erased digestBackendAssembly : Type 0
35parameter erased digestBackendRegister : Type 0
36constructor WordDigestBackendValue
37field unrestricted backendDigestLoad32 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly))))
38field unrestricted backendDigestLoad64 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly))))
39field unrestricted backendDigestLoad8 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly))))
40field unrestricted backendDigestStore32 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendRegister . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly))))
41field unrestricted backendDigestStore64 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendRegister . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly))))
42field unrestricted backendDigestStore8 : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendRegister . (pi unrestricted a3 : digestBackendAssembly . digestBackendAssembly))))
43field unrestricted backendDigestMov : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
44field unrestricted backendDigestAdd : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
45field unrestricted backendDigestAnd : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
46field unrestricted backendDigestOr : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
47field unrestricted backendDigestXor : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : digestBackendRegister . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
48field unrestricted backendDigestShl : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
49field unrestricted backendDigestShr : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
50field unrestricted backendDigestMovImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
51field unrestricted backendDigestAddImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
52field unrestricted backendDigestAndImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
53field unrestricted backendDigestCmpImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
54field unrestricted backendDigestMulImm : (pi unrestricted a0 : digestBackendRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
55field unrestricted backendDigestLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : digestBackendAssembly . digestBackendAssembly))
56field unrestricted backendDigestJumpIf : (pi unrestricted a0 : (family WordDigestCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : digestBackendAssembly . digestBackendAssembly)))
57field unrestricted backendDigestReturn : (pi unrestricted a0 : digestBackendAssembly . digestBackendAssembly)
58field unrestricted backendDigestEnd : digestBackendAssembly
59field unrestricted backendDigestRAX : digestBackendRegister
60field unrestricted backendDigestRBX : digestBackendRegister
61field unrestricted backendDigestRCX : digestBackendRegister
62field unrestricted backendDigestRDX : digestBackendRegister
63field unrestricted backendDigestRSI : digestBackendRegister
64field unrestricted backendDigestRDI : digestBackendRegister
65field unrestricted backendDigestRBP : digestBackendRegister
66field unrestricted backendDigestR8 : digestBackendRegister
67field unrestricted backendDigestR9 : digestBackendRegister
68field unrestricted backendDigestR10 : digestBackendRegister
69field unrestricted backendDigestR11 : digestBackendRegister
70field unrestricted backendDigestR12 : digestBackendRegister
71field unrestricted backendDigestR13 : digestBackendRegister
72field unrestricted backendDigestR14 : digestBackendRegister
73field unrestricted backendDigestR15 : digestBackendRegister
74
75end-family
76
77def wordDigestFor =
78 (lambda erased A : Type 0 .
79 (lambda unrestricted count : Nat .
80 (lambda unrestricted body : (pi unrestricted index : Nat . (pi unrestricted rest : A . A)) .
81 (lambda unrestricted tail : A .
82 (nat-eliminate
83 (lambda unrestricted current : Nat . A)
84 tail
85 (lambda unrestricted predecessor : Nat .
86 (lambda unrestricted induction : A .
87 (body
88 (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) predecessor)
89 induction)))
90 count)))))
91
92def digestRoundConstants =
93 (eliminate
94 SHA256Schedule
95 (lambda unrestricted current : (family SHA256Schedule) . (family StdList Nat))
96 sha256RoundConstants
97 (branch SHA256ScheduleEnd . (constructor StdList StdListEmpty Nat))
98 (branch
99 SHA256ScheduleNext
100 head
101 tail
102 induction
103 .
104 (constructor StdList StdListCons Nat (modelWord32ToNatural head) induction)))
105
106def digestInitialHash =
107 (eliminate
108 SHA256State
109 (lambda unrestricted current : (family SHA256State) . (family StdList Nat))
110 sha256InitialState
111 (branch
112 SHA256StateValue
113 a
114 b
115 c
116 d
117 e
118 f
119 g
120 h
121 .
122 (constructor
123 StdList
124 StdListCons
125 Nat
126 (modelWord32ToNatural a)
127 (constructor
128 StdList
129 StdListCons
130 Nat
131 (modelWord32ToNatural b)
132 (constructor
133 StdList
134 StdListCons
135 Nat
136 (modelWord32ToNatural c)
137 (constructor
138 StdList
139 StdListCons
140 Nat
141 (modelWord32ToNatural d)
142 (constructor
143 StdList
144 StdListCons
145 Nat
146 (modelWord32ToNatural e)
147 (constructor
148 StdList
149 StdListCons
150 Nat
151 (modelWord32ToNatural f)
152 (constructor
153 StdList
154 StdListCons
155 Nat
156 (modelWord32ToNatural g)
157 (constructor
158 StdList
159 StdListCons
160 Nat
161 (modelWord32ToNatural h)
162 (constructor StdList StdListEmpty Nat)))))))))))
163
164-- The work layout follows the schedule, constants, working words, hash and
165-- saved registers. Round up to a cache-line boundary; no per-consumer offsets.
166def digestWordBytes : Nat =
167 4
168
169def digestBlockBytes : Nat =
170 64
171
172def digestAddressBytes : Nat =
173 8
174
175def digestScheduleWords =
176 (stdListLength Nat digestRoundConstants)
177
178def digestStateWords =
179 (stdListLength Nat digestInitialHash)
180
181def digestScheduleBytes =
182 (naturalMultiply digestScheduleWords digestWordBytes)
183
184def digestStateBytes =
185 (naturalMultiply digestStateWords digestWordBytes)
186
187def digestW =
188 (lambda unrestricted t : Nat . (naturalMultiply digestWordBytes t))
189
190def digestK =
191 (lambda unrestricted t : Nat . (naturalAdd digestScheduleBytes (digestW t)))
192
193def digestVariablesAt =
194 (naturalMultiply 2 digestScheduleBytes)
195
196def digestVar =
197 (lambda unrestricted t : Nat . (naturalAdd digestVariablesAt (digestW t)))
198
199def digestHashAt =
200 (naturalAdd digestVariablesAt digestStateBytes)
201
202def digestH =
203 (lambda unrestricted t : Nat . (naturalAdd digestHashAt (digestW t)))
204
205def digestSavedAt =
206 (naturalAdd digestHashAt digestStateBytes)
207
208def digestSaved =
209 (lambda unrestricted t : Nat . (naturalAdd digestSavedAt (naturalMultiply digestAddressBytes t)))
210
211def digestSavedRegisters : Nat =
212 6
213
214-- The compression loops' remaining-pass count: the word after the saved
215-- registers, inside the same cache-line-rounded work area. The loops address
216-- each pass's schedule through RBP, which the compression saves and restores
217-- with the other callee-saved registers: RCX and R8 belong to callers'
218-- prepare/finish code (telemetry sealing keeps a count in RCX), and every
219-- other register is a round temporary.
220def digestLoopCounter =
221 (digestSaved digestSavedRegisters)
222
223def digestWorkAlignment : Nat =
224 64
225
226def digestWorkBytes =
227 (naturalMultiply
228 digestWorkAlignment
229 (naturalDivideUnchecked
230 (naturalAdd
231 (naturalAdd digestLoopCounter digestAddressBytes)
232 (naturalSaturatingSubtract digestWorkAlignment 1))
233 digestWorkAlignment))
234
235def digestAt =
236 (lambda unrestricted values : (family StdList Nat) .
237 (lambda unrestricted p : Nat .
238 (eliminate
239 StdOption
240 (lambda unrestricted current : (family StdOption Nat) . Nat)
241 (stdListIndex Nat values p)
242 (branch StdNone . 0)
243 (branch StdSome value . value))))
244
245def digestSlot =
246 (lambda unrestricted v : Nat .
247 (lambda unrestricted t : Nat .
248 (digestVar (naturalModuloUnchecked (naturalSaturatingSubtract (naturalAdd v 64) t) 8))))
249
250-- Runtime byte-string padding before the shared block compressor. The logical
251-- input/count/output/work roles are RDI/RSI/RDX/R9. The caller supplies a writable
252-- input followed by byteDigestPaddingBytes, and disjoint output/work regions.
253-- Null and negative Linux pointers, and counts above u32, refuse before writes.
254-- totalBytes names the original byte count register: RSI for a whole string,
255-- R8 for a stream tail. Its caller admits that total and the stream partition.
256-- Only RAX, RCX, RSI and caller-saved R10 change before the block routine saves
257-- its registers. RBX and the emitter's interpreter registers must survive.
258-- The refusal label belongs to the target entry wrapper; success falls through
259-- into its block routine. Both host ISAs specialize this one padding algorithm.
260def byteDigestPaddingBytes : Nat =
261 (naturalMultiply 2 digestBlockBytes)
262
263def wordDigestBytePaddingFor =
264 (lambda erased A : Type 0 .
265 (lambda erased R : Type 0 .
266 (lambda unrestricted backend : (family WordDigestBackend A R) .
267 (lambda unrestricted totalBytes : R .
268 (lambda unrestricted blocks : A .
269 (eliminate
270 WordDigestBackend
271 (lambda unrestricted current : (family WordDigestBackend A R) . A)
272 backend
273 (branch
274 WordDigestBackendValue
275 digestLoad32
276 digestLoad64
277 digestLoad8
278 digestStore32
279 digestStore64
280 digestStore8
281 digestMov
282 digestAdd
283 digestAnd
284 digestOr
285 digestXor
286 digestShl
287 digestShr
288 digestMovImm
289 digestAddImm
290 digestAndImm
291 digestCmpImm
292 digestMulImm
293 digestLabel
294 digestJumpIf
295 digestReturn
296 digestEnd
297 digestRAX
298 digestRBX
299 digestRCX
300 digestRDX
301 digestRSI
302 digestRDI
303 digestRBP
304 digestR8
305 digestR9
306 digestR10
307 digestR11
308 digestR12
309 digestR13
310 digestR14
311 digestR15
312 .
313 (digestCmpImm
314 digestRDI
315 0
316 (digestJumpIf
317 (constructor WordDigestCondition WordDigestNegative)
318 b"byte-digest-refused"
319 (digestJumpIf
320 (constructor WordDigestCondition WordDigestZero)
321 b"byte-digest-refused"
322 (digestMov
323 digestRAX
324 digestRSI
325 (digestShr
326 digestRAX
327 32
328 (digestCmpImm
329 digestRAX
330 0
331 (digestJumpIf
332 (constructor WordDigestCondition WordDigestNotZero)
333 b"byte-digest-refused"
334 (digestMov
335 digestR10
336 digestRDI
337 (digestAdd
338 digestR10
339 digestRSI
340 (digestMovImm
341 digestRAX
342 0
343 (wordDigestFor
344 A
345 (naturalDivideUnchecked
346 byteDigestPaddingBytes
347 digestAddressBytes)
348 (lambda unrestricted index : Nat .
349 (digestStore64
350 digestR10
351 (naturalMultiply index digestAddressBytes)
352 digestRAX))
353 (digestMovImm
354 digestRAX
355 128
356 (digestStore8
357 digestR10
358 0
359 digestRAX
360 (digestMov
361 digestRCX
362 totalBytes
363 (digestShl
364 digestRCX
365 3
366 (digestAddImm
367 digestRSI
368 (naturalAdd digestBlockBytes digestAddressBytes)
369 (digestShr
370 digestRSI
371 6
372 (digestMov
373 digestR10
374 digestRSI
375 (digestShl
376 digestR10
377 6
378 (digestAdd
379 digestR10
380 digestRDI
381 (digestAddImm
382 digestR10
383 4294967288
384 (wordDigestFor
385 A
386 digestAddressBytes
387 (lambda unrestricted index : Nat .
388 (lambda unrestricted rest : A .
389 (digestMov
390 digestRAX
391 digestRCX
392 (digestShr
393 digestRAX
394 (naturalMultiply 8 (naturalSaturatingSubtract 7 index))
395 (digestStore8 digestR10 index digestRAX rest)))))
396 blocks)))))))))))))))))))))))))))))
397
398def wordDigestCompressAssemblyFor =
399 (lambda erased A : Type 0 .
400 (lambda erased R : Type 0 .
401 (lambda unrestricted backend : (family WordDigestBackend A R) .
402 (lambda unrestricted prepare : (pi unrestricted tail : A . A) .
403 (lambda unrestricted initialize : (pi unrestricted tail : A . A) .
404 (lambda unrestricted finish : (pi unrestricted tail : A . A) .
405 (eliminate
406 WordDigestBackend
407 (lambda unrestricted current : (family WordDigestBackend A R) . A)
408 backend
409 (branch
410 WordDigestBackendValue
411 digestLoad32
412 digestLoad64
413 digestLoad8
414 digestStore32
415 digestStore64
416 digestStore8
417 digestMov
418 digestAdd
419 digestAnd
420 digestOr
421 digestXor
422 digestShl
423 digestShr
424 digestMovImm
425 digestAddImm
426 digestAndImm
427 digestCmpImm
428 digestMulImm
429 digestLabel
430 digestJumpIf
431 digestReturn
432 digestEnd
433 digestRAX
434 digestRBX
435 digestRCX
436 digestRDX
437 digestRSI
438 digestRDI
439 digestRBP
440 digestR8
441 digestR9
442 digestR10
443 digestR11
444 digestR12
445 digestR13
446 digestR14
447 digestR15
448 .
449 (let unrestricted digestFor =
450 (wordDigestFor A)
451 in
452 (let unrestricted digestRotate =
453 (lambda unrestricted d : R .
454 (lambda unrestricted s : R .
455 (lambda unrestricted n : Nat .
456 (lambda unrestricted rest : A .
457 (digestMov d s (digestShl d 32 (digestOr d s (digestShr d n rest))))))))
458 in
459 (let unrestricted digestSigma =
460 (lambda unrestricted d : R .
461 (lambda unrestricted t : R .
462 (lambda unrestricted s : R .
463 (lambda unrestricted x : Nat .
464 (lambda unrestricted y : Nat .
465 (lambda unrestricted z : Nat .
466 (lambda unrestricted shift : Nat .
467 (lambda unrestricted rest : A .
468 (digestRotate
469 d
470 s
471 x
472 (digestRotate
473 t
474 s
475 y
476 (digestXor
477 d
478 t
479 (nat-eliminate
480 (lambda unrestricted current : Nat . A)
481 (digestRotate t s z (digestXor d t rest))
482 (lambda unrestricted p : Nat .
483 (lambda unrestricted i : A .
484 (digestMov t s (digestShr t z (digestXor d t rest)))))
485 shift))))))))))))
486 in
487 (let unrestricted digestConstant =
488 (lambda unrestricted at : Nat .
489 (lambda unrestricted value : Nat .
490 (lambda unrestricted rest : A .
491 (digestMovImm
492 digestRAX
493 value
494 (digestStore32 digestR9 at digestRAX rest)))))
495 in
496 (let unrestricted digestMessageWord =
497 (lambda unrestricted i : Nat .
498 (lambda unrestricted rest : A .
499 (digestLoad8
500 digestRAX
501 digestRDI
502 (naturalMultiply 4 i)
503 (digestShl
504 digestRAX
505 8
506 (digestLoad8
507 digestRBX
508 digestRDI
509 (naturalAdd 1 (naturalMultiply 4 i))
510 (digestOr
511 digestRAX
512 digestRBX
513 (digestShl
514 digestRAX
515 8
516 (digestLoad8
517 digestRBX
518 digestRDI
519 (naturalAdd 2 (naturalMultiply 4 i))
520 (digestOr
521 digestRAX
522 digestRBX
523 (digestShl
524 digestRAX
525 8
526 (digestLoad8
527 digestRBX
528 digestRDI
529 (naturalAdd 3 (naturalMultiply 4 i))
530 (digestOr
531 digestRAX
532 digestRBX
533 (digestStore32 digestR9 (digestW i) digestRAX rest)))))))))))))
534 in
535 -- W[t] = s1(W[t-2]) + W[t-7] + s0(W[t-15]) + W[t-16], with t = 16 + k
536 -- and `base` addressing W[k] (displacements are word offsets from it).
537 (let unrestricted digestScheduleWord =
538 (lambda unrestricted base : R .
539 (lambda unrestricted k : Nat .
540 (lambda unrestricted rest : A .
541 (let unrestricted t =
542 (naturalAdd 16 k)
543 in
544 (digestLoad32
545 digestRAX
546 base
547 (digestW (naturalSaturatingSubtract t 15))
548 (digestSigma
549 digestRBX
550 digestR10
551 digestRAX
552 7
553 18
554 3
555 1
556 (digestLoad32
557 digestRAX
558 base
559 (digestW (naturalSaturatingSubtract t 2))
560 (digestSigma
561 digestR11
562 digestR10
563 digestRAX
564 17
565 19
566 10
567 1
568 (digestAdd
569 digestRBX
570 digestR11
571 (digestLoad32
572 digestR10
573 base
574 (digestW (naturalSaturatingSubtract t 16))
575 (digestAdd
576 digestRBX
577 digestR10
578 (digestLoad32
579 digestR10
580 base
581 (digestW (naturalSaturatingSubtract t 7))
582 (digestAdd
583 digestRBX
584 digestR10
585 (digestStore32 base (digestW t) digestRBX rest))))))))))))))
586 in
587 -- Round t of a group of eight: the working-word slots rotate with
588 -- t mod 8, so one group serves every round; `base` addresses W and
589 -- K of the group's first round.
590 (let unrestricted digestRound =
591 (lambda unrestricted base : R .
592 (lambda unrestricted t : Nat .
593 (lambda unrestricted rest : A .
594 -- t1 = h + S1(e) + ch(e, f, g) + K[t] + W[t], in rbx
595 (digestLoad32
596 digestRAX
597 digestR9
598 (digestSlot 4 t)
599 (digestSigma
600 digestRBX
601 digestR10
602 digestRAX
603 6
604 11
605 25
606 0
607 (digestLoad32
608 digestR11
609 digestR9
610 (digestSlot 5 t)
611 (digestMov
612 digestR10
613 digestRAX
614 (digestAnd
615 digestR10
616 digestR11
617 (digestLoad32
618 digestR12
619 digestR9
620 (digestSlot 6 t)
621 (digestMov
622 digestR11
623 digestRAX
624 (digestAnd
625 digestR11
626 digestR12
627 (digestXor
628 digestR11
629 digestR12
630 (digestXor
631 digestR10
632 digestR11
633 (digestAdd
634 digestRBX
635 digestR10
636 (digestLoad32
637 digestR10
638 digestR9
639 (digestSlot 7 t)
640 (digestAdd
641 digestRBX
642 digestR10
643 (digestLoad32
644 digestR10
645 base
646 (digestK t)
647 (digestAdd
648 digestRBX
649 digestR10
650 (digestLoad32
651 digestR10
652 base
653 (digestW t)
654 (digestAdd
655 digestRBX
656 digestR10
657 -- t2 = S0(a) + maj(a, b, c), in r10
658 (digestLoad32
659 digestRAX
660 digestR9
661 (digestSlot 0 t)
662 (digestSigma
663 digestR10
664 digestR11
665 digestRAX
666 2
667 13
668 22
669 0
670 (digestLoad32
671 digestR11
672 digestR9
673 (digestSlot 1 t)
674 (digestLoad32
675 digestR12
676 digestR9
677 (digestSlot 2 t)
678 (digestMov
679 digestR13
680 digestRAX
681 (digestAnd
682 digestR13
683 digestR11
684 (digestMov
685 digestR14
686 digestRAX
687 (digestAnd
688 digestR14
689 digestR12
690 (digestXor
691 digestR13
692 digestR14
693 (digestAnd
694 digestR11
695 digestR12
696 (digestXor
697 digestR13
698 digestR11
699 (digestAdd
700 digestR10
701 digestR13
702 -- d + t1 is the next e (d's slot), t1 + t2 the next a (h's slot)
703 (digestLoad32
704 digestR11
705 digestR9
706 (digestSlot 3 t)
707 (digestAdd
708 digestR11
709 digestRBX
710 (digestStore32
711 digestR9
712 (digestSlot 3 t)
713 digestR11
714 (digestAdd
715 digestRBX
716 digestR10
717 (digestStore32 digestR9 (digestSlot 7 t) digestRBX rest)))))))))))))))))))))))))))))))))))))
718 in
719 -- `count` passes of `body` with RBP = R9 + pass * stride: the
720 -- schedule and constants advance, the working-word slots do not.
721 -- The remaining count lives in the work area; RAX is free here.
722 (let unrestricted digestLoop =
723 (lambda unrestricted name : Bytes .
724 (lambda unrestricted count : Nat .
725 (lambda unrestricted stride : Nat .
726 (lambda unrestricted body : (pi unrestricted tail : A . A) .
727 (lambda unrestricted rest : A .
728 (digestMov
729 digestRBP
730 digestR9
731 (digestMovImm
732 digestRAX
733 count
734 (digestStore64
735 digestR9
736 digestLoopCounter
737 digestRAX
738 (digestLabel
739 name
740 (body
741 (digestAddImm
742 digestRBP
743 stride
744 (digestLoad64
745 digestRAX
746 digestR9
747 digestLoopCounter
748 (digestAddImm
749 digestRAX
750 0xFFFFFFFF
751 (digestStore64
752 digestR9
753 digestLoopCounter
754 digestRAX
755 (digestCmpImm
756 digestRAX
757 0
758 (digestJumpIf
759 (constructor WordDigestCondition WordDigestNotZero)
760 name
761 rest))))))))))))))))
762 in
763 (let unrestricted digestLoadVariable =
764 (lambda unrestricted i : Nat .
765 (lambda unrestricted rest : A .
766 (digestLoad32
767 digestRAX
768 digestR9
769 (digestH i)
770 (digestStore32 digestR9 (digestVar i) digestRAX rest))))
771 in
772 (let unrestricted digestAccumulate =
773 (lambda unrestricted i : Nat .
774 (lambda unrestricted rest : A .
775 (digestLoad32
776 digestRAX
777 digestR9
778 (digestH i)
779 (digestLoad32
780 digestRBX
781 digestR9
782 (digestVar i)
783 (digestAdd
784 digestRAX
785 digestRBX
786 (digestStore32 digestR9 (digestH i) digestRAX rest))))))
787 in
788 (let unrestricted digestSaveRegisters =
789 (lambda unrestricted rest : A .
790 (digestStore64
791 digestR9
792 (digestSaved 0)
793 digestRBX
794 (digestStore64
795 digestR9
796 (digestSaved 1)
797 digestR12
798 (digestStore64
799 digestR9
800 (digestSaved 2)
801 digestR13
802 (digestStore64
803 digestR9
804 (digestSaved 3)
805 digestR14
806 (digestStore64
807 digestR9
808 (digestSaved 4)
809 digestR15
810 (digestStore64 digestR9 (digestSaved 5) digestRBP rest)))))))
811 in
812 (let unrestricted digestRestoreRegisters =
813 (lambda unrestricted rest : A .
814 (digestLoad64
815 digestRBX
816 digestR9
817 (digestSaved 0)
818 (digestLoad64
819 digestR12
820 digestR9
821 (digestSaved 1)
822 (digestLoad64
823 digestR13
824 digestR9
825 (digestSaved 2)
826 (digestLoad64
827 digestR14
828 digestR9
829 (digestSaved 3)
830 (digestLoad64
831 digestR15
832 digestR9
833 (digestSaved 4)
834 (digestLoad64 digestRBP digestR9 (digestSaved 5) rest)))))))
835 in
836 (digestSaveRegisters
837 (prepare
838 (digestFor
839 64
840 (lambda unrestricted t : Nat .
841 (digestConstant
842 (digestK t)
843 (digestAt digestRoundConstants t)))
844 (initialize
845 (digestMov
846 digestR15
847 digestRDI
848 (digestLabel
849 b"seal-block"
850 (digestFor
851 16
852 digestMessageWord
853 (digestLoop
854 b"seal-schedule"
855 12
856 16
857 (digestFor 4 (digestScheduleWord digestRBP))
858 (digestFor
859 8
860 digestLoadVariable
861 (digestLoop
862 b"seal-rounds"
863 8
864 32
865 (digestFor 8 (digestRound digestRBP))
866 (digestFor
867 8
868 digestAccumulate
869 (digestAddImm
870 digestRDI
871 64
872 (digestAddImm
873 digestRSI
874 0xFFFFFFFF
875 (digestJumpIf
876 (constructor WordDigestCondition WordDigestNotZero)
877 b"seal-block"
878 (finish (digestRestoreRegisters (digestReturn digestEnd)))))))))))))))))))))))))))))))))))))
879
880-- Initialize only the chaining words; saved registers and the round scratch
881-- remain private to each compression call. Initialization does not erase them.
882def wordDigestInitializeFor =
883 (lambda erased A : Type 0 .
884 (lambda erased R : Type 0 .
885 (lambda unrestricted backend : (family WordDigestBackend A R) .
886 (lambda unrestricted tail : A .
887 (eliminate
888 WordDigestBackend
889 (lambda unrestricted current : (family WordDigestBackend A R) . A)
890 backend
891 (branch
892 WordDigestBackendValue
893 digestLoad32
894 digestLoad64
895 digestLoad8
896 digestStore32
897 digestStore64
898 digestStore8
899 digestMov
900 digestAdd
901 digestAnd
902 digestOr
903 digestXor
904 digestShl
905 digestShr
906 digestMovImm
907 digestAddImm
908 digestAndImm
909 digestCmpImm
910 digestMulImm
911 digestLabel
912 digestJumpIf
913 digestReturn
914 digestEnd
915 digestRAX
916 digestRBX
917 digestRCX
918 digestRDX
919 digestRSI
920 digestRDI
921 digestRBP
922 digestR8
923 digestR9
924 digestR10
925 digestR11
926 digestR12
927 digestR13
928 digestR14
929 digestR15
930 .
931 (wordDigestFor
932 A
933 digestStateWords
934 (lambda unrestricted i : Nat .
935 (lambda unrestricted rest : A .
936 (digestMovImm
937 digestRAX
938 (digestAt digestInitialHash i)
939 (digestStore32 digestR9 (digestH i) digestRAX rest))))
940 tail)))))))
941
942def wordDigestBlocksAssemblyFor =
943 (lambda erased A : Type 0 .
944 (lambda erased R : Type 0 .
945 (lambda unrestricted backend : (family WordDigestBackend A R) .
946 (lambda unrestricted prepare : (pi unrestricted tail : A . A) .
947 (lambda unrestricted finish : (pi unrestricted tail : A . A) .
948 (wordDigestCompressAssemblyFor
949 A
950 R
951 backend
952 prepare
953 (wordDigestInitializeFor A R backend)
954 finish))))))
955
956def wordDigestOutputFor =
957 (lambda erased A : Type 0 .
958 (lambda erased R : Type 0 .
959 (lambda unrestricted backend : (family WordDigestBackend A R) .
960 (lambda unrestricted tail : A .
961 (eliminate
962 WordDigestBackend
963 (lambda unrestricted current : (family WordDigestBackend A R) . A)
964 backend
965 (branch
966 WordDigestBackendValue
967 digestLoad32
968 digestLoad64
969 digestLoad8
970 digestStore32
971 digestStore64
972 digestStore8
973 digestMov
974 digestAdd
975 digestAnd
976 digestOr
977 digestXor
978 digestShl
979 digestShr
980 digestMovImm
981 digestAddImm
982 digestAndImm
983 digestCmpImm
984 digestMulImm
985 digestLabel
986 digestJumpIf
987 digestReturn
988 digestEnd
989 digestRAX
990 digestRBX
991 digestRCX
992 digestRDX
993 digestRSI
994 digestRDI
995 digestRBP
996 digestR8
997 digestR9
998 digestR10
999 digestR11
1000 digestR12
1001 digestR13
1002 digestR14
1003 digestR15
1004 .
1005 (wordDigestFor
1006 A
1007 digestStateBytes
1008 (lambda unrestricted q : Nat .
1009 (lambda unrestricted rest : A .
1010 (digestLoad32
1011 digestRAX
1012 digestR9
1013 (digestH (naturalDivideUnchecked q digestWordBytes))
1014 (digestShr
1015 digestRAX
1016 (naturalMultiply
1017 8
1018 (naturalSaturatingSubtract
1019 (naturalSaturatingSubtract digestWordBytes 1)
1020 (naturalModuloUnchecked q digestWordBytes)))
1021 (digestStore8 digestRDX q digestRAX rest)))))
1022 (digestMovImm digestRAX digestStateBytes tail))))))))
1023
1024-- Raw digest ABI: padded blocks at RDI, positive count at RSI, 32-byte output
1025-- at RDX, private work area at R9. RCX/R8 are unused. The caller proves valid
1026-- padding and nonoverlap. Returns 32; no timestamp write and no payload copy.
1027def wordDigestAssemblyFor =
1028 (lambda erased A : Type 0 .
1029 (lambda erased R : Type 0 .
1030 (lambda unrestricted backend : (family WordDigestBackend A R) .
1031 (wordDigestBlocksAssemblyFor
1032 A
1033 R
1034 backend
1035 (lambda unrestricted tail : A . tail)
1036 (wordDigestOutputFor A R backend)))))
1037
1038-- Same raw-block ABI as wordDigestAssemblyFor, with chaining words retained
1039-- in the work region. The caller supplies a positive number of complete blocks.
1040def wordDigestContinueAssemblyFor =
1041 (lambda erased A : Type 0 .
1042 (lambda erased R : Type 0 .
1043 (lambda unrestricted backend : (family WordDigestBackend A R) .
1044 (wordDigestCompressAssemblyFor
1045 A
1046 R
1047 backend
1048 (lambda unrestricted tail : A . tail)
1049 (lambda unrestricted tail : A . tail)
1050 (wordDigestOutputFor A R backend)))))
1051
1052-- A bounded stream window contains complete SHA blocks. It is a host buffering
1053-- policy, independent of a device or OS allocation quantum. The final suffix
1054-- needs two extra blocks. The plan's two words are full-window count and tail.
1055def byteDigestChunkShift : Nat =
1056 10
1057
1058def byteDigestChunkBytes : Nat =
1059 (naturalPowerOfTwo byteDigestChunkShift)
1060
1061def byteDigestChunkPlanBytes : Nat =
1062 (naturalMultiply 2 digestAddressBytes)
1063
1064def byteDigestChunkBufferBytes : Nat =
1065 (naturalAdd byteDigestChunkBytes byteDigestPaddingBytes)
1066
1067-- RDI: total u32 bytes; RSI: writable two-word chunk plan; R9: private
1068-- work area. Reject oversized totals before writes, initialize chaining words,
1069-- return 32. Valid disjoint destination/work buffers are the caller contract.
1070def wordDigestStreamStartFor =
1071 (lambda erased A : Type 0 .
1072 (lambda erased R : Type 0 .
1073 (lambda unrestricted backend : (family WordDigestBackend A R) .
1074 (eliminate
1075 WordDigestBackend
1076 (lambda unrestricted current : (family WordDigestBackend A R) . A)
1077 backend
1078 (branch
1079 WordDigestBackendValue
1080 digestLoad32
1081 digestLoad64
1082 digestLoad8
1083 digestStore32
1084 digestStore64
1085 digestStore8
1086 digestMov
1087 digestAdd
1088 digestAnd
1089 digestOr
1090 digestXor
1091 digestShl
1092 digestShr
1093 digestMovImm
1094 digestAddImm
1095 digestAndImm
1096 digestCmpImm
1097 digestMulImm
1098 digestLabel
1099 digestJumpIf
1100 digestReturn
1101 digestEnd
1102 digestRAX
1103 digestRBX
1104 digestRCX
1105 digestRDX
1106 digestRSI
1107 digestRDI
1108 digestRBP
1109 digestR8
1110 digestR9
1111 digestR10
1112 digestR11
1113 digestR12
1114 digestR13
1115 digestR14
1116 digestR15
1117 .
1118 (digestMov
1119 digestRAX
1120 digestRDI
1121 (digestShr
1122 digestRAX
1123 32
1124 (digestCmpImm
1125 digestRAX
1126 0
1127 (digestJumpIf
1128 (constructor WordDigestCondition WordDigestZero)
1129 b"stream-start"
1130 (digestMovImm
1131 digestRAX
1132 0
1133 (digestReturn
1134 (digestLabel
1135 b"stream-start"
1136 (digestMov
1137 digestRAX
1138 digestRDI
1139 (digestShr
1140 digestRAX
1141 byteDigestChunkShift
1142 (digestStore64
1143 digestRSI
1144 0
1145 digestRAX
1146 (digestMov
1147 digestRAX
1148 digestRDI
1149 (digestAndImm
1150 digestRAX
1151 (naturalSaturatingSubtract byteDigestChunkBytes 1)
1152 (digestStore64
1153 digestRSI
1154 digestAddressBytes
1155 digestRAX
1156 (wordDigestInitializeFor
1157 A
1158 R
1159 backend
1160 (digestMovImm
1161 digestRAX
1162 digestStateBytes
1163 (digestReturn digestEnd)))))))))))))))))))))
1164
1165-- Byte-digest ABI, with the original total in R8 and only the final window
1166-- tail at RDI/RSI. Prior full windows must have been compressed in this work
1167-- region. Zero-fill padding uses the original bit count, never the tail count.
1168def wordDigestStreamFinishFor =
1169 (lambda erased A : Type 0 .
1170 (lambda erased R : Type 0 .
1171 (lambda unrestricted backend : (family WordDigestBackend A R) .
1172 (eliminate
1173 WordDigestBackend
1174 (lambda unrestricted current : (family WordDigestBackend A R) . A)
1175 backend
1176 (branch
1177 WordDigestBackendValue
1178 digestLoad32
1179 digestLoad64
1180 digestLoad8
1181 digestStore32
1182 digestStore64
1183 digestStore8
1184 digestMov
1185 digestAdd
1186 digestAnd
1187 digestOr
1188 digestXor
1189 digestShl
1190 digestShr
1191 digestMovImm
1192 digestAddImm
1193 digestAndImm
1194 digestCmpImm
1195 digestMulImm
1196 digestLabel
1197 digestJumpIf
1198 digestReturn
1199 digestEnd
1200 digestRAX
1201 digestRBX
1202 digestRCX
1203 digestRDX
1204 digestRSI
1205 digestRDI
1206 digestRBP
1207 digestR8
1208 digestR9
1209 digestR10
1210 digestR11
1211 digestR12
1212 digestR13
1213 digestR14
1214 digestR15
1215 .
1216 (digestMov
1217 digestRAX
1218 digestR8
1219 (digestShr
1220 digestRAX
1221 32
1222 (digestCmpImm
1223 digestRAX
1224 0
1225 (digestJumpIf
1226 (constructor WordDigestCondition WordDigestNotZero)
1227 b"byte-digest-refused"
1228 (digestMov
1229 digestRAX
1230 digestR8
1231 (digestAndImm
1232 digestRAX
1233 (naturalSaturatingSubtract byteDigestChunkBytes 1)
1234 (digestXor
1235 digestRAX
1236 digestRSI
1237 (digestCmpImm
1238 digestRAX
1239 0
1240 (digestJumpIf
1241 (constructor WordDigestCondition WordDigestNotZero)
1242 b"byte-digest-refused"
1243 (wordDigestBytePaddingFor
1244 A
1245 R
1246 backend
1247 digestR8
1248 (wordDigestContinueAssemblyFor A R backend))))))))))))))))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.