def ap.e_sbi
bend-osdev-aes@0.1.0.0 · PROOF.bend:571
import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-aes@0.1.0.0/aes.bend as X
import bend-collections@1.0.0.0/src/crypto/aes/sbox.bend as SB
571def ap.e_sbi(c0: Bool, c1: Bool, c2: Bool, c3: Bool, c4: Bool, c5: Bool, c6: Bool, c7: Bool) -> {X.aes.isbox(SB.sbox(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}})) == U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, Word.zero(24n)}}}}}}}}} : U32}:
572 match c0 c1 c2 c3 c4 c5 c6 c7:
573 case False{} False{} False{} False{} False{} False{} False{} False{}:
574 {==}
575 case True{} False{} False{} False{} False{} False{} False{} False{}:
576 {==}
577 case False{} True{} False{} False{} False{} False{} False{} False{}:
578 {==}
579 case True{} True{} False{} False{} False{} False{} False{} False{}:
580 {==}
581 case False{} False{} True{} False{} False{} False{} False{} False{}:
582 {==}
583 case True{} False{} True{} False{} False{} False{} False{} False{}:
584 {==}
585 case False{} True{} True{} False{} False{} False{} False{} False{}:
586 {==}
587 case True{} True{} True{} False{} False{} False{} False{} False{}:
588 {==}
589 case False{} False{} False{} True{} False{} False{} False{} False{}:
590 {==}
591 case True{} False{} False{} True{} False{} False{} False{} False{}:
592 {==}
593 case False{} True{} False{} True{} False{} False{} False{} False{}:
594 {==}
595 case True{} True{} False{} True{} False{} False{} False{} False{}:
596 {==}
597 case False{} False{} True{} True{} False{} False{} False{} False{}:
598 {==}
599 case True{} False{} True{} True{} False{} False{} False{} False{}:
600 {==}
601 case False{} True{} True{} True{} False{} False{} False{} False{}:
602 {==}
603 case True{} True{} True{} True{} False{} False{} False{} False{}:
604 {==}
605 case False{} False{} False{} False{} True{} False{} False{} False{}:
606 {==}
607 case True{} False{} False{} False{} True{} False{} False{} False{}:
608 {==}
609 case False{} True{} False{} False{} True{} False{} False{} False{}:
610 {==}
611 case True{} True{} False{} False{} True{} False{} False{} False{}:
612 {==}
613 case False{} False{} True{} False{} True{} False{} False{} False{}:
614 {==}
615 case True{} False{} True{} False{} True{} False{} False{} False{}:
616 {==}
617 case False{} True{} True{} False{} True{} False{} False{} False{}:
618 {==}
619 case True{} True{} True{} False{} True{} False{} False{} False{}:
620 {==}
621 case False{} False{} False{} True{} True{} False{} False{} False{}:
622 {==}
623 case True{} False{} False{} True{} True{} False{} False{} False{}:
624 {==}
625 case False{} True{} False{} True{} True{} False{} False{} False{}:
626 {==}
627 case True{} True{} False{} True{} True{} False{} False{} False{}:
628 {==}
629 case False{} False{} True{} True{} True{} False{} False{} False{}:
630 {==}
631 case True{} False{} True{} True{} True{} False{} False{} False{}:
632 {==}
633 case False{} True{} True{} True{} True{} False{} False{} False{}:
634 {==}
635 case True{} True{} True{} True{} True{} False{} False{} False{}:
636 {==}
637 case False{} False{} False{} False{} False{} True{} False{} False{}:
638 {==}
639 case True{} False{} False{} False{} False{} True{} False{} False{}:
640 {==}
641 case False{} True{} False{} False{} False{} True{} False{} False{}:
642 {==}
643 case True{} True{} False{} False{} False{} True{} False{} False{}:
644 {==}
645 case False{} False{} True{} False{} False{} True{} False{} False{}:
646 {==}
647 case True{} False{} True{} False{} False{} True{} False{} False{}:
648 {==}
649 case False{} True{} True{} False{} False{} True{} False{} False{}:
650 {==}
651 case True{} True{} True{} False{} False{} True{} False{} False{}:
652 {==}
653 case False{} False{} False{} True{} False{} True{} False{} False{}:
654 {==}
655 case True{} False{} False{} True{} False{} True{} False{} False{}:
656 {==}
657 case False{} True{} False{} True{} False{} True{} False{} False{}:
658 {==}
659 case True{} True{} False{} True{} False{} True{} False{} False{}:
660 {==}
661 case False{} False{} True{} True{} False{} True{} False{} False{}:
662 {==}
663 case True{} False{} True{} True{} False{} True{} False{} False{}:
664 {==}
665 case False{} True{} True{} True{} False{} True{} False{} False{}:
666 {==}
667 case True{} True{} True{} True{} False{} True{} False{} False{}:
668 {==}
669 case False{} False{} False{} False{} True{} True{} False{} False{}:
670 {==}
671 case True{} False{} False{} False{} True{} True{} False{} False{}:
672 {==}
673 case False{} True{} False{} False{} True{} True{} False{} False{}:
674 {==}
675 case True{} True{} False{} False{} True{} True{} False{} False{}:
676 {==}
677 case False{} False{} True{} False{} True{} True{} False{} False{}:
678 {==}
679 case True{} False{} True{} False{} True{} True{} False{} False{}:
680 {==}
681 case False{} True{} True{} False{} True{} True{} False{} False{}:
682 {==}
683 case True{} True{} True{} False{} True{} True{} False{} False{}:
684 {==}
685 case False{} False{} False{} True{} True{} True{} False{} False{}:
686 {==}
687 case True{} False{} False{} True{} True{} True{} False{} False{}:
688 {==}
689 case False{} True{} False{} True{} True{} True{} False{} False{}:
690 {==}
691 case True{} True{} False{} True{} True{} True{} False{} False{}:
692 {==}
693 case False{} False{} True{} True{} True{} True{} False{} False{}:
694 {==}
695 case True{} False{} True{} True{} True{} True{} False{} False{}:
696 {==}
697 case False{} True{} True{} True{} True{} True{} False{} False{}:
698 {==}
699 case True{} True{} True{} True{} True{} True{} False{} False{}:
700 {==}
701 case False{} False{} False{} False{} False{} False{} True{} False{}:
702 {==}
703 case True{} False{} False{} False{} False{} False{} True{} False{}:
704 {==}
705 case False{} True{} False{} False{} False{} False{} True{} False{}:
706 {==}
707 case True{} True{} False{} False{} False{} False{} True{} False{}:
708 {==}
709 case False{} False{} True{} False{} False{} False{} True{} False{}:
710 {==}
711 case True{} False{} True{} False{} False{} False{} True{} False{}:
712 {==}
713 case False{} True{} True{} False{} False{} False{} True{} False{}:
714 {==}
715 case True{} True{} True{} False{} False{} False{} True{} False{}:
716 {==}
717 case False{} False{} False{} True{} False{} False{} True{} False{}:
718 {==}
719 case True{} False{} False{} True{} False{} False{} True{} False{}:
720 {==}
721 case False{} True{} False{} True{} False{} False{} True{} False{}:
722 {==}
723 case True{} True{} False{} True{} False{} False{} True{} False{}:
724 {==}
725 case False{} False{} True{} True{} False{} False{} True{} False{}:
726 {==}
727 case True{} False{} True{} True{} False{} False{} True{} False{}:
728 {==}
729 case False{} True{} True{} True{} False{} False{} True{} False{}:
730 {==}
731 case True{} True{} True{} True{} False{} False{} True{} False{}:
732 {==}
733 case False{} False{} False{} False{} True{} False{} True{} False{}:
734 {==}
735 case True{} False{} False{} False{} True{} False{} True{} False{}:
736 {==}
737 case False{} True{} False{} False{} True{} False{} True{} False{}:
738 {==}
739 case True{} True{} False{} False{} True{} False{} True{} False{}:
740 {==}
741 case False{} False{} True{} False{} True{} False{} True{} False{}:
742 {==}
743 case True{} False{} True{} False{} True{} False{} True{} False{}:
744 {==}
745 case False{} True{} True{} False{} True{} False{} True{} False{}:
746 {==}
747 case True{} True{} True{} False{} True{} False{} True{} False{}:
748 {==}
749 case False{} False{} False{} True{} True{} False{} True{} False{}:
750 {==}
751 case True{} False{} False{} True{} True{} False{} True{} False{}:
752 {==}
753 case False{} True{} False{} True{} True{} False{} True{} False{}:
754 {==}
755 case True{} True{} False{} True{} True{} False{} True{} False{}:
756 {==}
757 case False{} False{} True{} True{} True{} False{} True{} False{}:
758 {==}
759 case True{} False{} True{} True{} True{} False{} True{} False{}:
760 {==}
761 case False{} True{} True{} True{} True{} False{} True{} False{}:
762 {==}
763 case True{} True{} True{} True{} True{} False{} True{} False{}:
764 {==}
765 case False{} False{} False{} False{} False{} True{} True{} False{}:
766 {==}
767 case True{} False{} False{} False{} False{} True{} True{} False{}:
768 {==}
769 case False{} True{} False{} False{} False{} True{} True{} False{}:
770 {==}
771 case True{} True{} False{} False{} False{} True{} True{} False{}:
772 {==}
773 case False{} False{} True{} False{} False{} True{} True{} False{}:
774 {==}
775 case True{} False{} True{} False{} False{} True{} True{} False{}:
776 {==}
777 case False{} True{} True{} False{} False{} True{} True{} False{}:
778 {==}
779 case True{} True{} True{} False{} False{} True{} True{} False{}:
780 {==}
781 case False{} False{} False{} True{} False{} True{} True{} False{}:
782 {==}
783 case True{} False{} False{} True{} False{} True{} True{} False{}:
784 {==}
785 case False{} True{} False{} True{} False{} True{} True{} False{}:
786 {==}
787 case True{} True{} False{} True{} False{} True{} True{} False{}:
788 {==}
789 case False{} False{} True{} True{} False{} True{} True{} False{}:
790 {==}
791 case True{} False{} True{} True{} False{} True{} True{} False{}:
792 {==}
793 case False{} True{} True{} True{} False{} True{} True{} False{}:
794 {==}
795 case True{} True{} True{} True{} False{} True{} True{} False{}:
796 {==}
797 case False{} False{} False{} False{} True{} True{} True{} False{}:
798 {==}
799 case True{} False{} False{} False{} True{} True{} True{} False{}:
800 {==}
801 case False{} True{} False{} False{} True{} True{} True{} False{}:
802 {==}
803 case True{} True{} False{} False{} True{} True{} True{} False{}:
804 {==}
805 case False{} False{} True{} False{} True{} True{} True{} False{}:
806 {==}
807 case True{} False{} True{} False{} True{} True{} True{} False{}:
808 {==}
809 case False{} True{} True{} False{} True{} True{} True{} False{}:
810 {==}
811 case True{} True{} True{} False{} True{} True{} True{} False{}:
812 {==}
813 case False{} False{} False{} True{} True{} True{} True{} False{}:
814 {==}
815 case True{} False{} False{} True{} True{} True{} True{} False{}:
816 {==}
817 case False{} True{} False{} True{} True{} True{} True{} False{}:
818 {==}
819 case True{} True{} False{} True{} True{} True{} True{} False{}:
820 {==}
821 case False{} False{} True{} True{} True{} True{} True{} False{}:
822 {==}
823 case True{} False{} True{} True{} True{} True{} True{} False{}:
824 {==}
825 case False{} True{} True{} True{} True{} True{} True{} False{}:
826 {==}
827 case True{} True{} True{} True{} True{} True{} True{} False{}:
828 {==}
829 case False{} False{} False{} False{} False{} False{} False{} True{}:
830 {==}
831 case True{} False{} False{} False{} False{} False{} False{} True{}:
832 {==}
833 case False{} True{} False{} False{} False{} False{} False{} True{}:
834 {==}
835 case True{} True{} False{} False{} False{} False{} False{} True{}:
836 {==}
837 case False{} False{} True{} False{} False{} False{} False{} True{}:
838 {==}
839 case True{} False{} True{} False{} False{} False{} False{} True{}:
840 {==}
841 case False{} True{} True{} False{} False{} False{} False{} True{}:
842 {==}
843 case True{} True{} True{} False{} False{} False{} False{} True{}:
844 {==}
845 case False{} False{} False{} True{} False{} False{} False{} True{}:
846 {==}
847 case True{} False{} False{} True{} False{} False{} False{} True{}:
848 {==}
849 case False{} True{} False{} True{} False{} False{} False{} True{}:
850 {==}
851 case True{} True{} False{} True{} False{} False{} False{} True{}:
852 {==}
853 case False{} False{} True{} True{} False{} False{} False{} True{}:
854 {==}
855 case True{} False{} True{} True{} False{} False{} False{} True{}:
856 {==}
857 case False{} True{} True{} True{} False{} False{} False{} True{}:
858 {==}
859 case True{} True{} True{} True{} False{} False{} False{} True{}:
860 {==}
861 case False{} False{} False{} False{} True{} False{} False{} True{}:
862 {==}
863 case True{} False{} False{} False{} True{} False{} False{} True{}:
864 {==}
865 case False{} True{} False{} False{} True{} False{} False{} True{}:
866 {==}
867 case True{} True{} False{} False{} True{} False{} False{} True{}:
868 {==}
869 case False{} False{} True{} False{} True{} False{} False{} True{}:
870 {==}
871 case True{} False{} True{} False{} True{} False{} False{} True{}:
872 {==}
873 case False{} True{} True{} False{} True{} False{} False{} True{}:
874 {==}
875 case True{} True{} True{} False{} True{} False{} False{} True{}:
876 {==}
877 case False{} False{} False{} True{} True{} False{} False{} True{}:
878 {==}
879 case True{} False{} False{} True{} True{} False{} False{} True{}:
880 {==}
881 case False{} True{} False{} True{} True{} False{} False{} True{}:
882 {==}
883 case True{} True{} False{} True{} True{} False{} False{} True{}:
884 {==}
885 case False{} False{} True{} True{} True{} False{} False{} True{}:
886 {==}
887 case True{} False{} True{} True{} True{} False{} False{} True{}:
888 {==}
889 case False{} True{} True{} True{} True{} False{} False{} True{}:
890 {==}
891 case True{} True{} True{} True{} True{} False{} False{} True{}:
892 {==}
893 case False{} False{} False{} False{} False{} True{} False{} True{}:
894 {==}
895 case True{} False{} False{} False{} False{} True{} False{} True{}:
896 {==}
897 case False{} True{} False{} False{} False{} True{} False{} True{}:
898 {==}
899 case True{} True{} False{} False{} False{} True{} False{} True{}:
900 {==}
901 case False{} False{} True{} False{} False{} True{} False{} True{}:
902 {==}
903 case True{} False{} True{} False{} False{} True{} False{} True{}:
904 {==}
905 case False{} True{} True{} False{} False{} True{} False{} True{}:
906 {==}
907 case True{} True{} True{} False{} False{} True{} False{} True{}:
908 {==}
909 case False{} False{} False{} True{} False{} True{} False{} True{}:
910 {==}
911 case True{} False{} False{} True{} False{} True{} False{} True{}:
912 {==}
913 case False{} True{} False{} True{} False{} True{} False{} True{}:
914 {==}
915 case True{} True{} False{} True{} False{} True{} False{} True{}:
916 {==}
917 case False{} False{} True{} True{} False{} True{} False{} True{}:
918 {==}
919 case True{} False{} True{} True{} False{} True{} False{} True{}:
920 {==}
921 case False{} True{} True{} True{} False{} True{} False{} True{}:
922 {==}
923 case True{} True{} True{} True{} False{} True{} False{} True{}:
924 {==}
925 case False{} False{} False{} False{} True{} True{} False{} True{}:
926 {==}
927 case True{} False{} False{} False{} True{} True{} False{} True{}:
928 {==}
929 case False{} True{} False{} False{} True{} True{} False{} True{}:
930 {==}
931 case True{} True{} False{} False{} True{} True{} False{} True{}:
932 {==}
933 case False{} False{} True{} False{} True{} True{} False{} True{}:
934 {==}
935 case True{} False{} True{} False{} True{} True{} False{} True{}:
936 {==}
937 case False{} True{} True{} False{} True{} True{} False{} True{}:
938 {==}
939 case True{} True{} True{} False{} True{} True{} False{} True{}:
940 {==}
941 case False{} False{} False{} True{} True{} True{} False{} True{}:
942 {==}
943 case True{} False{} False{} True{} True{} True{} False{} True{}:
944 {==}
945 case False{} True{} False{} True{} True{} True{} False{} True{}:
946 {==}
947 case True{} True{} False{} True{} True{} True{} False{} True{}:
948 {==}
949 case False{} False{} True{} True{} True{} True{} False{} True{}:
950 {==}
951 case True{} False{} True{} True{} True{} True{} False{} True{}:
952 {==}
953 case False{} True{} True{} True{} True{} True{} False{} True{}:
954 {==}
955 case True{} True{} True{} True{} True{} True{} False{} True{}:
956 {==}
957 case False{} False{} False{} False{} False{} False{} True{} True{}:
958 {==}
959 case True{} False{} False{} False{} False{} False{} True{} True{}:
960 {==}
961 case False{} True{} False{} False{} False{} False{} True{} True{}:
962 {==}
963 case True{} True{} False{} False{} False{} False{} True{} True{}:
964 {==}
965 case False{} False{} True{} False{} False{} False{} True{} True{}:
966 {==}
967 case True{} False{} True{} False{} False{} False{} True{} True{}:
968 {==}
969 case False{} True{} True{} False{} False{} False{} True{} True{}:
970 {==}
971 case True{} True{} True{} False{} False{} False{} True{} True{}:
972 {==}
973 case False{} False{} False{} True{} False{} False{} True{} True{}:
974 {==}
975 case True{} False{} False{} True{} False{} False{} True{} True{}:
976 {==}
977 case False{} True{} False{} True{} False{} False{} True{} True{}:
978 {==}
979 case True{} True{} False{} True{} False{} False{} True{} True{}:
980 {==}
981 case False{} False{} True{} True{} False{} False{} True{} True{}:
982 {==}
983 case True{} False{} True{} True{} False{} False{} True{} True{}:
984 {==}
985 case False{} True{} True{} True{} False{} False{} True{} True{}:
986 {==}
987 case True{} True{} True{} True{} False{} False{} True{} True{}:
988 {==}
989 case False{} False{} False{} False{} True{} False{} True{} True{}:
990 {==}
991 case True{} False{} False{} False{} True{} False{} True{} True{}:
992 {==}
993 case False{} True{} False{} False{} True{} False{} True{} True{}:
994 {==}
995 case True{} True{} False{} False{} True{} False{} True{} True{}:
996 {==}
997 case False{} False{} True{} False{} True{} False{} True{} True{}:
998 {==}
999 case True{} False{} True{} False{} True{} False{} True{} True{}:
1000 {==}
1001 case False{} True{} True{} False{} True{} False{} True{} True{}:
1002 {==}
1003 case True{} True{} True{} False{} True{} False{} True{} True{}:
1004 {==}
1005 case False{} False{} False{} True{} True{} False{} True{} True{}:
1006 {==}
1007 case True{} False{} False{} True{} True{} False{} True{} True{}:
1008 {==}
1009 case False{} True{} False{} True{} True{} False{} True{} True{}:
1010 {==}
1011 case True{} True{} False{} True{} True{} False{} True{} True{}:
1012 {==}
1013 case False{} False{} True{} True{} True{} False{} True{} True{}:
1014 {==}
1015 case True{} False{} True{} True{} True{} False{} True{} True{}:
1016 {==}
1017 case False{} True{} True{} True{} True{} False{} True{} True{}:
1018 {==}
1019 case True{} True{} True{} True{} True{} False{} True{} True{}:
1020 {==}
1021 case False{} False{} False{} False{} False{} True{} True{} True{}:
1022 {==}
1023 case True{} False{} False{} False{} False{} True{} True{} True{}:
1024 {==}
1025 case False{} True{} False{} False{} False{} True{} True{} True{}:
1026 {==}
1027 case True{} True{} False{} False{} False{} True{} True{} True{}:
1028 {==}
1029 case False{} False{} True{} False{} False{} True{} True{} True{}:
1030 {==}
1031 case True{} False{} True{} False{} False{} True{} True{} True{}:
1032 {==}
1033 case False{} True{} True{} False{} False{} True{} True{} True{}:
1034 {==}
1035 case True{} True{} True{} False{} False{} True{} True{} True{}:
1036 {==}
1037 case False{} False{} False{} True{} False{} True{} True{} True{}:
1038 {==}
1039 case True{} False{} False{} True{} False{} True{} True{} True{}:
1040 {==}
1041 case False{} True{} False{} True{} False{} True{} True{} True{}:
1042 {==}
1043 case True{} True{} False{} True{} False{} True{} True{} True{}:
1044 {==}
1045 case False{} False{} True{} True{} False{} True{} True{} True{}:
1046 {==}
1047 case True{} False{} True{} True{} False{} True{} True{} True{}:
1048 {==}
1049 case False{} True{} True{} True{} False{} True{} True{} True{}:
1050 {==}
1051 case True{} True{} True{} True{} False{} True{} True{} True{}:
1052 {==}
1053 case False{} False{} False{} False{} True{} True{} True{} True{}:
1054 {==}
1055 case True{} False{} False{} False{} True{} True{} True{} True{}:
1056 {==}
1057 case False{} True{} False{} False{} True{} True{} True{} True{}:
1058 {==}
1059 case True{} True{} False{} False{} True{} True{} True{} True{}:
1060 {==}
1061 case False{} False{} True{} False{} True{} True{} True{} True{}:
1062 {==}
1063 case True{} False{} True{} False{} True{} True{} True{} True{}:
1064 {==}
1065 case False{} True{} True{} False{} True{} True{} True{} True{}:
1066 {==}
1067 case True{} True{} True{} False{} True{} True{} True{} True{}:
1068 {==}
1069 case False{} False{} False{} True{} True{} True{} True{} True{}:
1070 {==}
1071 case True{} False{} False{} True{} True{} True{} True{} True{}:
1072 {==}
1073 case False{} True{} False{} True{} True{} True{} True{} True{}:
1074 {==}
1075 case True{} True{} False{} True{} True{} True{} True{} True{}:
1076 {==}
1077 case False{} False{} True{} True{} True{} True{} True{} True{}:
1078 {==}
1079 case True{} False{} True{} True{} True{} True{} True{} True{}:
1080 {==}
1081 case False{} True{} True{} True{} True{} True{} True{} True{}:
1082 {==}
1083 case True{} True{} True{} True{} True{} True{} True{} True{}:
1084 {==}