def steps_append

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/ghash.bend:33

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as I
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as D

33def steps_append(+l1: List<&2, Bool>, +l2: List<&2, Bool>, +acc: I.Acc) -> {D.steps(List.append(&2, Bool, l1, l2), acc) == D.steps(l2, D.steps(l1, acc)) : I.Acc}:
34  match l1:
35    case Nil{}:
36      {==}
37    case c <> r:
38      steps_append(r, l2, I.step(D.bit(c), acc))