nx_prover.nx source
↩ module page · 236 lines · 8288 B
1// nx_prover.nx -- substrate-native bounded forward-chaining proof search.
2//
3// No AI in the loop. No external prover. Deterministic BFS over the
4// closed inference rules from nx_derive.nx, starting from axioms.
5//
6// Phase A0 capability:
7// * Axiom-citation chains (target == cited axiom)
8// * 1-step modus ponens (premise A and rule A->B in fact set)
9// * Substitution chains (a=b and P(a) in fact set -> P(b))
10// * Bounded cycle + depth
11//
12// genealogy_id: gentzen_1935 (sequent calculus) + robinson_1965 (resolution) +
13// wiedijk_qed_1994 (cross-verification vision)
14// lineage_id: formal_proof_search + bounded_inference
15// axioms: NX_AX_LOGIC_MODUS_PONENS_RULE, NX_AX_LOGIC_IDENTITY
16
17// nx_safety_envelope:
18// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
19// sil_target: SIL1
20// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
21// verdict: NOT_YET_EVALUATED
22
23import "syscalls.nx"
24import "nx_axioms.nx"
25import "nx_derive.nx"
26
27// ===== sealed verdicts =================================================
28
29const NX_PROVER_PROVED: i64 = 0
30const NX_PROVER_NOT_PROVED_BUDGET: i64 = 1
31const NX_PROVER_REFUTED: i64 = 2
32const NX_PROVER_NO_RULES_APPLY: i64 = 3
33
34// ===== fact set =======================================================
35//
36// Facts are tagged i64 statement IDs (caller assigns). Facts marked
37// AXIOM are leaves; INFERRED facts must reference their parent facts.
38//
39// For Phase A0 we track a flat array of fact IDs known to be true.
40// Each fact carries a kind tag (AXIOM or INFERRED) and parent indices
41// when applicable.
42
43struct Fact {
44 stmt_id: i64, // caller-defined
45 axiom_code: i64, // if kind==AXIOM, the NX_AX_* code; else 0
46 parent_a: i64, // -1 if root
47 parent_b: i64, // -1 if not 2-premise
48 rule_id: i64, // NX_DRULE_* used to derive
49 depth: i64, // distance from axiom leaves
50}
51
52const NX_FACT_BYTES: i64 = 48
53
54struct ProofState {
55 facts: *Fact,
56 n_facts: i64,
57 capacity: i64,
58 target: i64, // target stmt_id
59 cycle_count: i64,
60 found_idx: i64, // index of fact matching target, or -1
61}
62
63const NX_PROVER_MAX_FACTS: i64 = 1024
64
65func nx_prover_state_alloc(target: i64) -> *ProofState {
66 let raw: *u8 = sys_mmap(40)
67 let s: *ProofState = raw as *ProofState
68 s.facts = (sys_mmap(NX_PROVER_MAX_FACTS * NX_FACT_BYTES)) as *Fact
69 s.n_facts = 0
70 s.capacity = NX_PROVER_MAX_FACTS
71 s.target = target
72 s.cycle_count = 0
73 s.found_idx = -1
74 return s
75}
76
77func nx_prover_fact_at(s: *ProofState, i: i64) -> *Fact {
78 return (((s.facts as i64) + i * NX_FACT_BYTES) as *Fact)
79}
80
81// Add an axiom fact. Returns its index in the fact set.
82func nx_prover_add_axiom(s: *ProofState, stmt_id: i64, axiom_code: i64) -> i64 {
83 if s.n_facts >= s.capacity { return -1 }
84 if nx_axiom_is_valid(axiom_code) == 0 { return -2 }
85 let f: *Fact = nx_prover_fact_at(s, s.n_facts)
86 f.stmt_id = stmt_id
87 f.axiom_code = axiom_code
88 f.parent_a = -1
89 f.parent_b = -1
90 f.rule_id = NX_DRULE_AXIOM_CITATION
91 f.depth = 0
92 let idx: i64 = s.n_facts
93 s.n_facts = s.n_facts + 1
94 if stmt_id == s.target { s.found_idx = idx }
95 return idx
96}
97
98// Add an inferred fact. Returns its index.
99func nx_prover_add_inferred(s: *ProofState, stmt_id: i64,
100 rule: i64, parent_a: i64, parent_b: i64) -> i64 {
101 if s.n_facts >= s.capacity { return -1 }
102 if parent_a < 0 { return -2 }
103 if parent_a >= s.n_facts { return -3 }
104 let f: *Fact = nx_prover_fact_at(s, s.n_facts)
105 f.stmt_id = stmt_id
106 f.axiom_code = 0
107 f.parent_a = parent_a
108 f.parent_b = parent_b
109 f.rule_id = rule
110 let fa: *Fact = nx_prover_fact_at(s, parent_a)
111 var max_pd: i64 = fa.depth
112 if parent_b >= 0 {
113 if parent_b < s.n_facts {
114 let fb: *Fact = nx_prover_fact_at(s, parent_b)
115 let pd_b: i64 = fb.depth
116 if pd_b > max_pd { max_pd = pd_b }
117 }
118 }
119 f.depth = max_pd + 1
120 let idx: i64 = s.n_facts
121 s.n_facts = s.n_facts + 1
122 if stmt_id == s.target { s.found_idx = idx }
123 return idx
124}
125
126// Check if a target stmt_id is already in the fact set.
127func nx_prover_has_target(s: *ProofState) -> i64 {
128 if s.found_idx >= 0 { return 1 }
129 var i: i64 = 0
130 while i < s.n_facts {
131 let f: *Fact = nx_prover_fact_at(s, i)
132 if f.stmt_id == s.target {
133 s.found_idx = i
134 return 1
135 }
136 i = i + 1
137 }
138 return 0
139}
140
141// Has a specific stmt_id been derived?
142func nx_prover_has_stmt(s: *ProofState, stmt: i64) -> i64 {
143 var i: i64 = 0
144 while i < s.n_facts {
145 let f: *Fact = nx_prover_fact_at(s, i)
146 if f.stmt_id == stmt { return 1 }
147 i = i + 1
148 }
149 return 0
150}
151
152// ===== search step (forward chaining via modus-ponens-like rule)
153//
154// For Phase A0: each (premise, implication) pair where premise has
155// stmt_id = P and there's an "implication" stmt_id of the form
156// "P -> Q" produces a new fact Q.
157//
158// Implication facts are represented as pairs of stmt_ids in a separate
159// implication table. The caller registers known implications before
160// invoking search.
161//
162// implication_table[i*2] = premise_stmt
163// implication_table[i*2+1] = conclusion_stmt
164//
165// Substrate cycle: scan implications; for each whose premise is in
166// fact set, derive conclusion as new fact.
167
168func nx_prover_step_mp(s: *ProofState, impl_table: *i64, n_impls: i64) -> i64 {
169 var i: i64 = 0
170 var new_added: i64 = 0
171 while i < n_impls {
172 let p_stmt: i64 = impl_table[i * 2]
173 let q_stmt: i64 = impl_table[i * 2 + 1]
174 if nx_prover_has_stmt(s, p_stmt) == 1 {
175 if nx_prover_has_stmt(s, q_stmt) == 0 {
176 // Find premise index.
177 var prem_idx: i64 = -1
178 var j: i64 = 0
179 while j < s.n_facts {
180 let fj: *Fact = nx_prover_fact_at(s, j)
181 if fj.stmt_id == p_stmt { prem_idx = j; j = s.n_facts }
182 j = j + 1
183 }
184 if prem_idx >= 0 {
185 nx_prover_add_inferred(s, q_stmt, NX_DRULE_MODUS_PONENS,
186 prem_idx, -1)
187 new_added = new_added + 1
188 }
189 }
190 }
191 i = i + 1
192 }
193 return new_added
194}
195
196// ===== top-level search ===============================================
197//
198// Iterates modus-ponens steps until target found, no progress, or
199// cycle budget exhausted.
200
201func nx_prover_search(s: *ProofState, impl_table: *i64, n_impls: i64,
202 cycle_budget: i64) -> i64 {
203 if nx_prover_has_target(s) == 1 { return NX_PROVER_PROVED }
204 var cycles: i64 = 0
205 while cycles < cycle_budget {
206 let added: i64 = nx_prover_step_mp(s, impl_table, n_impls)
207 cycles = cycles + 1
208 s.cycle_count = cycles
209 if nx_prover_has_target(s) == 1 { return NX_PROVER_PROVED }
210 if added == 0 { return NX_PROVER_NO_RULES_APPLY }
211 }
212 return NX_PROVER_NOT_PROVED_BUDGET
213}
214
215// ===== chain reconstruction ============================================
216//
217// Once target found, walk parent chain to build a DerivationChain
218// from nx_derive.nx. Caller passes pre-allocated chain.
219
220func nx_prover_build_chain(s: *ProofState, chain: *DerivationChain) -> i64 {
221 if s.found_idx < 0 { return -1 }
222 // Walk facts and add to chain in topological (index) order.
223 var i: i64 = 0
224 while i <= s.found_idx {
225 let f: *Fact = nx_prover_fact_at(s, i)
226 if f.rule_id == NX_DRULE_AXIOM_CITATION {
227 nx_deriv_add_axiom(chain, f.stmt_id, f.axiom_code)
228 }
229 if f.rule_id != NX_DRULE_AXIOM_CITATION {
230 nx_deriv_add_step(chain, f.stmt_id, f.rule_id, f.parent_a, f.parent_b)
231 }
232 i = i + 1
233 }
234 nx_deriv_mark_theorem(chain)
235 return 0
236}