proofs/crypto/aes/sbox.bend source
proofs/crypto/aes/sbox.bend on the hub · documented module
import Baseimport ../../../src/crypto/aes/sbox.bend as Bimport ../../../spec/crypto/aes/aes.bend as S# Generated by tools/generators/aes/sbox.py. The constant-time byte# functions equal FIPS 197 on every U32 (both read only the low 8 bits).law sbox_byte_bits: for +b0: Bool for +b1: Bool for +b2: Bool for +b3: Bool for +b4: Bool for +b5: Bool for +b6: Bool for +b7: Bool {B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}def sbox_byte_bits(b0, b1, b2, b3, b4, b5, b6, b7): match b0 b1 b2 b3 b4 b5 b6 b7: case False{} False{} False{} False{} False{} False{} False{} False{}: {==} case True{} False{} False{} False{} False{} False{} False{} False{}: {==} case False{} True{} False{} False{} False{} False{} False{} False{}: {==} case True{} True{} False{} False{} False{} False{} False{} False{}: {==} case False{} False{} True{} False{} False{} False{} False{} False{}: {==} case True{} False{} True{} False{} False{} False{} False{} False{}: {==} case False{} True{} True{} False{} False{} False{} False{} False{}: {==} case True{} True{} True{} False{} False{} False{} False{} False{}: {==} case False{} False{} False{} True{} False{} False{} False{} False{}: {==} case True{} False{} False{} True{} False{} False{} False{} False{}: {==} case False{} True{} False{} True{} False{} False{} False{} False{}: {==} case True{} True{} False{} True{} False{} False{} False{} False{}: {==} case False{} False{} True{} True{} False{} False{} False{} False{}: {==} case True{} False{} True{} True{} False{} False{} False{} False{}: {==} case False{} True{} True{} True{} False{} False{} False{} False{}: {==} case True{} True{} True{} True{} False{} False{} False{} False{}: {==} case False{} False{} False{} False{} True{} False{} False{} False{}: {==} case True{} False{} False{} False{} True{} False{} False{} False{}: {==} case False{} True{} False{} False{} True{} False{} False{} False{}: {==} case True{} True{} False{} False{} True{} False{} False{} False{}: {==} case False{} False{} True{} False{} True{} False{} False{} False{}: {==} case True{} False{} True{} False{} True{} False{} False{} False{}: {==} case False{} True{} True{} False{} True{} False{} False{} False{}: {==} case True{} True{} True{} False{} True{} False{} False{} False{}: {==} case False{} False{} False{} True{} True{} False{} False{} False{}: {==} case True{} False{} False{} True{} True{} False{} False{} False{}: {==} case False{} True{} False{} True{} True{} False{} False{} False{}: {==} case True{} True{} False{} True{} True{} False{} False{} False{}: {==} case False{} False{} True{} True{} True{} False{} False{} False{}: {==} case True{} False{} True{} True{} True{} False{} False{} False{}: {==} case False{} True{} True{} True{} True{} False{} False{} False{}: {==} case True{} True{} True{} True{} True{} False{} False{} False{}: {==} case False{} False{} False{} False{} False{} True{} False{} False{}: {==} case True{} False{} False{} False{} False{} True{} False{} False{}: {==} case False{} True{} False{} False{} False{} True{} False{} False{}: {==} case True{} True{} False{} False{} False{} True{} False{} False{}: {==} case False{} False{} True{} False{} False{} True{} False{} False{}: {==} case True{} False{} True{} False{} False{} True{} False{} False{}: {==} case False{} True{} True{} False{} False{} True{} False{} False{}: {==} case True{} True{} True{} False{} False{} True{} False{} False{}: {==} case False{} False{} False{} True{} False{} True{} False{} False{}: {==} case True{} False{} False{} True{} False{} True{} False{} False{}: {==} case False{} True{} False{} True{} False{} True{} False{} False{}: {==} case True{} True{} False{} True{} False{} True{} False{} False{}: {==} case False{} False{} True{} True{} False{} True{} False{} False{}: {==} case True{} False{} True{} True{} False{} True{} False{} False{}: {==} case False{} True{} True{} True{} False{} True{} False{} False{}: {==} case True{} True{} True{} True{} False{} True{} False{} False{}: {==} case False{} False{} False{} False{} True{} True{} False{} False{}: {==} case True{} False{} False{} False{} True{} True{} False{} False{}: {==} case False{} True{} False{} False{} True{} True{} False{} False{}: {==} case True{} True{} False{} False{} True{} True{} False{} False{}: {==} case False{} False{} True{} False{} True{} True{} False{} False{}: {==} case True{} False{} True{} False{} True{} True{} False{} False{}: {==} case False{} True{} True{} False{} True{} True{} False{} False{}: {==} case True{} True{} True{} False{} True{} True{} False{} False{}: {==} case False{} False{} False{} True{} True{} True{} False{} False{}: {==} case True{} False{} False{} True{} True{} True{} False{} False{}: {==} case False{} True{} False{} True{} True{} True{} False{} False{}: {==} case True{} True{} False{} True{} True{} True{} False{} False{}: {==} case False{} False{} True{} True{} True{} True{} False{} False{}: {==} case True{} False{} True{} True{} True{} True{} False{} False{}: {==} case False{} True{} True{} True{} True{} True{} False{} False{}: {==} case True{} True{} True{} True{} True{} True{} False{} False{}: {==} case False{} False{} False{} False{} False{} False{} True{} False{}: {==} case True{} False{} False{} False{} False{} False{} True{} False{}: {==} case False{} True{} False{} False{} False{} False{} True{} False{}: {==} case True{} True{} False{} False{} False{} False{} True{} False{}: {==} case False{} False{} True{} False{} False{} False{} True{} False{}: {==} case True{} False{} True{} False{} False{} False{} True{} False{}: {==} case False{} True{} True{} False{} False{} False{} True{} False{}: {==} case True{} True{} True{} False{} False{} False{} True{} False{}: {==} case False{} False{} False{} True{} False{} False{} True{} False{}: {==} case True{} False{} False{} True{} False{} False{} True{} False{}: {==} case False{} True{} False{} True{} False{} False{} True{} False{}: {==} case True{} True{} False{} True{} False{} False{} True{} False{}: {==} case False{} False{} True{} True{} False{} False{} True{} False{}: {==} case True{} False{} True{} True{} False{} False{} True{} False{}: {==} case False{} True{} True{} True{} False{} False{} True{} False{}: {==} case True{} True{} True{} True{} False{} False{} True{} False{}: {==} case False{} False{} False{} False{} True{} False{} True{} False{}: {==} case True{} False{} False{} False{} True{} False{} True{} False{}: {==} case False{} True{} False{} False{} True{} False{} True{} False{}: {==} case True{} True{} False{} False{} True{} False{} True{} False{}: {==} case False{} False{} True{} False{} True{} False{} True{} False{}: {==} case True{} False{} True{} False{} True{} False{} True{} False{}: {==} case False{} True{} True{} False{} True{} False{} True{} False{}: {==} case True{} True{} True{} False{} True{} False{} True{} False{}: {==} case False{} False{} False{} True{} True{} False{} True{} False{}: {==} case True{} False{} False{} True{} True{} False{} True{} False{}: {==} case False{} True{} False{} True{} True{} False{} True{} False{}: {==} case True{} True{} False{} True{} True{} False{} True{} False{}: {==} case False{} False{} True{} True{} True{} False{} True{} False{}: {==} case True{} False{} True{} True{} True{} False{} True{} False{}: {==} case False{} True{} True{} True{} True{} False{} True{} False{}: {==} case True{} True{} True{} True{} True{} False{} True{} False{}: {==} case False{} False{} False{} False{} False{} True{} True{} False{}: {==} case True{} False{} False{} False{} False{} True{} True{} False{}: {==} case False{} True{} False{} False{} False{} True{} True{} False{}: {==} case True{} True{} False{} False{} False{} True{} True{} False{}: {==} case False{} False{} True{} False{} False{} True{} True{} False{}: {==} case True{} False{} True{} False{} False{} True{} True{} False{}: {==} case False{} True{} True{} False{} False{} True{} True{} False{}: {==} case True{} True{} True{} False{} False{} True{} True{} False{}: {==} case False{} False{} False{} True{} False{} True{} True{} False{}: {==} case True{} False{} False{} True{} False{} True{} True{} False{}: {==} case False{} True{} False{} True{} False{} True{} True{} False{}: {==} case True{} True{} False{} True{} False{} True{} True{} False{}: {==} case False{} False{} True{} True{} False{} True{} True{} False{}: {==} case True{} False{} True{} True{} False{} True{} True{} False{}: {==} case False{} True{} True{} True{} False{} True{} True{} False{}: {==} case True{} True{} True{} True{} False{} True{} True{} False{}: {==} case False{} False{} False{} False{} True{} True{} True{} False{}: {==} case True{} False{} False{} False{} True{} True{} True{} False{}: {==} case False{} True{} False{} False{} True{} True{} True{} False{}: {==} case True{} True{} False{} False{} True{} True{} True{} False{}: {==} case False{} False{} True{} False{} True{} True{} True{} False{}: {==} case True{} False{} True{} False{} True{} True{} True{} False{}: {==} case False{} True{} True{} False{} True{} True{} True{} False{}: {==} case True{} True{} True{} False{} True{} True{} True{} False{}: {==} case False{} False{} False{} True{} True{} True{} True{} False{}: {==} case True{} False{} False{} True{} True{} True{} True{} False{}: {==} case False{} True{} False{} True{} True{} True{} True{} False{}: {==} case True{} True{} False{} True{} True{} True{} True{} False{}: {==} case False{} False{} True{} True{} True{} True{} True{} False{}: {==} case True{} False{} True{} True{} True{} True{} True{} False{}: {==} case False{} True{} True{} True{} True{} True{} True{} False{}: {==} case True{} True{} True{} True{} True{} True{} True{} False{}: {==} case False{} False{} False{} False{} False{} False{} False{} True{}: {==} case True{} False{} False{} False{} False{} False{} False{} True{}: {==} case False{} True{} False{} False{} False{} False{} False{} True{}: {==} case True{} True{} False{} False{} False{} False{} False{} True{}: {==} case False{} False{} True{} False{} False{} False{} False{} True{}: {==} case True{} False{} True{} False{} False{} False{} False{} True{}: {==} case False{} True{} True{} False{} False{} False{} False{} True{}: {==} case True{} True{} True{} False{} False{} False{} False{} True{}: {==} case False{} False{} False{} True{} False{} False{} False{} True{}: {==} case True{} False{} False{} True{} False{} False{} False{} True{}: {==} case False{} True{} False{} True{} False{} False{} False{} True{}: {==} case True{} True{} False{} True{} False{} False{} False{} True{}: {==} case False{} False{} True{} True{} False{} False{} False{} True{}: {==} case True{} False{} True{} True{} False{} False{} False{} True{}: {==} case False{} True{} True{} True{} False{} False{} False{} True{}: {==} case True{} True{} True{} True{} False{} False{} False{} True{}: {==} case False{} False{} False{} False{} True{} False{} False{} True{}: {==} case True{} False{} False{} False{} True{} False{} False{} True{}: {==} case False{} True{} False{} False{} True{} False{} False{} True{}: {==} case True{} True{} False{} False{} True{} False{} False{} True{}: {==} case False{} False{} True{} False{} True{} False{} False{} True{}: {==} case True{} False{} True{} False{} True{} False{} False{} True{}: {==} case False{} True{} True{} False{} True{} False{} False{} True{}: {==} case True{} True{} True{} False{} True{} False{} False{} True{}: {==} case False{} False{} False{} True{} True{} False{} False{} True{}: {==} case True{} False{} False{} True{} True{} False{} False{} True{}: {==} case False{} True{} False{} True{} True{} False{} False{} True{}: {==} case True{} True{} False{} True{} True{} False{} False{} True{}: {==} case False{} False{} True{} True{} True{} False{} False{} True{}: {==} case True{} False{} True{} True{} True{} False{} False{} True{}: {==} case False{} True{} True{} True{} True{} False{} False{} True{}: {==} case True{} True{} True{} True{} True{} False{} False{} True{}: {==} case False{} False{} False{} False{} False{} True{} False{} True{}: {==} case True{} False{} False{} False{} False{} True{} False{} True{}: {==} case False{} True{} False{} False{} False{} True{} False{} True{}: {==} case True{} True{} False{} False{} False{} True{} False{} True{}: {==} case False{} False{} True{} False{} False{} True{} False{} True{}: {==} case True{} False{} True{} False{} False{} True{} False{} True{}: {==} case False{} True{} True{} False{} False{} True{} False{} True{}: {==} case True{} True{} True{} False{} False{} True{} False{} True{}: {==} case False{} False{} False{} True{} False{} True{} False{} True{}: {==} case True{} False{} False{} True{} False{} True{} False{} True{}: {==} case False{} True{} False{} True{} False{} True{} False{} True{}: {==} case True{} True{} False{} True{} False{} True{} False{} True{}: {==} case False{} False{} True{} True{} False{} True{} False{} True{}: {==} case True{} False{} True{} True{} False{} True{} False{} True{}: {==} case False{} True{} True{} True{} False{} True{} False{} True{}: {==} case True{} True{} True{} True{} False{} True{} False{} True{}: {==} case False{} False{} False{} False{} True{} True{} False{} True{}: {==} case True{} False{} False{} False{} True{} True{} False{} True{}: {==} case False{} True{} False{} False{} True{} True{} False{} True{}: {==} case True{} True{} False{} False{} True{} True{} False{} True{}: {==} case False{} False{} True{} False{} True{} True{} False{} True{}: {==} case True{} False{} True{} False{} True{} True{} False{} True{}: {==} case False{} True{} True{} False{} True{} True{} False{} True{}: {==} case True{} True{} True{} False{} True{} True{} False{} True{}: {==} case False{} False{} False{} True{} True{} True{} False{} True{}: {==} case True{} False{} False{} True{} True{} True{} False{} True{}: {==} case False{} True{} False{} True{} True{} True{} False{} True{}: {==} case True{} True{} False{} True{} True{} True{} False{} True{}: {==} case False{} False{} True{} True{} True{} True{} False{} True{}: {==} case True{} False{} True{} True{} True{} True{} False{} True{}: {==} case False{} True{} True{} True{} True{} True{} False{} True{}: {==} case True{} True{} True{} True{} True{} True{} False{} True{}: {==} case False{} False{} False{} False{} False{} False{} True{} True{}: {==} case True{} False{} False{} False{} False{} False{} True{} True{}: {==} case False{} True{} False{} False{} False{} False{} True{} True{}: {==} case True{} True{} False{} False{} False{} False{} True{} True{}: {==} case False{} False{} True{} False{} False{} False{} True{} True{}: {==} case True{} False{} True{} False{} False{} False{} True{} True{}: {==} case False{} True{} True{} False{} False{} False{} True{} True{}: {==} case True{} True{} True{} False{} False{} False{} True{} True{}: {==} case False{} False{} False{} True{} False{} False{} True{} True{}: {==} case True{} False{} False{} True{} False{} False{} True{} True{}: {==} case False{} True{} False{} True{} False{} False{} True{} True{}: {==} case True{} True{} False{} True{} False{} False{} True{} True{}: {==} case False{} False{} True{} True{} False{} False{} True{} True{}: {==} case True{} False{} True{} True{} False{} False{} True{} True{}: {==} case False{} True{} True{} True{} False{} False{} True{} True{}: {==} case True{} True{} True{} True{} False{} False{} True{} True{}: {==} case False{} False{} False{} False{} True{} False{} True{} True{}: {==} case True{} False{} False{} False{} True{} False{} True{} True{}: {==} case False{} True{} False{} False{} True{} False{} True{} True{}: {==} case True{} True{} False{} False{} True{} False{} True{} True{}: {==} case False{} False{} True{} False{} True{} False{} True{} True{}: {==} case True{} False{} True{} False{} True{} False{} True{} True{}: {==} case False{} True{} True{} False{} True{} False{} True{} True{}: {==} case True{} True{} True{} False{} True{} False{} True{} True{}: {==} case False{} False{} False{} True{} True{} False{} True{} True{}: {==} case True{} False{} False{} True{} True{} False{} True{} True{}: {==} case False{} True{} False{} True{} True{} False{} True{} True{}: {==} case True{} True{} False{} True{} True{} False{} True{} True{}: {==} case False{} False{} True{} True{} True{} False{} True{} True{}: {==} case True{} False{} True{} True{} True{} False{} True{} True{}: {==} case False{} True{} True{} True{} True{} False{} True{} True{}: {==} case True{} True{} True{} True{} True{} False{} True{} True{}: {==} case False{} False{} False{} False{} False{} True{} True{} True{}: {==} case True{} False{} False{} False{} False{} True{} True{} True{}: {==} case False{} True{} False{} False{} False{} True{} True{} True{}: {==} case True{} True{} False{} False{} False{} True{} True{} True{}: {==} case False{} False{} True{} False{} False{} True{} True{} True{}: {==} case True{} False{} True{} False{} False{} True{} True{} True{}: {==} case False{} True{} True{} False{} False{} True{} True{} True{}: {==} case True{} True{} True{} False{} False{} True{} True{} True{}: {==} case False{} False{} False{} True{} False{} True{} True{} True{}: {==} case True{} False{} False{} True{} False{} True{} True{} True{}: {==} case False{} True{} False{} True{} False{} True{} True{} True{}: {==} case True{} True{} False{} True{} False{} True{} True{} True{}: {==} case False{} False{} True{} True{} False{} True{} True{} True{}: {==} case True{} False{} True{} True{} False{} True{} True{} True{}: {==} case False{} True{} True{} True{} False{} True{} True{} True{}: {==} case True{} True{} True{} True{} False{} True{} True{} True{}: {==} case False{} False{} False{} False{} True{} True{} True{} True{}: {==} case True{} False{} False{} False{} True{} True{} True{} True{}: {==} case False{} True{} False{} False{} True{} True{} True{} True{}: {==} case True{} True{} False{} False{} True{} True{} True{} True{}: {==} case False{} False{} True{} False{} True{} True{} True{} True{}: {==} case True{} False{} True{} False{} True{} True{} True{} True{}: {==} case False{} True{} True{} False{} True{} True{} True{} True{}: {==} case True{} True{} True{} False{} True{} True{} True{} True{}: {==} case False{} False{} False{} True{} True{} True{} True{} True{}: {==} case True{} False{} False{} True{} True{} True{} True{} True{}: {==} case False{} True{} False{} True{} True{} True{} True{} True{}: {==} case True{} True{} False{} True{} True{} True{} True{} True{}: {==} case False{} False{} True{} True{} True{} True{} True{} True{}: {==} case True{} False{} True{} True{} True{} True{} True{} True{}: {==} case False{} True{} True{} True{} True{} True{} True{} True{}: {==} case True{} True{} True{} True{} True{} True{} True{} True{}: {==}law sbox_bits: for +b0: Bool for +b1: Bool for +b2: Bool for +b3: Bool for +b4: Bool for +b5: Bool for +b6: Bool for +b7: Bool for +b8: Bool for +b9: Bool for +b10: Bool for +b11: Bool for +b12: Bool for +b13: Bool for +b14: Bool for +b15: Bool for +b16: Bool for +b17: Bool for +b18: Bool for +b19: Bool for +b20: Bool for +b21: Bool for +b22: Bool for +b23: Bool for +b24: Bool for +b25: Bool for +b26: Bool for +b27: Bool for +b28: Bool for +b29: Bool for +b30: Bool for +b31: Bool {B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}def sbox_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31): Equal.trans(U32, B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), {==}, Equal.trans(U32, B.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), S.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), sbox_byte_bits(b0, b1, b2, b3, b4, b5, b6, b7), {==}))law sbox_ok: for +x: U32 {B.sbox(x) == S.sbox(x) : U32}def sbox_ok(x): match x: case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: sbox_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31)law xtime_bits: for b0: Bool for b1: Bool for b2: Bool for b3: Bool for b4: Bool for b5: Bool for b6: Bool for b7: Bool for b8: Bool for b9: Bool for b10: Bool for b11: Bool for b12: Bool for b13: Bool for b14: Bool for b15: Bool for b16: Bool for b17: Bool for b18: Bool for b19: Bool for b20: Bool for b21: Bool for b22: Bool for b23: Bool for b24: Bool for b25: Bool for b26: Bool for b27: Bool for b28: Bool for b29: Bool for b30: Bool for b31: Bool {B.xtime(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == S.mul(2, U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}def xtime_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31): match b0 b1 b2 b3 b4 b5 b6 b7: case False{} False{} False{} False{} False{} False{} False{} False{}: {==} case True{} False{} False{} False{} False{} False{} False{} False{}: {==} case False{} True{} False{} False{} False{} False{} False{} False{}: {==} case True{} True{} False{} False{} False{} False{} False{} False{}: {==} case False{} False{} True{} False{} False{} False{} False{} False{}: {==} case True{} False{} True{} False{} False{} False{} False{} False{}: {==} case False{} True{} True{} False{} False{} False{} False{} False{}: {==} case True{} True{} True{} False{} False{} False{} False{} False{}: {==} case False{} False{} False{} True{} False{} False{} False{} False{}: {==} case True{} False{} False{} True{} False{} False{} False{} False{}: {==} case False{} True{} False{} True{} False{} False{} False{} False{}: {==} case True{} True{} False{} True{} False{} False{} False{} False{}: {==} case False{} False{} True{} True{} False{} False{} False{} False{}: {==} case True{} False{} True{} True{} False{} False{} False{} False{}: {==} case False{} True{} True{} True{} False{} False{} False{} False{}: {==} case True{} True{} True{} True{} False{} False{} False{} False{}: {==} case False{} False{} False{} False{} True{} False{} False{} False{}: {==} case True{} False{} False{} False{} True{} False{} False{} False{}: {==} case False{} True{} False{} False{} True{} False{} False{} False{}: {==} case True{} True{} False{} False{} True{} False{} False{} False{}: {==} case False{} False{} True{} False{} True{} False{} False{} False{}: {==} case True{} False{} True{} False{} True{} False{} False{} False{}: {==} case False{} True{} True{} False{} True{} False{} False{} False{}: {==} case True{} True{} True{} False{} True{} False{} False{} False{}: {==} case False{} False{} False{} True{} True{} False{} False{} False{}: {==} case True{} False{} False{} True{} True{} False{} False{} False{}: {==} case False{} True{} False{} True{} True{} False{} False{} False{}: {==} case True{} True{} False{} True{} True{} False{} False{} False{}: {==} case False{} False{} True{} True{} True{} False{} False{} False{}: {==} case True{} False{} True{} True{} True{} False{} False{} False{}: {==} case False{} True{} True{} True{} True{} False{} False{} False{}: {==} case True{} True{} True{} True{} True{} False{} False{} False{}: {==} case False{} False{} False{} False{} False{} True{} False{} False{}: {==} case True{} False{} False{} False{} False{} True{} False{} False{}: {==} case False{} True{} False{} False{} False{} True{} False{} False{}: {==} case True{} True{} False{} False{} False{} True{} False{} False{}: {==} case False{} False{} True{} False{} False{} True{} False{} False{}: {==} case True{} False{} True{} False{} False{} True{} False{} False{}: {==} case False{} True{} True{} False{} False{} True{} False{} False{}: {==} case True{} True{} True{} False{} False{} True{} False{} False{}: {==} case False{} False{} False{} True{} False{} True{} False{} False{}: {==} case True{} False{} False{} True{} False{} True{} False{} False{}: {==} case False{} True{} False{} True{} False{} True{} False{} False{}: {==} case True{} True{} False{} True{} False{} True{} False{} False{}: {==} case False{} False{} True{} True{} False{} True{} False{} False{}: {==} case True{} False{} True{} True{} False{} True{} False{} False{}: {==} case False{} True{} True{} True{} False{} True{} False{} False{}: {==} case True{} True{} True{} True{} False{} True{} False{} False{}: {==} case False{} False{} False{} False{} True{} True{} False{} False{}: {==} case True{} False{} False{} False{} True{} True{} False{} False{}: {==} case False{} True{} False{} False{} True{} True{} False{} False{}: {==} case True{} True{} False{} False{} True{} True{} False{} False{}: {==} case False{} False{} True{} False{} True{} True{} False{} False{}: {==} case True{} False{} True{} False{} True{} True{} False{} False{}: {==} case False{} True{} True{} False{} True{} True{} False{} False{}: {==} case True{} True{} True{} False{} True{} True{} False{} False{}: {==} case False{} False{} False{} True{} True{} True{} False{} False{}: {==} case True{} False{} False{} True{} True{} True{} False{} False{}: {==} case False{} True{} False{} True{} True{} True{} False{} False{}: {==} case True{} True{} False{} True{} True{} True{} False{} False{}: {==} case False{} False{} True{} True{} True{} True{} False{} False{}: {==} case True{} False{} True{} True{} True{} True{} False{} False{}: {==} case False{} True{} True{} True{} True{} True{} False{} False{}: {==} case True{} True{} True{} True{} True{} True{} False{} False{}: {==} case False{} False{} False{} False{} False{} False{} True{} False{}: {==} case True{} False{} False{} False{} False{} False{} True{} False{}: {==} case False{} True{} False{} False{} False{} False{} True{} False{}: {==} case True{} True{} False{} False{} False{} False{} True{} False{}: {==} case False{} False{} True{} False{} False{} False{} True{} False{}: {==} case True{} False{} True{} False{} False{} False{} True{} False{}: {==} case False{} True{} True{} False{} False{} False{} True{} False{}: {==} case True{} True{} True{} False{} False{} False{} True{} False{}: {==} case False{} False{} False{} True{} False{} False{} True{} False{}: {==} case True{} False{} False{} True{} False{} False{} True{} False{}: {==} case False{} True{} False{} True{} False{} False{} True{} False{}: {==} case True{} True{} False{} True{} False{} False{} True{} False{}: {==} case False{} False{} True{} True{} False{} False{} True{} False{}: {==} case True{} False{} True{} True{} False{} False{} True{} False{}: {==} case False{} True{} True{} True{} False{} False{} True{} False{}: {==} case True{} True{} True{} True{} False{} False{} True{} False{}: {==} case False{} False{} False{} False{} True{} False{} True{} False{}: {==} case True{} False{} False{} False{} True{} False{} True{} False{}: {==} case False{} True{} False{} False{} True{} False{} True{} False{}: {==} case True{} True{} False{} False{} True{} False{} True{} False{}: {==} case False{} False{} True{} False{} True{} False{} True{} False{}: {==} case True{} False{} True{} False{} True{} False{} True{} False{}: {==} case False{} True{} True{} False{} True{} False{} True{} False{}: {==} case True{} True{} True{} False{} True{} False{} True{} False{}: {==} case False{} False{} False{} True{} True{} False{} True{} False{}: {==} case True{} False{} False{} True{} True{} False{} True{} False{}: {==} case False{} True{} False{} True{} True{} False{} True{} False{}: {==} case True{} True{} False{} True{} True{} False{} True{} False{}: {==} case False{} False{} True{} True{} True{} False{} True{} False{}: {==} case True{} False{} True{} True{} True{} False{} True{} False{}: {==} case False{} True{} True{} True{} True{} False{} True{} False{}: {==} case True{} True{} True{} True{} True{} False{} True{} False{}: {==} case False{} False{} False{} False{} False{} True{} True{} False{}: {==} case True{} False{} False{} False{} False{} True{} True{} False{}: {==} case False{} True{} False{} False{} False{} True{} True{} False{}: {==} case True{} True{} False{} False{} False{} True{} True{} False{}: {==} case False{} False{} True{} False{} False{} True{} True{} False{}: {==} case True{} False{} True{} False{} False{} True{} True{} False{}: {==} case False{} True{} True{} False{} False{} True{} True{} False{}: {==} case True{} True{} True{} False{} False{} True{} True{} False{}: {==} case False{} False{} False{} True{} False{} True{} True{} False{}: {==} case True{} False{} False{} True{} False{} True{} True{} False{}: {==} case False{} True{} False{} True{} False{} True{} True{} False{}: {==} case True{} True{} False{} True{} False{} True{} True{} False{}: {==} case False{} False{} True{} True{} False{} True{} True{} False{}: {==} case True{} False{} True{} True{} False{} True{} True{} False{}: {==} case False{} True{} True{} True{} False{} True{} True{} False{}: {==} case True{} True{} True{} True{} False{} True{} True{} False{}: {==} case False{} False{} False{} False{} True{} True{} True{} False{}: {==} case True{} False{} False{} False{} True{} True{} True{} False{}: {==} case False{} True{} False{} False{} True{} True{} True{} False{}: {==} case True{} True{} False{} False{} True{} True{} True{} False{}: {==} case False{} False{} True{} False{} True{} True{} True{} False{}: {==} case True{} False{} True{} False{} True{} True{} True{} False{}: {==} case False{} True{} True{} False{} True{} True{} True{} False{}: {==} case True{} True{} True{} False{} True{} True{} True{} False{}: {==} case False{} False{} False{} True{} True{} True{} True{} False{}: {==} case True{} False{} False{} True{} True{} True{} True{} False{}: {==} case False{} True{} False{} True{} True{} True{} True{} False{}: {==} case True{} True{} False{} True{} True{} True{} True{} False{}: {==} case False{} False{} True{} True{} True{} True{} True{} False{}: {==} case True{} False{} True{} True{} True{} True{} True{} False{}: {==} case False{} True{} True{} True{} True{} True{} True{} False{}: {==} case True{} True{} True{} True{} True{} True{} True{} False{}: {==} case False{} False{} False{} False{} False{} False{} False{} True{}: {==} case True{} False{} False{} False{} False{} False{} False{} True{}: {==} case False{} True{} False{} False{} False{} False{} False{} True{}: {==} case True{} True{} False{} False{} False{} False{} False{} True{}: {==} case False{} False{} True{} False{} False{} False{} False{} True{}: {==} case True{} False{} True{} False{} False{} False{} False{} True{}: {==} case False{} True{} True{} False{} False{} False{} False{} True{}: {==} case True{} True{} True{} False{} False{} False{} False{} True{}: {==} case False{} False{} False{} True{} False{} False{} False{} True{}: {==} case True{} False{} False{} True{} False{} False{} False{} True{}: {==} case False{} True{} False{} True{} False{} False{} False{} True{}: {==} case True{} True{} False{} True{} False{} False{} False{} True{}: {==} case False{} False{} True{} True{} False{} False{} False{} True{}: {==} case True{} False{} True{} True{} False{} False{} False{} True{}: {==} case False{} True{} True{} True{} False{} False{} False{} True{}: {==} case True{} True{} True{} True{} False{} False{} False{} True{}: {==} case False{} False{} False{} False{} True{} False{} False{} True{}: {==} case True{} False{} False{} False{} True{} False{} False{} True{}: {==} case False{} True{} False{} False{} True{} False{} False{} True{}: {==} case True{} True{} False{} False{} True{} False{} False{} True{}: {==} case False{} False{} True{} False{} True{} False{} False{} True{}: {==} case True{} False{} True{} False{} True{} False{} False{} True{}: {==} case False{} True{} True{} False{} True{} False{} False{} True{}: {==} case True{} True{} True{} False{} True{} False{} False{} True{}: {==} case False{} False{} False{} True{} True{} False{} False{} True{}: {==} case True{} False{} False{} True{} True{} False{} False{} True{}: {==} case False{} True{} False{} True{} True{} False{} False{} True{}: {==} case True{} True{} False{} True{} True{} False{} False{} True{}: {==} case False{} False{} True{} True{} True{} False{} False{} True{}: {==} case True{} False{} True{} True{} True{} False{} False{} True{}: {==} case False{} True{} True{} True{} True{} False{} False{} True{}: {==} case True{} True{} True{} True{} True{} False{} False{} True{}: {==} case False{} False{} False{} False{} False{} True{} False{} True{}: {==} case True{} False{} False{} False{} False{} True{} False{} True{}: {==} case False{} True{} False{} False{} False{} True{} False{} True{}: {==} case True{} True{} False{} False{} False{} True{} False{} True{}: {==} case False{} False{} True{} False{} False{} True{} False{} True{}: {==} case True{} False{} True{} False{} False{} True{} False{} True{}: {==} case False{} True{} True{} False{} False{} True{} False{} True{}: {==} case True{} True{} True{} False{} False{} True{} False{} True{}: {==} case False{} False{} False{} True{} False{} True{} False{} True{}: {==} case True{} False{} False{} True{} False{} True{} False{} True{}: {==} case False{} True{} False{} True{} False{} True{} False{} True{}: {==} case True{} True{} False{} True{} False{} True{} False{} True{}: {==} case False{} False{} True{} True{} False{} True{} False{} True{}: {==} case True{} False{} True{} True{} False{} True{} False{} True{}: {==} case False{} True{} True{} True{} False{} True{} False{} True{}: {==} case True{} True{} True{} True{} False{} True{} False{} True{}: {==} case False{} False{} False{} False{} True{} True{} False{} True{}: {==} case True{} False{} False{} False{} True{} True{} False{} True{}: {==} case False{} True{} False{} False{} True{} True{} False{} True{}: {==} case True{} True{} False{} False{} True{} True{} False{} True{}: {==} case False{} False{} True{} False{} True{} True{} False{} True{}: {==} case True{} False{} True{} False{} True{} True{} False{} True{}: {==} case False{} True{} True{} False{} True{} True{} False{} True{}: {==} case True{} True{} True{} False{} True{} True{} False{} True{}: {==} case False{} False{} False{} True{} True{} True{} False{} True{}: {==} case True{} False{} False{} True{} True{} True{} False{} True{}: {==} case False{} True{} False{} True{} True{} True{} False{} True{}: {==} case True{} True{} False{} True{} True{} True{} False{} True{}: {==} case False{} False{} True{} True{} True{} True{} False{} True{}: {==} case True{} False{} True{} True{} True{} True{} False{} True{}: {==} case False{} True{} True{} True{} True{} True{} False{} True{}: {==} case True{} True{} True{} True{} True{} True{} False{} True{}: {==} case False{} False{} False{} False{} False{} False{} True{} True{}: {==} case True{} False{} False{} False{} False{} False{} True{} True{}: {==} case False{} True{} False{} False{} False{} False{} True{} True{}: {==} case True{} True{} False{} False{} False{} False{} True{} True{}: {==} case False{} False{} True{} False{} False{} False{} True{} True{}: {==} case True{} False{} True{} False{} False{} False{} True{} True{}: {==} case False{} True{} True{} False{} False{} False{} True{} True{}: {==} case True{} True{} True{} False{} False{} False{} True{} True{}: {==} case False{} False{} False{} True{} False{} False{} True{} True{}: {==} case True{} False{} False{} True{} False{} False{} True{} True{}: {==} case False{} True{} False{} True{} False{} False{} True{} True{}: {==} case True{} True{} False{} True{} False{} False{} True{} True{}: {==} case False{} False{} True{} True{} False{} False{} True{} True{}: {==} case True{} False{} True{} True{} False{} False{} True{} True{}: {==} case False{} True{} True{} True{} False{} False{} True{} True{}: {==} case True{} True{} True{} True{} False{} False{} True{} True{}: {==} case False{} False{} False{} False{} True{} False{} True{} True{}: {==} case True{} False{} False{} False{} True{} False{} True{} True{}: {==} case False{} True{} False{} False{} True{} False{} True{} True{}: {==} case True{} True{} False{} False{} True{} False{} True{} True{}: {==} case False{} False{} True{} False{} True{} False{} True{} True{}: {==} case True{} False{} True{} False{} True{} False{} True{} True{}: {==} case False{} True{} True{} False{} True{} False{} True{} True{}: {==} case True{} True{} True{} False{} True{} False{} True{} True{}: {==} case False{} False{} False{} True{} True{} False{} True{} True{}: {==} case True{} False{} False{} True{} True{} False{} True{} True{}: {==} case False{} True{} False{} True{} True{} False{} True{} True{}: {==} case True{} True{} False{} True{} True{} False{} True{} True{}: {==} case False{} False{} True{} True{} True{} False{} True{} True{}: {==} case True{} False{} True{} True{} True{} False{} True{} True{}: {==} case False{} True{} True{} True{} True{} False{} True{} True{}: {==} case True{} True{} True{} True{} True{} False{} True{} True{}: {==} case False{} False{} False{} False{} False{} True{} True{} True{}: {==} case True{} False{} False{} False{} False{} True{} True{} True{}: {==} case False{} True{} False{} False{} False{} True{} True{} True{}: {==} case True{} True{} False{} False{} False{} True{} True{} True{}: {==} case False{} False{} True{} False{} False{} True{} True{} True{}: {==} case True{} False{} True{} False{} False{} True{} True{} True{}: {==} case False{} True{} True{} False{} False{} True{} True{} True{}: {==} case True{} True{} True{} False{} False{} True{} True{} True{}: {==} case False{} False{} False{} True{} False{} True{} True{} True{}: {==} case True{} False{} False{} True{} False{} True{} True{} True{}: {==} case False{} True{} False{} True{} False{} True{} True{} True{}: {==} case True{} True{} False{} True{} False{} True{} True{} True{}: {==} case False{} False{} True{} True{} False{} True{} True{} True{}: {==} case True{} False{} True{} True{} False{} True{} True{} True{}: {==} case False{} True{} True{} True{} False{} True{} True{} True{}: {==} case True{} True{} True{} True{} False{} True{} True{} True{}: {==} case False{} False{} False{} False{} True{} True{} True{} True{}: {==} case True{} False{} False{} False{} True{} True{} True{} True{}: {==} case False{} True{} False{} False{} True{} True{} True{} True{}: {==} case True{} True{} False{} False{} True{} True{} True{} True{}: {==} case False{} False{} True{} False{} True{} True{} True{} True{}: {==} case True{} False{} True{} False{} True{} True{} True{} True{}: {==} case False{} True{} True{} False{} True{} True{} True{} True{}: {==} case True{} True{} True{} False{} True{} True{} True{} True{}: {==} case False{} False{} False{} True{} True{} True{} True{} True{}: {==} case True{} False{} False{} True{} True{} True{} True{} True{}: {==} case False{} True{} False{} True{} True{} True{} True{} True{}: {==} case True{} True{} False{} True{} True{} True{} True{} True{}: {==} case False{} False{} True{} True{} True{} True{} True{} True{}: {==} case True{} False{} True{} True{} True{} True{} True{} True{}: {==} case False{} True{} True{} True{} True{} True{} True{} True{}: {==} case True{} True{} True{} True{} True{} True{} True{} True{}: {==}law xtime_ok: for +x: U32 {B.xtime(x) == S.mul(2, x) : U32}def xtime_ok(x): match x: case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: xtime_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31)law mul3_bits: for b0: Bool for b1: Bool for b2: Bool for b3: Bool for b4: Bool for b5: Bool for b6: Bool for b7: Bool for b8: Bool for b9: Bool for b10: Bool for b11: Bool for b12: Bool for b13: Bool for b14: Bool for b15: Bool for b16: Bool for b17: Bool for b18: Bool for b19: Bool for b20: Bool for b21: Bool for b22: Bool for b23: Bool for b24: Bool for b25: Bool for b26: Bool for b27: Bool for b28: Bool for b29: Bool for b30: Bool for b31: Bool {B.mul3(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == S.mul(3, U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}def mul3_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31): match b0 b1 b2 b3 b4 b5 b6 b7: case False{} False{} False{} False{} False{} False{} False{} False{}: {==} case True{} False{} False{} False{} False{} False{} False{} False{}: {==} case False{} True{} False{} False{} False{} False{} False{} False{}: {==} case True{} True{} False{} False{} False{} False{} False{} False{}: {==} case False{} False{} True{} False{} False{} False{} False{} False{}: {==} case True{} False{} True{} False{} False{} False{} False{} False{}: {==} case False{} True{} True{} False{} False{} False{} False{} False{}: {==} case True{} True{} True{} False{} False{} False{} False{} False{}: {==} case False{} False{} False{} True{} False{} False{} False{} False{}: {==} case True{} False{} False{} True{} False{} False{} False{} False{}: {==} case False{} True{} False{} True{} False{} False{} False{} False{}: {==} case True{} True{} False{} True{} False{} False{} False{} False{}: {==} case False{} False{} True{} True{} False{} False{} False{} False{}: {==} case True{} False{} True{} True{} False{} False{} False{} False{}: {==} case False{} True{} True{} True{} False{} False{} False{} False{}: {==} case True{} True{} True{} True{} False{} False{} False{} False{}: {==} case False{} False{} False{} False{} True{} False{} False{} False{}: {==} case True{} False{} False{} False{} True{} False{} False{} False{}: {==} case False{} True{} False{} False{} True{} False{} False{} False{}: {==} case True{} True{} False{} False{} True{} False{} False{} False{}: {==} case False{} False{} True{} False{} True{} False{} False{} False{}: {==} case True{} False{} True{} False{} True{} False{} False{} False{}: {==} case False{} True{} True{} False{} True{} False{} False{} False{}: {==} case True{} True{} True{} False{} True{} False{} False{} False{}: {==} case False{} False{} False{} True{} True{} False{} False{} False{}: {==} case True{} False{} False{} True{} True{} False{} False{} False{}: {==} case False{} True{} False{} True{} True{} False{} False{} False{}: {==} case True{} True{} False{} True{} True{} False{} False{} False{}: {==} case False{} False{} True{} True{} True{} False{} False{} False{}: {==} case True{} False{} True{} True{} True{} False{} False{} False{}: {==} case False{} True{} True{} True{} True{} False{} False{} False{}: {==} case True{} True{} True{} True{} True{} False{} False{} False{}: {==} case False{} False{} False{} False{} False{} True{} False{} False{}: {==} case True{} False{} False{} False{} False{} True{} False{} False{}: {==} case False{} True{} False{} False{} False{} True{} False{} False{}: {==} case True{} True{} False{} False{} False{} True{} False{} False{}: {==} case False{} False{} True{} False{} False{} True{} False{} False{}: {==} case True{} False{} True{} False{} False{} True{} False{} False{}: {==} case False{} True{} True{} False{} False{} True{} False{} False{}: {==} case True{} True{} True{} False{} False{} True{} False{} False{}: {==} case False{} False{} False{} True{} False{} True{} False{} False{}: {==} case True{} False{} False{} True{} False{} True{} False{} False{}: {==} case False{} True{} False{} True{} False{} True{} False{} False{}: {==} case True{} True{} False{} True{} False{} True{} False{} False{}: {==} case False{} False{} True{} True{} False{} True{} False{} False{}: {==} case True{} False{} True{} True{} False{} True{} False{} False{}: {==} case False{} True{} True{} True{} False{} True{} False{} False{}: {==} case True{} True{} True{} True{} False{} True{} False{} False{}: {==} case False{} False{} False{} False{} True{} True{} False{} False{}: {==} case True{} False{} False{} False{} True{} True{} False{} False{}: {==} case False{} True{} False{} False{} True{} True{} False{} False{}: {==} case True{} True{} False{} False{} True{} True{} False{} False{}: {==} case False{} False{} True{} False{} True{} True{} False{} False{}: {==} case True{} False{} True{} False{} True{} True{} False{} False{}: {==} case False{} True{} True{} False{} True{} True{} False{} False{}: {==} case True{} True{} True{} False{} True{} True{} False{} False{}: {==} case False{} False{} False{} True{} True{} True{} False{} False{}: {==} case True{} False{} False{} True{} True{} True{} False{} False{}: {==} case False{} True{} False{} True{} True{} True{} False{} False{}: {==} case True{} True{} False{} True{} True{} True{} False{} False{}: {==} case False{} False{} True{} True{} True{} True{} False{} False{}: {==} case True{} False{} True{} True{} True{} True{} False{} False{}: {==} case False{} True{} True{} True{} True{} True{} False{} False{}: {==} case True{} True{} True{} True{} True{} True{} False{} False{}: {==} case False{} False{} False{} False{} False{} False{} True{} False{}: {==} case True{} False{} False{} False{} False{} False{} True{} False{}: {==} case False{} True{} False{} False{} False{} False{} True{} False{}: {==} case True{} True{} False{} False{} False{} False{} True{} False{}: {==} case False{} False{} True{} False{} False{} False{} True{} False{}: {==} case True{} False{} True{} False{} False{} False{} True{} False{}: {==} case False{} True{} True{} False{} False{} False{} True{} False{}: {==} case True{} True{} True{} False{} False{} False{} True{} False{}: {==} case False{} False{} False{} True{} False{} False{} True{} False{}: {==} case True{} False{} False{} True{} False{} False{} True{} False{}: {==} case False{} True{} False{} True{} False{} False{} True{} False{}: {==} case True{} True{} False{} True{} False{} False{} True{} False{}: {==} case False{} False{} True{} True{} False{} False{} True{} False{}: {==} case True{} False{} True{} True{} False{} False{} True{} False{}: {==} case False{} True{} True{} True{} False{} False{} True{} False{}: {==} case True{} True{} True{} True{} False{} False{} True{} False{}: {==} case False{} False{} False{} False{} True{} False{} True{} False{}: {==} case True{} False{} False{} False{} True{} False{} True{} False{}: {==} case False{} True{} False{} False{} True{} False{} True{} False{}: {==} case True{} True{} False{} False{} True{} False{} True{} False{}: {==} case False{} False{} True{} False{} True{} False{} True{} False{}: {==} case True{} False{} True{} False{} True{} False{} True{} False{}: {==} case False{} True{} True{} False{} True{} False{} True{} False{}: {==} case True{} True{} True{} False{} True{} False{} True{} False{}: {==} case False{} False{} False{} True{} True{} False{} True{} False{}: {==} case True{} False{} False{} True{} True{} False{} True{} False{}: {==} case False{} True{} False{} True{} True{} False{} True{} False{}: {==} case True{} True{} False{} True{} True{} False{} True{} False{}: {==} case False{} False{} True{} True{} True{} False{} True{} False{}: {==} case True{} False{} True{} True{} True{} False{} True{} False{}: {==} case False{} True{} True{} True{} True{} False{} True{} False{}: {==} case True{} True{} True{} True{} True{} False{} True{} False{}: {==} case False{} False{} False{} False{} False{} True{} True{} False{}: {==} case True{} False{} False{} False{} False{} True{} True{} False{}: {==} case False{} True{} False{} False{} False{} True{} True{} False{}: {==} case True{} True{} False{} False{} False{} True{} True{} False{}: {==} case False{} False{} True{} False{} False{} True{} True{} False{}: {==} case True{} False{} True{} False{} False{} True{} True{} False{}: {==} case False{} True{} True{} False{} False{} True{} True{} False{}: {==} case True{} True{} True{} False{} False{} True{} True{} False{}: {==} case False{} False{} False{} True{} False{} True{} True{} False{}: {==} case True{} False{} False{} True{} False{} True{} True{} False{}: {==} case False{} True{} False{} True{} False{} True{} True{} False{}: {==} case True{} True{} False{} True{} False{} True{} True{} False{}: {==} case False{} False{} True{} True{} False{} True{} True{} False{}: {==} case True{} False{} True{} True{} False{} True{} True{} False{}: {==} case False{} True{} True{} True{} False{} True{} True{} False{}: {==} case True{} True{} True{} True{} False{} True{} True{} False{}: {==} case False{} False{} False{} False{} True{} True{} True{} False{}: {==} case True{} False{} False{} False{} True{} True{} True{} False{}: {==} case False{} True{} False{} False{} True{} True{} True{} False{}: {==} case True{} True{} False{} False{} True{} True{} True{} False{}: {==} case False{} False{} True{} False{} True{} True{} True{} False{}: {==} case True{} False{} True{} False{} True{} True{} True{} False{}: {==} case False{} True{} True{} False{} True{} True{} True{} False{}: {==} case True{} True{} True{} False{} True{} True{} True{} False{}: {==} case False{} False{} False{} True{} True{} True{} True{} False{}: {==} case True{} False{} False{} True{} True{} True{} True{} False{}: {==} case False{} True{} False{} True{} True{} True{} True{} False{}: {==} case True{} True{} False{} True{} True{} True{} True{} False{}: {==} case False{} False{} True{} True{} True{} True{} True{} False{}: {==} case True{} False{} True{} True{} True{} True{} True{} False{}: {==} case False{} True{} True{} True{} True{} True{} True{} False{}: {==} case True{} True{} True{} True{} True{} True{} True{} False{}: {==} case False{} False{} False{} False{} False{} False{} False{} True{}: {==} case True{} False{} False{} False{} False{} False{} False{} True{}: {==} case False{} True{} False{} False{} False{} False{} False{} True{}: {==} case True{} True{} False{} False{} False{} False{} False{} True{}: {==} case False{} False{} True{} False{} False{} False{} False{} True{}: {==} case True{} False{} True{} False{} False{} False{} False{} True{}: {==} case False{} True{} True{} False{} False{} False{} False{} True{}: {==} case True{} True{} True{} False{} False{} False{} False{} True{}: {==} case False{} False{} False{} True{} False{} False{} False{} True{}: {==} case True{} False{} False{} True{} False{} False{} False{} True{}: {==} case False{} True{} False{} True{} False{} False{} False{} True{}: {==} case True{} True{} False{} True{} False{} False{} False{} True{}: {==} case False{} False{} True{} True{} False{} False{} False{} True{}: {==} case True{} False{} True{} True{} False{} False{} False{} True{}: {==} case False{} True{} True{} True{} False{} False{} False{} True{}: {==} case True{} True{} True{} True{} False{} False{} False{} True{}: {==} case False{} False{} False{} False{} True{} False{} False{} True{}: {==} case True{} False{} False{} False{} True{} False{} False{} True{}: {==} case False{} True{} False{} False{} True{} False{} False{} True{}: {==} case True{} True{} False{} False{} True{} False{} False{} True{}: {==} case False{} False{} True{} False{} True{} False{} False{} True{}: {==} case True{} False{} True{} False{} True{} False{} False{} True{}: {==} case False{} True{} True{} False{} True{} False{} False{} True{}: {==} case True{} True{} True{} False{} True{} False{} False{} True{}: {==} case False{} False{} False{} True{} True{} False{} False{} True{}: {==} case True{} False{} False{} True{} True{} False{} False{} True{}: {==} case False{} True{} False{} True{} True{} False{} False{} True{}: {==} case True{} True{} False{} True{} True{} False{} False{} True{}: {==} case False{} False{} True{} True{} True{} False{} False{} True{}: {==} case True{} False{} True{} True{} True{} False{} False{} True{}: {==} case False{} True{} True{} True{} True{} False{} False{} True{}: {==} case True{} True{} True{} True{} True{} False{} False{} True{}: {==} case False{} False{} False{} False{} False{} True{} False{} True{}: {==} case True{} False{} False{} False{} False{} True{} False{} True{}: {==} case False{} True{} False{} False{} False{} True{} False{} True{}: {==} case True{} True{} False{} False{} False{} True{} False{} True{}: {==} case False{} False{} True{} False{} False{} True{} False{} True{}: {==} case True{} False{} True{} False{} False{} True{} False{} True{}: {==} case False{} True{} True{} False{} False{} True{} False{} True{}: {==} case True{} True{} True{} False{} False{} True{} False{} True{}: {==} case False{} False{} False{} True{} False{} True{} False{} True{}: {==} case True{} False{} False{} True{} False{} True{} False{} True{}: {==} case False{} True{} False{} True{} False{} True{} False{} True{}: {==} case True{} True{} False{} True{} False{} True{} False{} True{}: {==} case False{} False{} True{} True{} False{} True{} False{} True{}: {==} case True{} False{} True{} True{} False{} True{} False{} True{}: {==} case False{} True{} True{} True{} False{} True{} False{} True{}: {==} case True{} True{} True{} True{} False{} True{} False{} True{}: {==} case False{} False{} False{} False{} True{} True{} False{} True{}: {==} case True{} False{} False{} False{} True{} True{} False{} True{}: {==} case False{} True{} False{} False{} True{} True{} False{} True{}: {==} case True{} True{} False{} False{} True{} True{} False{} True{}: {==} case False{} False{} True{} False{} True{} True{} False{} True{}: {==} case True{} False{} True{} False{} True{} True{} False{} True{}: {==} case False{} True{} True{} False{} True{} True{} False{} True{}: {==} case True{} True{} True{} False{} True{} True{} False{} True{}: {==} case False{} False{} False{} True{} True{} True{} False{} True{}: {==} case True{} False{} False{} True{} True{} True{} False{} True{}: {==} case False{} True{} False{} True{} True{} True{} False{} True{}: {==} case True{} True{} False{} True{} True{} True{} False{} True{}: {==} case False{} False{} True{} True{} True{} True{} False{} True{}: {==} case True{} False{} True{} True{} True{} True{} False{} True{}: {==} case False{} True{} True{} True{} True{} True{} False{} True{}: {==} case True{} True{} True{} True{} True{} True{} False{} True{}: {==} case False{} False{} False{} False{} False{} False{} True{} True{}: {==} case True{} False{} False{} False{} False{} False{} True{} True{}: {==} case False{} True{} False{} False{} False{} False{} True{} True{}: {==} case True{} True{} False{} False{} False{} False{} True{} True{}: {==} case False{} False{} True{} False{} False{} False{} True{} True{}: {==} case True{} False{} True{} False{} False{} False{} True{} True{}: {==} case False{} True{} True{} False{} False{} False{} True{} True{}: {==} case True{} True{} True{} False{} False{} False{} True{} True{}: {==} case False{} False{} False{} True{} False{} False{} True{} True{}: {==} case True{} False{} False{} True{} False{} False{} True{} True{}: {==} case False{} True{} False{} True{} False{} False{} True{} True{}: {==} case True{} True{} False{} True{} False{} False{} True{} True{}: {==} case False{} False{} True{} True{} False{} False{} True{} True{}: {==} case True{} False{} True{} True{} False{} False{} True{} True{}: {==} case False{} True{} True{} True{} False{} False{} True{} True{}: {==} case True{} True{} True{} True{} False{} False{} True{} True{}: {==} case False{} False{} False{} False{} True{} False{} True{} True{}: {==} case True{} False{} False{} False{} True{} False{} True{} True{}: {==} case False{} True{} False{} False{} True{} False{} True{} True{}: {==} case True{} True{} False{} False{} True{} False{} True{} True{}: {==} case False{} False{} True{} False{} True{} False{} True{} True{}: {==} case True{} False{} True{} False{} True{} False{} True{} True{}: {==} case False{} True{} True{} False{} True{} False{} True{} True{}: {==} case True{} True{} True{} False{} True{} False{} True{} True{}: {==} case False{} False{} False{} True{} True{} False{} True{} True{}: {==} case True{} False{} False{} True{} True{} False{} True{} True{}: {==} case False{} True{} False{} True{} True{} False{} True{} True{}: {==} case True{} True{} False{} True{} True{} False{} True{} True{}: {==} case False{} False{} True{} True{} True{} False{} True{} True{}: {==} case True{} False{} True{} True{} True{} False{} True{} True{}: {==} case False{} True{} True{} True{} True{} False{} True{} True{}: {==} case True{} True{} True{} True{} True{} False{} True{} True{}: {==} case False{} False{} False{} False{} False{} True{} True{} True{}: {==} case True{} False{} False{} False{} False{} True{} True{} True{}: {==} case False{} True{} False{} False{} False{} True{} True{} True{}: {==} case True{} True{} False{} False{} False{} True{} True{} True{}: {==} case False{} False{} True{} False{} False{} True{} True{} True{}: {==} case True{} False{} True{} False{} False{} True{} True{} True{}: {==} case False{} True{} True{} False{} False{} True{} True{} True{}: {==} case True{} True{} True{} False{} False{} True{} True{} True{}: {==} case False{} False{} False{} True{} False{} True{} True{} True{}: {==} case True{} False{} False{} True{} False{} True{} True{} True{}: {==} case False{} True{} False{} True{} False{} True{} True{} True{}: {==} case True{} True{} False{} True{} False{} True{} True{} True{}: {==} case False{} False{} True{} True{} False{} True{} True{} True{}: {==} case True{} False{} True{} True{} False{} True{} True{} True{}: {==} case False{} True{} True{} True{} False{} True{} True{} True{}: {==} case True{} True{} True{} True{} False{} True{} True{} True{}: {==} case False{} False{} False{} False{} True{} True{} True{} True{}: {==} case True{} False{} False{} False{} True{} True{} True{} True{}: {==} case False{} True{} False{} False{} True{} True{} True{} True{}: {==} case True{} True{} False{} False{} True{} True{} True{} True{}: {==} case False{} False{} True{} False{} True{} True{} True{} True{}: {==} case True{} False{} True{} False{} True{} True{} True{} True{}: {==} case False{} True{} True{} False{} True{} True{} True{} True{}: {==} case True{} True{} True{} False{} True{} True{} True{} True{}: {==} case False{} False{} False{} True{} True{} True{} True{} True{}: {==} case True{} False{} False{} True{} True{} True{} True{} True{}: {==} case False{} True{} False{} True{} True{} True{} True{} True{}: {==} case True{} True{} False{} True{} True{} True{} True{} True{}: {==} case False{} False{} True{} True{} True{} True{} True{} True{}: {==} case True{} False{} True{} True{} True{} True{} True{} True{}: {==} case False{} True{} True{} True{} True{} True{} True{} True{}: {==} case True{} True{} True{} True{} True{} True{} True{} True{}: {==}law mul3_ok: for +x: U32 {B.mul3(x) == S.mul(3, x) : U32}def mul3_ok(x): match x: case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: mul3_bits(b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31)