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)))))))))))))))))))))))))))))))))))))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.