law state_cong

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

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

36law state_cong:
37  for +a: T.Quad
38  for +b: T.Quad
39  for +c: T.Quad
40  for +d: T.Quad
41  for +a2: T.Quad
42  for +b2: T.Quad
43  for +c2: T.Quad
44  for +d2: T.Quad
45  for +ea: {a == a2 : T.Quad}
46  for +eb: {b == b2 : T.Quad}
47  for +ec: {c == c2 : T.Quad}
48  for +ed: {d == d2 : T.Quad}
49  {T.S{a, b, c, d} == T.S{a2, b2, c2, d2} : T.State}