def mul_inv_aes.bits
bend-osdev-gf@0.1.1.0 · PROOF.bend:2877
import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
2877def mul_inv_aes.bits(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, +b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})), G.Gf8.inv(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})))) == 1 : U32}:
2878 match b0:
2879 case True{}:
2880 match b1:
2881 case True{}:
2882 match b2:
2883 case True{}:
2884 match b3:
2885 case True{}:
2886 match b4:
2887 case True{}:
2888 mul_inv_aes.s11111(b5, b6, b7)
2889 case False{}:
2890 mul_inv_aes.s11110(b5, b6, b7)
2891 case False{}:
2892 match b4:
2893 case True{}:
2894 mul_inv_aes.s11101(b5, b6, b7)
2895 case False{}:
2896 mul_inv_aes.s11100(b5, b6, b7)
2897 case False{}:
2898 match b3:
2899 case True{}:
2900 match b4:
2901 case True{}:
2902 mul_inv_aes.s11011(b5, b6, b7)
2903 case False{}:
2904 mul_inv_aes.s11010(b5, b6, b7)
2905 case False{}:
2906 match b4:
2907 case True{}:
2908 mul_inv_aes.s11001(b5, b6, b7)
2909 case False{}:
2910 mul_inv_aes.s11000(b5, b6, b7)
2911 case False{}:
2912 match b2:
2913 case True{}:
2914 match b3:
2915 case True{}:
2916 match b4:
2917 case True{}:
2918 mul_inv_aes.s10111(b5, b6, b7)
2919 case False{}:
2920 mul_inv_aes.s10110(b5, b6, b7)
2921 case False{}:
2922 match b4:
2923 case True{}:
2924 mul_inv_aes.s10101(b5, b6, b7)
2925 case False{}:
2926 mul_inv_aes.s10100(b5, b6, b7)
2927 case False{}:
2928 match b3:
2929 case True{}:
2930 match b4:
2931 case True{}:
2932 mul_inv_aes.s10011(b5, b6, b7)
2933 case False{}:
2934 mul_inv_aes.s10010(b5, b6, b7)
2935 case False{}:
2936 match b4:
2937 case True{}:
2938 mul_inv_aes.s10001(b5, b6, b7)
2939 case False{}:
2940 mul_inv_aes.s10000(b5, b6, b7)
2941 case False{}:
2942 match b1:
2943 case True{}:
2944 match b2:
2945 case True{}:
2946 match b3:
2947 case True{}:
2948 match b4:
2949 case True{}:
2950 mul_inv_aes.s01111(b5, b6, b7)
2951 case False{}:
2952 mul_inv_aes.s01110(b5, b6, b7)
2953 case False{}:
2954 match b4:
2955 case True{}:
2956 mul_inv_aes.s01101(b5, b6, b7)
2957 case False{}:
2958 mul_inv_aes.s01100(b5, b6, b7)
2959 case False{}:
2960 match b3:
2961 case True{}:
2962 match b4:
2963 case True{}:
2964 mul_inv_aes.s01011(b5, b6, b7)
2965 case False{}:
2966 mul_inv_aes.s01010(b5, b6, b7)
2967 case False{}:
2968 match b4:
2969 case True{}:
2970 mul_inv_aes.s01001(b5, b6, b7)
2971 case False{}:
2972 mul_inv_aes.s01000(b5, b6, b7)
2973 case False{}:
2974 match b2:
2975 case True{}:
2976 match b3:
2977 case True{}:
2978 match b4:
2979 case True{}:
2980 mul_inv_aes.s00111(b5, b6, b7)
2981 case False{}:
2982 mul_inv_aes.s00110(b5, b6, b7)
2983 case False{}:
2984 match b4:
2985 case True{}:
2986 mul_inv_aes.s00101(b5, b6, b7)
2987 case False{}:
2988 mul_inv_aes.s00100(b5, b6, b7)
2989 case False{}:
2990 match b3:
2991 case True{}:
2992 match b4:
2993 case True{}:
2994 mul_inv_aes.s00011(b5, b6, b7)
2995 case False{}:
2996 mul_inv_aes.s00010(b5, b6, b7)
2997 case False{}:
2998 match b4:
2999 case True{}:
3000 mul_inv_aes.s00001(b5, b6, b7)
3001 case False{}:
3002 mul_inv_aes.s00000(b5, b6, b7)