def exp_log_aes.bits
bend-osdev-gf@0.1.1.0 · PROOF.bend:4010
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
4010def exp_log_aes.bits(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, +b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.exp(G.Gf8.aes(), G.Gf8.log(G.Gf8.aes(), fixz(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})))) == fixz(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})) : U32}:
4011 match b0:
4012 case True{}:
4013 match b1:
4014 case True{}:
4015 match b2:
4016 case True{}:
4017 match b3:
4018 case True{}:
4019 match b4:
4020 case True{}:
4021 exp_log_aes.s11111(b5, b6, b7)
4022 case False{}:
4023 exp_log_aes.s11110(b5, b6, b7)
4024 case False{}:
4025 match b4:
4026 case True{}:
4027 exp_log_aes.s11101(b5, b6, b7)
4028 case False{}:
4029 exp_log_aes.s11100(b5, b6, b7)
4030 case False{}:
4031 match b3:
4032 case True{}:
4033 match b4:
4034 case True{}:
4035 exp_log_aes.s11011(b5, b6, b7)
4036 case False{}:
4037 exp_log_aes.s11010(b5, b6, b7)
4038 case False{}:
4039 match b4:
4040 case True{}:
4041 exp_log_aes.s11001(b5, b6, b7)
4042 case False{}:
4043 exp_log_aes.s11000(b5, b6, b7)
4044 case False{}:
4045 match b2:
4046 case True{}:
4047 match b3:
4048 case True{}:
4049 match b4:
4050 case True{}:
4051 exp_log_aes.s10111(b5, b6, b7)
4052 case False{}:
4053 exp_log_aes.s10110(b5, b6, b7)
4054 case False{}:
4055 match b4:
4056 case True{}:
4057 exp_log_aes.s10101(b5, b6, b7)
4058 case False{}:
4059 exp_log_aes.s10100(b5, b6, b7)
4060 case False{}:
4061 match b3:
4062 case True{}:
4063 match b4:
4064 case True{}:
4065 exp_log_aes.s10011(b5, b6, b7)
4066 case False{}:
4067 exp_log_aes.s10010(b5, b6, b7)
4068 case False{}:
4069 match b4:
4070 case True{}:
4071 exp_log_aes.s10001(b5, b6, b7)
4072 case False{}:
4073 exp_log_aes.s10000(b5, b6, b7)
4074 case False{}:
4075 match b1:
4076 case True{}:
4077 match b2:
4078 case True{}:
4079 match b3:
4080 case True{}:
4081 match b4:
4082 case True{}:
4083 exp_log_aes.s01111(b5, b6, b7)
4084 case False{}:
4085 exp_log_aes.s01110(b5, b6, b7)
4086 case False{}:
4087 match b4:
4088 case True{}:
4089 exp_log_aes.s01101(b5, b6, b7)
4090 case False{}:
4091 exp_log_aes.s01100(b5, b6, b7)
4092 case False{}:
4093 match b3:
4094 case True{}:
4095 match b4:
4096 case True{}:
4097 exp_log_aes.s01011(b5, b6, b7)
4098 case False{}:
4099 exp_log_aes.s01010(b5, b6, b7)
4100 case False{}:
4101 match b4:
4102 case True{}:
4103 exp_log_aes.s01001(b5, b6, b7)
4104 case False{}:
4105 exp_log_aes.s01000(b5, b6, b7)
4106 case False{}:
4107 match b2:
4108 case True{}:
4109 match b3:
4110 case True{}:
4111 match b4:
4112 case True{}:
4113 exp_log_aes.s00111(b5, b6, b7)
4114 case False{}:
4115 exp_log_aes.s00110(b5, b6, b7)
4116 case False{}:
4117 match b4:
4118 case True{}:
4119 exp_log_aes.s00101(b5, b6, b7)
4120 case False{}:
4121 exp_log_aes.s00100(b5, b6, b7)
4122 case False{}:
4123 match b3:
4124 case True{}:
4125 match b4:
4126 case True{}:
4127 exp_log_aes.s00011(b5, b6, b7)
4128 case False{}:
4129 exp_log_aes.s00010(b5, b6, b7)
4130 case False{}:
4131 match b4:
4132 case True{}:
4133 exp_log_aes.s00001(b5, b6, b7)
4134 case False{}:
4135 exp_log_aes.s00000(b5, b6, b7)