nx_ed25519_scalar.nx source
↩ module page · 228 lines · 8341 B
1// nx_ed25519_scalar.nx -- scalar reduction mod L + scalar mul.
2//
3// Phase 0b §I.1.C-2 of the Ed25519 completion arc per
4// docs/NISHI_TLS13_GAP_AUDIT.md. Builds on the point arithmetic
5// shipped in nx_ed25519_arith (T9). The two callables here are:
6//
7// sc_reduce(s_64_LE, out_32_LE)
8// Reduce a 64-byte little-endian scalar (typically a SHA-512
9// output) modulo L, the order of the Ed25519 prime-order
10// subgroup. Used during sign (to compute the per-message
11// nonce and the challenge) and verify (to reduce h before
12// scalar mul of the public key).
13//
14// ge_scalar_mul(out, scalar_32_LE, p)
15// Compute [s]P via standard MSB-first double-and-add using
16// the shipped ge_p3_double + ge_p3_add primitives.
17//
18// Where L = 2^252 + 27742317777372353535851937790883648493
19// = 0x10000000000000000000000000000000_14def9dea2f79cd65812631a5cf5d3ed
20//
21// Algorithm choice: MSB-first shift-and-(conditionally-add-then-
22// subtract-L) iteration. Compared to Bernstein's ref10 21-bit-
23// limb dense arithmetic, this is ~100x slower but 5x shorter LOC
24// and unambiguously correct. Verify/sign call sc_reduce twice and
25// scalar_mul once per signature; we'd rather have correctness
26// today and speed later via a perf-only refactor.
27//
28// What it does today:
29// - sc_reduce(64_LE_bytes, 32_LE_out)
30// - ge_scalar_mul(GeP3, 32_LE_scalar, GeP3)
31//
32// What it doesn't do yet:
33// - ge_double_scalar_mul (Straus-Shamir [a]P + [b]Q in single
34// pass; verify needs it for [S]B - [h]A; for v1 we'll do two
35// separate scalar muls + one add, slower but trivially correct)
36// - precomputed-basepoint table for fast [s]B (perf optimisation)
37//
38// KAT verified:
39// - sc_reduce(0^64) == 0^32
40// - sc_reduce(L padded to 64) == 0^32
41// - sc_reduce(2*L padded to 64) == 0^32
42// - sc_reduce(L+1 padded to 64) == 1 (32 bytes: 01 00 ... 00)
43// - sc_reduce(L-1) == L-1
44// - ge_scalar_mul([0]B) == identity
45// - ge_scalar_mul([1]B) == B
46// - ge_scalar_mul([2]B) == double(B)
47// - ge_scalar_mul([3]B) == B + B + B
48//
49// Composes with:
50// - nx_ed25519_arith (ge_p3_identity / double / add)
51// - future ed25519_verify + ed25519_sign (Piece 4)
52//
53// license_tier: INDEPENDENT_REDERIVE
54// genealogy_id: international-research-sources/ietf/rfc_8032
55// lineage_id: nishi_ed25519_scalar_q10
56
57// nx_safety_envelope:
58// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
59// sil_target: SIL1
60// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
61// verdict: NOT_YET_EVALUATED
62
63import "nx_syscalls.nx"
64import "nx_ed25519_point.nx"
65import "nx_ed25519_arith.nx"
66
67// L in 32-bit little-endian limbs (8 limbs cover bits 0..255):
68// L = 0x10000000_00000000_00000000_00000000_14def9de_a2f79cd6_5812631a_5cf5d3ed
69//
70// Writes the 8 32-bit-limb representation of L into `out` (treated
71// as 8 i64 slots; each holds a 32-bit value).
72func sc_l_limbs(out: *i64) -> i64 {
73 out[0] = 0x5cf5d3ed
74 out[1] = 0x5812631a
75 out[2] = 0xa2f79cd6
76 out[3] = 0x14def9de
77 out[4] = 0
78 out[5] = 0
79 out[6] = 0
80 out[7] = 0x10000000
81 return 0
82}
83
84// Compare 9-limb candidate to L (which occupies limbs[0..7], with
85// limbs[8] expected to be 0). Returns 1 if candidate >= L, 0 if <.
86func sc_ge_l(limbs: *i64) -> i64 {
87 let l: *i64 = sys_mmap(64) as *i64
88 sc_l_limbs(l)
89 // If the high limb (8) is non-zero, candidate definitely >= L.
90 if limbs[8] > 0 { return 1 }
91 // Otherwise compare from MSB (limb 7) down.
92 var i: i64 = 7
93 while i >= 0 {
94 let a: i64 = limbs[i] & 0xffffffff
95 let b: i64 = l[i] & 0xffffffff
96 if a > b { return 1 }
97 if a < b { return 0 }
98 i = i - 1
99 }
100 return 1 // equal counts as >=
101}
102
103// Subtract L from candidate in place (assumes candidate >= L).
104// Carry-borrow chain across 9 limbs (limbs[8] absorbs final borrow).
105func sc_sub_l(limbs: *i64) -> i64 {
106 let l: *i64 = sys_mmap(64) as *i64
107 sc_l_limbs(l)
108 var borrow: i64 = 0
109 var i: i64 = 0
110 while i < 9 {
111 let lv: i64 = limbs[i] & 0xffffffff
112 let rv: i64 = 0
113 // For i < 8, subtract L's limb; for i == 8 just propagate borrow.
114 var r: i64 = 0
115 if i < 8 {
116 r = l[i] & 0xffffffff
117 }
118 var diff: i64 = lv - r - borrow
119 if diff < 0 {
120 diff = diff + 0x100000000
121 borrow = 1
122 } else {
123 borrow = 0
124 }
125 limbs[i] = diff & 0xffffffff
126 i = i + 1
127 }
128 return 0
129}
130
131// Reduce a 64-byte little-endian scalar mod L into a 32-byte LE result.
132//
133// Algorithm: MSB-first iteration over 512 bits. Maintain N (the
134// running result) as 9 32-bit limbs. Per bit:
135// N = 2*N (shift left; can grow up to bit 253)
136// N += bit (add the current bit at position 0)
137// if N >= L: N -= L (single subtract is enough since N < 2L)
138// Final N < L; serialise low 32 bytes (limbs[0..7]).
139//
140// Correctness rationale: invariant N < L is preserved. After
141// shift left, N < 2L (since N < L originally). After adding the
142// bit (0 or 1), N < 2L + 1 ≤ 2L (since L >= 1). After conditional
143// subtract, N < L.
144//
145// Cost: 512 iterations * ~50 op = ~26000 ops. Acceptable for the
146// "twice per signature" call frequency.
147func sc_reduce(s_in: *u8, out_32: *u8) -> i64 {
148 let limbs: *i64 = sys_mmap(80) as *i64 // 9 i64 slots
149 var z: i64 = 0
150 while z < 9 {
151 limbs[z] = 0
152 z = z + 1
153 }
154 var byte_idx: i64 = 63
155 while byte_idx >= 0 {
156 let byte_val: i64 = s_in[byte_idx] & 0xff
157 var bit_idx: i64 = 7
158 while bit_idx >= 0 {
159 // Shift limbs left by 1 (LSB-first carry chain).
160 var carry: i64 = 0
161 var i: i64 = 0
162 while i < 9 {
163 let shifted: i64 = (limbs[i] << 1) | carry
164 carry = (shifted >> 32) & 1
165 limbs[i] = shifted & 0xffffffff
166 i = i + 1
167 }
168 // Add the current bit at position 0.
169 let bit: i64 = (byte_val >> bit_idx) & 1
170 if bit == 1 {
171 limbs[0] = (limbs[0] + 1) & 0xffffffff
172 // No carry propagation possible past +1 (since pre-shift bit 0 was 0)
173 }
174 // Conditionally subtract L.
175 if sc_ge_l(limbs) == 1 {
176 sc_sub_l(limbs)
177 }
178 bit_idx = bit_idx - 1
179 }
180 byte_idx = byte_idx - 1
181 }
182 // Serialise low 256 bits (8 32-bit limbs) as 32 LE bytes.
183 var bi: i64 = 0
184 while bi < 8 {
185 let v: i64 = limbs[bi] & 0xffffffff
186 out_32[bi * 4 + 0] = v & 0xff
187 out_32[bi * 4 + 1] = (v >> 8) & 0xff
188 out_32[bi * 4 + 2] = (v >> 16) & 0xff
189 out_32[bi * 4 + 3] = (v >> 24) & 0xff
190 bi = bi + 1
191 }
192 return 0
193}
194
195// Compute R = [s]P via MSB-first double-and-add. s is a 32-byte LE
196// scalar (already reduced mod L by caller, OR equal to L-1, etc.;
197// we don't re-reduce here -- caller responsibility).
198//
199// Cost: 256 doublings + ~128 adds (depending on Hamming weight of s).
200func ge_scalar_mul(out: *GeP3, scalar_32: *u8, p: *GeP3) -> i64 {
201 ge_p3_identity(out)
202 let temp: *GeP3 = ge_p3_alloc()
203 var byte_idx: i64 = 31
204 while byte_idx >= 0 {
205 let byte_val: i64 = scalar_32[byte_idx] & 0xff
206 var bit_idx: i64 = 7
207 while bit_idx >= 0 {
208 // double out
209 ge_p3_double(temp, out)
210 // copy temp -> out
211 fe_copy(out.X, temp.X)
212 fe_copy(out.Y, temp.Y)
213 fe_copy(out.Z, temp.Z)
214 fe_copy(out.T, temp.T)
215 // CONSTANT-TIME (SEC-CT-002): ALWAYS compute out+p, then masked-select it iff the
216 // secret bit is set -- NO data-dependent branch on the scalar bit. Byte-identical:
217 // bit=1 -> out := out+p (as before); bit=0 -> out unchanged (the add result is
218 // discarded by the cmov). ge_p3_add is the COMPLETE Edwards formula, so adding to the
219 // identity / any partial sum is well-defined, making the unconditional add safe.
220 let bit: i64 = (byte_val >> bit_idx) & 1
221 ge_p3_add(temp, out, p)
222 ge_p3_cmov(out, temp, bit)
223 bit_idx = bit_idx - 1
224 }
225 byte_idx = byte_idx - 1
226 }
227 return 0
228}