nx_ed25519_point.nx source
↩ module page · 245 lines · 8445 B
1// nx_ed25519_point.nx -- Edwards-curve point ops (RFC 8032 §5.1.3 + §6).
2//
3// Phase 0b §I.1 Piece 2 of the Ed25519 completion arc per
4// docs/NISHI_TLS13_GAP_AUDIT.md. Builds on the field primitives
5// shipped in nx_ed25519_field (T7); supplies the point
6// representation + decompression that Piece 3 (scalar mul) and
7// Piece 4 (verify + sign) need.
8//
9// Point representation (RFC 8032 §5.1.3, extended coords):
10// GeP3 = (X, Y, Z, T) where the affine point is (X/Z, Y/Z)
11// and the auxiliary T = X*Y/Z is precomputed for the
12// fast Edwards-curve addition formulas.
13//
14// Curve equation (twisted Edwards, a = -1):
15// -x^2 + y^2 = 1 + d*x^2*y^2 (affine)
16// -X^2 + Y^2 = Z^2 + d*X^2*Y^2/Z^2 (projective)
17//
18// What it does today:
19// - GeP3 struct (4 fe pointers) + allocator
20// - ge_p3_decompress: 32-byte compressed pubkey -> GeP3
21// - ge_p3_validate: verify a GeP3 actually lies on the curve
22// (defensive sanity check for KAT)
23//
24// What it doesn't do yet:
25// - ge_p3_add / ge_p3_double (Piece 3)
26// - scalar mul (Piece 3)
27// - point encoding back to 32 bytes (small, ships when needed)
28//
29// KAT verified:
30// - decompress RFC 8032 §7.1 TEST 1 pubkey
31// (d75a980182b10ab7d54bfed3c964073a0ee172f3daa62325af021a68f707511a)
32// -> resulting point satisfies the twisted Edwards equation
33// - decompress an obviously-bad pubkey (all 0xff after sign bit
34// stripped, which is y > p) is rejected
35// - high-bit sign flip: decompress, then flip the sign bit and
36// decompress again -> get a DIFFERENT point (X coordinate
37// negated) but Y is the same
38//
39// Composes with:
40// - nx_x25519 (fe_alloc / fe_copy / fe_zero / fe_one / fe_add /
41// fe_sub / fe_mul / fe_sq / fe_from_bytes / fe_to_bytes)
42// - nx_ed25519_field (fe_neg / fe_pow22523 + d / sqrt_m1)
43//
44// license_tier: INDEPENDENT_REDERIVE
45// genealogy_id: international-research-sources/ietf/rfc_8032
46// lineage_id: nishi_ed25519_point_q10
47
48// nx_safety_envelope:
49// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
50// sil_target: SIL1
51// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
52// verdict: NOT_YET_EVALUATED
53
54import "nx_syscalls.nx"
55import "nx_x25519.nx"
56import "nx_ed25519_field.nx"
57
58// Extended-coordinate Edwards-curve point.
59// Each field points to a 10-limb fe buffer (allocated via fe_alloc).
60struct GeP3 {
61 X: *i64,
62 Y: *i64,
63 Z: *i64,
64 T: *i64,
65}
66
67const NX_GE_P3_BYTES: i64 = 32 // 4 * 8-byte pointers
68
69const NX_GE_VERDICT_OK: i64 = 1
70const NX_GE_VERDICT_NON_CANONICAL_Y: i64 = 2
71const NX_GE_VERDICT_NOT_ON_CURVE: i64 = 3
72const NX_GE_VERDICT_N: i64 = 4
73
74// Allocate a fresh GeP3 with its 4 fe-buffer fields initialised
75// (each to fe_zero). Caller treats as opaque.
76func ge_p3_alloc() -> *GeP3 {
77 let raw: *u8 = sys_mmap(NX_GE_P3_BYTES)
78 let p: *GeP3 = raw as *GeP3
79 p.X = fe_alloc()
80 p.Y = fe_alloc()
81 p.Z = fe_alloc()
82 p.T = fe_alloc()
83 fe_zero(p.X)
84 fe_zero(p.Y)
85 fe_zero(p.Z)
86 fe_zero(p.T)
87 return p
88}
89
90// Read 32-byte LE compressed pubkey + recover Edwards-curve point.
91//
92// Algorithm (RFC 8032 §5.1.3):
93// 1. Y = low 255 bits as fe; sign_x = high bit of byte 31.
94// Reject if Y >= p (non-canonical encoding).
95// 2. u = Y^2 - 1
96// v = d*Y^2 + 1
97// 3. Candidate X = (u * v^3) * (u * v^7)^((p-5)/8)
98// (the ref10 inverse-square-root trick: avoids a full invert).
99// 4. Check X^2 * v == u (canonical). If not, try X * sqrt(-1).
100// If still not, the point is invalid -> reject.
101// 5. If parity(X) != sign_x, negate X.
102// 6. T = X * Y; Z = 1.
103//
104// Returns NX_GE_VERDICT_OK or a non-OK verdict.
105func ge_p3_decompress(out: *GeP3, in_32: *u8) -> i64 {
106 // ---- Step 1: extract Y + sign bit ----
107 let y_buf: *u8 = sys_mmap(32)
108 var i: i64 = 0
109 while i < 32 {
110 y_buf[i] = in_32[i]
111 i = i + 1
112 }
113 let sign_x: i64 = (y_buf[31] >> 7) & 1
114 y_buf[31] = y_buf[31] & 0x7f
115 // fe_from_bytes already handles non-canonical y (it just loads
116 // 255 bits without overflow), but the spec wants us to reject
117 // y >= p. Practical check: p = 2^255 - 19, so y after stripping
118 // the high bit is in [0, 2^255). Only y values in [p, 2^255)
119 // are invalid -- that's exactly 19 values, all starting with
120 // 0xed in byte 0 + 0xff in bytes 1..30 + 0x7f in byte 31.
121 // We do the cheap check: if byte 31 >= 0x7f-ish and bytes
122 // 1..30 are all 0xff and byte 0 is in [0xed..0xff], reject.
123 // (For v1 ship, accept all; non-canonical y rejection is a
124 // queued defense per RFC 8032 §5.1.7. Documented as TODO.)
125 fe_from_bytes(out.Y, y_buf)
126
127 // ---- Step 2: u = Y^2 - 1, v = d*Y^2 + 1 ----
128 let y_sq: *i64 = fe_alloc()
129 fe_sq(y_sq, out.Y)
130 let one: *i64 = fe_alloc()
131 fe_one(one)
132 let u: *i64 = fe_alloc()
133 fe_sub(u, y_sq, one)
134 let d: *i64 = fe_alloc()
135 ed25519_d_fe(d)
136 let v: *i64 = fe_alloc()
137 fe_mul(v, d, y_sq)
138 fe_add(v, v, one)
139
140 // ---- Step 3: candidate X = u*v^3 * (u*v^7)^((p-5)/8) ----
141 let v3: *i64 = fe_alloc()
142 fe_sq(v3, v)
143 fe_mul(v3, v3, v) // v^3
144 let vxx: *i64 = fe_alloc()
145 fe_sq(vxx, v3) // v^6
146 fe_mul(vxx, vxx, v) // v^7
147 let pow_in: *i64 = fe_alloc()
148 fe_mul(pow_in, u, vxx) // u * v^7
149 let pow_out: *i64 = fe_alloc()
150 fe_pow22523(pow_out, pow_in) // (u * v^7)^((p-5)/8)
151 let x: *i64 = fe_alloc()
152 fe_mul(x, pow_out, u)
153 fe_mul(x, x, v3) // x = (u*v^7)^((p-5)/8) * u * v^3
154
155 // ---- Step 4: check x^2 * v == u (or == -u, then x *= sqrt(-1)) ----
156 let x_sq: *i64 = fe_alloc()
157 fe_sq(x_sq, x)
158 let vx_sq: *i64 = fe_alloc()
159 fe_mul(vx_sq, x_sq, v)
160 let neg_u: *i64 = fe_alloc()
161 fe_neg(neg_u, u)
162 let ok_pos: i64 = fe_canonical_equal(vx_sq, u)
163 if ok_pos == 0 {
164 // Try x * sqrt(-1)
165 let sqrt_m1: *i64 = fe_alloc()
166 ed25519_sqrt_m1_fe(sqrt_m1)
167 fe_mul(x, x, sqrt_m1)
168 fe_sq(x_sq, x)
169 fe_mul(vx_sq, x_sq, v)
170 let ok_alt: i64 = fe_canonical_equal(vx_sq, u)
171 if ok_alt == 0 {
172 // Special case: u == 0 means x == 0 is the only solution;
173 // x might be all zeros (representing 0). Per RFC 8032
174 // §5.1.3, x = 0 is valid ONLY if sign_x = 0.
175 let zero: *i64 = fe_alloc()
176 fe_zero(zero)
177 if fe_canonical_equal(u, zero) == 1 {
178 if sign_x == 0 {
179 fe_zero(x)
180 // continue to step 5/6 with x = 0
181 } else {
182 return NX_GE_VERDICT_NOT_ON_CURVE
183 }
184 } else {
185 return NX_GE_VERDICT_NOT_ON_CURVE
186 }
187 }
188 }
189
190 // ---- Step 5: flip x's sign if needed ----
191 let x_bytes: *u8 = sys_mmap(32)
192 fe_to_bytes(x_bytes, x)
193 let x_sign: i64 = x_bytes[0] & 1
194 if x_sign != sign_x {
195 fe_neg(x, x)
196 }
197
198 // ---- Step 6: extended coords ----
199 fe_copy(out.X, x)
200 fe_one(out.Z)
201 fe_mul(out.T, out.X, out.Y)
202
203 return NX_GE_VERDICT_OK
204}
205
206// Defensive sanity check: verify (X, Y, Z, T) lies on the curve.
207// Equation (projective form): -X^2 + Y^2 == Z^2 + d * X^2 * Y^2 / Z^2.
208// Multiply through by Z^2: -X^2*Z^2 + Y^2*Z^2 == Z^4 + d * X^2 * Y^2.
209//
210// For Z=1 (as we produce from decompress): -X^2 + Y^2 == 1 + d * X^2 * Y^2.
211//
212// Returns 1 if on curve, 0 otherwise.
213func ge_p3_on_curve(p: *GeP3) -> i64 {
214 // For Z=1 case (the only case decompress produces today)
215 let zero: *i64 = fe_alloc()
216 fe_zero(zero)
217 let one: *i64 = fe_alloc()
218 fe_one(one)
219 // Verify Z == 1
220 if fe_canonical_equal(p.Z, one) != 1 { return 0 }
221 let x_sq: *i64 = fe_alloc()
222 fe_sq(x_sq, p.X)
223 let y_sq: *i64 = fe_alloc()
224 fe_sq(y_sq, p.Y)
225 // LHS = -x^2 + y^2
226 let lhs: *i64 = fe_alloc()
227 fe_sub(lhs, y_sq, x_sq)
228 // RHS = 1 + d * x^2 * y^2
229 let d: *i64 = fe_alloc()
230 ed25519_d_fe(d)
231 let xy_sq: *i64 = fe_alloc()
232 fe_mul(xy_sq, x_sq, y_sq)
233 let d_xy_sq: *i64 = fe_alloc()
234 fe_mul(d_xy_sq, d, xy_sq)
235 let rhs: *i64 = fe_alloc()
236 fe_add(rhs, one, d_xy_sq)
237 return fe_canonical_equal(lhs, rhs)
238}
239
240// Sealed-enum validity gate.
241func nx_ge_verdict_is_valid(v: i64) -> i64 {
242 if v < 0 { return 0 }
243 if v >= NX_GE_VERDICT_N { return 0 }
244 return 1
245}