nx_lia_legal_test.nx source
↩ module page · 207 lines · 11453 B
1// nx_lia_legal_test.nx -- exercise LIA decision + sovereignty audit.
2
3import "nx_lia.nx"
4import "nx_legal_audit.nx"
5
6// ===== T1: LIA -- SAT case (system has integer solution) ============
7// x + y == 5, x - y == 1, x >= 0, y >= 0
8// solution: x = 3, y = 2. Should return SAT.
9func t1_lia_sat() -> nx_int {
10 let s: *LiaSystem = nx_lia_system_new(2)
11 let c1: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
12 c1[0] = 1; c1[1] = 1
13 let _a1: nx_int = nx_lia_add(s, c1, -5, NX_LIA_REL_EQ) // x + y - 5 == 0
14 let c2: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
15 c2[0] = 1; c2[1] = -1
16 let _a2: nx_int = nx_lia_add(s, c2, -1, NX_LIA_REL_EQ) // x - y - 1 == 0
17 let c3: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
18 c3[0] = 1; c3[1] = 0
19 let _a3: nx_int = nx_lia_add(s, c3, 0, NX_LIA_REL_GE) // x >= 0
20 let c4: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
21 c4[0] = 0; c4[1] = 1
22 let _a4: nx_int = nx_lia_add(s, c4, 0, NX_LIA_REL_GE) // y >= 0
23 let witness: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
24 let v: nx_int = nx_lia_decide(s, witness)
25 if v != NX_LIA_SAT { return 1 }
26 if witness[0] != 3 { return 1 }
27 if witness[1] != 2 { return 1 }
28 return 0
29}
30
31// ===== T2: LIA -- UNSAT case (over-constrained) =====================
32// x + y == 5, x + y == 7, x >= 0, y >= 0. Contradicts.
33func t2_lia_unsat() -> nx_int {
34 let s: *LiaSystem = nx_lia_system_new(2)
35 let c1: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
36 c1[0] = 1; c1[1] = 1
37 let _a1: nx_int = nx_lia_add(s, c1, -5, NX_LIA_REL_EQ)
38 let c2: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
39 c2[0] = 1; c2[1] = 1
40 let _a2: nx_int = nx_lia_add(s, c2, -7, NX_LIA_REL_EQ)
41 let witness: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
42 let v: nx_int = nx_lia_decide(s, witness)
43 if v != NX_LIA_UNSAT { return 2 }
44 return 0
45}
46
47// ===== T3: LIA -- validity via negation =============================
48// Show: for all x, y in [-16, 16]: if x == y then x - y == 0.
49// Negation: x == y AND x - y != 0. Should be UNSAT.
50func t3_lia_validity() -> nx_int {
51 let s: *LiaSystem = nx_lia_system_new(2)
52 let c1: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
53 c1[0] = 1; c1[1] = -1
54 let _a1: nx_int = nx_lia_add(s, c1, 0, NX_LIA_REL_EQ) // x - y == 0
55 let c2: *nx_int = (sys_mmap((NX_LIA_MAX_VARS * 8) as i64)) as *nx_int
56 c2[0] = 1; c2[1] = -1
57 let _a2: nx_int = nx_lia_add(s, c2, 0, NX_LIA_REL_NE) // x - y != 0 -- contradiction
58 let valid: nx_int = nx_lia_validity(s)
59 if valid != 1 { return 3 }
60 return 0
61}
62
63// ===== T4: legal audit -- register native components, all CLEAN =====
64func t4_audit_clean() -> nx_int {
65 let a: *LegalAudit = nx_legal_audit_new(16)
66 let _i1: nx_int = nx_legal_register(a,
67 "nx_lia" as *u8, 6, 1929,
68 "Presburger" as *u8, 10,
69 NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED,
70 "QF-LIA decidable since 1929; algorithm by Cooper 1972, FM 1827" as *u8)
71 if _i1 < 0 { return 4 }
72 let _i2: nx_int = nx_legal_register(a,
73 "nx_kernel_v2" as *u8, 12, 1972,
74 "Milner-LCF" as *u8, 10,
75 NX_LICENSE_NATIVE_NX, NX_PATENT_NEVER_PATENTED,
76 "LCF kernel discipline; HOL Light 500 LOC reimplemented native" as *u8)
77 if _i2 < 0 { return 4 }
78 let _i3: nx_int = nx_legal_register(a,
79 "nx_calc_deriv" as *u8, 13, 1684,
80 "Leibniz-Newton" as *u8, 14,
81 NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED,
82 "Symbolic differentiation; chain rule is 340+ years old" as *u8)
83 if _i3 < 0 { return 4 }
84 let _i4: nx_int = nx_legal_register(a,
85 "nx_prove_propositional" as *u8, 22, 1934,
86 "Gentzen" as *u8, 7,
87 NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED,
88 "Sequent calculus; natural deduction by Gentzen 1934" as *u8)
89 if _i4 < 0 { return 4 }
90 let _i5: nx_int = nx_legal_register(a,
91 "nx_units" as *u8, 7, 1960,
92 "BIPM SI" as *u8, 7,
93 NX_LICENSE_NATIVE_NX, NX_PATENT_NEVER_PATENTED,
94 "SI base units; international standard, no IP claims" as *u8)
95 if _i5 < 0 { return 4 }
96 let _i6: nx_int = nx_legal_register(a,
97 "nx_arith" as *u8, 7, 1889,
98 "Peano" as *u8, 5,
99 NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED,
100 "Peano axioms 1889; foundational, public domain" as *u8)
101 if _i6 < 0 { return 4 }
102 let _i7: nx_int = nx_legal_register(a,
103 "nx_classical" as *u8, 12, 1908,
104 "Brouwer-Hilbert" as *u8, 15,
105 NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED,
106 "LEM + DNE + Peirce; classical logic axioms, public domain" as *u8)
107 if _i7 < 0 { return 4 }
108 let _i8: nx_int = nx_legal_register(a,
109 "nx_probability" as *u8, 14, 1933,
110 "Kolmogorov" as *u8, 10,
111 NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED,
112 "Kolmogorov axioms 1933; foundational probability theory" as *u8)
113 if _i8 < 0 { return 4 }
114 if a.n != 8 { return 4 }
115 if nx_legal_count_clean(a) != 8 { return 4 }
116 if nx_legal_count_refused(a) != 0 { return 4 }
117 if nx_legal_verify_sovereign(a) != 1 { return 4 }
118 return 0
119}
120
121// ===== T5: registration REFUSES non-native license =================
122// We try to register a hypothetical GPL2 component; engine must reject.
123func t5_audit_refuses_gpl() -> nx_int {
124 let a: *LegalAudit = nx_legal_audit_new(4)
125 let idx: nx_int = nx_legal_register(a,
126 "fake_gpl_dep" as *u8, 12, 2010,
127 "Anonymous" as *u8, 9,
128 NX_LICENSE_GPL2, NX_PATENT_EXPIRED,
129 "Hypothetical -- must be REFUSED at register time" as *u8)
130 if idx != -2 { return 5 } // expected sovereignty-stop
131 if a.n != 0 { return 5 } // entry NOT added
132 return 0
133}
134
135// ===== T6: registration REFUSES live-patent algorithm =============
136func t6_audit_refuses_live_patent() -> nx_int {
137 let a: *LegalAudit = nx_legal_audit_new(4)
138 let idx: nx_int = nx_legal_register(a,
139 "fake_patented_method" as *u8, 20, 2024,
140 "Big Corp" as *u8, 7,
141 NX_LICENSE_NATIVE_NX, NX_PATENT_LIVE,
142 "Hypothetical patented method -- REFUSED at register time" as *u8)
143 if idx != -3 { return 6 }
144 if a.n != 0 { return 6 }
145 return 0
146}
147
148func main() -> nx_exit {
149 println("=== nx_lia + nx_legal_audit smoke ===" as *u8)
150
151 let r1: nx_int = t1_lia_sat()
152 if r1 != 0 { println("T1 lia_sat FAIL" as *u8); return r1 }
153 println("T1 lia_sat PASS {x+y=5, x-y=1, x>=0, y>=0} -> x=3, y=2" as *u8)
154
155 let r2: nx_int = t2_lia_unsat()
156 if r2 != 0 { println("T2 lia_unsat FAIL" as *u8); return r2 }
157 println("T2 lia_unsat PASS contradictory system rejected" as *u8)
158
159 let r3: nx_int = t3_lia_validity()
160 if r3 != 0 { println("T3 lia_validity FAIL" as *u8); return r3 }
161 println("T3 lia_validity PASS (x==y) -> (x-y==0) proven valid via UNSAT negation" as *u8)
162
163 let r4: nx_int = t4_audit_clean()
164 if r4 != 0 { println("T4 audit_clean FAIL" as *u8); return r4 }
165 println("T4 audit_clean PASS 8 native components registered + verified sovereign" as *u8)
166
167 let r5: nx_int = t5_audit_refuses_gpl()
168 if r5 != 0 { println("T5 audit_refuses_gpl FAIL" as *u8); return r5 }
169 println("T5 audit_refuses_gpl PASS GPL2 registration REFUSED with code -2" as *u8)
170
171 let r6: nx_int = t6_audit_refuses_live_patent()
172 if r6 != 0 { println("T6 audit_refuses_live_patent FAIL" as *u8); return r6 }
173 println("T6 audit_refuses_live_patent PASS live-patent registration REFUSED with code -3" as *u8)
174
175 println("" as *u8)
176 println("=== Sovereignty + cleanliness summary ===" as *u8)
177 let a: *LegalAudit = nx_legal_audit_new(16)
178 let _i1: nx_int = nx_legal_register(a, "nx_lia" as *u8, 6, 1929, "Presburger" as *u8, 10, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
179 let _i2: nx_int = nx_legal_register(a, "nx_kernel_v2" as *u8, 12, 1972, "Milner-LCF" as *u8, 10, NX_LICENSE_NATIVE_NX, NX_PATENT_NEVER_PATENTED, "" as *u8)
180 let _i3: nx_int = nx_legal_register(a, "nx_calc_deriv" as *u8, 13, 1684, "Leibniz-Newton" as *u8, 14, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
181 let _i4: nx_int = nx_legal_register(a, "nx_prove_propositional" as *u8, 22, 1934, "Gentzen" as *u8, 7, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
182 let _i5: nx_int = nx_legal_register(a, "nx_units" as *u8, 7, 1960, "BIPM SI" as *u8, 7, NX_LICENSE_NATIVE_NX, NX_PATENT_NEVER_PATENTED, "" as *u8)
183 let _i6: nx_int = nx_legal_register(a, "nx_arith" as *u8, 7, 1889, "Peano" as *u8, 5, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
184 let _i7: nx_int = nx_legal_register(a, "nx_classical" as *u8, 12, 1908, "Brouwer-Hilbert" as *u8, 15, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
185 let _i8: nx_int = nx_legal_register(a, "nx_probability" as *u8, 14, 1933, "Kolmogorov" as *u8, 10, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
186 let _i9: nx_int = nx_legal_register(a, "nx_chem" as *u8, 7, 1869, "Mendeleev" as *u8, 9, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
187 let _ia: nx_int = nx_legal_register(a, "nx_linalg" as *u8, 9, 1858, "Cayley" as *u8, 6, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
188 let _ib: nx_int = nx_legal_register(a, "nx_calc_integrate" as *u8, 17, 1684, "Leibniz-Newton" as *u8, 14, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
189 let _ic: nx_int = nx_legal_register(a, "nx_calc_series" as *u8, 14, 1715, "Brook Taylor" as *u8, 12, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
190 let _id: nx_int = nx_legal_register(a, "nx_calc_solve" as *u8, 13, 1545, "Cardano-Ferrari" as *u8, 16, NX_LICENSE_NATIVE_NX, NX_PATENT_EXPIRED, "" as *u8)
191 let _ie: nx_int = nx_legal_register(a, "nx_ot_replay" as *u8, 12, 2010, "OpenTheory (Hurd)" as *u8, 18, NX_LICENSE_NATIVE_NX, NX_PATENT_NEVER_PATENTED, "" as *u8)
192 let _if: nx_int = nx_legal_register(a, "nx_render_cli" as *u8, 13, 1970, "ASCII art (folk)" as *u8, 16, NX_LICENSE_NATIVE_NX, NX_PATENT_NEVER_PATENTED, "" as *u8)
193 let _ig: nx_int = nx_legal_register(a, "nx_render_svg" as *u8, 13, 2001, "W3C SVG (open)" as *u8, 14, NX_LICENSE_NATIVE_NX, NX_PATENT_NEVER_PATENTED, "" as *u8)
194 let _v: nx_int = nx_legal_emit_all(a)
195 println("" as *u8)
196 print("Components registered : " as *u8); print_i64(a.n); println("" as *u8)
197 print("Clean : " as *u8); print_i64(nx_legal_count_clean(a)); println("" as *u8)
198 print("Refused : " as *u8); print_i64(nx_legal_count_refused(a)); println("" as *u8)
199 print("Sovereign verdict : " as *u8); print_i64(nx_legal_verify_sovereign(a))
200 println(" (1 = every entry NATIVE_NX, no live patent, no GPL)" as *u8)
201 println("" as *u8)
202 println("All algorithms reimplemented natively in NishiLang." as *u8)
203 println("Every component licensed NX_LICENSE_NATIVE_NX." as *u8)
204 println("Every algorithm's underlying math is patent-expired or never-patented." as *u8)
205 println("Zero linked code, zero runtime dependencies, zero CRT, no backdoors." as *u8)
206 return 0
207}