1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/penc.src; edit the .src 2 import Base 3 import ../../../spec/crypto/secp256k1/field.bend as FS 4 import ../../../spec/crypto/secp256k1/curve.bend as CV 5 import ../../../src/crypto/secp256k1/limbs.bend as L 6 import ../../../src/crypto/secp256k1/field.bend as F 7 import ../../../src/crypto/secp256k1/bytes.bend as B 8 import ../../../src/crypto/secp256k1/point.bend as P 9 import ../../lib/logic.bend as Lg 10 import ./limbs.bend as LV 11 import ./fieldops.bend as FO 12 import ./fieldpow.bend as FP 13 import ./fwrap.bend as FW 14 import ./bytes.bend as BY 15 import ./point.bend as PT 16 import ./sel.bend as PM 17 import ./paff.bend as PA 18 import ../../math/natural/arith.bend as NR 19 20 # SEC 1 encodings of src/crypto/secp256k1/point.bend (compressed and 21 # uncompressed encode, decode with decompression) against 22 # spec/crypto/secp256k1/curve.bend. 23 24 def mpv(+one: Nat, m: Maybe<&2, P.Point>) -> Maybe<&2, CV.SPoint>: 25 match m: 26 case None{}: None{} 27 case Some{q}: Some{PT.pv(one, q)} 28 29 def mpred(+one: Nat, m: Maybe<&2, P.Point>) -> Bool: 30 match m: 31 case None{}: True{} 32 case Some{q}: PT.pred(one, q) 33 34 # ---- encode ---- 35 36 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>}: 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 {==} 44 45 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>}: 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 {==} 55 56 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>}: 57 %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>} 58 enc_c_v(one, h1, P.to_affine(q), PA.aff_r(one, h1, q, hq)) 59 60 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>}: 61 %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>} 62 enc_u_v(one, h1, P.to_affine(q), PA.aff_r(one, h1, q, hq)) 63 64 # ---- x^3 + 7, on the curve ---- 65 66 def seven_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(7n, FS.prime(one)) == True{} : Bool}: 67 FO.small_lt_p(one, h1, 7n, {==}) 68 69 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}: 70 +h2 = FO.mul_r(one, h1, x, x, hx, hx) 71 +h3 = FO.mul_r(one, h1, F.mul(x, x), x, h2, hx) 72 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))) 73 74 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}: 75 +h2 = FO.mul_r(one, h1, x, x, hx, hx) 76 +h3 = FO.mul_r(one, h1, F.mul(x, x), x, h2, hx) 77 %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} 78 %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} 79 %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} 80 %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} 81 {==} 82 83 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}: 84 +hs = FO.mul_r(one, h1, y, y, hy, hy) 85 +hr = rhs_r(one, h1, x, hx) 86 %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} 87 %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} 88 %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} 89 {==} 90 91 # ---- decompression ---- 92 93 def one_v(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.value(one, F.one()) == 1n : Nat}: 94 FO.small_val(one, h1, 1n, PM.one_lt(one, h1)) 95 96 def one_r(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.red(one, F.one()) == True{} : Bool}: 97 FO.small_r(one, h1, 1n, PM.one_lt(one, h1)) 98 99 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>}: 100 match ok: 101 case True{}: 102 %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>} 103 {==} 104 case False{}: 105 {==} 106 107 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}: 108 match ok: 109 case True{}: 110 PT.pr3(one, x, y, F.one(), hx, hy, one_r(one, h1)) 111 case False{}: 112 {==} 113 114 def mod2_lt(+v: Nat) -> {Nat.is_lt(Nat.mod(v, 2n), 2n) == True{} : Bool}: 115 NR.dm_lt(1n, v) 116 117 # y or p - y by the parities q and par (both 0 or 1) 118 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}: 119 match q par: 120 case 0n 0n: 121 %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} 122 {==} 123 case 0n 1n: 124 %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} 125 FO.neg_v(one, h1, y, hy) 126 case 1n 0n: 127 %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} 128 FO.neg_v(one, h1, y, hy) 129 case 1n 1n: 130 %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} 131 {==} 132 case 2n+ +c _: 133 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)) 134 case _ 2n+ +c: 135 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)) 136 137 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}: 138 match q par: 139 case 0n 0n: 140 %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} 141 hy 142 case 0n 1n: 143 %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} 144 FO.neg_r(one, h1, y, hy) 145 case 1n 0n: 146 %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} 147 FO.neg_r(one, h1, y, hy) 148 case 1n 1n: 149 %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} 150 hy 151 case 2n+ +c _: 152 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)) 153 case _ 2n+ +c: 154 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)) 155 156 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}: 157 %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} 158 %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} 159 pick_v(one, h1, Nat.mod(FS.value(one, y), 2n), par, y, mod2_lt(FS.value(one, y)), hp, hy) 160 161 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}: 162 %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} 163 %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} 164 pick_r(one, h1, Nat.mod(FS.value(one, y), 2n), par, y, mod2_lt(FS.value(one, y)), hp, hy) 165 166 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>}: 167 +hs = FO.mul_r(one, h1, y, y, hy, hy) 168 %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>} 169 %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>} 170 %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>} 171 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))) 172 173 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>}: 174 +hr = rhs_r(one, h1, x, hx) 175 +hy = FP.sqrt_r(one, h1, P.rhs(x), hr) 176 %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>} 177 %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>} 178 %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>} 179 %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>} 180 %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>} 181 %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>} 182 %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>} 183 dy(one, h1, x, P.rhs(x), F.sqrt(P.rhs(x)), par, hr, hy, hp) 184 185 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}: 186 +hy = FP.sqrt_r(one, h1, P.rhs(x), rhs_r(one, h1, x, hx)) 187 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)))