nx_p256_modn.nx source
↩ module page · 385 lines · 12425 B
1// nx_p256_modn.nx -- arithmetic in Z/nZ where n is the NIST P-256
2// group order (the order of the base point G).
3//
4// Phase 0b §I.3 piece 3 of the ECDSA-P256 arc:
5// ✓ 2c. p256_scalar_mul (k * P) (THIS commit's predecessor)
6// ✓ 3. p256_modn arithmetic (THIS commit)
7// - 4. ecdsa_p256 verify (queued, FINAL)
8//
9// Naming distinction from existing shipped primitives:
10// - p256_field_* = arithmetic in F_p (the COORDINATE field)
11// - p256_scalar_mul = scalar-times-point operation (k * P)
12// - p256_modn_* = arithmetic in Z/nZ (the SCALAR field)
13//
14// ECDSA verify uses Z/nZ arithmetic for:
15// - reducing the message hash e mod n
16// - computing s^(-1) mod n (Fermat: s^(n-2))
17// - u1 = e * s_inv mod n
18// - u2 = r * s_inv mod n
19// - final equality check x_R mod n == r
20//
21// n (FIPS 186-5 §D.2.4):
22// n = 0xFFFFFFFF 00000000 FFFFFFFF FFFFFFFF
23// BCE6FAAD A7179E84 F3B9CAC2 FC632551
24// LE limb layout:
25// limb[0] = 0xFC632551 limb[4] = 0xFFFFFFFF
26// limb[1] = 0xF3B9CAC2 limb[5] = 0xFFFFFFFF
27// limb[2] = 0xA7179E84 limb[6] = 0x00000000
28// limb[3] = 0xBCE6FAAD limb[7] = 0xFFFFFFFF
29//
30// Public API:
31// p256_modn_load_n(out)
32// p256_modn_load_n_minus_2(out)
33// p256_modn_zero / one / copy / eq
34// p256_modn_add(r, a, b) -- (a + b) mod n
35// p256_modn_sub(r, a, b) -- (a - b) mod n
36// p256_modn_neg(r, a)
37// p256_modn_mul(r, a, b) -- (a * b) mod n
38// p256_modn_sq(r, a)
39// p256_modn_inv(out, a) -- Fermat a^(n-2) mod n
40// p256_modn_reduce(r, a) -- a in [0, 2^256) -> a mod n
41//
42// Aliasing: all functions accept out aliasing either input.
43//
44// What this file does NOT do (already shipped or queued):
45// - Scalar-times-point (shipped: nx_p256_scalar_mul.nx)
46// - ECDSA verify orchestration (queued: nx_ecdsa_p256.nx)
47//
48// Per Cardinals 9 (single-responsibility -- one modulus per
49// primitive), 22 (composition over a per-modulus configuration
50// flag), and 23 (preamble explains naming distinction).
51//
52// license_tier: INDEPENDENT_REDERIVE
53// genealogy_id: international-research-sources/nist/fips_186_5 + sec_g/sec1_v2
54// lineage_id: nishi_p256_modn_q10
55
56// nx_safety_envelope:
57// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
58// sil_target: SIL1
59// evidence: [bulk_applied_2026-05-19, p256-modn-scalar-arith]
60// verdict: NOT_YET_EVALUATED
61
62import "nx_syscalls.nx"
63import "nx_u256.nx"
64import "nx_u256_mul.nx"
65
66// Write n into out (8 limbs, LE order).
67func p256_modn_load_n(out: *i64) -> i64 {
68 out[0] = 0xFC632551
69 out[1] = 0xF3B9CAC2
70 out[2] = 0xA7179E84
71 out[3] = 0xBCE6FAAD
72 out[4] = 0xFFFFFFFF
73 out[5] = 0xFFFFFFFF
74 out[6] = 0
75 out[7] = 0xFFFFFFFF
76 return 0
77}
78
79// Write n-2 into out. Differs only in LSB limb.
80func p256_modn_load_n_minus_2(out: *i64) -> i64 {
81 out[0] = 0xFC63254F
82 out[1] = 0xF3B9CAC2
83 out[2] = 0xA7179E84
84 out[3] = 0xBCE6FAAD
85 out[4] = 0xFFFFFFFF
86 out[5] = 0xFFFFFFFF
87 out[6] = 0
88 out[7] = 0xFFFFFFFF
89 return 0
90}
91
92// --- Montgomery reduction constants for mod n (R = 2^256) ---
93// NPRIME0 = -n^-1 mod 2^32 ; R2 = 2^512 mod n. Computed + verified in
94// Python (montmul == a*b*R^-1 mod n and Fermat inverse correct over 200
95// random cases each). Used by p256_modn_mul_mont / the fast inverse.
96const NX_P256_MODN_NPRIME0: i64 = 0xEE00BC4F
97
98func p256_modn_load_R2(out: *i64) -> i64 {
99 out[0] = 0xBE79EEA2
100 out[1] = 0x83244C95
101 out[2] = 0x49BD6FA6
102 out[3] = 0x4699799C
103 out[4] = 0x2B6BEC59
104 out[5] = 0x2845B239
105 out[6] = 0xF3D95620
106 out[7] = 0x66E12D94
107 return 0
108}
109
110func p256_modn_zero(out: *i64) -> i64 { return u256_zero(out) }
111func p256_modn_one(out: *i64) -> i64 { return u256_one(out) }
112func p256_modn_copy(out: *i64, src: *i64) -> i64 { return u256_copy(out, src) }
113func p256_modn_eq(a: *i64, b: *i64) -> i64 { return u256_eq(a, b) }
114
115// (a + b) mod n. Inputs canonical (< n); output canonical.
116func p256_modn_add(r: *i64, a: *i64, b: *i64) -> i64 {
117 let _fm: i64 = nx_scratch_save()
118 let t: *i64 = u256_alloc()
119 let n: *i64 = u256_alloc()
120 p256_modn_load_n(n)
121 let carry: i64 = u256_add_with_carry(r, a, b)
122 let borrow: i64 = u256_sub_with_borrow(t, r, n)
123 if carry == 1 {
124 u256_copy(r, t)
125 } else {
126 if borrow == 0 {
127 u256_copy(r, t)
128 }
129 }
130 nx_scratch_restore(_fm)
131 return 0
132}
133
134// (a - b) mod n. Inputs canonical; output canonical.
135func p256_modn_sub(r: *i64, a: *i64, b: *i64) -> i64 {
136 let _fm: i64 = nx_scratch_save()
137 let n: *i64 = u256_alloc()
138 p256_modn_load_n(n)
139 let borrow: i64 = u256_sub_with_borrow(r, a, b)
140 if borrow == 1 {
141 u256_add_with_carry(r, r, n)
142 }
143 nx_scratch_restore(_fm)
144 return 0
145}
146
147// (-a) mod n.
148func p256_modn_neg(r: *i64, a: *i64) -> i64 {
149 if u256_is_zero(a) == 1 {
150 u256_zero(r)
151 return 0
152 }
153 let _fm: i64 = nx_scratch_save()
154 let n: *i64 = u256_alloc()
155 p256_modn_load_n(n)
156 u256_sub_with_borrow(r, n, a)
157 nx_scratch_restore(_fm)
158 return 0
159}
160
161// Reduce a 256-bit value mod n. Used for the hash-to-scalar step
162// in ECDSA verify (hash output is already <= 256 bits; if >= n
163// subtract once). Since n > 2^255, a single conditional subtract
164// suffices for any 256-bit input.
165//
166// Wait -- n > 2^255 is true (the top limb is 0xFFFFFFFF), but a
167// 256-bit input could be up to 2^256 - 1 which is much larger
168// than n. We may need multiple subtractions. Worst case:
169// input is in [n, 2^256) which has ~2^256 - n ≈ 2^256 - 2^256 +
170// small = bounded. Since 2^256 / n < 2, at most ONE subtract
171// is needed.
172func p256_modn_reduce(r: *i64, a: *i64) -> i64 {
173 let _fm: i64 = nx_scratch_save()
174 let n: *i64 = u256_alloc()
175 p256_modn_load_n(n)
176 u256_copy(r, a)
177 if u256_cmp(r, n) >= 0 {
178 u256_sub_with_borrow(r, r, n)
179 }
180 nx_scratch_restore(_fm)
181 return 0
182}
183
184// Local helpers used inside p256_modn_mul's reduction loop.
185// Defined BEFORE the caller per the NishiLang no-forward-ref rule.
186
187func u256_wide_shr_1_inplace(buf: *i64) -> i64 {
188 var i: i64 = NX_U256_WIDE_LIMBS - 1
189 var carry: i64 = 0
190 while i >= 0 {
191 let v: i64 = buf[i] & NX_U256_LIMB_MASK
192 let new_carry: i64 = v & 1
193 buf[i] = ((v >> 1) | (carry << (NX_U256_LIMB_BITS - 1))) & NX_U256_LIMB_MASK
194 carry = new_carry
195 i = i - 1
196 }
197 return 0
198}
199
200func u256_wide_sub_inplace(a: *i64, b: *i64) -> i64 {
201 var i: i64 = 0
202 var borrow: i64 = 0
203 while i < NX_U256_WIDE_LIMBS {
204 let d: i64 = (a[i] & NX_U256_LIMB_MASK) - (b[i] & NX_U256_LIMB_MASK) - borrow
205 if d < 0 {
206 a[i] = (d + (1 << NX_U256_LIMB_BITS)) & NX_U256_LIMB_MASK
207 borrow = 1
208 } else {
209 a[i] = d & NX_U256_LIMB_MASK
210 borrow = 0
211 }
212 i = i + 1
213 }
214 return borrow
215}
216
217// (a * b) mod n via wide_mul + bit-shift reduction. Same shape
218// as p256_field_mul but reducing mod n.
219//
220// Aliasing-safe: out may alias a or b.
221func p256_modn_mul(out_8: *i64, a: *i64, b: *i64) -> i64 {
222 let _fm: i64 = nx_scratch_save()
223 let c: *i64 = u256_wide_alloc()
224 let shifted_n: *i64 = u256_wide_alloc()
225 let n: *i64 = u256_alloc()
226 p256_modn_load_n(n)
227
228 u256_mul_wide(c, a, b)
229
230 var i: i64 = 0
231 while i < NX_U256_WIDE_LIMBS {
232 shifted_n[i] = 0
233 i = i + 1
234 }
235 i = 0
236 while i < NX_U256_LIMBS {
237 shifted_n[i + 8] = n[i]
238 i = i + 1
239 }
240
241 // 257 iterations: bit-by-bit reduction.
242 var k: i64 = 0
243 while k < 257 {
244 if u256_wide_cmp(c, shifted_n) >= 0 {
245 u256_wide_sub_inplace(c, shifted_n)
246 }
247 u256_wide_shr_1_inplace(shifted_n)
248 k = k + 1
249 }
250 u256_wide_copy_low(out_8, c)
251 nx_scratch_restore(_fm)
252 return 0
253}
254
255// (a * a) mod n via mul-with-self.
256func p256_modn_sq(out: *i64, a: *i64) -> i64 {
257 return p256_modn_mul(out, a, a)
258}
259
260// Extract bit at position bit_pos (0 = LSB) from an 8-limb LE int.
261func p256_modn_bit_at(limbs: *i64, bit_pos: i64) -> i64 {
262 let limb_idx: i64 = bit_pos / 32
263 let bit_in_limb: i64 = bit_pos - limb_idx * 32
264 let limb: i64 = limbs[limb_idx] & NX_U256_LIMB_MASK
265 return (limb >> bit_in_limb) & 1
266}
267
268// Montgomery multiply: a, b in Montgomery form (both < n); returns
269// out = a*b*R^-1 mod n (R = 2^256), per-limb CIOS REDC over 32-bit
270// limbs. Replaces the 257-iteration bit-shift reduction for the
271// inverse hot path (~10x). Aliasing-safe: out may alias a and/or b
272// (the product is taken into a separate wide buffer before out is
273// written). Same limb-overflow discipline as u256_mul_wide.
274func p256_modn_mul_mont(out: *i64, a: *i64, b: *i64) -> i64 {
275 let _fm: i64 = nx_scratch_save()
276 let n: *i64 = u256_alloc()
277 p256_modn_load_n(n)
278 let prod: *i64 = u256_wide_alloc()
279 u256_mul_wide(prod, a, b)
280 let S: *i64 = (nx_scratch(18 * 8)) as *i64
281 var z: i64 = 0
282 while z < 18 { S[z] = 0; z = z + 1 }
283 z = 0
284 while z < 16 { S[z] = prod[z] & NX_U256_LIMB_MASK; z = z + 1 }
285 var i: i64 = 0
286 while i < NX_U256_LIMBS {
287 let m: i64 = ((S[i] & NX_U256_LIMB_MASK) * NX_P256_MODN_NPRIME0) & NX_U256_LIMB_MASK
288 var carry: i64 = 0
289 var j: i64 = 0
290 while j < NX_U256_LIMBS {
291 let s: i64 = (S[i + j] & NX_U256_LIMB_MASK) + m * (n[j] & NX_U256_LIMB_MASK) + carry
292 S[i + j] = s & NX_U256_LIMB_MASK
293 carry = (s >> NX_U256_LIMB_BITS) & NX_U256_LIMB_MASK
294 j = j + 1
295 }
296 var k: i64 = i + 8
297 while carry != 0 {
298 let s2: i64 = (S[k] & NX_U256_LIMB_MASK) + carry
299 S[k] = s2 & NX_U256_LIMB_MASK
300 carry = (s2 >> NX_U256_LIMB_BITS) & NX_U256_LIMB_MASK
301 k = k + 1
302 }
303 i = i + 1
304 }
305 let res: *i64 = u256_alloc()
306 var t: i64 = 0
307 while t < NX_U256_LIMBS { res[t] = S[8 + t]; t = t + 1 }
308 let hi: i64 = S[16] & NX_U256_LIMB_MASK
309 if hi != 0 {
310 u256_sub_with_borrow(res, res, n)
311 } else {
312 if u256_cmp(res, n) >= 0 {
313 u256_sub_with_borrow(res, res, n)
314 }
315 }
316 u256_copy(out, res)
317 nx_scratch_restore(_fm)
318 return 0
319}
320
321// SLOW Fermat inverse (bit-shift reduction). Kept as the oracle
322// reference that the Montgomery fast path (p256_modn_inv) is verified
323// against. Aliasing-safe: out may alias a.
324func p256_modn_inv_slow(out: *i64, a: *i64) -> i64 {
325 let _fm: i64 = nx_scratch_save()
326 let exp: *i64 = u256_alloc()
327 p256_modn_load_n_minus_2(exp)
328
329 let base: *i64 = u256_alloc()
330 u256_copy(base, a)
331
332 let result: *i64 = u256_alloc()
333 p256_modn_one(result)
334
335 var bit_pos: i64 = 255
336 while bit_pos >= 0 {
337 p256_modn_sq(result, result)
338 if p256_modn_bit_at(exp, bit_pos) == 1 {
339 p256_modn_mul(result, result, base)
340 }
341 bit_pos = bit_pos - 1
342 }
343 u256_copy(out, result)
344 nx_scratch_restore(_fm)
345 return 0
346}
347
348// out = a^(-1) mod n via Fermat (a^(n-2)) with Montgomery multiply for
349// every square/multiply -> ~10x faster than the bit-shift modn_mul and
350// constant-time in the multiply. Aliasing-safe (a captured into Mont
351// form before out is written). Verified vs p256_modn_inv_slow + the
352// a*a^-1 == 1 identity in nx_p256_modn_mont_test.nx.
353func p256_modn_inv(out: *i64, a: *i64) -> i64 {
354 let _fm: i64 = nx_scratch_save()
355 let exp: *i64 = u256_alloc()
356 p256_modn_load_n_minus_2(exp)
357 let r2: *i64 = u256_alloc()
358 p256_modn_load_R2(r2)
359 let one: *i64 = u256_alloc()
360 p256_modn_one(one)
361 // base = a*R mod n (to Montgomery form); result = 1*R mod n (Mont 1)
362 let base: *i64 = u256_alloc()
363 p256_modn_mul_mont(base, a, r2)
364 let result: *i64 = u256_alloc()
365 p256_modn_mul_mont(result, one, r2)
366 var bit_pos: i64 = 255
367 while bit_pos >= 0 {
368 p256_modn_mul_mont(result, result, result)
369 if p256_modn_bit_at(exp, bit_pos) == 1 {
370 p256_modn_mul_mont(result, result, base)
371 }
372 bit_pos = bit_pos - 1
373 }
374 // convert out of Montgomery form: out = result * 1 * R^-1 mod n
375 let one2: *i64 = u256_alloc()
376 p256_modn_one(one2)
377 p256_modn_mul_mont(out, result, one2)
378 nx_scratch_restore(_fm)
379 return 0
380}
381
382// Compile-only smoke. Real KAT in nx_p256_modn_test.nx.
383func main() -> i64 {
384 return 0
385}