def diff_acc_zero

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

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

36def diff_acc_zero(+a: List<&2, U32>, +b: List<&2, U32>, +acc: U32,
37    zero: {U32.is_eq(AES.bytes_difference.go(a, b, acc), 0) == True{} : Bool}) ->
38    {U32.is_eq(acc, 0) == True{} : Bool}:
39    match a b:
40        case Nil{} Nil{}: zero
41        case Nil{} y <> ys:
42            Empty.absurd({U32.is_eq(acc, 0) == True{} : Bool},
43                Logic.false_true(zero))
44        case x <> xs Nil{}:
45            Empty.absurd({U32.is_eq(acc, 0) == True{} : Bool},
46                Logic.false_true(zero))
47        case x <> xs y <> ys:
48            acc2 = U32.or(acc, U32.xor(x, y))
49            step_zero = diff_acc_zero(xs, ys, acc2, zero)
50            both = Equal.trans(Bool,
51                Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, y), 0)),
52                U32.is_eq(acc2, 0), True{},
53                Equal.sym(Bool, U32.is_eq(acc2, 0),
54                    Bool.and(U32.is_eq(acc, 0),
55                        U32.is_eq(U32.xor(x, y), 0)),
56                    SW.u32_or_zero(acc, U32.xor(x, y))),
57                step_zero)
58            Logic.and_left(U32.is_eq(acc, 0),
59                U32.is_eq(U32.xor(x, y), 0), both)