~/jendhub

proofs/crypto/ed25519/prel.bend

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

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as SX
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as PT
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as FO
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw.bend as MW
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
17
18# edwards25519 point operations of src/crypto/ed25519/point.bend against
19# spec/crypto/ed25519.bend: the point relation Rp (each coordinate RL.R),
20# kept by addition, doubling, selection and double-and-add scalar
21# multiplication, for every point.
22
23def v(+x: U32) -> Nat:
24  U32.to_nat(x)
25
26def DP(-A: Data, -B: Data) -> Data:
27  Sigma<&2, &2, A, _ => B>
28
29def fst(-A: Data, -B: Data, +p: DP(A, B)) -> A:
30  match p:
31    case (a, b):
32      a
33
34def snd(-A: Data, -B: Data, +p: DP(A, B)) -> B:
35  match p:
36    case (a, b):
37      b
38
39def Rp(+pp: Nat, +p: PT.Pt, +q: SE.EPt) -> Data:
40  match p q:
41    case PT.Pt{x, y, z, t} SE.EPt{a, b, c, d}:
42      DP(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))))
43
44def mk(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +rx: RL.R(pp, x, a), +ry: RL.R(pp, y, b), +rz: RL.R(pp, z, c), +rt: RL.R(pp, t, d)) -> Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d}):
45  (rx, (ry, (rz, rt)))
46
47def rX(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +h: Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d})) -> RL.R(pp, x, a):
48  fst(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))), h)
49
50def rY(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +h: Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d})) -> RL.R(pp, y, b):
51  fst(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d)), snd(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))), h))
52
53def rZ(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +h: Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d})) -> RL.R(pp, z, c):
54  fst(RL.R(pp, z, c), RL.R(pp, t, d), snd(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d)), snd(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))), h)))
55
56def rT(+pp: Nat, +x: List<&2, U32>, +y: List<&2, U32>, +z: List<&2, U32>, +t: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat, +h: Rp(pp, PT.Pt{x, y, z, t}, SE.EPt{a, b, c, d})) -> RL.R(pp, t, d):
57  snd(RL.R(pp, z, c), RL.R(pp, t, d), snd(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d)), snd(RL.R(pp, x, a), DP(RL.R(pp, y, b), DP(RL.R(pp, z, c), RL.R(pp, t, d))), h)))
58
59# relation-level field operations
60def o(+pp: Nat, +x: List<&2, U32>, +a: Nat, +r: RL.R(pp, x, a)) -> {LM.okb(32n, x, 255n) == True{} : Bool}:
61  RL.r_o(pp, x, a, r)
62
63def c(+pp: Nat, +x: List<&2, U32>, +a: Nat, +r: RL.R(pp, x, a)) -> G.ceq(pp, FS.value(x), a):
64  RL.r_c(pp, x, a, r)
65
66def radd(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +y: List<&2, U32>, +a: Nat, +b: Nat, +rx: RL.R(pp, x, a), +ry: RL.R(pp, y, b)) -> RL.R(pp, F.add(x, y), FS.fadd(1n+pp, a, b)):
67  (FO.add_okb(one, h1, x, y, o(pp, x, a, rx), o(pp, y, b, ry)), RL.rc_add(one, h1, pp, hP, x, y, a, b, o(pp, x, a, rx), c(pp, x, a, rx), o(pp, y, b, ry), c(pp, y, b, ry)))
68
69def rsub(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +y: List<&2, U32>, +a: Nat, +b: Nat, +rx: RL.R(pp, x, a), +ry: RL.R(pp, y, b)) -> RL.R(pp, F.sub(x, y), FS.fsub(1n+pp, a, b)):
70  (FO.sub_okb(one, h1, x, y, o(pp, x, a, rx), o(pp, y, b, ry)), RL.rc_sub(one, h1, pp, hP, x, y, a, b, o(pp, x, a, rx), c(pp, x, a, rx), o(pp, y, b, ry), c(pp, y, b, ry)))
71
72def rmul(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +y: List<&2, U32>, +a: Nat, +b: Nat, +rx: RL.R(pp, x, a), +ry: RL.R(pp, y, b)) -> RL.R(pp, F.mul(x, y), FS.fmul(1n+pp, a, b)):
73  (MW.mul_okb(one, h1, x, y, o(pp, x, a, rx), o(pp, y, b, ry)), RL.rc_mul(one, h1, pp, hP, x, y, a, b, o(pp, x, a, rx), c(pp, x, a, rx), o(pp, y, b, ry), c(pp, y, b, ry)))
74
75def rsq(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +a: Nat, +rx: RL.R(pp, x, a)) -> RL.R(pp, F.sq(x), FS.fmul(1n+pp, a, a)):
76  rmul(one, h1, pp, hP, x, x, a, a, rx, rx)
77
78# ---- addition ----
79
80def add_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +cs: PT.Cs, +D: Nat, +rd2: RL.R(pp, PT.cs_d2(cs), FS.fadd(1n+pp, D, D)), +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +hp: Rp(pp, p, sp), +hq: Rp(pp, q, sq)) -> Rp(pp, PT.add(cs, p, q), SE.add(1n+pp, D, sp, sq)):
81  match p q sp sq:
82    case PT.Pt{+x1, +y1, +z1, +t1} PT.Pt{+x2, +y2, +z2, +t2} SE.EPt{+a1, +b1, +c1, +d1} SE.EPt{+a2, +b2, +c2, +d2}:
83      +P = {1n+pp : Nat}
84      +rx1 = rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
85      +ry1 = rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
86      +rz1 = rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
87      +rt1 = rT(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
88      +rx2 = rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
89      +ry2 = rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
90      +rz2 = rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
91      +rt2 = rT(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq)
92      +ra = rmul(one, h1, pp, hP, F.sub(y1, x1), F.sub(y2, x2), FS.fsub(P, b1, a1), FS.fsub(P, b2, a2), rsub(one, h1, pp, hP, y1, x1, b1, a1, ry1, rx1), rsub(one, h1, pp, hP, y2, x2, b2, a2, ry2, rx2))
93      +rb = rmul(one, h1, pp, hP, F.add(y1, x1), F.add(y2, x2), FS.fadd(P, b1, a1), FS.fadd(P, b2, a2), radd(one, h1, pp, hP, y1, x1, b1, a1, ry1, rx1), radd(one, h1, pp, hP, y2, x2, b2, a2, ry2, rx2))
94      +rc = rmul(one, h1, pp, hP, F.mul(t1, PT.cs_d2(cs)), t2, FS.fmul(P, d1, FS.fadd(P, D, D)), d2, rmul(one, h1, pp, hP, t1, PT.cs_d2(cs), d1, FS.fadd(P, D, D), rt1, rd2), rt2)
95      +rdd = rmul(one, h1, pp, hP, F.add(z1, z1), z2, FS.fadd(P, c1, c1), c2, radd(one, h1, pp, hP, z1, z1, c1, c1, rz1, rz1), rz2)
96      +ea = F.mul(F.sub(y1, x1), F.sub(y2, x2))
97      +EA = FS.fmul(P, FS.fsub(P, b1, a1), FS.fsub(P, b2, a2))
98      +eb = F.mul(F.add(y1, x1), F.add(y2, x2))
99      +EB = FS.fmul(P, FS.fadd(P, b1, a1), FS.fadd(P, b2, a2))
100      +ec = F.mul(F.mul(t1, PT.cs_d2(cs)), t2)
101      +EC = FS.fmul(P, FS.fmul(P, d1, FS.fadd(P, D, D)), d2)
102      +ed = F.mul(F.add(z1, z1), z2)
103      +ED = FS.fmul(P, FS.fadd(P, c1, c1), c2)
104      +re = rsub(one, h1, pp, hP, eb, ea, EB, EA, rb, ra)
105      +rf = rsub(one, h1, pp, hP, ed, ec, ED, EC, rdd, rc)
106      +rg = radd(one, h1, pp, hP, ed, ec, ED, EC, rdd, rc)
107      +rh = radd(one, h1, pp, hP, eb, ea, EB, EA, rb, ra)
108      +e = F.sub(eb, ea)
109      +f = F.sub(ed, ec)
110      +g = F.add(ed, ec)
111      +h = F.add(eb, ea)
112      +EE = FS.fsub(P, EB, EA)
113      +FF = FS.fsub(P, ED, EC)
114      +GG = FS.fadd(P, ED, EC)
115      +HH = FS.fadd(P, EB, EA)
116      mk(pp, F.mul(e, f), F.mul(g, h), F.mul(f, g), F.mul(e, h), FS.fmul(P, EE, FF), FS.fmul(P, GG, HH), FS.fmul(P, FF, GG), FS.fmul(P, EE, HH), rmul(one, h1, pp, hP, e, f, EE, FF, re, rf), rmul(one, h1, pp, hP, g, h, GG, HH, rg, rh), rmul(one, h1, pp, hP, f, g, FF, GG, rf, rg), rmul(one, h1, pp, hP, e, h, EE, HH, re, rh))
117
118# ---- doubling ----
119
120def double_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +p: PT.Pt, +sp: SE.EPt, +hp: Rp(pp, p, sp)) -> Rp(pp, PT.double(p), SE.double(1n+pp, sp)):
121  match p sp:
122    case PT.Pt{+x1, +y1, +z1, +t1} SE.EPt{+a1, +b1, +c1, +d1}:
123      +P = {1n+pp : Nat}
124      +rx1 = rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
125      +ry1 = rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
126      +rz1 = rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp)
127      +a = F.sq(x1)
128      +A = FS.fmul(P, a1, a1)
129      +ra = rsq(one, h1, pp, hP, x1, a1, rx1)
130      +b = F.sq(y1)
131      +B = FS.fmul(P, b1, b1)
132      +rb = rsq(one, h1, pp, hP, y1, b1, ry1)
133      +zz = F.sq(z1)
134      +ZZ = FS.fmul(P, c1, c1)
135      +rzz = rsq(one, h1, pp, hP, z1, c1, rz1)
136      +cc = F.add(zz, zz)
137      +CC = FS.fadd(P, ZZ, ZZ)
138      +rcc = radd(one, h1, pp, hP, zz, zz, ZZ, ZZ, rzz, rzz)
139      +h = F.add(a, b)
140      +HH = FS.fadd(P, A, B)
141      +rh = radd(one, h1, pp, hP, a, b, A, B, ra, rb)
142      +xy = F.add(x1, y1)
143      +XY = FS.fadd(P, a1, b1)
144      +rxy = radd(one, h1, pp, hP, x1, y1, a1, b1, rx1, ry1)
145      +e = F.sub(h, F.sq(xy))
146      +EE = FS.fsub(P, HH, FS.fmul(P, XY, XY))
147      +re = rsub(one, h1, pp, hP, h, F.sq(xy), HH, FS.fmul(P, XY, XY), rh, rsq(one, h1, pp, hP, xy, XY, rxy))
148      +g = F.sub(a, b)
149      +GG = FS.fsub(P, A, B)
150      +rg = rsub(one, h1, pp, hP, a, b, A, B, ra, rb)
151      +f = F.add(cc, g)
152      +FF = FS.fadd(P, CC, GG)
153      +rf = radd(one, h1, pp, hP, cc, g, CC, GG, rcc, rg)
154      mk(pp, F.mul(e, f), F.mul(g, h), F.mul(f, g), F.mul(e, h), FS.fmul(P, EE, FF), FS.fmul(P, GG, HH), FS.fmul(P, FF, GG), FS.fmul(P, EE, HH), rmul(one, h1, pp, hP, e, f, EE, FF, re, rf), rmul(one, h1, pp, hP, g, h, GG, HH, rg, rh), rmul(one, h1, pp, hP, f, g, FF, GG, rf, rg), rmul(one, h1, pp, hP, e, h, EE, HH, re, rh))
155
156# ---- selection ----
157
158def sel_eq0(+one: Nat, +h1: {one == 1n : Nat}, +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +pp: Nat, +hp: Rp(pp, p, sp), +hq: Rp(pp, q, sq)) -> {PT.select(0, p, q) == p : PT.Pt}:
159  match p q sp sq:
160    case PT.Pt{+x1, +y1, +z1, +t1} PT.Pt{+x2, +y2, +z2, +t2} SE.EPt{+a1, +b1, +c1, +d1} SE.EPt{+a2, +b2, +c2, +d2}:
161      +ox1 = o(pp, x1, a1, rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp))
162      +oy1 = o(pp, y1, b1, rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp))
163      +oz1 = o(pp, z1, c1, rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp))
164      +ot1 = o(pp, t1, d1, rT(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp))
165      +ox2 = o(pp, x2, a2, rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq))
166      +oy2 = o(pp, y2, b2, rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq))
167      +oz2 = o(pp, z2, c2, rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq))
168      +ot2 = o(pp, t2, d2, rT(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq))
169      %Equal.sym(List<&2, U32>, F.select(0, x1, x2), x1, FO.select0(one, h1, 32n, x1, x2, ox1, ox2)) : {PT.Pt{_, F.select(0, y1, y2), F.select(0, z1, z2), F.select(0, t1, t2)} == PT.Pt{x1, y1, z1, t1} : PT.Pt}
170      %Equal.sym(List<&2, U32>, F.select(0, y1, y2), y1, FO.select0(one, h1, 32n, y1, y2, oy1, oy2)) : {PT.Pt{x1, _, F.select(0, z1, z2), F.select(0, t1, t2)} == PT.Pt{x1, y1, z1, t1} : PT.Pt}
171      %Equal.sym(List<&2, U32>, F.select(0, z1, z2), z1, FO.select0(one, h1, 32n, z1, z2, oz1, oz2)) : {PT.Pt{x1, y1, _, F.select(0, t1, t2)} == PT.Pt{x1, y1, z1, t1} : PT.Pt}
172      %Equal.sym(List<&2, U32>, F.select(0, t1, t2), t1, FO.select0(one, h1, 32n, t1, t2, ot1, ot2)) : {PT.Pt{x1, y1, z1, _} == PT.Pt{x1, y1, z1, t1} : PT.Pt}
173      {==}
174
175def sel_eq1(+one: Nat, +h1: {one == 1n : Nat}, +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +pp: Nat, +hp: Rp(pp, p, sp), +hq: Rp(pp, q, sq)) -> {PT.select(1, p, q) == q : PT.Pt}:
176  match p q sp sq:
177    case PT.Pt{+x1, +y1, +z1, +t1} PT.Pt{+x2, +y2, +z2, +t2} SE.EPt{+a1, +b1, +c1, +d1} SE.EPt{+a2, +b2, +c2, +d2}:
178      +ox1 = o(pp, x1, a1, rX(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp))
179      +oy1 = o(pp, y1, b1, rY(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp))
180      +oz1 = o(pp, z1, c1, rZ(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp))
181      +ot1 = o(pp, t1, d1, rT(pp, x1, y1, z1, t1, a1, b1, c1, d1, hp))
182      +ox2 = o(pp, x2, a2, rX(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq))
183      +oy2 = o(pp, y2, b2, rY(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq))
184      +oz2 = o(pp, z2, c2, rZ(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq))
185      +ot2 = o(pp, t2, d2, rT(pp, x2, y2, z2, t2, a2, b2, c2, d2, hq))
186      %Equal.sym(List<&2, U32>, F.select(1, x1, x2), x2, FO.select1(one, h1, 32n, x1, x2, ox1, ox2)) : {PT.Pt{_, F.select(1, y1, y2), F.select(1, z1, z2), F.select(1, t1, t2)} == PT.Pt{x2, y2, z2, t2} : PT.Pt}
187      %Equal.sym(List<&2, U32>, F.select(1, y1, y2), y2, FO.select1(one, h1, 32n, y1, y2, oy1, oy2)) : {PT.Pt{x2, _, F.select(1, z1, z2), F.select(1, t1, t2)} == PT.Pt{x2, y2, z2, t2} : PT.Pt}
188      %Equal.sym(List<&2, U32>, F.select(1, z1, z2), z2, FO.select1(one, h1, 32n, z1, z2, oz1, oz2)) : {PT.Pt{x2, y2, _, F.select(1, t1, t2)} == PT.Pt{x2, y2, z2, t2} : PT.Pt}
189      %Equal.sym(List<&2, U32>, F.select(1, t1, t2), t2, FO.select1(one, h1, 32n, t1, t2, ot1, ot2)) : {PT.Pt{x2, y2, z2, _} == PT.Pt{x2, y2, z2, t2} : PT.Pt}
190      {==}
191
192def sel_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +s: U32, +b: Nat, +hs: {v(s) == b : Nat}, +hb: {Nat.is_le(b, 1n) == True{} : Bool}, +p: PT.Pt, +q: PT.Pt, +sp: SE.EPt, +sq: SE.EPt, +hp: Rp(pp, p, sp), +hq: Rp(pp, q, sq)) -> Rp(pp, PT.select(s, p, q), SE.pick(b, sp, sq)):
193  match b:
194    case 0n:
195      %Equal.sym(U32, s, 0, XB.u0(s, hs)) : Rp(pp, PT.select(_, p, q), sp)
196      %Equal.sym(PT.Pt, PT.select(0, p, q), p, sel_eq0(one, h1, p, q, sp, sq, pp, hp, hq)) : Rp(pp, _, sp)
197      hp
198    case 1n:
199      %Equal.sym(U32, s, 1, XB.u1(s, hs)) : Rp(pp, PT.select(_, p, q), sq)
200      %Equal.sym(PT.Pt, PT.select(1, p, q), q, sel_eq1(one, h1, p, q, sp, sq, pp, hp, hq)) : Rp(pp, _, sq)
201      hq
202    case 2n+z:
203      Empty.absurd(Rp(pp, PT.select(s, p, q), sq), L.false_true(hb))
204
205# ---- double-and-add ----
206
207def smul_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +n: Nat, +cs: PT.Cs, +D: Nat, +rd2: RL.R(pp, PT.cs_d2(cs), FS.fadd(1n+pp, D, D)), +bs: List<&2, U32>, +hbs: {LM.lea(bs, 255n) == True{} : Bool}, +p: PT.Pt, +sp: SE.EPt, +hp: Rp(pp, p, sp), +q: PT.Pt, +sq: SE.EPt, +hq: Rp(pp, q, sq)) -> Rp(pp, PT.smul(n, cs, bs, p, q), SE.smul(1n+pp, D, n, FS.value(bs), sp, sq)):
208  match n:
209    case 0n:
210      hq
211    case 1n+ +t:
212      +q2 = PT.double(q)
213      +sq2 = SE.double(1n+pp, sq)
214      +hq2 = double_rel(one, h1, pp, hP, q, sq, hq)
215      +r = PT.add(cs, q2, p)
216      +sr = SE.add(1n+pp, D, sq2, sp)
217      +hr = add_rel(one, h1, pp, hP, cs, D, rd2, q2, p, sq2, sp, hq2, hp)
218      +hs = sel_rel(one, h1, pp, X.kbit(bs, t), SX.kbit(FS.value(bs), t), XB.kbit_val(bs, t, hbs), XB.kbit_le(bs, t, hbs), q2, r, sq2, sr, hq2, hr)
219      smul_rel(one, h1, pp, hP, t, cs, D, rd2, bs, hbs, p, sp, hp, PT.select(X.kbit(bs, t), q2, r), SE.pick(SX.kbit(FS.value(bs), t), sq2, sr), hs)