# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/penc.src; edit the .src
import Base
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../../src/crypto/secp256k1/field.bend as F
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../../src/crypto/secp256k1/point.bend as P
import ../../lib/logic.bend as Lg
import ./limbs.bend as LV
import ./fieldops.bend as FO
import ./fieldpow.bend as FP
import ./fwrap.bend as FW
import ./bytes.bend as BY
import ./point.bend as PT
import ./sel.bend as PM
import ./paff.bend as PA
import ../../math/natural/arith.bend as NR

# SEC 1 encodings of src/crypto/secp256k1/point.bend (compressed and
# uncompressed encode, decode with decompression) against
# spec/crypto/secp256k1/curve.bend.

def mpv(+one: Nat, m: Maybe<&2, P.Point>) -> Maybe<&2, CV.SPoint>:
  match m:
    case None{}: None{}
    case Some{q}: Some{PT.pv(one, q)}

def mpred(+one: Nat, m: Maybe<&2, P.Point>) -> Bool:
  match m:
    case None{}: True{}
    case Some{q}: PT.pred(one, q)

# ---- encode ----

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

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>}
      {==}

def encode_compressed_v(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}) -> {P.encode_compressed(q) == CV.encode_compressed(FS.prime(one), PT.pv(one, q)) : List<&2, U32>}:
  %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, q)), PA.av(one, P.to_affine(q)), Equal.sym(CV.SAffine, PA.av(one, P.to_affine(q)), CV.to_affine(FS.prime(one), PT.pv(one, q)), PA.aff_v(one, h1, q, hq))) : {P.enc_c(P.to_affine(q)) == CV.enc_c(_) : List<&2, U32>}
  enc_c_v(one, h1, P.to_affine(q), PA.aff_r(one, h1, q, hq))

def encode_uncompressed_v(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}) -> {P.encode_uncompressed(q) == CV.encode_uncompressed(FS.prime(one), PT.pv(one, q)) : List<&2, U32>}:
  %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, q)), PA.av(one, P.to_affine(q)), Equal.sym(CV.SAffine, PA.av(one, P.to_affine(q)), CV.to_affine(FS.prime(one), PT.pv(one, q)), PA.aff_v(one, h1, q, hq))) : {P.enc_u(P.to_affine(q)) == CV.enc_u(_) : List<&2, U32>}
  enc_u_v(one, h1, P.to_affine(q), PA.aff_r(one, h1, q, hq))

# ---- x^3 + 7, on the curve ----

def seven_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(7n, FS.prime(one)) == True{} : Bool}:
  FO.small_lt_p(one, h1, 7n, {==})

def rhs_r(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {PT.red(one, x) == True{} : Bool}) -> {PT.red(one, P.rhs(x)) == True{} : Bool}:
  +h2 = FO.mul_r(one, h1, x, x, hx, hx)
  +h3 = FO.mul_r(one, h1, F.mul(x, x), x, h2, hx)
  FO.add_r(one, h1, F.mul(F.mul(x, x), x), F.small(7n), h3, FO.small_r(one, h1, 7n, seven_lt(one, h1)))

def rhs_v(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {PT.red(one, x) == True{} : Bool}) -> {FS.value(one, P.rhs(x)) == CV.rhs(FS.prime(one), FS.value(one, x)) : Nat}:
  +h2 = FO.mul_r(one, h1, x, x, hx, hx)
  +h3 = FO.mul_r(one, h1, F.mul(x, x), x, h2, hx)
  %Equal.sym(Nat, FS.value(one, F.add(F.mul(F.mul(x, x), x), F.small(7n))), FS.madd(FS.prime(one), FS.value(one, F.mul(F.mul(x, x), x)), FS.value(one, F.small(7n))), FO.add_v(one, h1, F.mul(F.mul(x, x), x), F.small(7n), h3, FO.small_r(one, h1, 7n, seven_lt(one, h1)))) : {_ == FS.madd(FS.prime(one), FS.mmul(FS.prime(one), FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, x)), FS.value(one, x)), 7n) : Nat}
  %Equal.sym(Nat, FS.value(one, F.mul(F.mul(x, x), x)), FS.mmul(FS.prime(one), FS.value(one, F.mul(x, x)), FS.value(one, x)), FO.mul_v(one, h1, F.mul(x, x), x, h2, hx)) : {FS.madd(FS.prime(one), _, FS.value(one, F.small(7n))) == FS.madd(FS.prime(one), FS.mmul(FS.prime(one), FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, x)), FS.value(one, x)), 7n) : Nat}
  %Equal.sym(Nat, FS.value(one, F.mul(x, x)), FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, x)), FO.mul_v(one, h1, x, x, hx, hx)) : {FS.madd(FS.prime(one), FS.mmul(FS.prime(one), _, FS.value(one, x)), FS.value(one, F.small(7n))) == FS.madd(FS.prime(one), FS.mmul(FS.prime(one), FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, x)), FS.value(one, x)), 7n) : Nat}
  %Equal.sym(Nat, FS.value(one, F.small(7n)), 7n, FO.small_val(one, h1, 7n, seven_lt(one, h1))) : {FS.madd(FS.prime(one), FS.mmul(FS.prime(one), FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, x)), FS.value(one, x)), _) == FS.madd(FS.prime(one), FS.mmul(FS.prime(one), FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, x)), FS.value(one, x)), 7n) : Nat}
  {==}

def on_curve_v(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +y: List<&2, Nat>, +hx: {PT.red(one, x) == True{} : Bool}, +hy: {PT.red(one, y) == True{} : Bool}) -> {P.on_curve(x, y) == CV.on_curve(FS.prime(one), FS.value(one, x), FS.value(one, y)) : Bool}:
  +hs = FO.mul_r(one, h1, y, y, hy, hy)
  +hr = rhs_r(one, h1, x, hx)
  %Equal.sym(Bool, F.eq(F.mul(y, y), P.rhs(x)), Nat.is_eq(FS.value(one, F.mul(y, y)), FS.value(one, P.rhs(x))), FW.eq_f(one, h1, F.mul(y, y), P.rhs(x), PM.l16(one, F.mul(y, y), hs), PM.l16(one, P.rhs(x), hr))) : {_ == Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), CV.rhs(FS.prime(one), FS.value(one, x))) : Bool}
  %Equal.sym(Nat, FS.value(one, F.mul(y, y)), FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), FO.mul_v(one, h1, y, y, hy, hy)) : {Nat.is_eq(_, FS.value(one, P.rhs(x))) == Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), CV.rhs(FS.prime(one), FS.value(one, x))) : Bool}
  %Equal.sym(Nat, FS.value(one, P.rhs(x)), CV.rhs(FS.prime(one), FS.value(one, x)), rhs_v(one, h1, x, hx)) : {Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), _) == Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), CV.rhs(FS.prime(one), FS.value(one, x))) : Bool}
  {==}

# ---- decompression ----

def one_v(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.value(one, F.one()) == 1n : Nat}:
  FO.small_val(one, h1, 1n, PM.one_lt(one, h1))

def one_r(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.red(one, F.one()) == True{} : Bool}:
  FO.small_r(one, h1, 1n, PM.one_lt(one, h1))

def dif_v(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +y: List<&2, Nat>, ok: Bool) -> {mpv(one, P.decompress_if(x, y, ok)) == CV.decompress_if(FS.value(one, x), FS.value(one, y), ok) : Maybe<&2, CV.SPoint>}:
  match ok:
    case True{}:
      %Equal.sym(Nat, FS.value(one, F.one()), 1n, one_v(one, h1)) : {Some{CV.SPoint{FS.value(one, x), FS.value(one, y), _}} == Some{CV.SPoint{FS.value(one, x), FS.value(one, y), 1n}} : Maybe<&2, CV.SPoint>}
      {==}
    case False{}:
      {==}

def dif_r(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +y: List<&2, Nat>, +hx: {PT.red(one, x) == True{} : Bool}, +hy: {PT.red(one, y) == True{} : Bool}, ok: Bool) -> {mpred(one, P.decompress_if(x, y, ok)) == True{} : Bool}:
  match ok:
    case True{}:
      PT.pr3(one, x, y, F.one(), hx, hy, one_r(one, h1))
    case False{}:
      {==}

def mod2_lt(+v: Nat) -> {Nat.is_lt(Nat.mod(v, 2n), 2n) == True{} : Bool}:
  NR.dm_lt(1n, v)

# y or p - y by the parities q and par (both 0 or 1)
def pick_v(+one: Nat, +h1: {one == 1n : Nat}, q: Nat, par: Nat, +y: List<&2, Nat>, +hq: {Nat.is_lt(q, 2n) == True{} : Bool}, +hp: {Nat.is_lt(par, 2n) == True{} : Bool}, +hy: {PT.red(one, y) == True{} : Bool}) -> {FS.value(one, F.select(Nat.sub(Nat.add(q, par), Nat.mul(Nat.mul(q, par), 2n)), F.neg(y), y)) == CV.pick_if(FS.prime(one), FS.value(one, y), Nat.is_eq(q, par)) : Nat}:
  match q par:
    case 0n 0n:
      %Equal.sym(List<&2, Nat>, L.select(0n, F.neg(y), y), y, PM.sel0(one, 16n, F.neg(y), y, PM.l16(one, F.neg(y), FO.neg_r(one, h1, y, hy)), PM.l16(one, y, hy))) : {FS.value(one, _) == FS.value(one, y) : Nat}
      {==}
    case 0n 1n:
      %Equal.sym(List<&2, Nat>, L.select(1n, F.neg(y), y), F.neg(y), PM.sel1(one, 16n, F.neg(y), y, PM.l16(one, F.neg(y), FO.neg_r(one, h1, y, hy)), PM.l16(one, y, hy))) : {FS.value(one, _) == FS.mneg(FS.prime(one), FS.value(one, y)) : Nat}
      FO.neg_v(one, h1, y, hy)
    case 1n 0n:
      %Equal.sym(List<&2, Nat>, L.select(1n, F.neg(y), y), F.neg(y), PM.sel1(one, 16n, F.neg(y), y, PM.l16(one, F.neg(y), FO.neg_r(one, h1, y, hy)), PM.l16(one, y, hy))) : {FS.value(one, _) == FS.mneg(FS.prime(one), FS.value(one, y)) : Nat}
      FO.neg_v(one, h1, y, hy)
    case 1n 1n:
      %Equal.sym(List<&2, Nat>, L.select(0n, F.neg(y), y), y, PM.sel0(one, 16n, F.neg(y), y, PM.l16(one, F.neg(y), FO.neg_r(one, h1, y, hy)), PM.l16(one, y, hy))) : {FS.value(one, _) == FS.value(one, y) : Nat}
      {==}
    case 2n+ +c _:
      Empty.absurd({FS.value(one, F.select(Nat.sub(Nat.add(2n+c, par), Nat.mul(Nat.mul(2n+c, par), 2n)), F.neg(y), y)) == CV.pick_if(FS.prime(one), FS.value(one, y), Nat.is_eq(2n+c, par)) : Nat}, PM.not01(c, hq))
    case _ 2n+ +c:
      Empty.absurd({FS.value(one, F.select(Nat.sub(Nat.add(q, 2n+c), Nat.mul(Nat.mul(q, 2n+c), 2n)), F.neg(y), y)) == CV.pick_if(FS.prime(one), FS.value(one, y), Nat.is_eq(q, 2n+c)) : Nat}, PM.not01(c, hp))

def pick_r(+one: Nat, +h1: {one == 1n : Nat}, q: Nat, par: Nat, +y: List<&2, Nat>, +hq: {Nat.is_lt(q, 2n) == True{} : Bool}, +hp: {Nat.is_lt(par, 2n) == True{} : Bool}, +hy: {PT.red(one, y) == True{} : Bool}) -> {PT.red(one, F.select(Nat.sub(Nat.add(q, par), Nat.mul(Nat.mul(q, par), 2n)), F.neg(y), y)) == True{} : Bool}:
  match q par:
    case 0n 0n:
      %Equal.sym(List<&2, Nat>, L.select(0n, F.neg(y), y), y, PM.sel0(one, 16n, F.neg(y), y, PM.l16(one, F.neg(y), FO.neg_r(one, h1, y, hy)), PM.l16(one, y, hy))) : {PT.red(one, _) == True{} : Bool}
      hy
    case 0n 1n:
      %Equal.sym(List<&2, Nat>, L.select(1n, F.neg(y), y), F.neg(y), PM.sel1(one, 16n, F.neg(y), y, PM.l16(one, F.neg(y), FO.neg_r(one, h1, y, hy)), PM.l16(one, y, hy))) : {PT.red(one, _) == True{} : Bool}
      FO.neg_r(one, h1, y, hy)
    case 1n 0n:
      %Equal.sym(List<&2, Nat>, L.select(1n, F.neg(y), y), F.neg(y), PM.sel1(one, 16n, F.neg(y), y, PM.l16(one, F.neg(y), FO.neg_r(one, h1, y, hy)), PM.l16(one, y, hy))) : {PT.red(one, _) == True{} : Bool}
      FO.neg_r(one, h1, y, hy)
    case 1n 1n:
      %Equal.sym(List<&2, Nat>, L.select(0n, F.neg(y), y), y, PM.sel0(one, 16n, F.neg(y), y, PM.l16(one, F.neg(y), FO.neg_r(one, h1, y, hy)), PM.l16(one, y, hy))) : {PT.red(one, _) == True{} : Bool}
      hy
    case 2n+ +c _:
      Empty.absurd({PT.red(one, F.select(Nat.sub(Nat.add(2n+c, par), Nat.mul(Nat.mul(2n+c, par), 2n)), F.neg(y), y)) == True{} : Bool}, PM.not01(c, hq))
    case _ 2n+ +c:
      Empty.absurd({PT.red(one, F.select(Nat.sub(Nat.add(q, 2n+c), Nat.mul(Nat.mul(q, 2n+c), 2n)), F.neg(y), y)) == True{} : Bool}, PM.not01(c, hp))

def lift_v(+one: Nat, +h1: {one == 1n : Nat}, +y: List<&2, Nat>, +par: Nat, +hy: {PT.red(one, y) == True{} : Bool}, +hp: {Nat.is_lt(par, 2n) == True{} : Bool}) -> {FS.value(one, P.lift_y(y, par)) == CV.pick_parity(FS.prime(one), FS.value(one, y), par) : Nat}:
  %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {FS.value(one, F.select(Nat.sub(Nat.add(_, par), Nat.mul(Nat.mul(F.parity(y), par), 2n)), F.neg(y), y)) == CV.pick_if(FS.prime(one), FS.value(one, y), Nat.is_eq(Nat.mod(FS.value(one, y), 2n), par)) : Nat}
  %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {FS.value(one, F.select(Nat.sub(Nat.add(Nat.mod(FS.value(one, y), 2n), par), Nat.mul(Nat.mul(_, par), 2n)), F.neg(y), y)) == CV.pick_if(FS.prime(one), FS.value(one, y), Nat.is_eq(Nat.mod(FS.value(one, y), 2n), par)) : Nat}
  pick_v(one, h1, Nat.mod(FS.value(one, y), 2n), par, y, mod2_lt(FS.value(one, y)), hp, hy)

def lift_r(+one: Nat, +h1: {one == 1n : Nat}, +y: List<&2, Nat>, +par: Nat, +hy: {PT.red(one, y) == True{} : Bool}, +hp: {Nat.is_lt(par, 2n) == True{} : Bool}) -> {PT.red(one, P.lift_y(y, par)) == True{} : Bool}:
  %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {PT.red(one, F.select(Nat.sub(Nat.add(_, par), Nat.mul(Nat.mul(F.parity(y), par), 2n)), F.neg(y), y)) == True{} : Bool}
  %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {PT.red(one, F.select(Nat.sub(Nat.add(Nat.mod(FS.value(one, y), 2n), par), Nat.mul(Nat.mul(_, par), 2n)), F.neg(y), y)) == True{} : Bool}
  pick_r(one, h1, Nat.mod(FS.value(one, y), 2n), par, y, mod2_lt(FS.value(one, y)), hp, hy)

def dy(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +r: List<&2, Nat>, +y: List<&2, Nat>, +par: Nat, +hr: {PT.red(one, r) == True{} : Bool}, +hy: {PT.red(one, y) == True{} : Bool}, +hp: {Nat.is_lt(par, 2n) == True{} : Bool}) -> {mpv(one, P.decompress_if(x, P.lift_y(y, par), F.eq(F.mul(y, y), r))) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), FS.value(one, y), par), Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), FS.value(one, r))) : Maybe<&2, CV.SPoint>}:
  +hs = FO.mul_r(one, h1, y, y, hy, hy)
  %Equal.sym(Bool, F.eq(F.mul(y, y), r), Nat.is_eq(FS.value(one, F.mul(y, y)), FS.value(one, r)), FW.eq_f(one, h1, F.mul(y, y), r, PM.l16(one, F.mul(y, y), hs), PM.l16(one, r, hr))) : {mpv(one, P.decompress_if(x, P.lift_y(y, par), _)) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), FS.value(one, y), par), Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), FS.value(one, r))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, FS.value(one, F.mul(y, y)), FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), FO.mul_v(one, h1, y, y, hy, hy)) : {mpv(one, P.decompress_if(x, P.lift_y(y, par), Nat.is_eq(_, FS.value(one, r)))) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), FS.value(one, y), par), Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), FS.value(one, r))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.pick_parity(FS.prime(one), FS.value(one, y), par), FS.value(one, P.lift_y(y, par)), Equal.sym(Nat, FS.value(one, P.lift_y(y, par)), CV.pick_parity(FS.prime(one), FS.value(one, y), par), lift_v(one, h1, y, par, hy, hp))) : {mpv(one, P.decompress_if(x, P.lift_y(y, par), Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), FS.value(one, r)))) == CV.decompress_if(FS.value(one, x), _, Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), FS.value(one, r))) : Maybe<&2, CV.SPoint>}
  dif_v(one, h1, x, P.lift_y(y, par), Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, y)), FS.value(one, r)))

def decompress_v(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +par: Nat, +hx: {PT.red(one, x) == True{} : Bool}, +hp: {Nat.is_lt(par, 2n) == True{} : Bool}) -> {mpv(one, P.decompress(x, par)) == CV.decompress(FS.prime(one), FS.value(one, x), par) : Maybe<&2, CV.SPoint>}:
  +hr = rhs_r(one, h1, x, hx)
  +hy = FP.sqrt_r(one, h1, P.rhs(x), hr)
  %Equal.sym(Nat, CV.rhs(FS.prime(one), FS.value(one, x)), FS.value(one, P.rhs(x)), Equal.sym(Nat, FS.value(one, P.rhs(x)), CV.rhs(FS.prime(one), FS.value(one, x)), rhs_v(one, h1, x, hx))) : {mpv(one, P.decompress_if(x, P.lift_y(F.sqrt(P.rhs(x)), par), F.eq(F.mul(F.sqrt(P.rhs(x)), F.sqrt(P.rhs(x))), P.rhs(x)))) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), FS.fsqrt(FS.prime(one), _), par), Nat.is_eq(FS.mmul(FS.prime(one), FS.fsqrt(FS.prime(one), CV.rhs(FS.prime(one), FS.value(one, x))), FS.fsqrt(FS.prime(one), CV.rhs(FS.prime(one), FS.value(one, x)))), CV.rhs(FS.prime(one), FS.value(one, x)))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.rhs(FS.prime(one), FS.value(one, x)), FS.value(one, P.rhs(x)), Equal.sym(Nat, FS.value(one, P.rhs(x)), CV.rhs(FS.prime(one), FS.value(one, x)), rhs_v(one, h1, x, hx))) : {mpv(one, P.decompress_if(x, P.lift_y(F.sqrt(P.rhs(x)), par), F.eq(F.mul(F.sqrt(P.rhs(x)), F.sqrt(P.rhs(x))), P.rhs(x)))) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), par), Nat.is_eq(FS.mmul(FS.prime(one), FS.fsqrt(FS.prime(one), _), FS.fsqrt(FS.prime(one), CV.rhs(FS.prime(one), FS.value(one, x)))), CV.rhs(FS.prime(one), FS.value(one, x)))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.rhs(FS.prime(one), FS.value(one, x)), FS.value(one, P.rhs(x)), Equal.sym(Nat, FS.value(one, P.rhs(x)), CV.rhs(FS.prime(one), FS.value(one, x)), rhs_v(one, h1, x, hx))) : {mpv(one, P.decompress_if(x, P.lift_y(F.sqrt(P.rhs(x)), par), F.eq(F.mul(F.sqrt(P.rhs(x)), F.sqrt(P.rhs(x))), P.rhs(x)))) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), par), Nat.is_eq(FS.mmul(FS.prime(one), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), FS.fsqrt(FS.prime(one), _)), CV.rhs(FS.prime(one), FS.value(one, x)))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.rhs(FS.prime(one), FS.value(one, x)), FS.value(one, P.rhs(x)), Equal.sym(Nat, FS.value(one, P.rhs(x)), CV.rhs(FS.prime(one), FS.value(one, x)), rhs_v(one, h1, x, hx))) : {mpv(one, P.decompress_if(x, P.lift_y(F.sqrt(P.rhs(x)), par), F.eq(F.mul(F.sqrt(P.rhs(x)), F.sqrt(P.rhs(x))), P.rhs(x)))) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), par), Nat.is_eq(FS.mmul(FS.prime(one), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x)))), _)) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), FS.value(one, F.sqrt(P.rhs(x))), Equal.sym(Nat, FS.value(one, F.sqrt(P.rhs(x))), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), FP.sqrt_v(one, h1, P.rhs(x), hr))) : {mpv(one, P.decompress_if(x, P.lift_y(F.sqrt(P.rhs(x)), par), F.eq(F.mul(F.sqrt(P.rhs(x)), F.sqrt(P.rhs(x))), P.rhs(x)))) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), _, par), Nat.is_eq(FS.mmul(FS.prime(one), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x)))), FS.value(one, P.rhs(x)))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), FS.value(one, F.sqrt(P.rhs(x))), Equal.sym(Nat, FS.value(one, F.sqrt(P.rhs(x))), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), FP.sqrt_v(one, h1, P.rhs(x), hr))) : {mpv(one, P.decompress_if(x, P.lift_y(F.sqrt(P.rhs(x)), par), F.eq(F.mul(F.sqrt(P.rhs(x)), F.sqrt(P.rhs(x))), P.rhs(x)))) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), FS.value(one, F.sqrt(P.rhs(x))), par), Nat.is_eq(FS.mmul(FS.prime(one), _, FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x)))), FS.value(one, P.rhs(x)))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), FS.value(one, F.sqrt(P.rhs(x))), Equal.sym(Nat, FS.value(one, F.sqrt(P.rhs(x))), FS.fsqrt(FS.prime(one), FS.value(one, P.rhs(x))), FP.sqrt_v(one, h1, P.rhs(x), hr))) : {mpv(one, P.decompress_if(x, P.lift_y(F.sqrt(P.rhs(x)), par), F.eq(F.mul(F.sqrt(P.rhs(x)), F.sqrt(P.rhs(x))), P.rhs(x)))) == CV.decompress_if(FS.value(one, x), CV.pick_parity(FS.prime(one), FS.value(one, F.sqrt(P.rhs(x))), par), Nat.is_eq(FS.mmul(FS.prime(one), FS.value(one, F.sqrt(P.rhs(x))), _), FS.value(one, P.rhs(x)))) : Maybe<&2, CV.SPoint>}
  dy(one, h1, x, P.rhs(x), F.sqrt(P.rhs(x)), par, hr, hy, hp)

def decompress_r(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +par: Nat, +hx: {PT.red(one, x) == True{} : Bool}, +hp: {Nat.is_lt(par, 2n) == True{} : Bool}) -> {mpred(one, P.decompress(x, par)) == True{} : Bool}:
  +hy = FP.sqrt_r(one, h1, P.rhs(x), rhs_r(one, h1, x, hx))
  dif_r(one, h1, x, P.lift_y(F.sqrt(P.rhs(x)), par), hx, lift_r(one, h1, F.sqrt(P.rhs(x)), par, hy, hp), F.eq(F.mul(F.sqrt(P.rhs(x)), F.sqrt(P.rhs(x))), P.rhs(x)))