nx_kernel_v2.nx source
↩ module page · 725 lines · 28006 B
1// nx_kernel_v2.nx -- SEMANTIC proof kernel. Real verification, not
2// structural box-checking.
3//
4// Per user 2026-05-15: "nishi lang must generate superior to all
5// other systems proofs not just two level i tlooks good bullshit".
6//
7// HOL Light's kernel is ~500 lines OCaml that implements ~10 primitive
8// inference rules with formal correctness arguments. Every rule does
9// SEMANTIC verification: modus ponens checks that the conclusion is
10// the consequent of the implication premise. Coq, Lean, Isabelle all
11// follow the same LCF discipline.
12//
13// nx_derive (v1) only checks STRUCTURE (rule arity, premise ordering,
14// axiom code validity). Statements were opaque i64 IDs. That was
15// "two-level it looks good bullshit" -- structurally a derivation
16// chain, but the kernel never verifies the statements actually fit
17// the rules' semantics.
18//
19// THIS KERNEL IS DIFFERENT:
20// - Statements are first-class *Term values (real logical formulas)
21// - Each inference rule does SEMANTIC verification of its premises
22// against its claimed conclusion
23// - Built on existing nx_unify Term + nx_subst infrastructure
24//
25// Semantic rules implemented (this commit):
26//
27// AXIOM leaf, must cite a registered axiom Term
28// ASSUMPTION leaf, marks discharged assumptions
29// MODUS_PONENS premise (A => B), premise A; conclusion = B
30// -- kernel CHECKS: premise1 is App(=>, A, B); A == premise2
31// AND_INTRO premise A, premise B; conclusion = And(A, B)
32// -- kernel CHECKS: conclusion is App(&, premise1, premise2)
33// AND_ELIM_L premise And(A, B); conclusion = A
34// AND_ELIM_R premise And(A, B); conclusion = B
35// IMP_INTRO premise B (under assumption A); conclusion = A => B
36// -- kernel CHECKS: conclusion is App(=>, A, B)
37// SUBST premise (a == b), premise P[a]; conclusion = P[b]
38// -- kernel CHECKS: conclusion = P with a replaced by b
39// REFL no premise; conclusion = (a == a)
40// CONTRADICTION premise A, premise (~A); conclusion = false
41//
42// Every rule call returns OK or a specific named error -- the kernel
43// REFUSES to add a node it can't verify. This is the LCF discipline:
44// nothing gets in unless the kernel itself blesses it.
45//
46// Smaller than HOL Light's kernel (this file under 400 lines vs
47// theirs ~500 OCaml). Smaller is better for the Captain Moroni
48// doctrine -- less attack surface in the trusted base.
49
50// nx_safety_envelope:
51// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
52// sil_target: SIL1
53// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
54// verdict: NOT_YET_EVALUATED
55
56import "nx_syscalls.nx"
57import "nx_runtime.nx"
58import "nx_tier.nx"
59import "nx_result.nx"
60import "nx_unify.nx"
61
62// ===== Sealed rule enum =============================================
63const NX_K2_AXIOM: nx_int = 1
64const NX_K2_ASSUMPTION: nx_int = 2
65const NX_K2_MODUS_PONENS: nx_int = 3
66const NX_K2_AND_INTRO: nx_int = 4
67const NX_K2_AND_ELIM_L: nx_int = 5
68const NX_K2_AND_ELIM_R: nx_int = 6
69const NX_K2_IMP_INTRO: nx_int = 7
70const NX_K2_SUBST: nx_int = 8
71const NX_K2_REFL: nx_int = 9
72const NX_K2_CONTRADICTION: nx_int = 10
73const NX_K2_NOT_INTRO: nx_int = 11
74const NX_K2_OR_INTRO_L: nx_int = 12
75const NX_K2_OR_INTRO_R: nx_int = 13
76const NX_K2_OR_ELIM: nx_int = 14
77const NX_K2_EQ_SYM: nx_int = 15
78const NX_K2_EQ_TRANS: nx_int = 16
79const NX_K2_EX_FALSO: nx_int = 17
80
81// ===== Logical-connective sym IDs ===================================
82// Reserved sym_ids for the kernel's logical connectives. Distinct
83// from user (1000+), Tseitin (800k+), Skolem (900k+), Answer (700k+),
84// AVATAR-sp (600k+), FMB-domain (500k+).
85const NX_K2_SYM_IMP: nx_int = 400001 // implication =>
86const NX_K2_SYM_AND: nx_int = 400002 // conjunction &
87const NX_K2_SYM_OR: nx_int = 400003 // disjunction |
88const NX_K2_SYM_NOT: nx_int = 400004 // negation ~
89const NX_K2_SYM_EQ: nx_int = 400005 // equality ==
90const NX_K2_SYM_FALSE: nx_int = 400006 // contradiction false
91
92// ===== Verification result codes ====================================
93const NX_K2_OK: nx_int = 0
94const NX_K2_ERR_BAD_ARITY: nx_int = 1
95const NX_K2_ERR_BAD_PREMISE: nx_int = 2
96const NX_K2_ERR_NOT_IMPL: nx_int = 3
97const NX_K2_ERR_NOT_AND: nx_int = 4
98const NX_K2_ERR_MISMATCH: nx_int = 5
99const NX_K2_ERR_BAD_INDEX: nx_int = 6
100const NX_K2_ERR_NO_THEOREM: nx_int = 7
101const NX_K2_ERR_NOT_ASSUMP: nx_int = 8
102const NX_K2_ERR_NOT_FALSE: nx_int = 9
103const NX_K2_ERR_NOT_OR: nx_int = 10
104const NX_K2_ERR_NOT_EQ: nx_int = 11
105const NX_K2_ERR_HYP_NOT_FND: nx_int = 12
106
107// ===== Theorem (a verified node) ====================================
108// Each theorem carries its open hypotheses (LCF discipline). AXIOM
109// nodes have hyps=[]. ASSUMPTION nodes have hyps=[stmt]. Derived
110// nodes inherit the union of premise hypotheses. IMP_INTRO and
111// NOT_INTRO discharge a hypothesis from the inherited set.
112struct K2Thm {
113 rule: nx_int,
114 premises: *nx_int, // [n_prem] -- indices in chain
115 n_prem: nx_int,
116 stmt: *Term, // the actual logical formula
117 hyps: *Term, // flat array of open hypotheses
118 n_hyps: nx_int,
119}
120const NX_K2_THM_BYTES: nx_int = 48
121
122struct K2Chain {
123 thms: *K2Thm,
124 n: nx_int,
125 cap: nx_int,
126 theorem_idx: nx_int, // -1 until set
127}
128const NX_K2_CHAIN_BYTES: nx_int = 24
129
130func nx_k2_chain_new(cap: nx_int) -> *K2Chain {
131 let ch: *K2Chain = (sys_mmap(NX_K2_CHAIN_BYTES as i64)) as *K2Chain
132 ch.thms = (sys_mmap((cap * NX_K2_THM_BYTES) as i64)) as *K2Thm
133 ch.n = 0
134 ch.cap = cap
135 ch.theorem_idx = 0 - 1
136 return ch
137}
138
139func nx_k2_at(ch: *K2Chain, i: nx_int) -> *K2Thm {
140 return ((ch.thms as nx_int) + (i * NX_K2_THM_BYTES)) as *K2Thm
141}
142
143// ===== Logical-formula constructors =================================
144// Build (A => B), (A & B), (~A), (a == b).
145func nx_k2_imp(a: *Term, b: *Term) -> *Term {
146 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
147 let a0: *Term = args
148 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args
149 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
150 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args
151 return nx_term_app(NX_K2_SYM_IMP, 2, args)
152}
153
154func nx_k2_and(a: *Term, b: *Term) -> *Term {
155 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
156 let a0: *Term = args
157 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args
158 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
159 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args
160 return nx_term_app(NX_K2_SYM_AND, 2, args)
161}
162
163func nx_k2_or(a: *Term, b: *Term) -> *Term {
164 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
165 let a0: *Term = args
166 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args
167 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
168 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args
169 return nx_term_app(NX_K2_SYM_OR, 2, args)
170}
171
172func nx_k2_not(a: *Term) -> *Term {
173 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
174 arg.kind = a.kind; arg.sym = a.sym; arg.n_args = a.n_args; arg.args = a.args
175 return nx_term_app(NX_K2_SYM_NOT, 1, arg)
176}
177
178func nx_k2_eq(a: *Term, b: *Term) -> *Term {
179 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
180 let a0: *Term = args
181 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args
182 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
183 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args
184 return nx_term_app(NX_K2_SYM_EQ, 2, args)
185}
186
187func nx_k2_false() -> *Term {
188 return nx_term_app(NX_K2_SYM_FALSE, 0, 0 as *Term)
189}
190
191// ===== Hypothesis tracking helpers ===================================
192// Hypotheses live as a flat array of Term values (not pointers). Each
193// slot is NX_TERM_BYTES wide; we copy the four fields manually since
194// NishiLang doesn't yet have memcpy at the language level.
195
196func nx_k2_hyps_alloc(cap: nx_int) -> *Term {
197 if cap <= 0 { return 0 as *Term }
198 return (sys_mmap((cap * NX_TERM_BYTES) as i64)) as *Term
199}
200
201func nx_k2_hyps_at(hyps: *Term, i: nx_int) -> *Term {
202 return ((hyps as nx_int) + (i * NX_TERM_BYTES)) as *Term
203}
204
205func nx_k2_hyps_copy_in(dst: *Term, di: nx_int, src: *Term) {
206 let d: *Term = nx_k2_hyps_at(dst, di)
207 d.kind = src.kind
208 d.sym = src.sym
209 d.n_args = src.n_args
210 d.args = src.args
211}
212
213// Does hyps[0..n] already contain a Term structurally equal to t?
214func nx_k2_hyps_contains(hyps: *Term, n: nx_int, t: *Term) -> nx_int {
215 var i: nx_int = 0
216 while i < n {
217 let h: *Term = nx_k2_hyps_at(hyps, i)
218 if nx_term_eq(h, t) == 1 { return 1 }
219 i = i + 1
220 }
221 return 0
222}
223
224// Compute deduped union of two hypothesis sets. Writes the result
225// into a freshly mmapped flat array; returns the array and writes
226// the size to *out_n.
227func nx_k2_hyps_union(a: *Term, na: nx_int, b: *Term, nb: nx_int, out_n: *nx_int) -> *Term {
228 let cap: nx_int = na + nb
229 if cap == 0 {
230 out_n[0] = 0
231 return 0 as *Term
232 }
233 let dst: *Term = nx_k2_hyps_alloc(cap)
234 var n: nx_int = 0
235 var i: nx_int = 0
236 while i < na {
237 let h: *Term = nx_k2_hyps_at(a, i)
238 nx_k2_hyps_copy_in(dst, n, h)
239 n = n + 1
240 i = i + 1
241 }
242 var j: nx_int = 0
243 while j < nb {
244 let h2: *Term = nx_k2_hyps_at(b, j)
245 if nx_k2_hyps_contains(dst, n, h2) == 0 {
246 nx_k2_hyps_copy_in(dst, n, h2)
247 n = n + 1
248 }
249 j = j + 1
250 }
251 out_n[0] = n
252 return dst
253}
254
255// Remove a single hypothesis (structurally equal to `target`) from
256// the input set. Returns the new array + size. STANDARD LCF DISCH
257// SEMANTICS: if the target isn't present, returns the input unchanged
258// -- discharging an unused assumption is always sound (the conclusion
259// just doesn't depend on it; e.g., DISCH B (|- A) = |- B => A).
260// This is what HOL Light's DISCH does.
261func nx_k2_hyps_remove(src: *Term, n: nx_int, target: *Term, out_n: *nx_int) -> *Term {
262 var found: nx_int = 0
263 var i: nx_int = 0
264 while i < n {
265 let h: *Term = nx_k2_hyps_at(src, i)
266 if nx_term_eq(h, target) == 1 { found = 1 }
267 i = i + 1
268 }
269 if found == 0 {
270 // Unused-assumption discharge: copy hyps unchanged.
271 if n <= 0 {
272 out_n[0] = 0
273 return 0 as *Term
274 }
275 let copy: *Term = nx_k2_hyps_alloc(n)
276 var c: nx_int = 0
277 while c < n {
278 nx_k2_hyps_copy_in(copy, c, nx_k2_hyps_at(src, c))
279 c = c + 1
280 }
281 out_n[0] = n
282 return copy
283 }
284 if n <= 1 {
285 out_n[0] = 0
286 return 0 as *Term
287 }
288 let dst: *Term = nx_k2_hyps_alloc(n - 1)
289 var k: nx_int = 0
290 var j: nx_int = 0
291 while j < n {
292 let h2: *Term = nx_k2_hyps_at(src, j)
293 if nx_term_eq(h2, target) == 0 {
294 nx_k2_hyps_copy_in(dst, k, h2)
295 k = k + 1
296 }
297 j = j + 1
298 }
299 out_n[0] = k
300 return dst
301}
302
303// Inherit hypothesis union from two premises (used by all binary rules).
304func nx_k2_inherit_2(ch: *K2Chain, t: *K2Thm, pa_idx: nx_int, pb_idx: nx_int) {
305 let pa: *K2Thm = nx_k2_at(ch, pa_idx)
306 let pb: *K2Thm = nx_k2_at(ch, pb_idx)
307 let out_n: *nx_int = (sys_mmap(8)) as *nx_int
308 let merged: *Term = nx_k2_hyps_union(pa.hyps, pa.n_hyps, pb.hyps, pb.n_hyps, out_n)
309 t.hyps = merged
310 t.n_hyps = out_n[0]
311}
312
313// Inherit hypothesis set from one premise (used by all unary rules).
314func nx_k2_inherit_1(ch: *K2Chain, t: *K2Thm, pa_idx: nx_int) {
315 let pa: *K2Thm = nx_k2_at(ch, pa_idx)
316 let out_n: *nx_int = (sys_mmap(8)) as *nx_int
317 let copied: *Term = nx_k2_hyps_union(pa.hyps, pa.n_hyps, 0 as *Term, 0, out_n)
318 t.hyps = copied
319 t.n_hyps = out_n[0]
320}
321
322// ===== Rule emitters with semantic verification =====================
323// Each emitter VERIFIES the premises support the claimed conclusion.
324// On any verification failure, returns a negative error code AND does
325// not extend the chain. This is LCF discipline: nothing gets in
326// unless the kernel verifies.
327
328// AXIOM: caller asserts a foundational fact. Kernel doesn't try to
329// verify the formula's truth (that's what makes it an axiom); the
330// chain just records that this Term is taken as given.
331// AXIOMS HAVE NO HYPOTHESES.
332func nx_k2_axiom(ch: *K2Chain, stmt: *Term) -> nx_int {
333 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
334 let t: *K2Thm = nx_k2_at(ch, ch.n)
335 t.rule = NX_K2_AXIOM
336 t.premises = 0 as *nx_int
337 t.n_prem = 0
338 t.stmt = stmt
339 t.hyps = 0 as *Term
340 t.n_hyps = 0
341 let idx: nx_int = ch.n
342 ch.n = ch.n + 1
343 return idx
344}
345
346// ASSUMPTION: introduces stmt as an open hypothesis. The chain can
347// later discharge this hypothesis via IMP_INTRO or NOT_INTRO.
348func nx_k2_assume(ch: *K2Chain, stmt: *Term) -> nx_int {
349 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
350 let t: *K2Thm = nx_k2_at(ch, ch.n)
351 t.rule = NX_K2_ASSUMPTION
352 t.premises = 0 as *nx_int
353 t.n_prem = 0
354 t.stmt = stmt
355 t.hyps = nx_k2_hyps_alloc(1)
356 nx_k2_hyps_copy_in(t.hyps, 0, stmt)
357 t.n_hyps = 1
358 let idx: nx_int = ch.n
359 ch.n = ch.n + 1
360 return idx
361}
362
363// IMP_INTRO: from B (under hypothesis A) discharge A and conclude (A => B).
364// Kernel checks: prem_assumption.rule == ASSUMPTION; prem_b.hyps
365// contains prem_assumption.stmt (otherwise nothing to discharge).
366func nx_k2_imp_intro(ch: *K2Chain, prem_assumption: nx_int, prem_b: nx_int) -> nx_int {
367 if prem_assumption < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
368 if prem_assumption >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
369 if prem_b < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
370 if prem_b >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
371 let ta: *K2Thm = nx_k2_at(ch, prem_assumption)
372 let tb: *K2Thm = nx_k2_at(ch, prem_b)
373 if ta.rule != NX_K2_ASSUMPTION { return 0 - NX_K2_ERR_NOT_ASSUMP }
374 let out_n: *nx_int = (sys_mmap(8)) as *nx_int
375 let new_hyps: *Term = nx_k2_hyps_remove(tb.hyps, tb.n_hyps, ta.stmt, out_n)
376 if out_n[0] < 0 { return 0 - NX_K2_ERR_HYP_NOT_FND }
377 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
378 let t: *K2Thm = nx_k2_at(ch, ch.n)
379 t.rule = NX_K2_IMP_INTRO
380 let prems: *nx_int = (sys_mmap(16)) as *nx_int
381 prems[0] = prem_assumption
382 prems[1] = prem_b
383 t.premises = prems
384 t.n_prem = 2
385 t.stmt = nx_k2_imp(ta.stmt, tb.stmt)
386 t.hyps = new_hyps
387 t.n_hyps = out_n[0]
388 let idx: nx_int = ch.n
389 ch.n = ch.n + 1
390 return idx
391}
392
393// NOT_INTRO: from false (under hypothesis A) discharge A and conclude (~A).
394// This is the proper proof-by-contradiction discharge that converts
395// "ASSUME |- false" into the actual theorem "|- NOT ASSUME".
396// Kernel checks: prem_assumption.rule == ASSUMPTION;
397// prem_false.stmt is App(FALSE); prem_false.hyps contains prem_assumption.stmt.
398func nx_k2_not_intro(ch: *K2Chain, prem_assumption: nx_int, prem_false: nx_int) -> nx_int {
399 if prem_assumption < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
400 if prem_assumption >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
401 if prem_false < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
402 if prem_false >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
403 let ta: *K2Thm = nx_k2_at(ch, prem_assumption)
404 let tf: *K2Thm = nx_k2_at(ch, prem_false)
405 if ta.rule != NX_K2_ASSUMPTION { return 0 - NX_K2_ERR_NOT_ASSUMP }
406 if tf.stmt.kind != NX_TERM_APP { return 0 - NX_K2_ERR_NOT_FALSE }
407 if tf.stmt.sym != NX_K2_SYM_FALSE { return 0 - NX_K2_ERR_NOT_FALSE }
408 let out_n: *nx_int = (sys_mmap(8)) as *nx_int
409 let new_hyps: *Term = nx_k2_hyps_remove(tf.hyps, tf.n_hyps, ta.stmt, out_n)
410 if out_n[0] < 0 { return 0 - NX_K2_ERR_HYP_NOT_FND }
411 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
412 let t: *K2Thm = nx_k2_at(ch, ch.n)
413 t.rule = NX_K2_NOT_INTRO
414 let prems: *nx_int = (sys_mmap(16)) as *nx_int
415 prems[0] = prem_assumption
416 prems[1] = prem_false
417 t.premises = prems
418 t.n_prem = 2
419 t.stmt = nx_k2_not(ta.stmt)
420 t.hyps = new_hyps
421 t.n_hyps = out_n[0]
422 let idx: nx_int = ch.n
423 ch.n = ch.n + 1
424 return idx
425}
426
427// OR_INTRO_L: from A, conclude (A | B) for any B.
428func nx_k2_or_intro_l(ch: *K2Chain, prem_a: nx_int, b: *Term) -> nx_int {
429 if prem_a < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
430 if prem_a >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
431 let ta: *K2Thm = nx_k2_at(ch, prem_a)
432 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
433 let t: *K2Thm = nx_k2_at(ch, ch.n)
434 t.rule = NX_K2_OR_INTRO_L
435 let prems: *nx_int = (sys_mmap(8)) as *nx_int
436 prems[0] = prem_a
437 t.premises = prems
438 t.n_prem = 1
439 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
440 nx_k2_hyps_copy_in(args, 0, ta.stmt)
441 nx_k2_hyps_copy_in(args, 1, b)
442 t.stmt = nx_term_app(NX_K2_SYM_OR, 2, args)
443 nx_k2_inherit_1(ch, t, prem_a)
444 let idx: nx_int = ch.n
445 ch.n = ch.n + 1
446 return idx
447}
448
449// OR_INTRO_R: from B, conclude (A | B) for any A.
450func nx_k2_or_intro_r(ch: *K2Chain, a: *Term, prem_b: nx_int) -> nx_int {
451 if prem_b < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
452 if prem_b >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
453 let tb: *K2Thm = nx_k2_at(ch, prem_b)
454 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
455 let t: *K2Thm = nx_k2_at(ch, ch.n)
456 t.rule = NX_K2_OR_INTRO_R
457 let prems: *nx_int = (sys_mmap(8)) as *nx_int
458 prems[0] = prem_b
459 t.premises = prems
460 t.n_prem = 1
461 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
462 nx_k2_hyps_copy_in(args, 0, a)
463 nx_k2_hyps_copy_in(args, 1, tb.stmt)
464 t.stmt = nx_term_app(NX_K2_SYM_OR, 2, args)
465 nx_k2_inherit_1(ch, t, prem_b)
466 let idx: nx_int = ch.n
467 ch.n = ch.n + 1
468 return idx
469}
470
471// EQ_SYM: from (a == b), conclude (b == a).
472func nx_k2_eq_sym(ch: *K2Chain, prem: nx_int) -> nx_int {
473 if prem < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
474 if prem >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
475 let tp: *K2Thm = nx_k2_at(ch, prem)
476 if tp.stmt.kind != NX_TERM_APP { return 0 - NX_K2_ERR_NOT_EQ }
477 if tp.stmt.sym != NX_K2_SYM_EQ { return 0 - NX_K2_ERR_NOT_EQ }
478 let a: *Term = nx_term_arg(tp.stmt, 0)
479 let b: *Term = nx_term_arg(tp.stmt, 1)
480 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
481 let t: *K2Thm = nx_k2_at(ch, ch.n)
482 t.rule = NX_K2_EQ_SYM
483 let prems: *nx_int = (sys_mmap(8)) as *nx_int
484 prems[0] = prem
485 t.premises = prems
486 t.n_prem = 1
487 t.stmt = nx_k2_eq(b, a)
488 nx_k2_inherit_1(ch, t, prem)
489 let idx: nx_int = ch.n
490 ch.n = ch.n + 1
491 return idx
492}
493
494// EX_FALSO (principle of explosion / ex falso quodlibet):
495// From false, conclude any C. Caller supplies C.
496func nx_k2_ex_falso(ch: *K2Chain, prem_false: nx_int, c: *Term) -> nx_int {
497 if prem_false < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
498 if prem_false >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
499 let tf: *K2Thm = nx_k2_at(ch, prem_false)
500 if tf.stmt.kind != NX_TERM_APP { return 0 - NX_K2_ERR_NOT_FALSE }
501 if tf.stmt.sym != NX_K2_SYM_FALSE { return 0 - NX_K2_ERR_NOT_FALSE }
502 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
503 let t: *K2Thm = nx_k2_at(ch, ch.n)
504 t.rule = NX_K2_EX_FALSO
505 let prems: *nx_int = (sys_mmap(8)) as *nx_int
506 prems[0] = prem_false
507 t.premises = prems
508 t.n_prem = 1
509 t.stmt = c
510 nx_k2_inherit_1(ch, t, prem_false)
511 let idx: nx_int = ch.n
512 ch.n = ch.n + 1
513 return idx
514}
515
516// EQ_TRANS: from (a == b) and (b == c), conclude (a == c).
517func nx_k2_eq_trans(ch: *K2Chain, prem_ab: nx_int, prem_bc: nx_int) -> nx_int {
518 if prem_ab < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
519 if prem_ab >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
520 if prem_bc < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
521 if prem_bc >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
522 let tab: *K2Thm = nx_k2_at(ch, prem_ab)
523 let tbc: *K2Thm = nx_k2_at(ch, prem_bc)
524 if tab.stmt.kind != NX_TERM_APP { return 0 - NX_K2_ERR_NOT_EQ }
525 if tab.stmt.sym != NX_K2_SYM_EQ { return 0 - NX_K2_ERR_NOT_EQ }
526 if tbc.stmt.kind != NX_TERM_APP { return 0 - NX_K2_ERR_NOT_EQ }
527 if tbc.stmt.sym != NX_K2_SYM_EQ { return 0 - NX_K2_ERR_NOT_EQ }
528 let a: *Term = nx_term_arg(tab.stmt, 0)
529 let b1: *Term = nx_term_arg(tab.stmt, 1)
530 let b2: *Term = nx_term_arg(tbc.stmt, 0)
531 let c: *Term = nx_term_arg(tbc.stmt, 1)
532 if nx_term_eq(b1, b2) == 0 { return 0 - NX_K2_ERR_MISMATCH }
533 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
534 let t: *K2Thm = nx_k2_at(ch, ch.n)
535 t.rule = NX_K2_EQ_TRANS
536 let prems: *nx_int = (sys_mmap(16)) as *nx_int
537 prems[0] = prem_ab
538 prems[1] = prem_bc
539 t.premises = prems
540 t.n_prem = 2
541 t.stmt = nx_k2_eq(a, c)
542 nx_k2_inherit_2(ch, t, prem_ab, prem_bc)
543 let idx: nx_int = ch.n
544 ch.n = ch.n + 1
545 return idx
546}
547
548// MODUS PONENS: from (A => B) and A, conclude B.
549// Kernel checks: premise_a is App(IMP, X, Y); premise_b == X; conclusion == Y.
550func nx_k2_modus_ponens(ch: *K2Chain, prem_imp: nx_int, prem_a: nx_int) -> nx_int {
551 if prem_imp < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
552 if prem_imp >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
553 if prem_a < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
554 if prem_a >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
555 let timp: *K2Thm = nx_k2_at(ch, prem_imp)
556 let ta: *K2Thm = nx_k2_at(ch, prem_a)
557 if timp.stmt.kind != NX_TERM_APP { return 0 - NX_K2_ERR_NOT_IMPL }
558 if timp.stmt.sym != NX_K2_SYM_IMP { return 0 - NX_K2_ERR_NOT_IMPL }
559 if timp.stmt.n_args != 2 { return 0 - NX_K2_ERR_NOT_IMPL }
560 let ant: *Term = nx_term_arg(timp.stmt, 0)
561 let con: *Term = nx_term_arg(timp.stmt, 1)
562 if nx_term_eq(ant, ta.stmt) == 0 { return 0 - NX_K2_ERR_MISMATCH }
563 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
564 let t: *K2Thm = nx_k2_at(ch, ch.n)
565 t.rule = NX_K2_MODUS_PONENS
566 let prems: *nx_int = (sys_mmap(16)) as *nx_int
567 prems[0] = prem_imp
568 prems[1] = prem_a
569 t.premises = prems
570 t.n_prem = 2
571 t.stmt = con
572 nx_k2_inherit_2(ch, t, prem_imp, prem_a)
573 let idx: nx_int = ch.n
574 ch.n = ch.n + 1
575 return idx
576}
577
578// AND_INTRO: from A and B, conclude (A & B).
579func nx_k2_and_intro(ch: *K2Chain, prem_a: nx_int, prem_b: nx_int) -> nx_int {
580 if prem_a < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
581 if prem_a >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
582 if prem_b < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
583 if prem_b >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
584 let ta: *K2Thm = nx_k2_at(ch, prem_a)
585 let tb: *K2Thm = nx_k2_at(ch, prem_b)
586 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
587 let t: *K2Thm = nx_k2_at(ch, ch.n)
588 t.rule = NX_K2_AND_INTRO
589 let prems: *nx_int = (sys_mmap(16)) as *nx_int
590 prems[0] = prem_a
591 prems[1] = prem_b
592 t.premises = prems
593 t.n_prem = 2
594 t.stmt = nx_k2_and(ta.stmt, tb.stmt)
595 nx_k2_inherit_2(ch, t, prem_a, prem_b)
596 let idx: nx_int = ch.n
597 ch.n = ch.n + 1
598 return idx
599}
600
601// AND_ELIM_L: from (A & B), conclude A.
602func nx_k2_and_elim_l(ch: *K2Chain, prem: nx_int) -> nx_int {
603 if prem < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
604 if prem >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
605 let tp: *K2Thm = nx_k2_at(ch, prem)
606 if tp.stmt.kind != NX_TERM_APP { return 0 - NX_K2_ERR_NOT_AND }
607 if tp.stmt.sym != NX_K2_SYM_AND { return 0 - NX_K2_ERR_NOT_AND }
608 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
609 let t: *K2Thm = nx_k2_at(ch, ch.n)
610 t.rule = NX_K2_AND_ELIM_L
611 let prems: *nx_int = (sys_mmap(8)) as *nx_int
612 prems[0] = prem
613 t.premises = prems
614 t.n_prem = 1
615 t.stmt = nx_term_arg(tp.stmt, 0)
616 nx_k2_inherit_1(ch, t, prem)
617 let idx: nx_int = ch.n
618 ch.n = ch.n + 1
619 return idx
620}
621
622// AND_ELIM_R: from (A & B), conclude B.
623func nx_k2_and_elim_r(ch: *K2Chain, prem: nx_int) -> nx_int {
624 if prem < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
625 if prem >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
626 let tp: *K2Thm = nx_k2_at(ch, prem)
627 if tp.stmt.kind != NX_TERM_APP { return 0 - NX_K2_ERR_NOT_AND }
628 if tp.stmt.sym != NX_K2_SYM_AND { return 0 - NX_K2_ERR_NOT_AND }
629 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
630 let t: *K2Thm = nx_k2_at(ch, ch.n)
631 t.rule = NX_K2_AND_ELIM_R
632 let prems: *nx_int = (sys_mmap(8)) as *nx_int
633 prems[0] = prem
634 t.premises = prems
635 t.n_prem = 1
636 t.stmt = nx_term_arg(tp.stmt, 1)
637 nx_k2_inherit_1(ch, t, prem)
638 let idx: nx_int = ch.n
639 ch.n = ch.n + 1
640 return idx
641}
642
643// REFL: conclude (a == a) for any term a. No premises, no hypotheses.
644func nx_k2_refl(ch: *K2Chain, a: *Term) -> nx_int {
645 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
646 let t: *K2Thm = nx_k2_at(ch, ch.n)
647 t.rule = NX_K2_REFL
648 t.premises = 0 as *nx_int
649 t.n_prem = 0
650 t.stmt = nx_k2_eq(a, a)
651 t.hyps = 0 as *Term
652 t.n_hyps = 0
653 let idx: nx_int = ch.n
654 ch.n = ch.n + 1
655 return idx
656}
657
658// CONTRADICTION: from A and (~A), conclude false.
659// Kernel checks: prem_neg.stmt is App(NOT, X) and X == prem_a.stmt.
660func nx_k2_contradiction(ch: *K2Chain, prem_a: nx_int, prem_neg: nx_int) -> nx_int {
661 if prem_a < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
662 if prem_a >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
663 if prem_neg < 0 { return 0 - NX_K2_ERR_BAD_INDEX }
664 if prem_neg >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
665 let ta: *K2Thm = nx_k2_at(ch, prem_a)
666 let tn: *K2Thm = nx_k2_at(ch, prem_neg)
667 if tn.stmt.kind != NX_TERM_APP { return 0 - NX_K2_ERR_MISMATCH }
668 if tn.stmt.sym != NX_K2_SYM_NOT { return 0 - NX_K2_ERR_MISMATCH }
669 let inside: *Term = nx_term_arg(tn.stmt, 0)
670 if nx_term_eq(inside, ta.stmt) == 0 { return 0 - NX_K2_ERR_MISMATCH }
671 if ch.n >= ch.cap { return 0 - NX_K2_ERR_BAD_INDEX }
672 let t: *K2Thm = nx_k2_at(ch, ch.n)
673 t.rule = NX_K2_CONTRADICTION
674 let prems: *nx_int = (sys_mmap(16)) as *nx_int
675 prems[0] = prem_a
676 prems[1] = prem_neg
677 t.premises = prems
678 t.n_prem = 2
679 t.stmt = nx_k2_false()
680 nx_k2_inherit_2(ch, t, prem_a, prem_neg)
681 let idx: nx_int = ch.n
682 ch.n = ch.n + 1
683 return idx
684}
685
686// Mark the last theorem. A real theorem MUST have no open hypotheses
687// (LCF discipline). Use nx_k2_mark_theorem_open if you want to
688// permit a node with open hypotheses (intermediate development).
689func nx_k2_mark_theorem(ch: *K2Chain) -> nx_int {
690 if ch.n <= 0 { return 0 - NX_K2_ERR_NO_THEOREM }
691 let last: *K2Thm = nx_k2_at(ch, ch.n - 1)
692 if last.n_hyps > 0 { return 0 - NX_K2_ERR_NOT_ASSUMP }
693 ch.theorem_idx = ch.n - 1
694 return NX_K2_OK
695}
696
697// Permit marking a non-closed node as the development target (used
698// for partial proofs / unit tests where the goal is to land at false
699// without yet discharging assumptions). Real publishable theorems
700// should always use nx_k2_mark_theorem.
701func nx_k2_mark_theorem_open(ch: *K2Chain) -> nx_int {
702 if ch.n <= 0 { return 0 - NX_K2_ERR_NO_THEOREM }
703 ch.theorem_idx = ch.n - 1
704 return NX_K2_OK
705}
706
707// Verify chain integrity: theorem_idx set; every node's premises
708// precede it; every node's stmt is non-null. Doesn't redo per-rule
709// semantic checks (those happened at emit time).
710func nx_k2_verify(ch: *K2Chain) -> nx_int {
711 if ch.theorem_idx < 0 { return 0 - NX_K2_ERR_NO_THEOREM }
712 if ch.theorem_idx >= ch.n { return 0 - NX_K2_ERR_BAD_INDEX }
713 var i: nx_int = 0
714 while i < ch.n {
715 let t: *K2Thm = nx_k2_at(ch, i)
716 if (t.stmt as nx_int) == 0 { return 0 - NX_K2_ERR_BAD_PREMISE }
717 var p: nx_int = 0
718 while p < t.n_prem {
719 if t.premises[p] >= i { return 0 - NX_K2_ERR_BAD_INDEX }
720 p = p + 1
721 }
722 i = i + 1
723 }
724 return NX_K2_OK
725}