def mul_inv_rs.bits
bend-osdev-gf@0.1.1.0 · PROOF.bend:5143
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
5143def mul_inv_rs.bits(+b0: Bool, +b1: Bool, +b2: Bool, +b3: Bool, +b4: Bool, +b5: Bool, +b6: Bool, +b7: Bool) -> {G.Gf8.mul(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})), G.Gf8.inv(G.Gf8.rs(), fixz(G.Gf8Bits.to(G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7})))) == 1 : U32}:
5144 match b0:
5145 case True{}:
5146 match b1:
5147 case True{}:
5148 match b2:
5149 case True{}:
5150 match b3:
5151 case True{}:
5152 match b4:
5153 case True{}:
5154 mul_inv_rs.s11111(b5, b6, b7)
5155 case False{}:
5156 mul_inv_rs.s11110(b5, b6, b7)
5157 case False{}:
5158 match b4:
5159 case True{}:
5160 mul_inv_rs.s11101(b5, b6, b7)
5161 case False{}:
5162 mul_inv_rs.s11100(b5, b6, b7)
5163 case False{}:
5164 match b3:
5165 case True{}:
5166 match b4:
5167 case True{}:
5168 mul_inv_rs.s11011(b5, b6, b7)
5169 case False{}:
5170 mul_inv_rs.s11010(b5, b6, b7)
5171 case False{}:
5172 match b4:
5173 case True{}:
5174 mul_inv_rs.s11001(b5, b6, b7)
5175 case False{}:
5176 mul_inv_rs.s11000(b5, b6, b7)
5177 case False{}:
5178 match b2:
5179 case True{}:
5180 match b3:
5181 case True{}:
5182 match b4:
5183 case True{}:
5184 mul_inv_rs.s10111(b5, b6, b7)
5185 case False{}:
5186 mul_inv_rs.s10110(b5, b6, b7)
5187 case False{}:
5188 match b4:
5189 case True{}:
5190 mul_inv_rs.s10101(b5, b6, b7)
5191 case False{}:
5192 mul_inv_rs.s10100(b5, b6, b7)
5193 case False{}:
5194 match b3:
5195 case True{}:
5196 match b4:
5197 case True{}:
5198 mul_inv_rs.s10011(b5, b6, b7)
5199 case False{}:
5200 mul_inv_rs.s10010(b5, b6, b7)
5201 case False{}:
5202 match b4:
5203 case True{}:
5204 mul_inv_rs.s10001(b5, b6, b7)
5205 case False{}:
5206 mul_inv_rs.s10000(b5, b6, b7)
5207 case False{}:
5208 match b1:
5209 case True{}:
5210 match b2:
5211 case True{}:
5212 match b3:
5213 case True{}:
5214 match b4:
5215 case True{}:
5216 mul_inv_rs.s01111(b5, b6, b7)
5217 case False{}:
5218 mul_inv_rs.s01110(b5, b6, b7)
5219 case False{}:
5220 match b4:
5221 case True{}:
5222 mul_inv_rs.s01101(b5, b6, b7)
5223 case False{}:
5224 mul_inv_rs.s01100(b5, b6, b7)
5225 case False{}:
5226 match b3:
5227 case True{}:
5228 match b4:
5229 case True{}:
5230 mul_inv_rs.s01011(b5, b6, b7)
5231 case False{}:
5232 mul_inv_rs.s01010(b5, b6, b7)
5233 case False{}:
5234 match b4:
5235 case True{}:
5236 mul_inv_rs.s01001(b5, b6, b7)
5237 case False{}:
5238 mul_inv_rs.s01000(b5, b6, b7)
5239 case False{}:
5240 match b2:
5241 case True{}:
5242 match b3:
5243 case True{}:
5244 match b4:
5245 case True{}:
5246 mul_inv_rs.s00111(b5, b6, b7)
5247 case False{}:
5248 mul_inv_rs.s00110(b5, b6, b7)
5249 case False{}:
5250 match b4:
5251 case True{}:
5252 mul_inv_rs.s00101(b5, b6, b7)
5253 case False{}:
5254 mul_inv_rs.s00100(b5, b6, b7)
5255 case False{}:
5256 match b3:
5257 case True{}:
5258 match b4:
5259 case True{}:
5260 mul_inv_rs.s00011(b5, b6, b7)
5261 case False{}:
5262 mul_inv_rs.s00010(b5, b6, b7)
5263 case False{}:
5264 match b4:
5265 case True{}:
5266 mul_inv_rs.s00001(b5, b6, b7)
5267 case False{}:
5268 mul_inv_rs.s00000(b5, b6, b7)