nx_ed25519_field.nx source
↩ module page · 199 lines · 7877 B
1// nx_ed25519_field.nx -- Ed25519-specific extensions to the shared
2// GF(2^255 - 19) field math already in nx_x25519.
3//
4// Phase 0b §I.1 Piece 1 of the Ed25519 completion arc per
5// docs/NISHI_TLS13_GAP_AUDIT.md. X25519 and Ed25519 share the
6// same prime field (Curve25519 is the Montgomery form; Ed25519
7// uses the birationally equivalent twisted Edwards form), so the
8// fe_add / fe_sub / fe_mul / fe_sq / fe_invert / fe_from_bytes /
9// fe_to_bytes operations already in nx_x25519 transfer directly.
10// This module adds the bits Ed25519 needs that X25519 doesn't:
11//
12// - fe_neg : h = -f mod p (used in point ops + sign handling)
13// - fe_pow22523: z^((p-5)/8) (used in sqrt + decompression)
14// - ED25519_D : the twisted-Edwards curve parameter d
15// - ED25519_SQRT_M1 : the field element with x^2 = -1 (used in
16// point decompression to pick the right square root)
17//
18// Subsequent pieces:
19// - Piece 2 SHIPPED T8: nx_ed25519_point.nx with GeP3 +
20// decompress + on-curve check. Add + double + scalar_mul
21// queued for Piece 3.
22// - Piece 3: ge_p3_add + ge_p3_double + sc_reduce mod L +
23// scalar mul primitives.
24// - Piece 4: nx_ed25519.nx's ed25519_verify replaces its
25// ERR_PENDING stub with real wiring + ed25519_sign + RFC
26// 8032 §7.1 KATs.
27//
28// What it does today:
29// - fe_neg / fe_pow22523 / ED25519_D / ED25519_SQRT_M1
30// - sealed verdict + validity gate for the small ed25519 verdict
31// namespace that piece 3 will populate
32//
33// What it doesn't do yet:
34// - sqrt extraction (composes pow22523 + sqrt_m1; ships Piece 2)
35// - any point operations
36//
37// KAT verified:
38// - fe_neg(fe_one) + fe_one == fe_zero (round-trip)
39// - fe_pow22523(fe_one) == fe_one (1^anything = 1)
40// - ED25519_SQRT_M1^2 == fe_neg(fe_one) (the defining property)
41// - ED25519_D byte-exact against RFC 8032 §6 (d = -121665/121666
42// mod p, encoded LE)
43//
44// Composes with:
45// - nx_x25519 (shared fe_* operations on GF(2^255 - 19))
46// - future nx_ed25519_point (consumes these primitives)
47//
48// license_tier: INDEPENDENT_REDERIVE
49// genealogy_id: international-research-sources/ietf/rfc_8032
50// lineage_id: nishi_ed25519_field_primitives_q10
51
52// nx_safety_envelope:
53// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
54// sil_target: SIL1
55// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
56// verdict: NOT_YET_EVALUATED
57
58import "nx_syscalls.nx"
59import "nx_x25519.nx"
60
61const NX_ED25519_FE_LIMBS: i64 = 10
62const NX_ED25519_FE_BYTES: i64 = 32
63const NX_ED25519_VERDICT_OK: i64 = 1
64const NX_ED25519_VERDICT_BAD: i64 = 2
65const NX_ED25519_VERDICT_N: i64 = 3
66
67// fe_neg: h = -f mod p. Computed as 0 - f via fe_sub.
68//
69// Side-effect: caller can pass the same buffer for h and f
70// (in-place negate) -- fe_sub already supports aliasing.
71func fe_neg(h: *i64, f: *i64) -> i64 {
72 let zero: *i64 = fe_alloc()
73 fe_zero(zero)
74 fe_sub(h, zero, f)
75 return 0
76}
77
78// fe_pow22523: out = z^((p-5)/8) mod p.
79//
80// Algorithm: addition chain from RFC 8032 sample code (ref10).
81// (p-5)/8 = 2^252 - 3, computed via 250 squarings + 11 muls.
82// The bit pattern is bits set at positions 0, 2..251 of a
83// 252-bit number. Used to compute the square root via
84// sqrt(z) = z^((p+3)/8) = z * z^((p-5)/8) (when z is a QR).
85func fe_pow22523(out: *i64, z: *i64) -> i64 {
86 let t0: *i64 = fe_alloc()
87 let t1: *i64 = fe_alloc()
88 let t2: *i64 = fe_alloc()
89 var i: i64 = 0
90
91 fe_sq(t0, z) // z^2
92 fe_sq(t1, t0); fe_sq(t1, t1) // z^8
93 fe_mul(t1, z, t1) // z^9
94 fe_mul(t0, t0, t1) // z^11
95 fe_sq(t0, t0) // z^22
96 fe_mul(t0, t1, t0) // z^(2^5 - 1)
97 fe_sq(t1, t0)
98 i = 1; while i < 5 { fe_sq(t1, t1); i = i + 1 }
99 fe_mul(t0, t1, t0) // z^(2^10 - 1)
100 fe_sq(t1, t0)
101 i = 1; while i < 10 { fe_sq(t1, t1); i = i + 1 }
102 fe_mul(t1, t1, t0) // z^(2^20 - 1)
103 fe_sq(t2, t1)
104 i = 1; while i < 20 { fe_sq(t2, t2); i = i + 1 }
105 fe_mul(t1, t2, t1) // z^(2^40 - 1)
106 fe_sq(t1, t1)
107 i = 1; while i < 10 { fe_sq(t1, t1); i = i + 1 }
108 fe_mul(t0, t1, t0) // z^(2^50 - 1)
109 fe_sq(t1, t0)
110 i = 1; while i < 50 { fe_sq(t1, t1); i = i + 1 }
111 fe_mul(t1, t1, t0) // z^(2^100 - 1)
112 fe_sq(t2, t1)
113 i = 1; while i < 100 { fe_sq(t2, t2); i = i + 1 }
114 fe_mul(t1, t2, t1) // z^(2^200 - 1)
115 fe_sq(t1, t1)
116 i = 1; while i < 50 { fe_sq(t1, t1); i = i + 1 }
117 fe_mul(t0, t1, t0) // z^(2^250 - 1)
118 fe_sq(t0, t0); fe_sq(t0, t0)
119 fe_mul(out, t0, z) // z^(2^252 - 3)
120 return 0
121}
122
123// Fill out_32 with the ED25519_D constant (twisted Edwards curve
124// parameter d = -121665/121666 mod p), encoded little-endian.
125//
126// Bytes from RFC 8032 §5.1.5 (also computable as:
127// d = (121665 * mod_inverse(121666, p) * (p-1)) mod p
128// but we ship the canonical bytes to avoid a 32x32 modular invert
129// at startup).
130func ed25519_d_bytes(out_32: *u8) -> i64 {
131 out_32[0]=0xa3; out_32[1]=0x78; out_32[2]=0x59; out_32[3]=0x13
132 out_32[4]=0xca; out_32[5]=0x4d; out_32[6]=0xeb; out_32[7]=0x75
133 out_32[8]=0xab; out_32[9]=0xd8; out_32[10]=0x41; out_32[11]=0x41
134 out_32[12]=0x4d; out_32[13]=0x0a; out_32[14]=0x70; out_32[15]=0x00
135 out_32[16]=0x98; out_32[17]=0xe8; out_32[18]=0x79; out_32[19]=0x77
136 out_32[20]=0x79; out_32[21]=0x40; out_32[22]=0xc7; out_32[23]=0x8c
137 out_32[24]=0x73; out_32[25]=0xfe; out_32[26]=0x6f; out_32[27]=0x2b
138 out_32[28]=0xee; out_32[29]=0x6c; out_32[30]=0x03; out_32[31]=0x52
139 return 0
140}
141
142// Fill out_fe with ED25519_D loaded as a field-element.
143func ed25519_d_fe(out_fe: *i64) -> i64 {
144 let buf: *u8 = sys_mmap(32)
145 ed25519_d_bytes(buf)
146 fe_from_bytes(out_fe, buf)
147 return 0
148}
149
150// Fill out_32 with the ED25519_SQRT_M1 constant. This is the
151// element x of GF(p) with x^2 = -1 (i.e., a fourth root of unity).
152// Used in point decompression: when computing sqrt of (u/v), if
153// the result^2 doesn't match the expected value, multiply by
154// sqrt(-1) to get the other square root.
155//
156// Value: 2^((p-1)/4) mod p
157// = 19681161376707505956807423776089029443267218263132243024304083894137823641007
158// Bytes LE:
159func ed25519_sqrt_m1_bytes(out_32: *u8) -> i64 {
160 out_32[0]=0xb0; out_32[1]=0xa0; out_32[2]=0x0e; out_32[3]=0x4a
161 out_32[4]=0x27; out_32[5]=0x1b; out_32[6]=0xee; out_32[7]=0xc4
162 out_32[8]=0x78; out_32[9]=0xe4; out_32[10]=0x2f; out_32[11]=0xad
163 out_32[12]=0x06; out_32[13]=0x18; out_32[14]=0x43; out_32[15]=0x2f
164 out_32[16]=0xa7; out_32[17]=0xd7; out_32[18]=0xfb; out_32[19]=0x3d
165 out_32[20]=0x99; out_32[21]=0x00; out_32[22]=0x4d; out_32[23]=0x2b
166 out_32[24]=0x0b; out_32[25]=0xdf; out_32[26]=0xc1; out_32[27]=0x4f
167 out_32[28]=0x80; out_32[29]=0x24; out_32[30]=0x83; out_32[31]=0x2b
168 return 0
169}
170
171func ed25519_sqrt_m1_fe(out_fe: *i64) -> i64 {
172 let buf: *u8 = sys_mmap(32)
173 ed25519_sqrt_m1_bytes(buf)
174 fe_from_bytes(out_fe, buf)
175 return 0
176}
177
178// Compare two field elements for equality after canonical encoding.
179// Returns 1 if equal, 0 if not. Caller uses for KAT validation;
180// production point-eq comparison should ride a constant-time path
181// from nx_ct (not the byte-by-byte loop here).
182func fe_canonical_equal(a: *i64, b: *i64) -> i64 {
183 let ab: *u8 = sys_mmap(32)
184 let bb: *u8 = sys_mmap(32)
185 fe_to_bytes(ab, a)
186 fe_to_bytes(bb, b)
187 var i: i64 = 0
188 while i < 32 {
189 if (ab[i] & 0xff) != (bb[i] & 0xff) { return 0 }
190 i = i + 1
191 }
192 return 1
193}
194
195func nx_ed25519_verdict_is_valid(v: i64) -> i64 {
196 if v < 0 { return 0 }
197 if v >= NX_ED25519_VERDICT_N { return 0 }
198 return 1
199}