nx_kernel_v2_test.nx source
↩ module page · 104 lines · 4563 B
1// nx_kernel_v2_test.nx -- exercise the semantic kernel.
2//
3// Three scenarios:
4// T1. Valid modus ponens chain -- kernel accepts.
5// T2. Modus ponens with MISMATCHED antecedent -- kernel REJECTS.
6// This is the test that distinguishes a real kernel from a
7// rubber stamp. HOL Light, Coq, Lean all reject this; the
8// v1 (structural) kernel would not.
9// T3. AND-intro then AND-elim_L round-trip -- kernel preserves
10// the formula structure.
11
12import "nx_syscalls.nx"
13import "nx_runtime.nx"
14import "nx_tier.nx"
15import "nx_unify.nx"
16import "nx_kernel_v2.nx"
17
18// User constants for the demo: P, Q, R, A.
19const SYM_P: nx_int = 1001
20const SYM_Q: nx_int = 1002
21const SYM_R: nx_int = 1003
22const SYM_A: nx_int = 1004
23
24func main() -> nx_exit {
25 println("=== nx_kernel_v2 -- semantic proof kernel ===" as *u8)
26
27 // ---- T1: valid modus ponens (P, P=>Q |- Q) ----
28 println("[T1] valid modus ponens (P, P=>Q |- Q):" as *u8)
29 let ch1: *K2Chain = nx_k2_chain_new(8)
30 let p: *Term = nx_term_const(SYM_P)
31 let q: *Term = nx_term_const(SYM_Q)
32 let imp_pq: *Term = nx_k2_imp(p, q)
33 let _i0: nx_int = nx_k2_axiom(ch1, imp_pq)
34 let _i1: nx_int = nx_k2_axiom(ch1, p)
35 let i2: nx_int = nx_k2_modus_ponens(ch1, 0, 1)
36 print(" modus_ponens result: " as *u8); print_i64(i2); println("" as *u8)
37 if i2 < 0 {
38 println(" FAIL: kernel rejected a valid MP" as *u8)
39 return 1
40 }
41 let _t: nx_int = nx_k2_mark_theorem(ch1)
42 let v1: nx_int = nx_k2_verify(ch1)
43 print(" verify: " as *u8); print_i64(v1); println("" as *u8)
44 if v1 != NX_K2_OK {
45 println(" FAIL: T1 verify rejected" as *u8)
46 return 1
47 }
48 println(" T1 PASS (kernel accepted the proof)" as *u8)
49
50 // ---- T2: invalid MP (R, P=>Q ?- Q) -- kernel must REJECT ----
51 println("[T2] INVALID modus ponens (R, P=>Q ?- Q):" as *u8)
52 println(" premise2 is R but antecedent of (P=>Q) is P -- kernel must reject" as *u8)
53 let ch2: *K2Chain = nx_k2_chain_new(8)
54 let p2: *Term = nx_term_const(SYM_P)
55 let q2: *Term = nx_term_const(SYM_Q)
56 let r2: *Term = nx_term_const(SYM_R)
57 let imp_pq2: *Term = nx_k2_imp(p2, q2)
58 let _j0: nx_int = nx_k2_axiom(ch2, imp_pq2)
59 let _j1: nx_int = nx_k2_axiom(ch2, r2)
60 let j2: nx_int = nx_k2_modus_ponens(ch2, 0, 1)
61 print(" modus_ponens result: " as *u8); print_i64(j2); println("" as *u8)
62 if j2 >= 0 {
63 println(" FAIL: kernel accepted a BAD MP -- this is the bullshit case" as *u8)
64 return 1
65 }
66 print(" expected error: -" as *u8); print_i64(NX_K2_ERR_MISMATCH)
67 print(" got: " as *u8); print_i64(j2); println("" as *u8)
68 if j2 != (0 - NX_K2_ERR_MISMATCH) {
69 println(" WARN: rejected but with unexpected error code" as *u8)
70 }
71 println(" T2 PASS (kernel REJECTED the bad inference)" as *u8)
72
73 // ---- T3: AND_INTRO + AND_ELIM round-trip ----
74 println("[T3] AND_INTRO then AND_ELIM_L round-trip:" as *u8)
75 let ch3: *K2Chain = nx_k2_chain_new(8)
76 let pa: *Term = nx_term_const(SYM_P)
77 let qa: *Term = nx_term_const(SYM_Q)
78 let _k0: nx_int = nx_k2_axiom(ch3, pa)
79 let _k1: nx_int = nx_k2_axiom(ch3, qa)
80 let k2: nx_int = nx_k2_and_intro(ch3, 0, 1)
81 if k2 < 0 { println(" FAIL: AND_INTRO rejected" as *u8); return 1 }
82 let k3: nx_int = nx_k2_and_elim_l(ch3, k2)
83 if k3 < 0 { println(" FAIL: AND_ELIM_L rejected" as *u8); return 1 }
84 // The resulting stmt at k3 should be structurally equal to pa.
85 let thm3: *K2Thm = nx_k2_at(ch3, k3)
86 let recovered: *Term = thm3.stmt
87 if nx_term_eq(recovered, pa) == 0 {
88 println(" FAIL: AND round-trip lost structure" as *u8)
89 return 1
90 }
91 println(" T3 PASS (formula structure preserved through AND round-trip)" as *u8)
92
93 println("" as *u8)
94 println("=== nx_kernel_v2 SEMANTIC verification VERIFIED ===" as *u8)
95 println("Distinguishing claim vs HOL Light:" as *u8)
96 println(" + smaller kernel (~400 LOC vs HOL Light's ~500 OCaml)" as *u8)
97 println(" + Captain Moroni doctrine: defensive-only, smaller attack surface" as *u8)
98 println(" + REJECTS bad inferences (T2 above) at emit time, LCF-style" as *u8)
99 println(" - lemma library still tiny (HOL Light ~10K)" as *u8)
100 println(" - tactics layer not yet built (HOL Light has full LCF tactic interp)" as *u8)
101 println("Honest verdict per cardinal: WIN on auditability + rule rejection," as *u8)
102 println("LOSE_BIG on lemma corpus + tactics layer. Named work for next sessions." as *u8)
103 return 0
104}