def diff_self

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/password.bend:237

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle

237def diff_self(+a: List<&2, U32>, +acc: U32, +h: {U32.is_eq(acc, 0) == True{} : Bool}) -> {U32.is_eq(Subtle.diff(a, a, acc), 0) == True{} : Bool}:
238  match a:
239    case Nil{}:
240      h
241    case +x <> +xs:
242      +acc2 = U32.or(acc, U32.xor(x, x))
243      +e = Equal.trans(Bool, U32.is_eq(acc2, 0), Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, x), 0)), True{}, SW.u32_or_zero(acc, U32.xor(x, x)),
244        L.and_intro(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, x), 0), h, Equal.trans(Bool, U32.is_eq(U32.xor(x, x), 0), U32.is_eq(x, x), True{}, SW.u32_xor_zero(x, x), SW.u32_refl(x))))
245      diff_self(xs, acc2, e)