~/jendhub

proofs/crypto/secp256k1/point.bend

bend-collections-laws-crypto@1.0.0.0 · 263 lines · 35 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/point.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/field.bend as F
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend as FO
9
10# The group operations of src/crypto/secp256k1/point.bend against
11# spec/crypto/secp256k1/curve.bend: the register programs (RCB 2016
12# Algorithms 7 and 9) run on field elements compute, register by register,
13# the values the specification's programs compute on the natural numbers.
14
15def pr(+one: Nat) -> Nat:
16  FS.prime(one)
17
18def red(+one: Nat, +x: List<&2, Nat>) -> Bool:
19  FS.reduced(one, FS.prime(one), x)
20
21def vals(+one: Nat, rs: List<&2, List<&2, Nat>>) -> List<&2, Nat>:
22  match rs:
23    case Nil{}: Nil{}
24    case r <> t: FS.value(one, r) <> vals(one, t)
25
26def allred(+one: Nat, rs: List<&2, List<&2, Nat>>) -> Bool:
27  match rs:
28    case Nil{}: True{}
29    case r <> t: Bool.and(red(one, r), allred(one, t))
30
31def cop(op: P.Op) -> CV.SOp:
32  match op:
33    case P.OAdd{i, j}: CV.SAdd{i, j}
34    case P.OSub{i, j}: CV.SSub{i, j}
35    case P.OMul{i, j}: CV.SMul{i, j}
36
37def cprog(ops: List<&2, P.Op>) -> List<&2, CV.SOp>:
38  match ops:
39    case Nil{}: Nil{}
40    case o <> t: cop(o) <> cprog(t)
41
42# ---- registers ----
43
44def zero_r(+one: Nat, +h1: {one == 1n : Nat}) -> {red(one, F.zero()) == True{} : Bool}:
45  FO.small_r(one, h1, 0n, FO.small_lt_p(one, h1, 0n, {==}))
46
47def zero_v(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.value(one, F.zero()) == 0n : Nat}:
48  FO.small_val(one, h1, 0n, FO.small_lt_p(one, h1, 0n, {==}))
49
50def nth_r(+one: Nat, +h1: {one == 1n : Nat}, i: Nat, rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {red(one, P.nth(i, rs)) == True{} : Bool}:
51  match i rs:
52    case 0n Nil{}:
53      zero_r(one, h1)
54    case 1n+k Nil{}:
55      zero_r(one, h1)
56    case 0n +r <> +t:
57      Lg.and_left(red(one, r), allred(one, t), h)
58    case 1n+ +k +r <> +t:
59      nth_r(one, h1, k, t, Lg.and_right(red(one, r), allred(one, t), h))
60
61def nth_v(+one: Nat, +h1: {one == 1n : Nat}, i: Nat, rs: List<&2, List<&2, Nat>>) -> {FS.value(one, P.nth(i, rs)) == CV.nth(i, vals(one, rs)) : Nat}:
62  match i rs:
63    case 0n Nil{}:
64      zero_v(one, h1)
65    case 1n+k Nil{}:
66      zero_v(one, h1)
67    case 0n r <> t:
68      {==}
69    case 1n+ +k r <> +t:
70      nth_v(one, h1, k, t)
71
72def exec_r(+one: Nat, +h1: {one == 1n : Nat}, op: P.Op, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {red(one, P.exec(op, rs)) == True{} : Bool}:
73  match op:
74    case P.OAdd{+i, +j}:
75      FO.add_r(one, h1, P.nth(i, rs), P.nth(j, rs), nth_r(one, h1, i, rs, h), nth_r(one, h1, j, rs, h))
76    case P.OSub{+i, +j}:
77      FO.sub_r(one, h1, P.nth(i, rs), P.nth(j, rs), nth_r(one, h1, i, rs, h), nth_r(one, h1, j, rs, h))
78    case P.OMul{+i, +j}:
79      FO.mul_r(one, h1, P.nth(i, rs), P.nth(j, rs), nth_r(one, h1, i, rs, h), nth_r(one, h1, j, rs, h))
80
81def exec_v(+one: Nat, +h1: {one == 1n : Nat}, op: P.Op, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {FS.value(one, P.exec(op, rs)) == CV.exec(FS.prime(one), cop(op), vals(one, rs)) : Nat}:
82  match op:
83    case P.OAdd{+i, +j}:
84      %Equal.sym(Nat, FS.value(one, F.add(P.nth(i, rs), P.nth(j, rs))), FS.madd(FS.prime(one), FS.value(one, P.nth(i, rs)), FS.value(one, P.nth(j, rs))), FO.add_v(one, h1, P.nth(i, rs), P.nth(j, rs), nth_r(one, h1, i, rs, h), nth_r(one, h1, j, rs, h))) : {_ == FS.madd(FS.prime(one), CV.nth(i, vals(one, rs)), CV.nth(j, vals(one, rs))) : Nat}
85      %Equal.sym(Nat, FS.value(one, P.nth(i, rs)), CV.nth(i, vals(one, rs)), nth_v(one, h1, i, rs)) : {FS.madd(FS.prime(one), _, FS.value(one, P.nth(j, rs))) == FS.madd(FS.prime(one), CV.nth(i, vals(one, rs)), CV.nth(j, vals(one, rs))) : Nat}
86      %Equal.sym(Nat, FS.value(one, P.nth(j, rs)), CV.nth(j, vals(one, rs)), nth_v(one, h1, j, rs)) : {FS.madd(FS.prime(one), CV.nth(i, vals(one, rs)), _) == FS.madd(FS.prime(one), CV.nth(i, vals(one, rs)), CV.nth(j, vals(one, rs))) : Nat}
87      {==}
88    case P.OSub{+i, +j}:
89      %Equal.sym(Nat, FS.value(one, F.sub(P.nth(i, rs), P.nth(j, rs))), FS.msub(FS.prime(one), FS.value(one, P.nth(i, rs)), FS.value(one, P.nth(j, rs))), FO.sub_v(one, h1, P.nth(i, rs), P.nth(j, rs), nth_r(one, h1, i, rs, h), nth_r(one, h1, j, rs, h))) : {_ == FS.msub(FS.prime(one), CV.nth(i, vals(one, rs)), CV.nth(j, vals(one, rs))) : Nat}
90      %Equal.sym(Nat, FS.value(one, P.nth(i, rs)), CV.nth(i, vals(one, rs)), nth_v(one, h1, i, rs)) : {FS.msub(FS.prime(one), _, FS.value(one, P.nth(j, rs))) == FS.msub(FS.prime(one), CV.nth(i, vals(one, rs)), CV.nth(j, vals(one, rs))) : Nat}
91      %Equal.sym(Nat, FS.value(one, P.nth(j, rs)), CV.nth(j, vals(one, rs)), nth_v(one, h1, j, rs)) : {FS.msub(FS.prime(one), CV.nth(i, vals(one, rs)), _) == FS.msub(FS.prime(one), CV.nth(i, vals(one, rs)), CV.nth(j, vals(one, rs))) : Nat}
92      {==}
93    case P.OMul{+i, +j}:
94      %Equal.sym(Nat, FS.value(one, F.mul(P.nth(i, rs), P.nth(j, rs))), FS.mmul(FS.prime(one), FS.value(one, P.nth(i, rs)), FS.value(one, P.nth(j, rs))), FO.mul_v(one, h1, P.nth(i, rs), P.nth(j, rs), nth_r(one, h1, i, rs, h), nth_r(one, h1, j, rs, h))) : {_ == FS.mmul(FS.prime(one), CV.nth(i, vals(one, rs)), CV.nth(j, vals(one, rs))) : Nat}
95      %Equal.sym(Nat, FS.value(one, P.nth(i, rs)), CV.nth(i, vals(one, rs)), nth_v(one, h1, i, rs)) : {FS.mmul(FS.prime(one), _, FS.value(one, P.nth(j, rs))) == FS.mmul(FS.prime(one), CV.nth(i, vals(one, rs)), CV.nth(j, vals(one, rs))) : Nat}
96      %Equal.sym(Nat, FS.value(one, P.nth(j, rs)), CV.nth(j, vals(one, rs)), nth_v(one, h1, j, rs)) : {FS.mmul(FS.prime(one), CV.nth(i, vals(one, rs)), _) == FS.mmul(FS.prime(one), CV.nth(i, vals(one, rs)), CV.nth(j, vals(one, rs))) : Nat}
97      {==}
98
99def vals_app(+one: Nat, rs: List<&2, List<&2, Nat>>, +x: List<&2, Nat>) -> {vals(one, List.append(&2, List<&2, Nat>, rs, [x])) == List.append(&2, Nat, vals(one, rs), [FS.value(one, x)]) : List<&2, Nat>}:
100  match rs:
101    case Nil{}:
102      {==}
103    case +r <> +t:
104      Equal.cong(List<&2, Nat>, List<&2, Nat>, l => FS.value(one, r) <> l, vals(one, List.append(&2, List<&2, Nat>, t, [x])), List.append(&2, Nat, vals(one, t), [FS.value(one, x)]), vals_app(one, t, x))
105
106def allred_app(+one: Nat, rs: List<&2, List<&2, Nat>>, +x: List<&2, Nat>, +h: {allred(one, rs) == True{} : Bool}, +hx: {red(one, x) == True{} : Bool}) -> {allred(one, List.append(&2, List<&2, Nat>, rs, [x])) == True{} : Bool}:
107  match rs:
108    case Nil{}:
109      Lg.and_intro(red(one, x), True{}, hx, {==})
110    case +r <> +t:
111      Lg.and_intro(red(one, r), allred(one, List.append(&2, List<&2, Nat>, t, [x])), Lg.and_left(red(one, r), allred(one, t), h), allred_app(one, t, x, Lg.and_right(red(one, r), allred(one, t), h), hx))
112
113def run_go_r(+one: Nat, +h1: {one == 1n : Nat}, prog: List<&2, P.Op>, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {allred(one, P.run_go(prog, rs)) == True{} : Bool}:
114  match prog:
115    case Nil{}:
116      h
117    case +op <> +t:
118      run_go_r(one, h1, t, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)]), allred_app(one, rs, P.exec(op, rs), h, exec_r(one, h1, op, rs, h)))
119
120def run_go_v(+one: Nat, +h1: {one == 1n : Nat}, prog: List<&2, P.Op>, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {vals(one, P.run_go(prog, rs)) == CV.run_go(FS.prime(one), cprog(prog), vals(one, rs)) : List<&2, Nat>}:
121  match prog:
122    case Nil{}:
123      {==}
124    case +op <> +t:
125      +rs2 = List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)])
126      +h2 = allred_app(one, rs, P.exec(op, rs), h, exec_r(one, h1, op, rs, h))
127      %Equal.sym(List<&2, Nat>, vals(one, P.run_go(t, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)]))), CV.run_go(FS.prime(one), cprog(t), vals(one, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)]))), run_go_v(one, h1, t, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)]), h2)) : {_ == CV.run_go(FS.prime(one), cprog(t), List.append(&2, Nat, vals(one, rs), [CV.exec(FS.prime(one), cop(op), vals(one, rs))])) : List<&2, Nat>}
128      %Equal.sym(List<&2, Nat>, vals(one, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)])), List.append(&2, Nat, vals(one, rs), [FS.value(one, P.exec(op, rs))]), vals_app(one, rs, P.exec(op, rs))) : {CV.run_go(FS.prime(one), cprog(t), _) == CV.run_go(FS.prime(one), cprog(t), List.append(&2, Nat, vals(one, rs), [CV.exec(FS.prime(one), cop(op), vals(one, rs))])) : List<&2, Nat>}
129      %Equal.sym(Nat, FS.value(one, P.exec(op, rs)), CV.exec(FS.prime(one), cop(op), vals(one, rs)), exec_v(one, h1, op, rs, h)) : {CV.run_go(FS.prime(one), cprog(t), List.append(&2, Nat, vals(one, rs), [_])) == CV.run_go(FS.prime(one), cprog(t), List.append(&2, Nat, vals(one, rs), [CV.exec(FS.prime(one), cop(op), vals(one, rs))])) : List<&2, Nat>}
130      {==}
131
132# run looks at its first register first
133def run_is(prog: List<&2, P.Op>, rs: List<&2, List<&2, Nat>>) -> {P.run(prog, rs) == P.run_go(prog, rs) : List<&2, List<&2, Nat>>}:
134  match rs:
135    case Nil{}:
136      {==}
137    case Nil{} <> t:
138      {==}
139    case (y <> u) <> t:
140      {==}
141
142def srun_is(+p: Nat, prog: List<&2, CV.SOp>, rs: List<&2, Nat>) -> {CV.run(p, prog, rs) == CV.run_go(p, prog, rs) : List<&2, Nat>}:
143  match rs:
144    case Nil{}:
145      {==}
146    case 0n <> t:
147      {==}
148    case (1n+k) <> t:
149      {==}
150
151def run_r(+one: Nat, +h1: {one == 1n : Nat}, +prog: List<&2, P.Op>, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {allred(one, P.run(prog, rs)) == True{} : Bool}:
152  %Equal.sym(List<&2, List<&2, Nat>>, P.run(prog, rs), P.run_go(prog, rs), run_is(prog, rs)) : {allred(one, _) == True{} : Bool}
153  run_go_r(one, h1, prog, rs, h)
154
155def run_v(+one: Nat, +h1: {one == 1n : Nat}, +prog: List<&2, P.Op>, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {vals(one, P.run(prog, rs)) == CV.run(FS.prime(one), cprog(prog), vals(one, rs)) : List<&2, Nat>}:
156  %Equal.sym(List<&2, List<&2, Nat>>, P.run(prog, rs), P.run_go(prog, rs), run_is(prog, rs)) : {vals(one, _) == CV.run(FS.prime(one), cprog(prog), vals(one, rs)) : List<&2, Nat>}
157  %Equal.sym(List<&2, Nat>, CV.run(FS.prime(one), cprog(prog), vals(one, rs)), CV.run_go(FS.prime(one), cprog(prog), vals(one, rs)), srun_is(FS.prime(one), cprog(prog), vals(one, rs))) : {vals(one, P.run_go(prog, rs)) == _ : List<&2, Nat>}
158  run_go_v(one, h1, prog, rs, h)
159
160# ---- points ----
161
162def pv(+one: Nat, p: P.Point) -> CV.SPoint:
163  match p:
164    case P.Point{x, y, z}: CV.SPoint{FS.value(one, x), FS.value(one, y), FS.value(one, z)}
165
166def pred(+one: Nat, p: P.Point) -> Bool:
167  match p:
168    case P.Point{x, y, z}: Bool.and(red(one, x), Bool.and(red(one, y), red(one, z)))
169
170def b3_r(+one: Nat, +h1: {one == 1n : Nat}) -> {red(one, P.b3()) == True{} : Bool}:
171  FO.small_r(one, h1, 21n, FO.small_lt_p(one, h1, 21n, {==}))
172
173def b3_v(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.value(one, P.b3()) == 21n : Nat}:
174  FO.small_val(one, h1, 21n, FO.small_lt_p(one, h1, 21n, {==}))
175
176def add_prog_eq() -> {cprog(P.add_prog()) == CV.add_prog() : List<&2, CV.SOp>}:
177  {==}
178
179def dbl_prog_eq() -> {cprog(P.dbl_prog()) == CV.dbl_prog() : List<&2, CV.SOp>}:
180  {==}
181
182def regs7(+one: Nat, +h1: {one == 1n : Nat}, +x1: List<&2, Nat>, +y1: List<&2, Nat>, +z1: List<&2, Nat>, +x2: List<&2, Nat>, +y2: List<&2, Nat>, +z2: List<&2, Nat>, +h: {Bool.and(red(one, x1), Bool.and(red(one, y1), red(one, z1))) == True{} : Bool}, +g: {Bool.and(red(one, x2), Bool.and(red(one, y2), red(one, z2))) == True{} : Bool}) -> {allred(one, [x1, y1, z1, x2, y2, z2, P.b3()]) == True{} : Bool}:
183  +hx = Lg.and_left(red(one, x1), Bool.and(red(one, y1), red(one, z1)), h)
184  +hy = Lg.and_left(red(one, y1), red(one, z1), Lg.and_right(red(one, x1), Bool.and(red(one, y1), red(one, z1)), h))
185  +hz = Lg.and_right(red(one, y1), red(one, z1), Lg.and_right(red(one, x1), Bool.and(red(one, y1), red(one, z1)), h))
186  +gx = Lg.and_left(red(one, x2), Bool.and(red(one, y2), red(one, z2)), g)
187  +gy = Lg.and_left(red(one, y2), red(one, z2), Lg.and_right(red(one, x2), Bool.and(red(one, y2), red(one, z2)), g))
188  +gz = Lg.and_right(red(one, y2), red(one, z2), Lg.and_right(red(one, x2), Bool.and(red(one, y2), red(one, z2)), g))
189  +hb = b3_r(one, h1)
190  Lg.and_intro(red(one, x1), allred(one, [y1, z1, x2, y2, z2, P.b3()]), hx, Lg.and_intro(red(one, y1), allred(one, [z1, x2, y2, z2, P.b3()]), hy, Lg.and_intro(red(one, z1), allred(one, [x2, y2, z2, P.b3()]), hz, Lg.and_intro(red(one, x2), allred(one, [y2, z2, P.b3()]), gx, Lg.and_intro(red(one, y2), allred(one, [z2, P.b3()]), gy, Lg.and_intro(red(one, z2), allred(one, [P.b3()]), gz, Lg.and_intro(red(one, P.b3()), True{}, hb, {==})))))))
191
192def vals7(+one: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +c: List<&2, Nat>, +d: List<&2, Nat>, +e: List<&2, Nat>, +f: List<&2, Nat>, +g: List<&2, Nat>) -> {vals(one, [a, b, c, d, e, f, g]) == [FS.value(one, a), FS.value(one, b), FS.value(one, c), FS.value(one, d), FS.value(one, e), FS.value(one, f), FS.value(one, g)] : List<&2, Nat>}:
193  {==}
194
195def padd_v(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, b: P.Point, +ha: {pred(one, a) == True{} : Bool}, +hb: {pred(one, b) == True{} : Bool}) -> {pv(one, P.add(a, b)) == CV.padd(FS.prime(one), pv(one, a), pv(one, b)) : CV.SPoint}:
196  match a b:
197    case P.Point{+x1, +y1, +z1} P.Point{+x2, +y2, +z2}:
198      +hr = regs7(one, h1, x1, y1, z1, x2, y2, z2, ha, hb)
199      %Equal.sym(Nat, FS.value(one, P.nth(33n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(33n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), nth_v(one, h1, 33n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))) : {CV.SPoint{_, FS.value(one, P.nth(36n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), FS.value(one, P.nth(39n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
200      %Equal.sym(Nat, FS.value(one, P.nth(36n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), nth_v(one, h1, 36n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))) : {CV.SPoint{CV.nth(33n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), _, FS.value(one, P.nth(39n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
201      %Equal.sym(Nat, FS.value(one, P.nth(39n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), nth_v(one, h1, 39n, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))) : {CV.SPoint{CV.nth(33n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), _} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
202      %Equal.sym(List<&2, Nat>, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])), CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])), run_v(one, h1, P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()], hr)) : {CV.SPoint{CV.nth(33n, _), CV.nth(36n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
203      %Equal.sym(List<&2, Nat>, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])), CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])), run_v(one, h1, P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()], hr)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, _), CV.nth(39n, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
204      %Equal.sym(List<&2, Nat>, vals(one, P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])), CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])), run_v(one, h1, P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()], hr)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, _)} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
205      %Equal.sym(List<&2, CV.SOp>, cprog(P.add_prog()), CV.add_prog(), add_prog_eq()) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), _, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
206      %Equal.sym(List<&2, CV.SOp>, cprog(P.add_prog()), CV.add_prog(), add_prog_eq()) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, CV.run(FS.prime(one), _, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, CV.run(FS.prime(one), cprog(P.add_prog()), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
207      %Equal.sym(List<&2, CV.SOp>, cprog(P.add_prog()), CV.add_prog(), add_prog_eq()) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, CV.run(FS.prime(one), _, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
208      %Equal.sym(List<&2, Nat>, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())], vals7(one, x1, y1, z1, x2, y2, z2, P.b3())) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), _)), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]))), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
209      %Equal.sym(List<&2, Nat>, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())], vals7(one, x1, y1, z1, x2, y2, z2, P.b3())) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), _)), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), vals(one, [x1, y1, z1, x2, y2, z2, P.b3()])))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
210      %Equal.sym(List<&2, Nat>, vals(one, [x1, y1, z1, x2, y2, z2, P.b3()]), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())], vals7(one, x1, y1, z1, x2, y2, z2, P.b3())) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())])), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), _))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
211      %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), _])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())])), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())]))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
212      %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), 21n])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), _])), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), FS.value(one, P.b3())]))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
213      %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(33n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), 21n])), CV.nth(36n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), 21n])), CV.nth(39n, CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), _]))} == CV.add_out(CV.run(FS.prime(one), CV.add_prog(), [FS.value(one, x1), FS.value(one, y1), FS.value(one, z1), FS.value(one, x2), FS.value(one, y2), FS.value(one, z2), CV.b3()])) : CV.SPoint}
214      {==}
215
216def regs4(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +y: List<&2, Nat>, +z: List<&2, Nat>, +h: {Bool.and(red(one, x), Bool.and(red(one, y), red(one, z))) == True{} : Bool}) -> {allred(one, [x, y, z, P.b3()]) == True{} : Bool}:
217  +hx = Lg.and_left(red(one, x), Bool.and(red(one, y), red(one, z)), h)
218  +hy = Lg.and_left(red(one, y), red(one, z), Lg.and_right(red(one, x), Bool.and(red(one, y), red(one, z)), h))
219  +hz = Lg.and_right(red(one, y), red(one, z), Lg.and_right(red(one, x), Bool.and(red(one, y), red(one, z)), h))
220  +hb = b3_r(one, h1)
221  Lg.and_intro(red(one, x), allred(one, [y, z, P.b3()]), hx, Lg.and_intro(red(one, y), allred(one, [z, P.b3()]), hy, Lg.and_intro(red(one, z), allred(one, [P.b3()]), hz, Lg.and_intro(red(one, P.b3()), True{}, hb, {==}))))
222
223def vals4(+one: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +c: List<&2, Nat>, +d: List<&2, Nat>) -> {vals(one, [a, b, c, d]) == [FS.value(one, a), FS.value(one, b), FS.value(one, c), FS.value(one, d)] : List<&2, Nat>}:
224  {==}
225
226def pdbl_v(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, +ha: {pred(one, a) == True{} : Bool}) -> {pv(one, P.dbl(a)) == CV.pdbl(FS.prime(one), pv(one, a)) : CV.SPoint}:
227  match a:
228    case P.Point{+x, +y, +z}:
229      +hr = regs4(one, h1, x, y, z, ha)
230      %Equal.sym(Nat, FS.value(one, P.nth(21n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(21n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), nth_v(one, h1, 21n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))) : {CV.SPoint{_, FS.value(one, P.nth(18n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), FS.value(one, P.nth(13n, P.run(P.dbl_prog(), [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
231      %Equal.sym(Nat, FS.value(one, P.nth(18n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(18n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), nth_v(one, h1, 18n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))) : {CV.SPoint{CV.nth(21n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), _, FS.value(one, P.nth(13n, P.run(P.dbl_prog(), [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
232      %Equal.sym(Nat, FS.value(one, P.nth(13n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(13n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), nth_v(one, h1, 13n, P.run(P.dbl_prog(), [x, y, z, P.b3()]))) : {CV.SPoint{CV.nth(21n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(18n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), _} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
233      %Equal.sym(List<&2, Nat>, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])), CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])), run_v(one, h1, P.dbl_prog(), [x, y, z, P.b3()], hr)) : {CV.SPoint{CV.nth(21n, _), CV.nth(18n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()]))), CV.nth(13n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
234      %Equal.sym(List<&2, Nat>, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])), CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])), run_v(one, h1, P.dbl_prog(), [x, y, z, P.b3()], hr)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()]))), CV.nth(18n, _), CV.nth(13n, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
235      %Equal.sym(List<&2, Nat>, vals(one, P.run(P.dbl_prog(), [x, y, z, P.b3()])), CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])), run_v(one, h1, P.dbl_prog(), [x, y, z, P.b3()], hr)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()]))), CV.nth(18n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()]))), CV.nth(13n, _)} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
236      %Equal.sym(List<&2, CV.SOp>, cprog(P.dbl_prog()), CV.dbl_prog(), dbl_prog_eq()) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), _, vals(one, [x, y, z, P.b3()]))), CV.nth(18n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()]))), CV.nth(13n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
237      %Equal.sym(List<&2, CV.SOp>, cprog(P.dbl_prog()), CV.dbl_prog(), dbl_prog_eq()) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()]))), CV.nth(18n, CV.run(FS.prime(one), _, vals(one, [x, y, z, P.b3()]))), CV.nth(13n, CV.run(FS.prime(one), cprog(P.dbl_prog()), vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
238      %Equal.sym(List<&2, CV.SOp>, cprog(P.dbl_prog()), CV.dbl_prog(), dbl_prog_eq()) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()]))), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()]))), CV.nth(13n, CV.run(FS.prime(one), _, vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
239      %Equal.sym(List<&2, Nat>, vals(one, [x, y, z, P.b3()]), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())], vals4(one, x, y, z, P.b3())) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), _)), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()]))), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
240      %Equal.sym(List<&2, Nat>, vals(one, [x, y, z, P.b3()]), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())], vals4(one, x, y, z, P.b3())) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), _)), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), vals(one, [x, y, z, P.b3()])))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
241      %Equal.sym(List<&2, Nat>, vals(one, [x, y, z, P.b3()]), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())], vals4(one, x, y, z, P.b3())) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())])), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), _))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
242      %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), _])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())])), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())]))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
243      %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), 21n])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), _])), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), FS.value(one, P.b3())]))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
244      %Equal.sym(Nat, FS.value(one, P.b3()), 21n, b3_v(one, h1)) : {CV.SPoint{CV.nth(21n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), 21n])), CV.nth(18n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), 21n])), CV.nth(13n, CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), _]))} == CV.dbl_out(CV.run(FS.prime(one), CV.dbl_prog(), [FS.value(one, x), FS.value(one, y), FS.value(one, z), CV.b3()])) : CV.SPoint}
245      {==}
246
247# the results are reduced
248def pr3(+one: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +c: List<&2, Nat>, +ha: {red(one, a) == True{} : Bool}, +hb: {red(one, b) == True{} : Bool}, +hc: {red(one, c) == True{} : Bool}) -> {pred(one, P.Point{a, b, c}) == True{} : Bool}:
249  Lg.and_intro(red(one, a), Bool.and(red(one, b), red(one, c)), ha, Lg.and_intro(red(one, b), red(one, c), hb, hc))
250
251def padd_r(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, b: P.Point, +ha: {pred(one, a) == True{} : Bool}, +hb: {pred(one, b) == True{} : Bool}) -> {pred(one, P.add(a, b)) == True{} : Bool}:
252  match a b:
253    case P.Point{+x1, +y1, +z1} P.Point{+x2, +y2, +z2}:
254      +hr = run_r(one, h1, P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()], regs7(one, h1, x1, y1, z1, x2, y2, z2, ha, hb))
255      +rs = P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])
256      pr3(one, P.nth(33n, rs), P.nth(36n, rs), P.nth(39n, rs), nth_r(one, h1, 33n, rs, hr), nth_r(one, h1, 36n, rs, hr), nth_r(one, h1, 39n, rs, hr))
257
258def pdbl_r(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, +ha: {pred(one, a) == True{} : Bool}) -> {pred(one, P.dbl(a)) == True{} : Bool}:
259  match a:
260    case P.Point{+x, +y, +z}:
261      +hr = run_r(one, h1, P.dbl_prog(), [x, y, z, P.b3()], regs4(one, h1, x, y, z, ha))
262      +rs = P.run(P.dbl_prog(), [x, y, z, P.b3()])
263      pr3(one, P.nth(21n, rs), P.nth(18n, rs), P.nth(13n, rs), nth_r(one, h1, 21n, rs, hr), nth_r(one, h1, 18n, rs, hr), nth_r(one, h1, 13n, rs, hr))