law quad_cong

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T

13# Congruence of the record constructors (one rewrite per field, on variables).
14law quad_cong:
15  for +a: U32
16  for +b: U32
17  for +c: U32
18  for +d: U32
19  for +a2: U32
20  for +b2: U32
21  for +c2: U32
22  for +d2: U32
23  for +ea: {a == a2 : U32}
24  for +eb: {b == b2 : U32}
25  for +ec: {c == c2 : U32}
26  for +ed: {d == d2 : U32}
27  {T.W{a, b, c, d} == T.W{a2, b2, c2, d2} : T.Quad}