def diff_same

qasim-bend-kit@0.1.0.2 · proof/AES_TagCompareProof.bend:6

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
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/proofs/lib/logic.bend as Logic

6def diff_same(+a: List<&2, U32>, +acc: U32,
7    acc_zero: {U32.is_eq(acc, 0) == True{} : Bool}) ->
8    {U32.is_eq(AES.bytes_difference.go(a, a, acc), 0) == True{} : Bool}:
9    match a:
10        case Nil{}: acc_zero
11        case x <> xs:
12            xor_zero = Equal.trans(Bool,
13                U32.is_eq(U32.xor(x, x), 0), U32.is_eq(x, x), True{},
14                SW.u32_xor_zero(x, x), SW.u32_refl(x))
15            both = Logic.and_intro(U32.is_eq(acc, 0),
16                U32.is_eq(U32.xor(x, x), 0), acc_zero, xor_zero)
17            next_zero = Equal.trans(Bool,
18                U32.is_eq(U32.or(acc, U32.xor(x, x)), 0),
19                Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, x), 0)),
20                True{}, SW.u32_or_zero(acc, U32.xor(x, x)), both)
21            diff_same(xs, U32.or(acc, U32.xor(x, x)), next_zero)