~/jendhub

proofs/crypto/secp256k1/penc.bend

bend-collections-laws-crypto@1.0.0.0 · 187 lines · 22 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/penc.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend as FO
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend as FP
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as PM
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA
18import bend-collections-laws-crypto@1.0.0.0/proofs/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
24def 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
29def 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
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      {==}
44
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      {==}
55
56def 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
60def 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
66def 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
69def 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
74def 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
83def 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
93def 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
96def 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
99def 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
107def 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
114def 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)
118def 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
137def 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
156def 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
161def 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
166def 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
173def 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
185def 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)))