def xor_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/gcm.bend:39

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/spec/crypto/aes/gcm.bend as G

39def xor_ok(+xs: List<&2, U32>, +ks: List<&2, U32>) -> {I.xor_bytes(xs, ks) == G.xor_bytes(xs, ks) : List<&2, U32>}:
40  match xs ks:
41    case x <> xt k <> kt:
42      %xor_ok(xt, kt) : {U32.xor(x, k) <> I.xor_bytes(xt, kt) == U32.xor(x, k) <> _ : List<&2, U32>}
43      {==}
44    case Nil{} _:
45      {==}
46    case x <> xt Nil{}:
47      {==}