nx_atp_to_derive_test.nx source
↩ module page · 80 lines · 3636 B
1// nx_atp_to_derive_test.nx -- bridge smoke.
2// Builds a small ATP proof, converts to nx_derive chain, asserts
3// chain shape.
4
5import "nx_syscalls.nx"
6import "nx_runtime.nx"
7import "nx_tier.nx"
8import "nx_result.nx"
9import "nx_axioms.nx"
10import "nx_derive.nx"
11import "nx_proof_log.nx"
12import "nx_atp_to_derive.nx"
13
14func main() -> nx_exit {
15 println("=== ATP -> nx_derive bridge smoke ===" as *u8)
16 var fails: nx_int = 0
17
18 // Build a 4-entry ATP proof:
19 // 0: INPUT axiom-cite (PEANO_PA1)
20 // 1: INPUT axiom-cite (PEANO_PA2)
21 // 2: RES (parents 0, 1) -- contradiction
22 // 3: AVATAR_SPLIT (parent 2) -- conjunction-elim
23 let log: *ProofLog = nx_proof_log_new(8)
24 let _i0: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
25 let _i1: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
26 let _i2: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_RES, 0, 1)
27 let _i3: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_AVATAR_SPLIT, 2, 0 - 1)
28
29 // Axiom codes for INPUT entries.
30 let ax_codes: *nx_int = (sys_mmap((8 * 8) as i64)) as *nx_int
31 ax_codes[0] = NX_AX_PEANO_PA1_ZERO_EXISTS
32 ax_codes[1] = NX_AX_PEANO_PA2_SUCCESSOR
33 ax_codes[2] = 0 // ignored (not INPUT)
34 ax_codes[3] = 0 // ignored
35
36 let chain: *DerivationChain = nx_deriv_chain_alloc(8 as i64)
37 let n: nx_int = nx_atp_to_derive(log, ax_codes, chain)
38
39 print(" bridge produced n_nodes=" as *u8); print_i64(n); println("" as *u8)
40
41 // ---------- Test 1: 4 nodes emitted -------------------------
42 if n == 4 { println(" 1. 4 chain nodes (1:1 with ProofLog) PASS" as *u8) }
43 else { println(" 1. wrong count FAIL" as *u8); fails = fails + 1 }
44
45 // ---------- Test 2: node 0 is axiom citation ---------------
46 let n0: *DerivationNode = nx_deriv_node_at(chain, 0)
47 if n0.rule_id == NX_DRULE_AXIOM_CITATION {
48 if n0.axiom_code == NX_AX_PEANO_PA1_ZERO_EXISTS {
49 println(" 2. node 0 cites PEANO_PA1 PASS" as *u8)
50 } else { println(" 2. wrong axiom code FAIL" as *u8); fails = fails + 1 }
51 } else { println(" 2. node 0 not axiom citation FAIL" as *u8); fails = fails + 1 }
52
53 // ---------- Test 3: node 2 is CONTRADICTION (RES bridge) ---
54 let n2: *DerivationNode = nx_deriv_node_at(chain, 2)
55 if n2.rule_id == NX_DRULE_CONTRADICTION {
56 if n2.premise_a == 0 {
57 if n2.premise_b == 1 {
58 println(" 3. RES -> CONTRADICTION (premises 0, 1) PASS" as *u8)
59 } else { println(" 3. premise_b wrong FAIL" as *u8); fails = fails + 1 }
60 } else { println(" 3. premise_a wrong FAIL" as *u8); fails = fails + 1 }
61 } else { println(" 3. RES not bridged to CONTRADICTION FAIL" as *u8); fails = fails + 1 }
62
63 // ---------- Test 4: node 3 is CONJ_ELIM (AVATAR_SPLIT bridge) -
64 let n3: *DerivationNode = nx_deriv_node_at(chain, 3)
65 if n3.rule_id == NX_DRULE_CONJ_ELIM {
66 if n3.premise_a == 2 {
67 if n3.premise_b == 0 - 1 {
68 println(" 4. AVATAR_SPLIT -> CONJ_ELIM (unary, parent 2) PASS" as *u8)
69 } else { println(" 4. premise_b should be -1 for unary FAIL" as *u8); fails = fails + 1 }
70 } else { println(" 4. premise_a wrong FAIL" as *u8); fails = fails + 1 }
71 } else { println(" 4. AVATAR_SPLIT not bridged to CONJ_ELIM FAIL" as *u8); fails = fails + 1 }
72
73 println("" as *u8)
74 if fails == 0 {
75 println("=== ALL 4 ATP-bridge tests PASS ===" as *u8)
76 return 0
77 }
78 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
79 return 1
80}