nx_p256_point_add.nx source
↩ module page · 177 lines · 5494 B
1// nx_p256_point_add.nx -- P-256 Jacobian point addition.
2//
3// Phase 0b §I.3 piece 2b of the ECDSA-P256 arc:
4// ✓ ...all earlier pieces shipped...
5// ✓ 2. p256_point: struct + double + to_affine + on_curve
6// (ecc7ad5f)
7// ✓ 2b. p256_point_add (THIS commit)
8// - 2c. p256_scalar_mul (queued)
9// - 3. p256_scalar mod n (queued)
10// - 4. ecdsa_p256 verify (queued)
11//
12// Algorithm (SEC 1 v2.0 §2.2.1.4, Jacobian + Jacobian):
13//
14// if Z1 == 0: return P2
15// if Z2 == 0: return P1
16// U1 = X1 * Z2^2
17// U2 = X2 * Z1^2
18// S1 = Y1 * Z2^3
19// S2 = Y2 * Z1^3
20// if U1 == U2:
21// if S1 == S2: return double(P1) -- P1 == P2
22// else: return infinity -- P1 == -P2 (additive inverse)
23// H = U2 - U1
24// R = S2 - S1
25// H2 = H^2
26// H3 = H * H2
27// U1H2 = U1 * H2
28// X3 = R^2 - H3 - 2 * U1H2
29// Y3 = R * (U1H2 - X3) - S1 * H3
30// Z3 = H * Z1 * Z2
31//
32// Cost per add: 12 mults + 4 squares + ~6 add/sub. Combined with
33// our slow field_mul (~4100 limb-ops per mul), one add takes
34// ~70K limb-ops. Double-and-add over a 256-bit scalar is ~256
35// doublings + ~128 adds = ~25M limb-ops per scalar-mult, or
36// ~2.5s per scalar-mult on qemu. Acceptable for first-cut ECDSA
37// verify; Solinas reduction will eventually cut this 10-25x.
38//
39// Public API:
40// p256_point_add(out, p1, p2)
41//
42// Aliasing: out MAY equal p1 or p2 (inputs snapshotted into
43// locals before any write).
44//
45// Per Cardinal 9 (single-responsibility -- add is its own primitive),
46// 22 (composition -- 16 field-ops compose into one curve-op), and
47// 23 (preamble explains the U1==U2 sub-cases).
48//
49// license_tier: INDEPENDENT_REDERIVE
50// genealogy_id: international-research-sources/sec_g/sec1_v2 + nist/fips_186_5
51// lineage_id: nishi_p256_point_add_q10
52
53// nx_safety_envelope:
54// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
55// sil_target: SIL1
56// evidence: [bulk_applied_2026-05-19, p256-jacobian-add]
57// verdict: NOT_YET_EVALUATED
58
59import "nx_syscalls.nx"
60import "nx_u256.nx"
61import "nx_p256_field.nx"
62import "nx_p256_field_mul.nx"
63import "nx_p256_point.nx"
64
65// out = p1 + p2 on the curve.
66//
67// Aliasing-safe across all combinations of out, p1, p2.
68func p256_point_add(out: *P256Point, p1: *P256Point, p2: *P256Point) -> i64 {
69 // Infinity cases first.
70 if p256_point_is_infinity(p1) == 1 {
71 p256_point_copy(out, p2)
72 return 0
73 }
74 if p256_point_is_infinity(p2) == 1 {
75 p256_point_copy(out, p1)
76 return 0
77 }
78
79 // Snapshot inputs into locals so out may alias p1 or p2.
80 let _fm: i64 = nx_scratch_save()
81 let X1: *i64 = u256_alloc()
82 let Y1: *i64 = u256_alloc()
83 let Z1: *i64 = u256_alloc()
84 let X2: *i64 = u256_alloc()
85 let Y2: *i64 = u256_alloc()
86 let Z2: *i64 = u256_alloc()
87 u256_copy(X1, p1.x)
88 u256_copy(Y1, p1.y)
89 u256_copy(Z1, p1.z)
90 u256_copy(X2, p2.x)
91 u256_copy(Y2, p2.y)
92 u256_copy(Z2, p2.z)
93
94 // U1 = X1 * Z2^2, U2 = X2 * Z1^2
95 let Z1_sq: *i64 = u256_alloc()
96 let Z2_sq: *i64 = u256_alloc()
97 p256_field_sq(Z1_sq, Z1)
98 p256_field_sq(Z2_sq, Z2)
99 let U1: *i64 = u256_alloc()
100 let U2: *i64 = u256_alloc()
101 p256_field_mul(U1, X1, Z2_sq)
102 p256_field_mul(U2, X2, Z1_sq)
103
104 // S1 = Y1 * Z2^3, S2 = Y2 * Z1^3
105 let Z1_cu: *i64 = u256_alloc()
106 let Z2_cu: *i64 = u256_alloc()
107 p256_field_mul(Z1_cu, Z1_sq, Z1)
108 p256_field_mul(Z2_cu, Z2_sq, Z2)
109 let S1: *i64 = u256_alloc()
110 let S2: *i64 = u256_alloc()
111 p256_field_mul(S1, Y1, Z2_cu)
112 p256_field_mul(S2, Y2, Z1_cu)
113
114 // Handle U1 == U2 case (points are either equal or additive inverses).
115 if p256_field_eq(U1, U2) == 1 {
116 if p256_field_eq(S1, S2) == 1 {
117 // P1 == P2 -> double(P1). Use the shipped double primitive
118 // on the snapshot to avoid touching p1 if out aliases it.
119 let snap: *P256Point = p256_point_alloc()
120 u256_copy(snap.x, X1)
121 u256_copy(snap.y, Y1)
122 u256_copy(snap.z, Z1)
123 p256_point_double(out, snap)
124 nx_scratch_restore(_fm)
125 return 0
126 }
127 // P1 == -P2 -> infinity
128 p256_point_zero(out)
129 nx_scratch_restore(_fm)
130 return 0
131 }
132
133 // General case.
134 let H: *i64 = u256_alloc()
135 let R: *i64 = u256_alloc()
136 p256_field_sub(H, U2, U1)
137 p256_field_sub(R, S2, S1)
138
139 let H2: *i64 = u256_alloc()
140 let H3: *i64 = u256_alloc()
141 let U1H2: *i64 = u256_alloc()
142 p256_field_sq(H2, H)
143 p256_field_mul(H3, H, H2)
144 p256_field_mul(U1H2, U1, H2)
145
146 // X3 = R^2 - H3 - 2*U1H2
147 let X3: *i64 = u256_alloc()
148 let tmp: *i64 = u256_alloc()
149 p256_field_sq(X3, R)
150 p256_field_sub(X3, X3, H3)
151 p256_field_add(tmp, U1H2, U1H2)
152 p256_field_sub(X3, X3, tmp)
153
154 // Y3 = R * (U1H2 - X3) - S1 * H3
155 let Y3: *i64 = u256_alloc()
156 let inner: *i64 = u256_alloc()
157 p256_field_sub(inner, U1H2, X3)
158 p256_field_mul(Y3, R, inner)
159 p256_field_mul(tmp, S1, H3)
160 p256_field_sub(Y3, Y3, tmp)
161
162 // Z3 = H * Z1 * Z2
163 let Z3: *i64 = u256_alloc()
164 p256_field_mul(Z3, H, Z1)
165 p256_field_mul(Z3, Z3, Z2)
166
167 u256_copy(out.x, X3)
168 u256_copy(out.y, Y3)
169 u256_copy(out.z, Z3)
170 nx_scratch_restore(_fm)
171 return 0
172}
173
174// Compile-only smoke. Real KAT in nx_p256_point_add_test.nx.
175func main() -> i64 {
176 return 0
177}