Penc.enc_u_v: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as Penc
Lines 45-54 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend&start_line=45&end_line=54

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

def 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>}:
  match a:
    case P.Affine{+x, +y}:
      +hx = Lg.and_left(PT.red(one, x), PT.red(one, y), ha)
      +hy = Lg.and_right(PT.red(one, x), PT.red(one, y), ha)
      %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>}
      %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>}
      %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>}
      %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>}
      {==}

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=to_be_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=ev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=ev_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=ared
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=av
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=red
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=l16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=enc_u
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=i2osp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=to_be
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=Affine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=enc_u