nx_p256_field.nx source
↩ module page · 165 lines · 5644 B
1// nx_p256_field.nx -- NIST P-256 prime field arithmetic.
2//
3// Phase 0b §I.3 piece 1 of the ECDSA-P256 arc. Composes the
4// nx_u256 big-int primitives (commit 6ff89dd8) with the P-256
5// prime
6//
7// p = 2^256 - 2^224 + 2^192 + 2^96 - 1
8// = FFFFFFFF 00000001 00000000 00000000
9// 00000000 FFFFFFFF FFFFFFFF FFFFFFFF (big-endian)
10//
11// into modular add / subtract / negate primitives operating on
12// F_p elements in canonical form (each element in [0, p)).
13//
14// Public API:
15// p256_field_load_p(out) -- write the prime into a buffer
16// p256_field_zero(out) / p256_field_one(out)
17// p256_field_copy(out, src)
18// p256_field_eq(a, b) -> 0|1
19// p256_field_add(r, a, b) -- r = (a + b) mod p
20// p256_field_sub(r, a, b) -- r = (a - b) mod p
21// p256_field_neg(r, a) -- r = (-a) mod p
22// nx_p256_field_verdict_is_valid(v)
23//
24// Preconditions: callers MUST pass operands already reduced
25// to canonical form [0, p). All outputs are guaranteed canonical.
26//
27// What this primitive does NOT do (queued for §1b):
28// - Multiplication (schoolbook 8x8 = 16 limbs, then Solinas
29// reduction using p's special form).
30// - Squaring (mul fast path).
31// - Modular inverse (Fermat: a^(p-2) mod p, ~256 squarings
32// + ~30 muls).
33// - These are bigger arcs; add/sub/neg ship first because every
34// point operation uses them and they're well-defined alone.
35//
36// Algorithm references:
37// - FIPS 186-5 §D.2.4 (P-256 prime + base point + group order)
38// - SEC 1 v2.0 §2.2.1 (Weierstrass curve over F_p form)
39// - HAC §14.2.1 (modular add/subtract conditional steps)
40// - BoringSSL p256.c (modern u32-limb reference for layout)
41//
42// Per Cardinal 9: this primitive does ONE thing (F_p add/sub/neg).
43// Per Cardinal 12: every operation produces canonical-form output.
44// Per Cardinal 23: preamble explains WHY mul + invert are split.
45//
46// license_tier: INDEPENDENT_REDERIVE
47// genealogy_id: international-research-sources/nist/fips_186_5
48// lineage_id: nishi_p256_field_q10
49
50// nx_safety_envelope:
51// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
52// sil_target: SIL1
53// evidence: [bulk_applied_2026-05-19, p256-field-add-sub-neg]
54// verdict: NOT_YET_EVALUATED
55
56import "nx_syscalls.nx"
57import "nx_u256.nx"
58
59const NX_P256_FIELD_OK: i64 = 1
60const NX_P256_FIELD_BAD: i64 = 2
61const NX_P256_FIELD_VERDICT_N: i64 = 3
62
63func nx_p256_field_verdict_is_valid(v: i64) -> i64 {
64 if v < NX_P256_FIELD_OK { return 0 }
65 if v >= NX_P256_FIELD_VERDICT_N { return 0 }
66 return 1
67}
68
69// Write the P-256 prime p into out (8 limbs, LE order).
70//
71// p = 0xFFFFFFFF_00000001_00000000_00000000_00000000_FFFFFFFF_FFFFFFFF_FFFFFFFF
72//
73// LE limb layout (limb[0] = LSB, limb[7] = MSB):
74// limb[0] = 0xFFFFFFFF
75// limb[1] = 0xFFFFFFFF
76// limb[2] = 0xFFFFFFFF
77// limb[3] = 0x00000000
78// limb[4] = 0x00000000
79// limb[5] = 0x00000000
80// limb[6] = 0x00000001
81// limb[7] = 0xFFFFFFFF
82func p256_field_load_p(out: *i64) -> i64 {
83 out[0] = 0xFFFFFFFF
84 out[1] = 0xFFFFFFFF
85 out[2] = 0xFFFFFFFF
86 out[3] = 0
87 out[4] = 0
88 out[5] = 0
89 out[6] = 1
90 out[7] = 0xFFFFFFFF
91 return 0
92}
93
94// Forward primitive wrappers (u256_* aliases under field name).
95func p256_field_zero(out: *i64) -> i64 { return u256_zero(out) }
96func p256_field_one(out: *i64) -> i64 { return u256_one(out) }
97func p256_field_copy(out: *i64, src: *i64) -> i64 { return u256_copy(out, src) }
98func p256_field_eq(a: *i64, b: *i64) -> i64 { return u256_eq(a, b) }
99
100// r = (a + b) mod p. Inputs a, b assumed canonical (< p);
101// output r is canonical.
102//
103// Algorithm: compute (r, carry) = a + b. Compute (t, borrow) = r - p.
104// If carry==1 (sum overflowed 2^256) OR borrow==0 (r >= p), the
105// canonical result is t. Otherwise r is already canonical.
106//
107// Aliasing-safe (out may equal a or b) per u256 contract.
108func p256_field_add(r: *i64, a: *i64, b: *i64) -> i64 {
109 let _fm: i64 = nx_scratch_save()
110 let t: *i64 = u256_alloc()
111 let p: *i64 = u256_alloc()
112 p256_field_load_p(p)
113 let carry: i64 = u256_add_with_carry(r, a, b)
114 let borrow: i64 = u256_sub_with_borrow(t, r, p)
115 if carry == 1 {
116 u256_copy(r, t)
117 } else {
118 if borrow == 0 {
119 u256_copy(r, t)
120 }
121 }
122 nx_scratch_restore(_fm)
123 return 0
124}
125
126// r = (a - b) mod p. Inputs a, b canonical; output canonical.
127//
128// Algorithm: compute (r, borrow) = a - b. If borrow==1 (a < b),
129// add p back to bring r into [0, p). Adding p when r underflowed
130// reaches a value < p because (a - b + p) for a, b in [0, p) lies
131// in [0, p) (since -b > -p, so a - b > -p, so a - b + p > 0; and
132// a < p, b >= 0 so a - b < p, so a - b + p < 2p).
133func p256_field_sub(r: *i64, a: *i64, b: *i64) -> i64 {
134 let _fm: i64 = nx_scratch_save()
135 let p: *i64 = u256_alloc()
136 p256_field_load_p(p)
137 let borrow: i64 = u256_sub_with_borrow(r, a, b)
138 if borrow == 1 {
139 u256_add_with_carry(r, r, p)
140 }
141 nx_scratch_restore(_fm)
142 return 0
143}
144
145// r = (-a) mod p. Inputs canonical; output canonical.
146//
147// For a == 0, -a = 0 (since p == 0 mod p).
148// For a > 0, -a mod p = p - a.
149func p256_field_neg(r: *i64, a: *i64) -> i64 {
150 if u256_is_zero(a) == 1 {
151 u256_zero(r)
152 return 0
153 }
154 let _fm: i64 = nx_scratch_save()
155 let p: *i64 = u256_alloc()
156 p256_field_load_p(p)
157 u256_sub_with_borrow(r, p, a)
158 nx_scratch_restore(_fm)
159 return 0
160}
161
162// Compile-only smoke. Real KAT in nx_p256_field_test.nx.
163func main() -> i64 {
164 return 0
165}