nx_triangulation_battery.nx source
↩ module page · 184 lines · 6473 B
1// nx_triangulation_battery.nx -- substrate-side triangulated proof
2// that algorithms can be called via NishiLang AND produce the proper
3// result, with NO external dependencies.
4//
5// Per user 2026-05-14: "we want proofs that any algorithm can be
6// called via nishi and have the proper result via nishi lang itself
7// in a triangulated fashion".
8//
9// Method: for each primitive under test (AUT), run the AUT plus TWO
10// independent witnesses:
11// W1 = known-vector oracle (hardcoded expected answer)
12// W2 = algebraic identity (compute the same value via a different
13// path, often by composing other substrate primitives)
14// If AUT == W1 == W2, the result is TRIANGULATED on that input.
15//
16// Aggregate verdict over the battery: tri_total, tri_agree, tri_fail.
17//
18// genealogy_id: substrate_triangulation_battery_2026_05_14
19// lineage_id: self_verified_correctness
20
21// nx_safety_envelope:
22// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
23// sil_target: SIL1
24// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
25// verdict: NOT_YET_EVALUATED
26
27import "nx_syscalls.nx"
28import "nx_runtime.nx"
29import "nx_tier.nx"
30import "nx_add_5.nx"
31import "nx_add_10.nx"
32import "nx_add_20.nx"
33import "nx_classical_unpatented.nx"
34import "nx_binary_search.nx"
35import "nx_lcm.nx"
36
37func nx_tri_check(label: *u8, aut: nx_int, w1: nx_int, w2: nx_int,
38 agree: *nx_int, fail: *nx_int) {
39 print(label)
40 print(": AUT=" as *u8); print_i64(aut)
41 print(" W1=" as *u8); print_i64(w1)
42 print(" W2=" as *u8); print_i64(w2)
43 if aut == w1 {
44 if aut == w2 {
45 println(" -> TRIANGULATED" as *u8)
46 agree[0] = agree[0] + 1
47 return
48 }
49 }
50 println(" -> DISAGREE" as *u8)
51 fail[0] = fail[0] + 1
52}
53
54func main() -> nx_exit {
55 let agree: *nx_int = (sys_mmap(8)) as *nx_int
56 let fail: *nx_int = (sys_mmap(8)) as *nx_int
57 agree[0] = 0
58 fail[0] = 0
59
60 println("==================================================================" as *u8)
61 println("TRIANGULATION BATTERY -- substrate-self-verified correctness proofs" as *u8)
62 println("each row: 1 AUT + 2 independent witnesses must all agree" as *u8)
63 println("==================================================================" as *u8)
64 println("" as *u8)
65
66 // === Arithmetic stubs (constant-offset) ============================
67 // AUT: nx_add_10(7); W1: 7+10 oracle; W2: nx_add_5(7) + 5 chain
68 nx_tri_check("nx_add_10(7) " as *u8,
69 nx_add_10(7),
70 7 + 10,
71 nx_add_5(7) + 5,
72 agree, fail)
73
74 nx_tri_check("nx_add_20(13) " as *u8,
75 nx_add_20(13),
76 13 + 20,
77 nx_add_10(13) + 10,
78 agree, fail)
79
80 nx_tri_check("nx_add_5(100) " as *u8,
81 nx_add_5(100),
82 100 + 5,
83 nx_add_10(95), // (95 + 10 = 105) via alternate offset
84 agree, fail)
85
86 // === Number theory =================================================
87 // gcd(12, 8) = 4. W2 uses recursive identity gcd(a,b) = gcd(b, a%b)
88 nx_tri_check("nx_gcd_euclidean(12, 8) " as *u8,
89 nx_gcd_euclidean(12, 8),
90 4,
91 nx_gcd_euclidean(8, 12 - 8), // gcd(8, 4) = 4
92 agree, fail)
93
94 nx_tri_check("nx_gcd_euclidean(48, 36) " as *u8,
95 nx_gcd_euclidean(48, 36),
96 12,
97 nx_gcd_euclidean(36, 48 - 36), // gcd(36, 12) = 12
98 agree, fail)
99
100 // lcm(4, 6) = 12. W2 uses identity lcm(a,b) = a*b / gcd(a,b)
101 nx_tri_check("nx_lcm(4, 6) " as *u8,
102 nx_lcm(4, 6),
103 12,
104 (4 * 6) / nx_gcd_euclidean(4, 6),
105 agree, fail)
106
107 nx_tri_check("nx_lcm(15, 25) " as *u8,
108 nx_lcm(15, 25),
109 75,
110 (15 * 25) / nx_gcd_euclidean(15, 25),
111 agree, fail)
112
113 // Fibonacci F(10) = 55. W2 uses recursive identity F(n)=F(n-1)+F(n-2)
114 nx_tri_check("nx_fibonacci(10) " as *u8,
115 nx_fibonacci(10),
116 55,
117 nx_fibonacci(9) + nx_fibonacci(8),
118 agree, fail)
119
120 nx_tri_check("nx_fibonacci(15) " as *u8,
121 nx_fibonacci(15),
122 610,
123 nx_fibonacci(14) + nx_fibonacci(13),
124 agree, fail)
125
126 // === Bit manipulation ==============================================
127 // popcount(0x55) = 4 (01010101). W2: popcount(0xAA) = 4 (complement)
128 nx_tri_check("nx_popcount_swar(0x55) " as *u8,
129 nx_popcount_swar(0x55),
130 4,
131 nx_popcount_swar(0xAA),
132 agree, fail)
133
134 // popcount(0xFF) = 8. W2: popcount(0xF0) + popcount(0x0F)
135 nx_tri_check("nx_popcount_swar(0xFF) " as *u8,
136 nx_popcount_swar(0xFF),
137 8,
138 nx_popcount_swar(0xF0) + nx_popcount_swar(0x0F),
139 agree, fail)
140
141 // === Integer sqrt ==================================================
142 // isqrt(100) = 10. W2: isqrt(99) since 9^2 < 100 means isqrt(99)=9
143 nx_tri_check("nx_isqrt_newton(100) " as *u8,
144 nx_isqrt_newton(100),
145 10,
146 nx_isqrt_newton(99) + 1, // isqrt(99)=9, +1=10
147 agree, fail)
148
149 // isqrt(144) = 12
150 nx_tri_check("nx_isqrt_newton(144) " as *u8,
151 nx_isqrt_newton(144),
152 12,
153 nx_isqrt_newton(143) + 1,
154 agree, fail)
155
156 // === Binary search =================================================
157 // arr = [10, 20, 30, 40, 50]; search for 30 should return idx 2
158 let arr: *nx_int = (sys_mmap(40)) as *nx_int
159 arr[0] = 10
160 arr[1] = 20
161 arr[2] = 30
162 arr[3] = 40
163 arr[4] = 50
164 nx_tri_check("nx_binary_search([10..50], 30)" as *u8,
165 nx_binary_search(arr, 5, 30) as nx_int,
166 2,
167 nx_binary_search_lower_bound(arr, 5, 30) as nx_int,
168 agree, fail)
169
170 nx_tri_check("nx_binary_search([10..50], 50)" as *u8,
171 nx_binary_search(arr, 5, 50) as nx_int,
172 4,
173 nx_binary_search_lower_bound(arr, 5, 50) as nx_int,
174 agree, fail)
175
176 // === aggregate verdict ============================================
177 println("" as *u8)
178 println("==================================================================" as *u8)
179 print("TRIANGULATED: " as *u8); print_i64(agree[0]); println("" as *u8)
180 print("DISAGREE: " as *u8); print_i64(fail[0]); println("" as *u8)
181 println("==================================================================" as *u8)
182 if fail[0] > 0 { return 1 }
183 return 0
184}