nx_prover_eval_test.nx source
↩ module page · 119 lines · 4792 B
1// nx_prover_eval_test.nx -- realistic prover capability benchmark.
2//
3// 8 test cases of progressively harder proof shapes:
4// case 1 1-axiom-only trivial
5// case 2 2-step MP chain (A, A->B, B->C => C)
6// case 3 5-step MP chain
7// case 4 10-step MP chain
8// case 5 wide branching (axiom A; 10 unrelated impls; target = via_A)
9// case 6 missing premise (target unreachable; expect NO_RULES)
10// case 7 beyond budget (50-step chain, budget 10; expect FAILED_BUDGET)
11// case 8 deep chain inside large budget (50-step chain, budget 200)
12
13import "syscalls.nx"
14import "nx_axioms.nx"
15import "nx_prover.nx"
16import "nx_prover_eval.nx"
17
18func main() -> i64 {
19 let sum: *EvalSummary = nx_eval_summary_alloc()
20 let result: *EvalResult = (sys_mmap(NX_EVAL_RESULT_BYTES)) as *EvalResult
21
22 // === Case 1: trivial axiom citation (target = axiom stmt_id 1) ===
23 let axs1: *i64 = (sys_mmap(8)) as *i64
24 axs1[0] = NX_AX_PEANO_PA1_ZERO_EXISTS
25 let impls1: *i64 = (sys_mmap(8)) as *i64
26 nx_eval_run_case(1, axs1, 1, impls1, 0, 1, 10, result)
27 if result.outcome != NX_EVAL_OUTCOME_PROVED { return 11 }
28 nx_eval_accumulate(sum, result)
29
30 // === Case 2: 2-step chain (1 -> 2 -> 3, target 3) ===
31 let axs2: *i64 = (sys_mmap(8)) as *i64
32 axs2[0] = NX_AX_PEANO_PA1_ZERO_EXISTS
33 let impls2: *i64 = (sys_mmap(40)) as *i64
34 impls2[0] = 1; impls2[1] = 2
35 impls2[2] = 2; impls2[3] = 3
36 nx_eval_run_case(2, axs2, 1, impls2, 2, 3, 10, result)
37 if result.outcome != NX_EVAL_OUTCOME_PROVED { return 12 }
38 nx_eval_accumulate(sum, result)
39
40 // === Case 3: 5-step chain (1 -> 2 -> 3 -> 4 -> 5 -> 6, target 6) ===
41 let axs3: *i64 = (sys_mmap(8)) as *i64
42 axs3[0] = NX_AX_PEANO_PA1_ZERO_EXISTS
43 let impls3: *i64 = (sys_mmap(80)) as *i64
44 var i3: i64 = 0
45 while i3 < 5 {
46 impls3[i3 * 2] = i3 + 1
47 impls3[i3 * 2 + 1] = i3 + 2
48 i3 = i3 + 1
49 }
50 nx_eval_run_case(3, axs3, 1, impls3, 5, 6, 10, result)
51 if result.outcome != NX_EVAL_OUTCOME_PROVED { return 13 }
52 nx_eval_accumulate(sum, result)
53
54 // === Case 4: 10-step chain ===
55 let impls4: *i64 = (sys_mmap(160)) as *i64
56 var i4: i64 = 0
57 while i4 < 10 {
58 impls4[i4 * 2] = i4 + 1
59 impls4[i4 * 2 + 1] = i4 + 2
60 i4 = i4 + 1
61 }
62 nx_eval_run_case(4, axs3, 1, impls4, 10, 11, 20, result)
63 if result.outcome != NX_EVAL_OUTCOME_PROVED { return 14 }
64 nx_eval_accumulate(sum, result)
65
66 // === Case 5: wide branching (10 unrelated impls + 1 target-relevant chain) ===
67 let impls5: *i64 = (sys_mmap(200)) as *i64
68 // 10 unrelated implications: 100 -> 101, 200 -> 201, ...
69 var i5: i64 = 0
70 while i5 < 10 {
71 impls5[i5 * 2] = 100 + i5 * 10
72 impls5[i5 * 2 + 1] = 101 + i5 * 10
73 i5 = i5 + 1
74 }
75 // 11th impl: target chain 1 -> 999
76 impls5[20] = 1; impls5[21] = 999
77 nx_eval_run_case(5, axs3, 1, impls5, 11, 999, 20, result)
78 if result.outcome != NX_EVAL_OUTCOME_PROVED { return 15 }
79 nx_eval_accumulate(sum, result)
80
81 // === Case 6: missing premise (target unreachable) ===
82 let impls6: *i64 = (sys_mmap(40)) as *i64
83 impls6[0] = 50; impls6[1] = 51 // axiom is 1; impl needs 50
84 nx_eval_run_case(6, axs3, 1, impls6, 1, 51, 10, result)
85 if result.outcome != NX_EVAL_OUTCOME_NO_RULES { return 16 }
86 nx_eval_accumulate(sum, result)
87
88 // === Case 7: beyond budget (50-step chain, budget 10) ===
89 let impls7: *i64 = (sys_mmap(800)) as *i64
90 var i7: i64 = 0
91 while i7 < 50 {
92 impls7[i7 * 2] = i7 + 1
93 impls7[i7 * 2 + 1] = i7 + 2
94 i7 = i7 + 1
95 }
96 nx_eval_run_case(7, axs3, 1, impls7, 50, 51, 10, result)
97 // Phase A0 adds one new fact per cycle when an impl applies;
98 // with budget 10 we reach fact 11, not target 51. Should be
99 // FAILED_BUDGET (not NO_RULES because rules ARE applying).
100 if result.outcome != NX_EVAL_OUTCOME_FAILED_BUDGET { return 17 }
101 nx_eval_accumulate(sum, result)
102
103 // === Case 8: same 50-step chain with generous budget 200 ===
104 nx_eval_run_case(8, axs3, 1, impls7, 50, 51, 200, result)
105 if result.outcome != NX_EVAL_OUTCOME_PROVED { return 18 }
106 nx_eval_accumulate(sum, result)
107
108 // === Summary ===
109 nx_eval_emit_summary(2, sum)
110
111 if sum.n_cases != 8 { return 30 }
112 // We expect 6 PROVED (cases 1-5, 8) + 1 NO_RULES (case 6) + 1 FAILED_BUDGET (case 7).
113 if sum.n_proved != 6 { return 31 }
114 if sum.n_no_rules != 1 { return 32 }
115 if sum.n_failed_budget != 1 { return 33 }
116 // Total cycles should be modest (forward chaining is efficient).
117 if sum.total_cycles > 500 { return 34 }
118 return 0
119}