nx_i256.nx source
↩ module page · 267 lines · 7659 B
1// nx_i256.nx -- 256-bit signed integer (N3 in numeric tier ladder).
2//
3// Proves the substrate is NOT locked to i64. Companion to nx_i128;
4// extends the ladder one tier higher. 4-limb representation
5// (l0 + l1*2^64 + l2*2^128 + l3*2^192) with two's complement sign.
6//
7// Per numeric tier ladder cardinal:
8// N0 i32 (smaller, for tight memory budgets)
9// N1 i64 (default for most physical-world quantities)
10// N2 i128 (nx_i128.nx)
11// N3 i256 (THIS file -- atoms in a body, cryptographic moduli)
12// N4 i512+ (future)
13// N5 bigint (future, arbitrary precision)
14// N6 rational (future)
15// N7 Q-decimal (future)
16// N8 CAS (future, symbolic)
17// N9 interval (future, bounded uncertainty)
18//
19// Hardware-tier-agnostic: same i64 limbs work on RV32 / RV64 / x86 / ARM.
20// Cost: ~4x i64 for memory, ~8x for multiply. Use only when needed.
21//
22// genealogy_id: knuth_TAOCP_4.3.1_multiprecision + arbitrary_precision
23// + bignum_radix_2_64_lineage
24// lineage_id: limb_array_integer + two_s_complement
25// axioms: NX_AX_ALG_ASSOCIATIVITY + NX_AX_ALG_DISTRIBUTIVITY
26// (carry propagation preserves these for sufficiently many
27// limbs; with 4 limbs we represent any |x| < 2^255)
28
29// nx_safety_envelope:
30// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
31// sil_target: SIL1
32// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
33// verdict: NOT_YET_EVALUATED
34
35import "syscalls.nx"
36import "nx_axioms.nx"
37
38struct I256 {
39 l0: i64, // least significant
40 l1: i64,
41 l2: i64,
42 l3: i64, // most significant (sign bit in MSB)
43}
44
45const NX_I256_BYTES: i64 = 32
46
47// ===== allocation + basic state =========================================
48
49func nx_i256_alloc() -> *I256 {
50 let raw: *u8 = sys_mmap(NX_I256_BYTES)
51 let z: *I256 = raw as *I256
52 z.l0 = 0
53 z.l1 = 0
54 z.l2 = 0
55 z.l3 = 0
56 return z
57}
58
59func nx_i256_set_i64(z: *I256, v: i64) -> i64 {
60 z.l0 = v
61 z.l1 = 0
62 z.l2 = 0
63 z.l3 = 0
64 // sign-extend if negative
65 if v < 0 {
66 z.l1 = -1
67 z.l2 = -1
68 z.l3 = -1
69 }
70 return 0
71}
72
73func nx_i256_copy(dst: *I256, src: *I256) -> i64 {
74 dst.l0 = src.l0
75 dst.l1 = src.l1
76 dst.l2 = src.l2
77 dst.l3 = src.l3
78 return 0
79}
80
81func nx_i256_is_zero(z: *I256) -> i64 {
82 if z.l0 != 0 { return 0 }
83 if z.l1 != 0 { return 0 }
84 if z.l2 != 0 { return 0 }
85 if z.l3 != 0 { return 0 }
86 return 1
87}
88
89func nx_i256_is_neg(z: *I256) -> i64 {
90 if z.l3 < 0 { return 1 }
91 return 0
92}
93
94// ===== addition (z += b) ==============================================
95//
96// 4-limb add with carry propagation. Each limb is unsigned in the
97// addition; carries propagate through l0 -> l1 -> l2 -> l3.
98//
99// Carry detection: when unsigned a + b wraps, the sum (as signed)
100// is less than either input (treating both as unsigned). We use
101// a simpler test: cast to "unsigned" comparison by checking if the
102// result's high bit changed direction.
103
104func nx_i256_add_with_carry(a: i64, b: i64, carry_in: i64,
105 out_sum: *i64) -> i64 {
106 let s1: i64 = a + b
107 var c1: i64 = 0
108 // overflow if (a >= 0 && b >= 0 && s1 < 0) -- signed-twos-comp test
109 // OR (a < 0 && b < 0 && s1 >= 0) -- both negative wrap to positive
110 if a >= 0 {
111 if b >= 0 {
112 if s1 < 0 { c1 = 1 }
113 }
114 }
115 if a < 0 {
116 if b < 0 {
117 c1 = 1
118 }
119 if b >= 0 {
120 if s1 >= 0 { c1 = 1 }
121 }
122 }
123 if a >= 0 {
124 if b < 0 {
125 if s1 >= 0 { c1 = 1 }
126 }
127 }
128 let s2: i64 = s1 + carry_in
129 var c2: i64 = 0
130 if s1 == -1 { if carry_in == 1 { c2 = 1 } }
131 out_sum[0] = s2
132 return c1 + c2
133}
134
135func nx_i256_add(z: *I256, b: *I256) -> i64 {
136 let tmp: *i64 = (sys_mmap(8)) as *i64
137 let c1: i64 = nx_i256_add_with_carry(z.l0, b.l0, 0, tmp)
138 z.l0 = tmp[0]
139 let c2: i64 = nx_i256_add_with_carry(z.l1, b.l1, c1, tmp)
140 z.l1 = tmp[0]
141 let c3: i64 = nx_i256_add_with_carry(z.l2, b.l2, c2, tmp)
142 z.l2 = tmp[0]
143 let c4: i64 = nx_i256_add_with_carry(z.l3, b.l3, c3, tmp)
144 z.l3 = tmp[0]
145 return c4 // overflow indicator
146}
147
148// ===== bitwise negation + two's complement negate (uses add above) ====
149
150func nx_i256_neg(z: *I256) -> i64 {
151 z.l0 = z.l0 ^ -1
152 z.l1 = z.l1 ^ -1
153 z.l2 = z.l2 ^ -1
154 z.l3 = z.l3 ^ -1
155 let one: *I256 = nx_i256_alloc()
156 one.l0 = 1
157 nx_i256_add(z, one)
158 return 0
159}
160
161// ===== subtraction (z -= b) -- add the negation =======================
162
163func nx_i256_sub(z: *I256, b: *I256) -> i64 {
164 let neg_b: *I256 = nx_i256_alloc()
165 nx_i256_copy(neg_b, b)
166 nx_i256_neg(neg_b)
167 return nx_i256_add(z, neg_b)
168}
169
170// ===== multiply by small i64 (z *= k) ================================
171//
172// Schoolbook: split each limb into hi/lo 32-bit halves, multiply by k,
173// propagate carries. Result truncated to 256 bits.
174
175func nx_i256_mul_i64(z: *I256, k: i64) -> i64 {
176 // Sign handling: track signs, work with magnitude, restore at end.
177 var z_neg: i64 = 0
178 if nx_i256_is_neg(z) == 1 {
179 z_neg = 1
180 nx_i256_neg(z)
181 }
182 var k_neg: i64 = 0
183 var kk: i64 = k
184 if kk < 0 { k_neg = 1; kk = -kk }
185
186 let LO: i64 = 0xFFFFFFFF
187 let SH: i64 = 32
188
189 let k_lo: i64 = kk & LO
190 let k_hi: i64 = (kk >> SH) & LO
191
192 let limbs: *i64 = (sys_mmap(8 * 8)) as *i64 // 8 u32 half-limbs
193 limbs[0] = z.l0 & LO
194 limbs[1] = (z.l0 >> SH) & LO
195 limbs[2] = z.l1 & LO
196 limbs[3] = (z.l1 >> SH) & LO
197 limbs[4] = z.l2 & LO
198 limbs[5] = (z.l2 >> SH) & LO
199 limbs[6] = z.l3 & LO
200 limbs[7] = (z.l3 >> SH) & LO
201
202 let out: *i64 = (sys_mmap(8 * 8)) as *i64
203 var i: i64 = 0
204 while i < 8 { out[i] = 0; i = i + 1 }
205
206 var ii: i64 = 0
207 while ii < 8 {
208 let a: i64 = limbs[ii]
209 // multiply by k_lo
210 var carry: i64 = 0
211 var j: i64 = 0
212 if ii + j < 8 {
213 let p: i64 = a * k_lo + out[ii + j] + carry
214 out[ii + j] = p & LO
215 carry = (p >> SH) & LO
216 }
217 // multiply by k_hi (shifted by 1 half-limb)
218 if ii + 1 < 8 {
219 let p2: i64 = a * k_hi + out[ii + 1] + carry
220 out[ii + 1] = p2 & LO
221 carry = (p2 >> SH) & LO
222 }
223 // any further carry goes one more position
224 if ii + 2 < 8 {
225 out[ii + 2] = out[ii + 2] + carry
226 }
227 ii = ii + 1
228 }
229
230 z.l0 = out[0] | (out[1] << SH)
231 z.l1 = out[2] | (out[3] << SH)
232 z.l2 = out[4] | (out[5] << SH)
233 z.l3 = out[6] | (out[7] << SH)
234
235 var final_neg: i64 = 0
236 if z_neg == 1 { if k_neg == 0 { final_neg = 1 } }
237 if z_neg == 0 { if k_neg == 1 { final_neg = 1 } }
238 if final_neg == 1 { nx_i256_neg(z) }
239 return 0
240}
241
242// ===== left shift (z <<= n) =============================================
243
244func nx_i256_shl(z: *I256, n: i64) -> i64 {
245 if n <= 0 { return 0 }
246 if n >= 256 {
247 z.l0 = 0; z.l1 = 0; z.l2 = 0; z.l3 = 0
248 return 0
249 }
250 var shift: i64 = n
251 // Whole-limb shifts (64 bits each)
252 while shift >= 64 {
253 z.l3 = z.l2
254 z.l2 = z.l1
255 z.l1 = z.l0
256 z.l0 = 0
257 shift = shift - 64
258 }
259 if shift > 0 {
260 let inv: i64 = 64 - shift
261 z.l3 = (z.l3 << shift) | (z.l2 >> inv)
262 z.l2 = (z.l2 << shift) | (z.l1 >> inv)
263 z.l1 = (z.l1 << shift) | (z.l0 >> inv)
264 z.l0 = z.l0 << shift
265 }
266 return 0
267}