def enc_u_v

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

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/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/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

45def enc_u_v(+one: Nat, +h1: {one == 1n : Nat}, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {P.enc_u(a) == CV.enc_u(PA.av(one, a)) : List<&2, U32>}:
46  match a:
47    case P.Affine{+x, +y}:
48      +hx = Lg.and_left(PT.red(one, x), PT.red(one, y), ha)
49      +hy = Lg.and_right(PT.red(one, x), PT.red(one, y), ha)
50      %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))) : {4 <> List.append(&2, U32, _, B.to_be(y)) == 4 <> List.append(&2, U32, CV.i2osp(32n, FS.value(one, x)), CV.i2osp(32n, FS.value(one, y))) : List<&2, U32>}
51      %Equal.sym(List<&2, U32>, B.to_be(y), CV.i2osp(32n, LV.ev(y)), BY.to_be_v(one, h1, y, PM.l16(one, y, hy))) : {4 <> List.append(&2, U32, CV.i2osp(32n, LV.ev(x)), _) == 4 <> List.append(&2, U32, CV.i2osp(32n, FS.value(one, x)), CV.i2osp(32n, FS.value(one, y))) : List<&2, U32>}
52      %Equal.sym(Nat, FS.value(one, x), LV.ev(x), LV.ev_value(one, h1, x)) : {4 <> List.append(&2, U32, CV.i2osp(32n, LV.ev(x)), CV.i2osp(32n, LV.ev(y))) == 4 <> List.append(&2, U32, CV.i2osp(32n, _), CV.i2osp(32n, FS.value(one, y))) : List<&2, U32>}
53      %Equal.sym(Nat, FS.value(one, y), LV.ev(y), LV.ev_value(one, h1, y)) : {4 <> List.append(&2, U32, CV.i2osp(32n, LV.ev(x)), CV.i2osp(32n, LV.ev(y))) == 4 <> List.append(&2, U32, CV.i2osp(32n, LV.ev(x)), CV.i2osp(32n, _)) : List<&2, U32>}
54      {==}