def enc_c_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/penc.bend:36

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as PM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA

36def enc_c_v(+one: Nat, +h1: {one == 1n : Nat}, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {P.enc_c(a) == CV.enc_c(PA.av(one, a)) : List<&2, U32>}:
37  match a:
38    case P.Affine{+x, +y}:
39      +hx = Lg.and_left(PT.red(one, x), PT.red(one, y), ha)
40      %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {U32.from_nat(Nat.add(_, 2n)) <> B.to_be(x) == U32.from_nat(Nat.add(Nat.mod(FS.value(one, y), 2n), 2n)) <> CV.i2osp(32n, FS.value(one, x)) : List<&2, U32>}
41      %Equal.sym(List<&2, U32>, B.to_be(x), CV.i2osp(32n, LV.ev(x)), BY.to_be_v(one, h1, x, PM.l16(one, x, hx))) : {U32.from_nat(Nat.add(Nat.mod(FS.value(one, y), 2n), 2n)) <> _ == U32.from_nat(Nat.add(Nat.mod(FS.value(one, y), 2n), 2n)) <> CV.i2osp(32n, FS.value(one, x)) : List<&2, U32>}
42      %Equal.sym(Nat, FS.value(one, x), LV.ev(x), LV.ev_value(one, h1, x)) : {U32.from_nat(Nat.add(Nat.mod(FS.value(one, y), 2n), 2n)) <> CV.i2osp(32n, LV.ev(x)) == U32.from_nat(Nat.add(Nat.mod(FS.value(one, y), 2n), 2n)) <> CV.i2osp(32n, _) : List<&2, U32>}
43      {==}