law xor4_cong

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/cipher.bend:85

import Base

85law xor4_cong:
86  for +p: U32
87  for +q: U32
88  for +r: U32
89  for +s: U32
90  for +p2: U32
91  for +q2: U32
92  for +r2: U32
93  for +s2: U32
94  for +ep: {p == p2 : U32}
95  for +eq: {q == q2 : U32}
96  for +er: {r == r2 : U32}
97  for +es: {s == s2 : U32}
98  {U32.xor(U32.xor(U32.xor(p, q), r), s) == U32.xor(U32.xor(U32.xor(p2, q2), r2), s2) : U32}