law step

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/proof.bend:37

import Base

37law step:
38  for +acc: U32
39  for +x: U32
40  for +y: U32
41  for +e: Bool
42  {Bool.and(U32.is_eq(U32.or(acc, U32.xor(x, y)), 0), e) == Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), e)) : Bool}