law step

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/subtle/proof.bend:8

import Base

8# Gate for src/crypto/subtle.bend: `bend proofs/crypto/subtle/proof.bend`.
9#
10# The accumulator invariant (the shape of HACL*'s lbytes_eq proof): after
11# the common prefix, "lengths agree and the accumulator is zero" is "the
12# starting accumulator is zero and the lists are equal".
13law step:
14  for +acc: U32
15  for +x: U32
16  for +y: U32
17  for +e: Bool
18  {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}