law xtime_bits

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

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

582law xtime_bits:
583  for b0: Bool
584  for b1: Bool
585  for b2: Bool
586  for b3: Bool
587  for b4: Bool
588  for b5: Bool
589  for b6: Bool
590  for b7: Bool
591  for b8: Bool
592  for b9: Bool
593  for b10: Bool
594  for b11: Bool
595  for b12: Bool
596  for b13: Bool
597  for b14: Bool
598  for b15: Bool
599  for b16: Bool
600  for b17: Bool
601  for b18: Bool
602  for b19: Bool
603  for b20: Bool
604  for b21: Bool
605  for b22: Bool
606  for b23: Bool
607  for b24: Bool
608  for b25: Bool
609  for b26: Bool
610  for b27: Bool
611  for b28: Bool
612  for b29: Bool
613  for b30: Bool
614  for b31: Bool
615  {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}