def xor_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pschn.bend:45

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend as SS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend as SC

45def xor_v(xs: List<&2, U32>, ys: List<&2, U32>) -> {SC.xor_bytes(xs, ys) == SS.xor_bytes(xs, ys) : List<&2, U32>}:
46  match xs ys:
47    case +x <> xt +y <> yt:
48      Equal.cong(List<&2, U32>, List<&2, U32>, l => U32.xor(x, y) <> l, SC.xor_bytes(xt, yt), SS.xor_bytes(xt, yt), xor_v(xt, yt))
49    case Nil{} _:
50      {==}
51    case _ Nil{}:
52      {==}