nx_prover_eval.nx source
↩ module page · 174 lines · 5529 B
1// nx_prover_eval.nx -- honest benchmark of nx_prover capability + timing.
2//
3// Builds realistic test scenarios + measures (a) success rate
4// (b) cycles needed (c) per-theorem wall time. Reports gaps where
5// the current Phase A0 prover (forward chaining + MP) fails.
6//
7// genealogy_id: brodal_okasaki_1996 (data structures) +
8// wos_overbeek_lusk_boyle_1992 (atp benchmarks)
9// lineage_id: theorem_proving_benchmark + timing
10
11// nx_safety_envelope:
12// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
13// sil_target: SIL1
14// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
15// verdict: NOT_YET_EVALUATED
16
17import "syscalls.nx"
18import "nx_axioms.nx"
19import "nx_clock.nx"
20import "nx_derive.nx"
21import "nx_prover.nx"
22
23// ===== eval result =====================================================
24
25const NX_EVAL_OUTCOME_PROVED: i64 = 0
26const NX_EVAL_OUTCOME_FAILED_BUDGET: i64 = 1
27const NX_EVAL_OUTCOME_NO_RULES: i64 = 2
28const NX_EVAL_OUTCOME_TIMEOUT: i64 = 3
29
30struct EvalCase {
31 case_id: i64,
32 name: *u8,
33 n_axioms: i64,
34 n_impls: i64,
35 target_id: i64,
36 expected_depth: i64, // pedagogical: how many MP steps needed
37}
38
39const NX_EVAL_CASE_BYTES: i64 = 40
40
41struct EvalResult {
42 case_id: i64,
43 outcome: i64,
44 cycles: i64,
45 facts_built: i64,
46 elapsed_ns: i64,
47}
48
49const NX_EVAL_RESULT_BYTES: i64 = 40
50
51struct EvalSummary {
52 n_cases: i64,
53 n_proved: i64,
54 n_failed_budget: i64,
55 n_no_rules: i64,
56 n_timeout: i64,
57 total_cycles: i64,
58 total_facts: i64,
59 total_ns: i64,
60}
61
62func nx_eval_summary_alloc() -> *EvalSummary {
63 let raw: *u8 = sys_mmap(64)
64 let s: *EvalSummary = raw as *EvalSummary
65 s.n_cases = 0
66 s.n_proved = 0
67 s.n_failed_budget = 0
68 s.n_no_rules = 0
69 s.n_timeout = 0
70 s.total_cycles = 0
71 s.total_facts = 0
72 s.total_ns = 0
73 return s
74}
75
76// Run one eval case: stand up a prover state with the axiom list +
77// implication table, attempt to prove target_id, time the call,
78// classify the outcome.
79func nx_eval_run_case(case_id: i64,
80 axiom_codes: *i64, n_axioms: i64,
81 impl_table: *i64, n_impls: i64,
82 target_id: i64,
83 cycle_budget: i64,
84 result: *EvalResult) -> i64 {
85 let s: *ProofState = nx_prover_state_alloc(target_id)
86 // Seed axioms. Each axiom gets stmt_id = i+1.
87 var i: i64 = 0
88 while i < n_axioms {
89 nx_prover_add_axiom(s, i + 1, axiom_codes[i])
90 i = i + 1
91 }
92 let t0: i64 = nx_clock_gettime(NX_CLOCK_MONOTONIC)
93 let verdict: i64 = nx_prover_search(s, impl_table, n_impls, cycle_budget)
94 let t1: i64 = nx_clock_gettime(NX_CLOCK_MONOTONIC)
95 result.case_id = case_id
96 result.cycles = s.cycle_count
97 result.facts_built = s.n_facts
98 result.elapsed_ns = t1 - t0
99 if verdict == NX_PROVER_PROVED { result.outcome = NX_EVAL_OUTCOME_PROVED }
100 if verdict == NX_PROVER_NOT_PROVED_BUDGET { result.outcome = NX_EVAL_OUTCOME_FAILED_BUDGET }
101 if verdict == NX_PROVER_NO_RULES_APPLY { result.outcome = NX_EVAL_OUTCOME_NO_RULES }
102 if verdict == NX_PROVER_REFUTED { result.outcome = NX_EVAL_OUTCOME_FAILED_BUDGET }
103 return 0
104}
105
106// Accumulate one result into a summary.
107func nx_eval_accumulate(summary: *EvalSummary, r: *EvalResult) -> i64 {
108 summary.n_cases = summary.n_cases + 1
109 if r.outcome == NX_EVAL_OUTCOME_PROVED { summary.n_proved = summary.n_proved + 1 }
110 if r.outcome == NX_EVAL_OUTCOME_FAILED_BUDGET { summary.n_failed_budget = summary.n_failed_budget + 1 }
111 if r.outcome == NX_EVAL_OUTCOME_NO_RULES { summary.n_no_rules = summary.n_no_rules + 1 }
112 if r.outcome == NX_EVAL_OUTCOME_TIMEOUT { summary.n_timeout = summary.n_timeout + 1 }
113 summary.total_cycles = summary.total_cycles + r.cycles
114 summary.total_facts = summary.total_facts + r.facts_built
115 summary.total_ns = summary.total_ns + r.elapsed_ns
116 return 0
117}
118
119// ===== JSON emit ======================================================
120
121func ev_putc(fd: i64, c: i64) -> i64 {
122 let buf: *u8 = sys_mmap(1)
123 buf[0] = c & 0xFF
124 sys_write(fd, buf, 1)
125 return 0
126}
127
128func ev_str(fd: i64, s: *u8, n: i64) -> i64 {
129 sys_write(fd, s, n)
130 return 0
131}
132
133func ev_i64(fd: i64, n: i64) -> i64 {
134 if n < 0 {
135 ev_putc(fd, 45)
136 return ev_i64(fd, -n)
137 }
138 if n == 0 {
139 ev_putc(fd, 48)
140 return 0
141 }
142 let digits: *u8 = sys_mmap(32)
143 var d: i64 = 0
144 var v: i64 = n
145 while v > 0 {
146 digits[d] = (v % 10) + 48
147 v = v / 10
148 d = d + 1
149 }
150 while d > 0 {
151 d = d - 1
152 ev_putc(fd, digits[d])
153 }
154 return 0
155}
156
157func nx_eval_emit_summary(fd: i64, sum: *EvalSummary) -> i64 {
158 ev_str(fd, "{\"phase\":\"PROVER_EVAL\",\"n_cases\":", 34)
159 ev_i64(fd, sum.n_cases)
160 ev_str(fd, ",\"n_proved\":", 12)
161 ev_i64(fd, sum.n_proved)
162 ev_str(fd, ",\"n_failed_budget\":", 19)
163 ev_i64(fd, sum.n_failed_budget)
164 ev_str(fd, ",\"n_no_rules\":", 14)
165 ev_i64(fd, sum.n_no_rules)
166 ev_str(fd, ",\"total_cycles\":", 16)
167 ev_i64(fd, sum.total_cycles)
168 ev_str(fd, ",\"total_facts\":", 15)
169 ev_i64(fd, sum.total_facts)
170 ev_str(fd, ",\"total_ns\":", 12)
171 ev_i64(fd, sum.total_ns)
172 ev_str(fd, "}\n", 2)
173 return 0
174}