nx_ed25519_arith.nx source
↩ module page · 235 lines · 7369 B
1// nx_ed25519_arith.nx -- Edwards-curve point arithmetic (RFC 8032).
2//
3// Phase 0b §I.1.C-1 of the Ed25519 completion arc per
4// docs/NISHI_TLS13_GAP_AUDIT.md. Builds on the field primitives
5// (T7) and point decompression (T8) with the arithmetic that
6// scalar multiplication needs: point doubling, point addition,
7// point negation, identity, and the compressed-form encoder used
8// for equality testing + the public-key wire format.
9//
10// Formulas: Bernstein + Lange "Twisted Edwards Curves Revisited"
11// (Asiacrypt 2008), extended coordinates, a = -1. These are
12// the dbl-2008-hwcd-3 doubling and add-2008-hwcd-3 addition
13// from the Explicit-Formulas Database (EFD), which are the
14// standard reference choices for Ed25519.
15//
16// What it does today:
17// - ge_p3_identity: returns the curve identity (0, 1, 1, 0)
18// - ge_p3_negate: in-place negate (X' = -X, T' = -T)
19// - ge_p3_double: 4M + 4S; consumes only X1, Y1, Z1 (T1 unused)
20// - ge_p3_add: 9M; general extended-coord addition
21// - ge_p3_compress: normalize Z to 1 via fe_invert, encode Y +
22// sign-of-X bit into 32 LE bytes
23// - ge_p3_equal: compare two GeP3 by their compressed encodings
24//
25// What it doesn't do yet:
26// - scalar multiplication (Piece 3b uses double + add to build it)
27// - sc_reduce mod L (Piece 3c; 21-bit limb scalar reduction)
28// - ge_p3_madd (mixed addition with precomputed-form points;
29// a perf optimization, not a correctness requirement)
30//
31// KAT verified:
32// - identity point passes on-curve check
33// - basepoint doubled satisfies the curve equation
34// - basepoint + basepoint == double(basepoint) (verified by
35// compressing both and comparing bytes)
36// - P + (-P) compresses to the identity encoding (32 zero bytes
37// except byte 0 = 0x01; the canonical encoding of y=1, x=0)
38// - encode(decompress(B_compressed)) == B_compressed (round-trip)
39//
40// Composes with:
41// - nx_x25519 (fe_* + fe_invert for compress)
42// - nx_ed25519_field (fe_neg + ED25519_D for arithmetic)
43// - nx_ed25519_point (GeP3 struct + on-curve check)
44//
45// license_tier: INDEPENDENT_REDERIVE
46// genealogy_id: international-research-sources/ietf/rfc_8032
47// lineage_id: nishi_ed25519_arith_q10
48
49// nx_safety_envelope:
50// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
51// sil_target: SIL1
52// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
53// verdict: NOT_YET_EVALUATED
54
55import "nx_syscalls.nx"
56import "nx_x25519.nx"
57import "nx_ed25519_field.nx"
58import "nx_ed25519_point.nx"
59
60// Curve identity in extended coords: (0, 1, 1, 0).
61func ge_p3_identity(out: *GeP3) -> i64 {
62 fe_zero(out.X)
63 fe_one(out.Y)
64 fe_one(out.Z)
65 fe_zero(out.T)
66 return 0
67}
68
69// Negate in place: -P = (-X, Y, Z, -T).
70// (The y coordinate is invariant under point negation on Edwards
71// curves; only the x coordinate flips sign. T = X*Y/Z flips with X.)
72func ge_p3_negate(out: *GeP3, p: *GeP3) -> i64 {
73 fe_neg(out.X, p.X)
74 fe_copy(out.Y, p.Y)
75 fe_copy(out.Z, p.Z)
76 fe_neg(out.T, p.T)
77 return 0
78}
79
80// Doubling: 2P = (X3, Y3, Z3, T3).
81// dbl-2008-hwcd-3 formulas (a = -1):
82// A = X1^2
83// B = Y1^2
84// C = 2*Z1^2
85// D = -A
86// E = (X1+Y1)^2 - A - B
87// G = D + B
88// F = G - C
89// H = D - B
90// X3 = E * F
91// Y3 = G * H
92// T3 = E * H
93// Z3 = F * G
94// Cost: 4M + 4S + 6 adds + 1 neg.
95func ge_p3_double(out: *GeP3, p: *GeP3) -> i64 {
96 let A: *i64 = fe_alloc()
97 let B: *i64 = fe_alloc()
98 let C: *i64 = fe_alloc()
99 let D: *i64 = fe_alloc()
100 let E: *i64 = fe_alloc()
101 let G: *i64 = fe_alloc()
102 let F: *i64 = fe_alloc()
103 let H: *i64 = fe_alloc()
104 let tmp_xy: *i64 = fe_alloc()
105 fe_sq(A, p.X)
106 fe_sq(B, p.Y)
107 fe_sq(C, p.Z)
108 fe_add(C, C, C) // C = 2*Z^2
109 fe_neg(D, A) // D = -A
110 fe_add(tmp_xy, p.X, p.Y)
111 fe_sq(E, tmp_xy) // E = (X+Y)^2
112 fe_sub(E, E, A) // E -= A
113 fe_sub(E, E, B) // E -= B
114 fe_add(G, D, B)
115 fe_sub(F, G, C)
116 fe_sub(H, D, B)
117 fe_mul(out.X, E, F)
118 fe_mul(out.Y, G, H)
119 fe_mul(out.T, E, H)
120 fe_mul(out.Z, F, G)
121 return 0
122}
123
124// Addition: P1 + P2 = (X3, Y3, Z3, T3).
125// add-2008-hwcd-3 formulas (a = -1):
126// A = (Y1 - X1) * (Y2 - X2)
127// B = (Y1 + X1) * (Y2 + X2)
128// C = T1 * 2*d * T2
129// D = Z1 * 2 * Z2
130// E = B - A
131// F = D - C
132// G = D + C
133// H = B + A
134// X3 = E * F
135// Y3 = G * H
136// T3 = E * H
137// Z3 = F * G
138// Cost: 9M + 7 adds + 1 mul-by-2d (precomputed).
139func ge_p3_add(out: *GeP3, p1: *GeP3, p2: *GeP3) -> i64 {
140 let A: *i64 = fe_alloc()
141 let B: *i64 = fe_alloc()
142 let C: *i64 = fe_alloc()
143 let D: *i64 = fe_alloc()
144 let E: *i64 = fe_alloc()
145 let F: *i64 = fe_alloc()
146 let G: *i64 = fe_alloc()
147 let H: *i64 = fe_alloc()
148 let yx1: *i64 = fe_alloc()
149 let yx2: *i64 = fe_alloc()
150 let yp1: *i64 = fe_alloc()
151 let yp2: *i64 = fe_alloc()
152 let two_d: *i64 = fe_alloc()
153 let tt: *i64 = fe_alloc()
154 let zz: *i64 = fe_alloc()
155
156 // A = (Y1 - X1) * (Y2 - X2)
157 fe_sub(yx1, p1.Y, p1.X)
158 fe_sub(yx2, p2.Y, p2.X)
159 fe_mul(A, yx1, yx2)
160
161 // B = (Y1 + X1) * (Y2 + X2)
162 fe_add(yp1, p1.Y, p1.X)
163 fe_add(yp2, p2.Y, p2.X)
164 fe_mul(B, yp1, yp2)
165
166 // C = T1 * 2*d * T2 (compute as ((T1 * T2) * (2*d)))
167 ed25519_d_fe(two_d)
168 fe_add(two_d, two_d, two_d) // 2*d
169 fe_mul(tt, p1.T, p2.T)
170 fe_mul(C, tt, two_d)
171
172 // D = Z1 * 2 * Z2
173 fe_mul(zz, p1.Z, p2.Z)
174 fe_add(D, zz, zz)
175
176 fe_sub(E, B, A)
177 fe_sub(F, D, C)
178 fe_add(G, D, C)
179 fe_add(H, B, A)
180
181 fe_mul(out.X, E, F)
182 fe_mul(out.Y, G, H)
183 fe_mul(out.T, E, H)
184 fe_mul(out.Z, F, G)
185 return 0
186}
187
188// Constant-time conditional move of a whole extended point: dst = (flag==1) ? src : dst.
189// Branchless (mirrors fe_cmov over all four coordinates) -- the constant-time scalar multiply
190// uses this to select the "add" result without a data-dependent branch on the secret bit.
191func ge_p3_cmov(dst: *GeP3, src: *GeP3, flag: i64) -> i64 {
192 fe_cmov(dst.X, src.X, flag)
193 fe_cmov(dst.Y, src.Y, flag)
194 fe_cmov(dst.Z, src.Z, flag)
195 fe_cmov(dst.T, src.T, flag)
196 return 0
197}
198
199// Compressed encoding: encode point as 32 LE bytes.
200// Algorithm:
201// 1. zi = Z^-1 (single fe_invert)
202// 2. x = X * zi; y = Y * zi
203// 3. Encode y as 32 LE bytes; set high bit of byte 31 = parity(x)
204func ge_p3_compress(out_32: *u8, p: *GeP3) -> i64 {
205 let zi: *i64 = fe_alloc()
206 fe_invert(zi, p.Z)
207 let x_aff: *i64 = fe_alloc()
208 let y_aff: *i64 = fe_alloc()
209 fe_mul(x_aff, p.X, zi)
210 fe_mul(y_aff, p.Y, zi)
211 // Encode Y
212 fe_to_bytes(out_32, y_aff)
213 // Extract sign of x from canonical encoding
214 let x_bytes: *u8 = sys_mmap(32)
215 fe_to_bytes(x_bytes, x_aff)
216 let sign: i64 = x_bytes[0] & 1
217 // Set high bit of byte 31
218 out_32[31] = (out_32[31] & 0x7f) | ((sign & 1) << 7)
219 return 0
220}
221
222// Equality via compressed encoding. Returns 1 if equal, 0 otherwise.
223// Not constant-time; suitable for KAT.
224func ge_p3_equal(p1: *GeP3, p2: *GeP3) -> i64 {
225 let c1: *u8 = sys_mmap(32)
226 let c2: *u8 = sys_mmap(32)
227 ge_p3_compress(c1, p1)
228 ge_p3_compress(c2, p2)
229 var i: i64 = 0
230 while i < 32 {
231 if (c1[i] & 0xff) != (c2[i] & 0xff) { return 0 }
232 i = i + 1
233 }
234 return 1
235}