def parity_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:70

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

70def parity_v(+xs: List<&2, Nat>) -> {Nat.mod(L.hd0(xs), 2n) == Nat.mod(LV.ev(xs), 2n) : Nat}:
71  match xs:
72    case Nil{}:
73      {==}
74    case +x <> +t:
75      Equal.sym(Nat, Nat.mod(Nat.add(x, C.shift(16n, LV.ev(t))), 2n), Nat.mod(x, 2n), WW.odd_limb(15n, x, LV.ev(t)))