nx_prover_test.nx source
↩ module page · 68 lines · 2594 B
1// nx_prover_test.nx -- smoke for substrate-native prover.
2
3import "syscalls.nx"
4import "nx_axioms.nx"
5import "nx_derive.nx"
6import "nx_prover.nx"
7
8func main() -> i64 {
9 // Setup: prove that target stmt_id=99 follows from axioms + 2 implications.
10 // Statements:
11 // 1: axiom PA1 (zero exists)
12 // 2: axiom PA2 (successor function)
13 // 3: derived (1 -> 3) "successor of zero exists"
14 // 99: derived (3 -> 99) "1 exists"
15 // Implications: 1 -> 3, 3 -> 99
16
17 let s: *ProofState = nx_prover_state_alloc(99)
18 nx_prover_add_axiom(s, 1, NX_AX_PEANO_PA1_ZERO_EXISTS)
19 nx_prover_add_axiom(s, 2, NX_AX_PEANO_PA2_SUCCESSOR)
20
21 let impl: *i64 = (sys_mmap(40)) as *i64
22 impl[0] = 1; impl[1] = 3
23 impl[2] = 3; impl[3] = 99
24
25 let v: i64 = nx_prover_search(s, impl, 2, 10)
26 if v != NX_PROVER_PROVED { return 10 }
27 if s.found_idx < 0 { return 11 }
28 if s.cycle_count > 5 { return 12 } // should find in <= 5 cycles
29
30 // Build derivation chain and verify.
31 let chain: *DerivationChain = nx_deriv_chain_alloc(16)
32 nx_prover_build_chain(s, chain)
33 if nx_deriv_verify(chain) != NX_DERIV_VERIFY_OK { return 20 }
34
35 // === negative test: budget exhausted ===
36 let s2: *ProofState = nx_prover_state_alloc(99)
37 nx_prover_add_axiom(s2, 1, NX_AX_PEANO_PA1_ZERO_EXISTS)
38 // No implications -> can't reach 99.
39 let empty_impl: *i64 = (sys_mmap(8)) as *i64
40 let v2: i64 = nx_prover_search(s2, empty_impl, 0, 10)
41 if v2 != NX_PROVER_NO_RULES_APPLY { return 30 }
42
43 // === negative test: target already in facts (trivial) ===
44 let s3: *ProofState = nx_prover_state_alloc(5)
45 nx_prover_add_axiom(s3, 5, NX_AX_PEANO_PA1_ZERO_EXISTS)
46 let v3: i64 = nx_prover_search(s3, empty_impl, 0, 10)
47 if v3 != NX_PROVER_PROVED { return 40 }
48
49 // === deeper chain: 1 -> 2 -> 3 -> 4 -> ... -> 10 ===
50 let s4: *ProofState = nx_prover_state_alloc(10)
51 nx_prover_add_axiom(s4, 1, NX_AX_PEANO_PA1_ZERO_EXISTS)
52 let chain_impl: *i64 = (sys_mmap(160)) as *i64
53 var i: i64 = 0
54 while i < 9 {
55 chain_impl[i * 2] = i + 1
56 chain_impl[i * 2 + 1] = i + 2
57 i = i + 1
58 }
59 let v4: i64 = nx_prover_search(s4, chain_impl, 9, 20)
60 if v4 != NX_PROVER_PROVED { return 50 }
61
62 // === verify chain reconstruction PASSES nx_deriv_verify ===
63 let chain4: *DerivationChain = nx_deriv_chain_alloc(32)
64 nx_prover_build_chain(s4, chain4)
65 if nx_deriv_verify(chain4) != NX_DERIV_VERIFY_OK { return 60 }
66
67 return 0
68}