nx_derive_test.nx source
↩ module page · 75 lines · 3127 B
1// nx_derive_test.nx -- smoke for axiom + derivation primitives.
2//
3// Concrete derivation: from Peano PA1 (zero exists) + PA2 (successor)
4// + PA5 (induction) we derive a trivial theorem "1 exists" by
5// universal-instantiation-style application of PA2 to PA1.
6// (The substrate doesn't interpret the statements -- it verifies the
7// STRUCTURE: axioms cited are valid; rules match arity; theorem marked.)
8
9import "syscalls.nx"
10import "nx_axioms.nx"
11import "nx_derive.nx"
12
13const STMT_ZERO_EXISTS: i64 = 1
14const STMT_SUCCESSOR_OF_ZERO_EXISTS: i64 = 2
15
16func main() -> i64 {
17 let ch: *DerivationChain = nx_deriv_chain_alloc(16)
18
19 // Leaf 0: axiom Peano PA1 -- 0 exists.
20 let a0: i64 = nx_deriv_add_axiom(ch, STMT_ZERO_EXISTS,
21 NX_AX_PEANO_PA1_ZERO_EXISTS)
22 if a0 < 0 { return 10 }
23
24 // Leaf 1: axiom Peano PA2 -- successor function.
25 let a1: i64 = nx_deriv_add_axiom(ch, 99,
26 NX_AX_PEANO_PA2_SUCCESSOR)
27 if a1 < 0 { return 11 }
28
29 // Internal 2: substitution applied to (0 exists, succ is function)
30 // gives (succ(0) exists). We model this as a 2-premise step.
31 let n2: i64 = nx_deriv_add_step(ch, STMT_SUCCESSOR_OF_ZERO_EXISTS,
32 NX_DRULE_SUBSTITUTION, a0, a1)
33 if n2 < 0 { return 12 }
34
35 nx_deriv_mark_theorem(ch)
36 let v: i64 = nx_deriv_verify(ch)
37 if v != NX_DERIV_VERIFY_OK { return 20 }
38
39 // ===== negative tests ============================================
40
41 // Invalid axiom code (out of range).
42 let ch_bad: *DerivationChain = nx_deriv_chain_alloc(4)
43 let bad1: i64 = nx_deriv_add_axiom(ch_bad, 1, 9999)
44 if bad1 != -2 { return 30 }
45
46 // Unknown rule.
47 let ch_rule: *DerivationChain = nx_deriv_chain_alloc(4)
48 nx_deriv_add_axiom(ch_rule, 1, NX_AX_PEANO_PA1_ZERO_EXISTS)
49 let bad2: i64 = nx_deriv_add_step(ch_rule, 2, 9999, 0, -1)
50 if bad2 != -3 { return 31 }
51
52 // Missing theorem mark.
53 let ch_nt: *DerivationChain = nx_deriv_chain_alloc(4)
54 nx_deriv_add_axiom(ch_nt, 1, NX_AX_PEANO_PA1_ZERO_EXISTS)
55 let vnt: i64 = nx_deriv_verify(ch_nt)
56 if vnt != NX_DERIV_VERIFY_NO_THEOREM { return 32 }
57
58 // Premise out of order: try to cite a future node.
59 let ch_oop: *DerivationChain = nx_deriv_chain_alloc(4)
60 // We can't directly add a node citing an out-of-order premise via
61 // the safe API, since nx_deriv_add_step rejects premise >= n_nodes.
62 // Instead, verify rejects manually-corrupted node.
63 nx_deriv_add_axiom(ch_oop, 1, NX_AX_PEANO_PA1_ZERO_EXISTS)
64 // Add a node then corrupt premise to point forward.
65 let nx_oop: i64 = nx_deriv_add_step(ch_oop, 2,
66 NX_DRULE_UNIVERSAL_INSTANT, 0, -1)
67 if nx_oop < 0 { return 33 }
68 let node1: *DerivationNode = nx_deriv_node_at(ch_oop, 1)
69 node1.premise_a = 99 // corrupt
70 nx_deriv_mark_theorem(ch_oop)
71 let v_oop: i64 = nx_deriv_verify(ch_oop)
72 if v_oop != NX_DERIV_VERIFY_PREMISE_OUT_OF_ORDER { return 34 }
73
74 return 0
75}