1	import Base
2	import ../curve25519/field.bend as F
3	import ../curve25519/x25519.bend as X
4	
5	# edwards25519 points (RFC 8032 section 5.1): -x^2 + y^2 = 1 + d x^2 y^2
6	# over GF(2^255 - 19), in extended homogeneous coordinates (X : Y : Z : T),
7	# x = X / Z, y = Y / Z, x y = T / Z. Addition and doubling are the RFC's
8	# formulas (section 5.1.4), encoding and decoding sections 5.1.2 and 5.1.3.
9	# The curve constants are computed once from small integers by the proved
10	# field operations and passed along (Cs).
11	
12	type Pt is Data:
13	  Pt{x: List<&2, U32>, y: List<&2, U32>, z: List<&2, U32>, t: List<&2, U32>}
14	
15	# d = -121665 / 121666, 2 d, sqrt(-1) = 2^((p - 1) / 4)
16	type Cs is Data:
17	  Cs{d: List<&2, U32>, d2: List<&2, U32>, sqm1: List<&2, U32>}
18	
19	def c121665() -> List<&2, U32>:
20	  [65, 219, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
21	   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
22	
23	def c121666() -> List<&2, U32>:
24	  [66, 219, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
25	   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
26	
27	# 2^((p - 1) / 4), (p - 1) / 4 = 2^253 - 5: 250 one bits, then 0 1 1
28	def pow_p14(+x: List<&2, U32>) -> List<&2, U32>:
29	  F.pow_bits(x, [False{}, True{}, True{}], F.pow_ones(x, 249n, x))
30	
31	def cs_d(c: Cs) -> List<&2, U32>:
32	  match c:
33	    case Cs{d, d2, s}:
34	      d
35	
36	def cs_d2(c: Cs) -> List<&2, U32>:
37	  match c:
38	    case Cs{d, d2, s}:
39	      d2
40	
41	def cs_s(c: Cs) -> List<&2, U32>:
42	  match c:
43	    case Cs{d, d2, s}:
44	      s
45	
46	# k itself; taking an input list xs keeps the proof checker from computing
47	# with the constant k while xs is unknown (it would otherwise evaluate the
48	# whole field arithmetic on constants whenever it compares two terms)
49	def lit(xs: List<&2, U32>, k: List<&2, U32>) -> List<&2, U32>:
50	  match xs:
51	    case Nil{}:
52	      k
53	    case Con{h, t}:
54	      k
55	
56	def cs_of(+d: List<&2, U32>, +xs: List<&2, U32>) -> Cs:
57	  Cs{d, F.add(d, d), pow_p14(lit(xs, F.small(2)))}
58	
59	# the curve constants, computed (xs is any input, see lit)
60	def consts(+xs: List<&2, U32>) -> Cs:
61	  cs_of(F.mul(F.neg(lit(xs, c121665())), F.inv(lit(xs, c121666()))), xs)
62	
63	def identity() -> Pt:
64	  Pt{F.zero(), F.one(), F.one(), F.zero()}
65	
66	# RFC 8032 5.1.4, addition
67	def add(+c: Cs, p: Pt, q: Pt) -> Pt:
68	  match p q:
69	    case Pt{+x1, +y1, +z1, +t1} Pt{+x2, +y2, +z2, +t2}:
70	      +a = F.mul(F.sub(y1, x1), F.sub(y2, x2))
71	      +b = F.mul(F.add(y1, x1), F.add(y2, x2))
72	      +cc = F.mul(F.mul(t1, cs_d2(c)), t2)
73	      +dd = F.mul(F.add(z1, z1), z2)
74	      +e = F.sub(b, a)
75	      +f = F.sub(dd, cc)
76	      +g = F.add(dd, cc)
77	      +h = F.add(b, a)
78	      Pt{F.mul(e, f), F.mul(g, h), F.mul(f, g), F.mul(e, h)}
79	
80	# RFC 8032 5.1.4, doubling
81	def double(p: Pt) -> Pt:
82	  match p:
83	    case Pt{+x1, +y1, +z1, t1}:
84	      +a = F.sq(x1)
85	      +b = F.sq(y1)
86	      +zz = F.sq(z1)
87	      +cc = F.add(zz, zz)
88	      +h = F.add(a, b)
89	      +e = F.sub(h, F.sq(F.add(x1, y1)))
90	      +g = F.sub(a, b)
91	      +f = F.add(cc, g)
92	      Pt{F.mul(e, f), F.mul(g, h), F.mul(f, g), F.mul(e, h)}
93	
94	# s == 0: p; s == 1: q
95	def select(+s: U32, p: Pt, q: Pt) -> Pt:
96	  match p q:
97	    case Pt{x1, y1, z1, t1} Pt{x2, y2, z2, t2}:
98	      Pt{F.select(s, x1, x2), F.select(s, y1, y2), F.select(s, z1, z2), F.select(s, t1, t2)}
99	
100	# [bits t = n - 1 .. 0 of bs] p added to 2^n q: double, add, select
101	def smul(n: Nat, +c: Cs, +bs: List<&2, U32>, +p: Pt, q: Pt) -> Pt:
102	  match n:
103	    case 0n:
104	      q
105	    case 1n+ +t:
106	      +q2 = double(q)
107	      smul(t, c, bs, p, select(X.kbit(bs, t), q2, add(c, q2, p)))
108	
109	# [k] p for a byte-string scalar k
110	def mul(+c: Cs, +k: List<&2, U32>, +p: Pt) -> Pt:
111	  smul(X.bitlen(k), c, k, p, identity())
112	
113	# the last byte with bit 7 set to b (the canonical y has it clear)
114	def set_top(xs: List<&2, U32>, +b: U32) -> List<&2, U32>:
115	  match xs:
116	    case Nil{}:
117	      Nil{}
118	    case Con{x, xt}:
119	      match xt:
120	        case Nil{}:
121	          Con{U32.or(x, U32.shln(b, 7n)), Nil{}}
122	        case Con{y, yt}:
123	          Con{x, set_top(Con{y, yt}, b)}
124	
125	# RFC 8032 5.1.2
126	def encode(p: Pt) -> List<&2, U32>:
127	  match p:
128	    case Pt{+x, +y, +z, t}:
129	      +zi = F.inv(z)
130	      set_top(F.to_bytes(F.mul(y, zi)), F.parity(F.mul(x, zi)))
131	
132	# y >= p: the carry of y + 2^256 - p is not 0
133	def ge_p(+y: List<&2, U32>) -> Bool:
134	  Bool.not(U32.is_eq(F.cr_out(F.carry(F.addl(y, F.comp_p()), 0)), 0))
135	
136	def dec_fin(+x: List<&2, U32>, +y: List<&2, U32>, +x0: U32, fail: Bool) -> Maybe<&2, Pt>:
137	  match fail:
138	    case True{}:
139	      None{}
140	    case False{}:
141	      +x2 = F.select(U32.xor(F.parity(x), x0), x, F.neg(x))
142	      Some{Pt{x2, y, F.one(), F.mul(x2, y)}}
143	
144	def dec_root(+c: Cs, +x: List<&2, U32>, +y: List<&2, U32>, +x0: U32, +u: List<&2, U32>, +vxx: List<&2, U32>, is_u: Bool, is_nu: Bool) -> Maybe<&2, Pt>:
145	  match is_u:
146	    case True{}:
147	      dec_fin(x, y, x0, Bool.and(F.is_zero(x), U32.is_eq(x0, 1)))
148	    case False{}:
149	      match is_nu:
150	        case True{}:
151	          +x1 = F.mul(x, cs_s(c))
152	          dec_fin(x1, y, x0, Bool.and(F.is_zero(x1), U32.is_eq(x0, 1)))
153	        case False{}:
154	          None{}
155	
156	def dec_y(+c: Cs, +y: List<&2, U32>, +x0: U32, bad: Bool) -> Maybe<&2, Pt>:
157	  match bad:
158	    case True{}:
159	      None{}
160	    case False{}:
161	      +yy = F.sq(y)
162	      +u = F.sub(yy, F.one())
163	      +v = F.add(F.mul(cs_d(c), yy), F.one())
164	      +v3 = F.mul(F.sq(v), v)
165	      +v7 = F.mul(F.sq(v3), v)
166	      +x = F.mul(F.mul(u, v3), F.pow_p58(F.mul(u, v7)))
167	      +vxx = F.mul(v, F.sq(x))
168	      dec_root(c, x, y, x0, u, vxx, F.eq(vxx, u), F.eq(vxx, F.neg(u)))
169	
170	# RFC 8032 5.1.3 on 32 bytes below 256
171	def decode(+c: Cs, +bs: List<&2, U32>) -> Maybe<&2, Pt>:
172	  +y = F.of_bytes(bs)
173	  dec_y(c, y, X.kbit(bs, 255n), ge_p(y))
174	
175	# the same point: X1 Z2 == X2 Z1 and Y1 Z2 == Y2 Z1
176	def equal(p: Pt, q: Pt) -> Bool:
177	  match p q:
178	    case Pt{+x1, +y1, +z1, t1} Pt{+x2, +y2, +z2, t2}:
179	      Bool.and(F.eq(F.mul(x1, z2), F.mul(x2, z1)), F.eq(F.mul(y1, z2), F.mul(y2, z1)))
180	
181	# the base point: y = 4 / 5, x even
182	def base_of(m: Maybe<&2, Pt>) -> Pt:
183	  match m:
184	    case None{}:
185	      identity()
186	    case Some{p}:
187	      p
188	
189	def base(+c: Cs, +xs: List<&2, U32>) -> Pt:
190	  base_of(decode(c, F.to_bytes(F.mul(lit(xs, F.small(4)), F.inv(lit(xs, F.small(5)))))))