law mul3_bits

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/sbox.bend:1141

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/sbox.bend as B
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S

1141law mul3_bits:
1142  for b0: Bool
1143  for b1: Bool
1144  for b2: Bool
1145  for b3: Bool
1146  for b4: Bool
1147  for b5: Bool
1148  for b6: Bool
1149  for b7: Bool
1150  for b8: Bool
1151  for b9: Bool
1152  for b10: Bool
1153  for b11: Bool
1154  for b12: Bool
1155  for b13: Bool
1156  for b14: Bool
1157  for b15: Bool
1158  for b16: Bool
1159  for b17: Bool
1160  for b18: Bool
1161  for b19: Bool
1162  for b20: Bool
1163  for b21: Bool
1164  for b22: Bool
1165  for b23: Bool
1166  for b24: Bool
1167  for b25: Bool
1168  for b26: Bool
1169  for b27: Bool
1170  for b28: Bool
1171  for b29: Bool
1172  for b30: Bool
1173  for b31: Bool
1174  {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}