nx_derive.nx source
↩ module page · 342 lines · 12821 B
1// nx_derive.nx -- verifiable derivation chains from axioms to theorems.
2//
3// "A mathematician can start from zero and build all the way into what
4// they are proposing or proving." -- user, 2026-05-10
5//
6// This primitive enforces that discipline: every theorem the substrate
7// claims must show a derivation chain rooted in the foundational
8// axioms (nx_axioms.nx). Substrate runs nx_derive_verify on each
9// chain; any chain with an unrecognized axiom OR an unsupported rule
10// is REJECTED.
11//
12// A derivation is a DAG of DerivationNode nodes:
13// - LEAF nodes cite an axiom (axiom_code != 0)
14// - INTERNAL nodes cite a rule_id + premise_ids
15// - One node is marked as the THEOREM (the derivation's conclusion)
16//
17// Rules supported (closed enum):
18// modus_ponens A, A->B |- B
19// modus_tollens ~B, A->B |- ~A
20// universal_instant forall x P(x) |- P(t)
21// existential_gen P(t) |- exists x P(x)
22// substitution A=B, P(A) |- P(B)
23// induction P(0), P(n)->P(n+1) |- forall n P(n)
24// conjunction_intro A, B |- A^B
25// conjunction_elim A^B |- A (or B)
26// disjunction_intro A |- A v B
27// contradiction A, ~A |- false
28// contraposition A->B |- ~B->~A
29// transitivity_eq A=B, B=C |- A=C
30// trans_inequality A<=B, B<=C |- A<=C
31//
32// genealogy_id: hilbert_1899 + frege_1879 + russell_whitehead_1910
33// lineage_id: formal_proof_theory
34
35// nx_safety_envelope:
36// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
37// sil_target: SIL1
38// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
39// verdict: NOT_YET_EVALUATED
40
41import "syscalls.nx"
42import "nx_axioms.nx"
43
44// ===== rule IDs (sealed enum) ===========================================
45
46const NX_DRULE_AXIOM_CITATION: i64 = 0
47const NX_DRULE_MODUS_PONENS: i64 = 1
48const NX_DRULE_MODUS_TOLLENS: i64 = 2
49const NX_DRULE_UNIVERSAL_INSTANT: i64 = 3
50const NX_DRULE_EXISTENTIAL_GEN: i64 = 4
51const NX_DRULE_SUBSTITUTION: i64 = 5
52const NX_DRULE_INDUCTION: i64 = 6
53const NX_DRULE_CONJ_INTRO: i64 = 7
54const NX_DRULE_CONJ_ELIM: i64 = 8
55const NX_DRULE_DISJ_INTRO: i64 = 9
56const NX_DRULE_CONTRADICTION: i64 = 10
57const NX_DRULE_CONTRAPOSITION: i64 = 11
58const NX_DRULE_TRANSITIVITY_EQ: i64 = 12
59const NX_DRULE_TRANS_INEQUALITY: i64 = 13
60const NX_DRULE_ALGEBRA_REWRITE: i64 = 14 // e.g., distributivity application
61const NX_DRULE_DEFINITION: i64 = 15 // expansion of a definition
62
63func nx_drule_name(code: i64) -> *u8 {
64 if code == NX_DRULE_AXIOM_CITATION { return "axiom citation" }
65 if code == NX_DRULE_MODUS_PONENS { return "modus ponens" }
66 if code == NX_DRULE_MODUS_TOLLENS { return "modus tollens" }
67 if code == NX_DRULE_UNIVERSAL_INSTANT { return "universal instantiation" }
68 if code == NX_DRULE_EXISTENTIAL_GEN { return "existential generalization" }
69 if code == NX_DRULE_SUBSTITUTION { return "substitution of equals" }
70 if code == NX_DRULE_INDUCTION { return "mathematical induction" }
71 if code == NX_DRULE_CONJ_INTRO { return "conjunction introduction" }
72 if code == NX_DRULE_CONJ_ELIM { return "conjunction elimination" }
73 if code == NX_DRULE_DISJ_INTRO { return "disjunction introduction" }
74 if code == NX_DRULE_CONTRADICTION { return "contradiction" }
75 if code == NX_DRULE_CONTRAPOSITION { return "contraposition" }
76 if code == NX_DRULE_TRANSITIVITY_EQ { return "transitivity of equality" }
77 if code == NX_DRULE_TRANS_INEQUALITY { return "transitivity of inequality" }
78 if code == NX_DRULE_ALGEBRA_REWRITE { return "algebraic rewrite" }
79 if code == NX_DRULE_DEFINITION { return "definition expansion" }
80 return "unknown rule"
81}
82
83// Number of premises a rule requires. Used by verifier to check arity.
84func nx_drule_arity(code: i64) -> i64 {
85 if code == NX_DRULE_AXIOM_CITATION { return 0 }
86 if code == NX_DRULE_MODUS_PONENS { return 2 }
87 if code == NX_DRULE_MODUS_TOLLENS { return 2 }
88 if code == NX_DRULE_UNIVERSAL_INSTANT { return 1 }
89 if code == NX_DRULE_EXISTENTIAL_GEN { return 1 }
90 if code == NX_DRULE_SUBSTITUTION { return 2 }
91 if code == NX_DRULE_INDUCTION { return 2 } // P(0), P(n)->P(n+1)
92 if code == NX_DRULE_CONJ_INTRO { return 2 }
93 if code == NX_DRULE_CONJ_ELIM { return 1 }
94 if code == NX_DRULE_DISJ_INTRO { return 1 }
95 if code == NX_DRULE_CONTRADICTION { return 2 }
96 if code == NX_DRULE_CONTRAPOSITION { return 1 }
97 if code == NX_DRULE_TRANSITIVITY_EQ { return 2 }
98 if code == NX_DRULE_TRANS_INEQUALITY { return 2 }
99 if code == NX_DRULE_ALGEBRA_REWRITE { return 1 }
100 if code == NX_DRULE_DEFINITION { return 1 }
101 return -1
102}
103
104// ===== node + chain structures =========================================
105//
106// Each node has fixed slots for up to 2 premise indices (sufficient
107// for binary rules). For induction the two slots are P(0) and the
108// step P(n)->P(n+1) — exactly 2.
109//
110// Stmt is a free-form i64 statement ID (caller-defined; the substrate
111// doesn't interpret statements, only verifies that the structure is
112// valid -- node X cites a rule whose arity matches the number of
113// premises, and any axiom citation references a valid NX_AX_* code).
114
115struct DerivationNode {
116 node_id: i64, // self
117 rule_id: i64, // sealed NX_DRULE_*
118 axiom_code: i64, // if rule_id == AXIOM_CITATION; else 0
119 premise_a: i64, // index of first premise (or -1)
120 premise_b: i64, // index of second premise (or -1)
121 stmt_id: i64, // caller-assigned statement identifier
122 is_theorem: i64, // 1 if this is the conclusion node
123}
124
125const NX_DERIV_NODE_BYTES: i64 = 56
126
127struct DerivationChain {
128 nodes: *DerivationNode,
129 n_nodes: i64,
130 capacity: i64,
131}
132
133func nx_deriv_chain_alloc(capacity: i64) -> *DerivationChain {
134 let raw: *u8 = sys_mmap(24)
135 let ch: *DerivationChain = raw as *DerivationChain
136 ch.nodes = (sys_mmap(capacity * NX_DERIV_NODE_BYTES)) as *DerivationNode
137 ch.n_nodes = 0
138 ch.capacity = capacity
139 return ch
140}
141
142func nx_deriv_node_at(ch: *DerivationChain, i: i64) -> *DerivationNode {
143 return (((ch.nodes as i64) + i * NX_DERIV_NODE_BYTES) as *DerivationNode)
144}
145
146// Append an axiom-citation leaf node. Returns the node index.
147func nx_deriv_add_axiom(ch: *DerivationChain, stmt_id: i64,
148 axiom_code: i64) -> i64 {
149 if ch.n_nodes >= ch.capacity { return -1 }
150 if nx_axiom_is_valid(axiom_code) == 0 { return -2 }
151 let n: *DerivationNode = nx_deriv_node_at(ch, ch.n_nodes)
152 n.node_id = ch.n_nodes
153 n.rule_id = NX_DRULE_AXIOM_CITATION
154 n.axiom_code = axiom_code
155 n.premise_a = -1
156 n.premise_b = -1
157 n.stmt_id = stmt_id
158 n.is_theorem = 0
159 let idx: i64 = ch.n_nodes
160 ch.n_nodes = ch.n_nodes + 1
161 return idx
162}
163
164// Append an internal node. Returns the node index or negative error.
165func nx_deriv_add_step(ch: *DerivationChain, stmt_id: i64,
166 rule_id: i64, prem_a: i64, prem_b: i64) -> i64 {
167 if ch.n_nodes >= ch.capacity { return -1 }
168 let arity: i64 = nx_drule_arity(rule_id)
169 if arity < 0 { return -3 } // unknown rule
170 // Premise count must match rule arity.
171 if arity == 1 {
172 if prem_a < 0 { return -4 }
173 if prem_b != -1 { return -5 }
174 }
175 if arity == 2 {
176 if prem_a < 0 { return -4 }
177 if prem_b < 0 { return -4 }
178 }
179 if arity == 0 { // shouldn't happen here
180 return -6
181 }
182 if prem_a >= ch.n_nodes { return -7 }
183 if arity == 2 {
184 if prem_b >= ch.n_nodes { return -7 }
185 }
186 let n: *DerivationNode = nx_deriv_node_at(ch, ch.n_nodes)
187 n.node_id = ch.n_nodes
188 n.rule_id = rule_id
189 n.axiom_code = 0
190 n.premise_a = prem_a
191 n.premise_b = prem_b
192 n.stmt_id = stmt_id
193 n.is_theorem = 0
194 let idx: i64 = ch.n_nodes
195 ch.n_nodes = ch.n_nodes + 1
196 return idx
197}
198
199// Mark the last-added node as the theorem (conclusion).
200func nx_deriv_mark_theorem(ch: *DerivationChain) -> i64 {
201 if ch.n_nodes <= 0 { return -1 }
202 let n: *DerivationNode = nx_deriv_node_at(ch, ch.n_nodes - 1)
203 n.is_theorem = 1
204 return 0
205}
206
207// ===== verifier =========================================================
208//
209// Verify that every node is structurally valid:
210// - axiom leaves cite a recognized NX_AX_* code
211// - internal nodes cite a known rule with matching arity
212// - premise indices reference earlier nodes (topological order)
213// - exactly one node is marked as the theorem
214//
215// Returns 0 on PASS; negative code on FAIL.
216
217const NX_DERIV_VERIFY_OK: i64 = 0
218const NX_DERIV_VERIFY_NO_NODES: i64 = -10
219const NX_DERIV_VERIFY_UNKNOWN_AXIOM: i64 = -11
220const NX_DERIV_VERIFY_UNKNOWN_RULE: i64 = -12
221const NX_DERIV_VERIFY_ARITY_MISMATCH: i64 = -13
222const NX_DERIV_VERIFY_PREMISE_OUT_OF_ORDER: i64 = -14
223const NX_DERIV_VERIFY_NO_THEOREM: i64 = -15
224const NX_DERIV_VERIFY_MULTIPLE_THEOREMS: i64 = -16
225
226func nx_deriv_verify(ch: *DerivationChain) -> i64 {
227 if ch.n_nodes <= 0 { return NX_DERIV_VERIFY_NO_NODES }
228 var theorem_count: i64 = 0
229 var i: i64 = 0
230 while i < ch.n_nodes {
231 let n: *DerivationNode = nx_deriv_node_at(ch, i)
232 if n.rule_id == NX_DRULE_AXIOM_CITATION {
233 if nx_axiom_is_valid(n.axiom_code) == 0 {
234 return NX_DERIV_VERIFY_UNKNOWN_AXIOM
235 }
236 }
237 if n.rule_id != NX_DRULE_AXIOM_CITATION {
238 let arity: i64 = nx_drule_arity(n.rule_id)
239 if arity < 0 { return NX_DERIV_VERIFY_UNKNOWN_RULE }
240 if arity >= 1 {
241 if n.premise_a < 0 { return NX_DERIV_VERIFY_ARITY_MISMATCH }
242 if n.premise_a >= i { return NX_DERIV_VERIFY_PREMISE_OUT_OF_ORDER }
243 }
244 if arity == 2 {
245 if n.premise_b < 0 { return NX_DERIV_VERIFY_ARITY_MISMATCH }
246 if n.premise_b >= i { return NX_DERIV_VERIFY_PREMISE_OUT_OF_ORDER }
247 }
248 if arity == 1 {
249 if n.premise_b != -1 { return NX_DERIV_VERIFY_ARITY_MISMATCH }
250 }
251 }
252 if n.is_theorem == 1 { theorem_count = theorem_count + 1 }
253 i = i + 1
254 }
255 if theorem_count == 0 { return NX_DERIV_VERIFY_NO_THEOREM }
256 if theorem_count > 1 { return NX_DERIV_VERIFY_MULTIPLE_THEOREMS }
257 return NX_DERIV_VERIFY_OK
258}
259
260// ===== walker (emits derivation chain to fd) ===========================
261//
262// Used by primitives to explain their lineage from axioms up. Format:
263// step i: rule=<name> from premises {a,b} -> stmt #N
264// step j: axiom <code>=<name> -> stmt #N
265// theorem stmt #M
266
267func dw_putc(fd: i64, c: i64) -> i64 {
268 let buf: *u8 = sys_mmap(1)
269 buf[0] = c & 0xFF
270 sys_write(fd, buf, 1)
271 return 0
272}
273
274func dw_str(fd: i64, s: *u8, len: i64) -> i64 {
275 sys_write(fd, s, len)
276 return 0
277}
278
279func dw_strz(fd: i64, s: *u8) -> i64 {
280 var i: i64 = 0
281 while s[i] != 0 { i = i + 1 }
282 sys_write(fd, s, i)
283 return i
284}
285
286func dw_i64(fd: i64, n: i64) -> i64 {
287 if n < 0 {
288 dw_putc(fd, 45)
289 return dw_i64(fd, -n)
290 }
291 if n == 0 {
292 dw_putc(fd, 48)
293 return 0
294 }
295 let digits: *u8 = sys_mmap(32)
296 var d: i64 = 0
297 var v: i64 = n
298 while v > 0 {
299 digits[d] = (v % 10) + 48
300 v = v / 10
301 d = d + 1
302 }
303 while d > 0 {
304 d = d - 1
305 dw_putc(fd, digits[d])
306 }
307 return 0
308}
309
310func nx_deriv_walk(fd: i64, ch: *DerivationChain) -> i64 {
311 var i: i64 = 0
312 while i < ch.n_nodes {
313 let n: *DerivationNode = nx_deriv_node_at(ch, i)
314 dw_str(fd, "step ", 5)
315 dw_i64(fd, i)
316 dw_str(fd, ": ", 2)
317 if n.rule_id == NX_DRULE_AXIOM_CITATION {
318 dw_str(fd, "AXIOM ", 6)
319 dw_i64(fd, n.axiom_code)
320 dw_str(fd, " (", 2)
321 dw_strz(fd, nx_axiom_name(n.axiom_code))
322 dw_str(fd, ")", 1)
323 }
324 if n.rule_id != NX_DRULE_AXIOM_CITATION {
325 dw_str(fd, "rule ", 5)
326 dw_strz(fd, nx_drule_name(n.rule_id))
327 dw_str(fd, " from {", 7)
328 dw_i64(fd, n.premise_a)
329 if n.premise_b >= 0 {
330 dw_str(fd, ",", 1)
331 dw_i64(fd, n.premise_b)
332 }
333 dw_str(fd, "}", 1)
334 }
335 dw_str(fd, " -> stmt#", 9)
336 dw_i64(fd, n.stmt_id)
337 if n.is_theorem == 1 { dw_str(fd, " [THEOREM]", 11) }
338 dw_str(fd, "\n", 1)
339 i = i + 1
340 }
341 return 0
342}