nx_theorem_ingest.nx source
↩ module page · 416 lines · 17572 B
1// nx_theorem_ingest.nx -- ingest machine-readable theorem corpora.
2//
3// Strategy doc: docs/THEOREM_INGESTION_STRATEGY.md
4//
5// Phase P0 implementation: minimal MetaMath-style tokenizer + chain
6// builder + ingestion driver. Reads a corpus from disk via
7// sys_read_file, parses statements, translates proof tokens into
8// DerivationChain objects, runs nx_deriv_verify, emits ledger entry.
9//
10// MetaMath statement grammar (subset we accept in P0):
11//
12// $c c1 c2 ... $. declare constants
13// $v v1 v2 ... $. declare variables
14// $f label v term $. variable-type hypothesis
15// $e label term $. logical hypothesis
16// $a label term $. axiom assertion
17// $p label term $= proof-tokens $. provable theorem with proof
18// $( comment $) comment block
19// ${ ... $} scope block
20//
21// We focus on $a / $p / $e since those carry the substrate-relevant
22// structure. $c / $v / $f are tracked as a symbol table.
23//
24// genealogy_id: megill_metamath_1992 + russell_whitehead_1910 (formal_proof)
25// lineage_id: formal_proof_theory + token_substitution
26
27// nx_safety_envelope:
28// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
29// sil_target: SIL1
30// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
31// verdict: NOT_YET_EVALUATED
32
33import "syscalls.nx"
34import "nx_axioms.nx"
35import "nx_derive.nx"
36import "nx_lex.nx"
37import "nx_loop.nx"
38
39// ===== sealed status codes =============================================
40
41const NX_INGEST_OK: i64 = 0
42const NX_INGEST_TOKENIZE_ERROR: i64 = -1
43const NX_INGEST_UNKNOWN_STATEMENT: i64 = -2
44const NX_INGEST_UNMAPPED_AXIOM: i64 = -3
45const NX_INGEST_VERIFY_FAILED: i64 = -4
46const NX_INGEST_OUT_OF_CAPACITY: i64 = -5
47const NX_INGEST_BAD_PROOF_TOKEN: i64 = -6
48
49// ===== token kinds =====================================================
50
51const NX_MM_TOK_NONE: i64 = 0
52const NX_MM_TOK_LABEL: i64 = 1 // identifier
53const NX_MM_TOK_DOLLAR_A: i64 = 2 // $a
54const NX_MM_TOK_DOLLAR_P: i64 = 3 // $p
55const NX_MM_TOK_DOLLAR_E: i64 = 4 // $e
56const NX_MM_TOK_DOLLAR_F: i64 = 5 // $f
57const NX_MM_TOK_DOLLAR_C: i64 = 6 // $c
58const NX_MM_TOK_DOLLAR_V: i64 = 7 // $v
59const NX_MM_TOK_DOLLAR_EQ: i64 = 8 // $=
60const NX_MM_TOK_DOLLAR_DOT: i64 = 9 // $.
61const NX_MM_TOK_DOLLAR_LBR: i64 = 10 // ${
62const NX_MM_TOK_DOLLAR_RBR: i64 = 11 // $}
63const NX_MM_TOK_DOLLAR_LPAREN: i64 = 12 // $(
64const NX_MM_TOK_DOLLAR_RPAREN: i64 = 13 // $)
65
66// ===== ingest state ====================================================
67//
68// Maintains a database of labeled statements as we walk the corpus.
69// For P0 we cap capacities at modest values; later phases scale up.
70
71const NX_INGEST_MAX_THEOREMS: i64 = 1024
72const NX_INGEST_MAX_LABEL_LEN: i64 = 64
73const NX_INGEST_THEOREM_BYTES: i64 = 88 // label(64) + kind(8) + n_proof(8) + chain(8)
74
75struct IngestTheorem {
76 label: *u8, // string ptr (NX_INGEST_MAX_LABEL_LEN bytes)
77 kind: i64, // NX_MM_TOK_DOLLAR_A or _P
78 n_proof: i64, // proof token count (P only)
79 chain: *DerivationChain, // verified chain (P only)
80}
81
82struct IngestDb {
83 theorems: *IngestTheorem,
84 n_theorems: i64,
85 capacity: i64,
86 n_passed: i64, // PASSED nx_deriv_verify
87 n_rejected: i64, // verify rejected
88}
89
90func nx_ingest_db_alloc() -> *IngestDb {
91 let raw: *u8 = sys_mmap(40)
92 let db: *IngestDb = raw as *IngestDb
93 db.theorems = (sys_mmap(NX_INGEST_MAX_THEOREMS * NX_INGEST_THEOREM_BYTES)) as *IngestTheorem
94 db.n_theorems = 0
95 db.capacity = NX_INGEST_MAX_THEOREMS
96 db.n_passed = 0
97 db.n_rejected = 0
98 return db
99}
100
101func nx_ingest_th_at(db: *IngestDb, i: i64) -> *IngestTheorem {
102 return (((db.theorems as i64) + i * NX_INGEST_THEOREM_BYTES) as *IngestTheorem)
103}
104
105// ===== tokenizer =======================================================
106//
107// Tokenizes a buffer character by character. Returns one token kind
108// and writes the label text to `out_label` (if it's a TOK_LABEL).
109// Advances *pos past consumed characters.
110//
111// Whitespace and $( ... $) comment blocks are skipped.
112
113// is_ws canonical in nx_lex.nx (nx_lex_is_ws).
114
115func nx_mm_skip_ws(buf: *u8, pos: *i64, len: i64) -> i64 {
116 while pos[0] < len {
117 let c: i64 = buf[pos[0]]
118 if nx_lex_is_ws(c) == 1 {
119 pos[0] = pos[0] + 1
120 }
121 if c == 36 { // '$'
122 if pos[0] + 1 < len {
123 if buf[pos[0] + 1] == 40 { // '$('
124 pos[0] = pos[0] + 2
125 // Skip until $) -- bound by file length.
126 let lp_c: *NxLoopFrame = nx_loop_begin(len + 1)
127 while nx_loop_step(lp_c) == 1 {
128 if pos[0] + 1 >= len {
129 pos[0] = len
130 nx_loop_break(lp_c)
131 } else {
132 var matched: i64 = 0
133 if buf[pos[0]] == 36 {
134 if buf[pos[0] + 1] == 41 {
135 matched = 1
136 pos[0] = pos[0] + 2
137 }
138 }
139 if matched == 1 {
140 nx_loop_break(lp_c)
141 } else {
142 pos[0] = pos[0] + 1
143 }
144 }
145 }
146 }
147 }
148 if buf[pos[0]] != 36 { return 0 }
149 if pos[0] + 1 < len {
150 if buf[pos[0] + 1] != 40 { return 0 }
151 }
152 }
153 if nx_lex_is_ws(c) == 0 {
154 if c != 36 { return 0 }
155 if pos[0] + 1 < len {
156 if buf[pos[0] + 1] != 40 { return 0 }
157 }
158 if pos[0] + 1 >= len { return 0 }
159 }
160 }
161 return 0
162}
163
164// Returns token kind; writes label (null-terminated) into out_label.
165func nx_mm_next_token(buf: *u8, pos: *i64, len: i64,
166 out_label: *u8) -> i64 {
167 nx_mm_skip_ws(buf, pos, len)
168 if pos[0] >= len { return NX_MM_TOK_NONE }
169 let c0: i64 = buf[pos[0]]
170 if c0 == 36 { // '$' prefix
171 if pos[0] + 1 >= len { return NX_MM_TOK_NONE }
172 let c1: i64 = buf[pos[0] + 1]
173 pos[0] = pos[0] + 2
174 if c1 == 97 { return NX_MM_TOK_DOLLAR_A } // 'a'
175 if c1 == 112 { return NX_MM_TOK_DOLLAR_P } // 'p'
176 if c1 == 101 { return NX_MM_TOK_DOLLAR_E } // 'e'
177 if c1 == 102 { return NX_MM_TOK_DOLLAR_F } // 'f'
178 if c1 == 99 { return NX_MM_TOK_DOLLAR_C } // 'c'
179 if c1 == 118 { return NX_MM_TOK_DOLLAR_V } // 'v'
180 if c1 == 61 { return NX_MM_TOK_DOLLAR_EQ } // '='
181 if c1 == 46 { return NX_MM_TOK_DOLLAR_DOT } // '.'
182 if c1 == 123 { return NX_MM_TOK_DOLLAR_LBR } // '{'
183 if c1 == 125 { return NX_MM_TOK_DOLLAR_RBR } // '}'
184 return NX_MM_TOK_NONE
185 }
186 // Otherwise label: read until ws or $.
187 var i: i64 = 0
188 while pos[0] < len {
189 let c: i64 = buf[pos[0]]
190 if nx_lex_is_ws(c) == 1 { pos[0] = pos[0] + 0 ; }
191 if nx_lex_is_ws(c) == 1 {
192 out_label[i] = 0
193 return NX_MM_TOK_LABEL
194 }
195 if c == 36 {
196 out_label[i] = 0
197 return NX_MM_TOK_LABEL
198 }
199 if i < NX_INGEST_MAX_LABEL_LEN - 1 {
200 out_label[i] = c
201 i = i + 1
202 }
203 pos[0] = pos[0] + 1
204 }
205 out_label[i] = 0
206 return NX_MM_TOK_LABEL
207}
208
209// ===== axiom-name to nx_axioms.nx code mapping ========================
210//
211// For P0 we hand-code a small dictionary; phase P1 will load a full
212// dictionary from a .mmd (metamath-dictionary) sidecar file.
213
214func nx_ingest_axiom_lookup(name: *u8) -> i64 {
215 // ax-mp -> modus ponens
216 if name[0] == 97 { // 'a'
217 if name[1] == 120 { // 'x'
218 if name[2] == 45 { // '-'
219 if name[3] == 109 { // 'm'
220 if name[4] == 112 { // 'p'
221 return NX_AX_LOGIC_MODUS_PONENS_RULE
222 }
223 }
224 if name[3] == 49 { // '1' (ax-1)
225 return NX_AX_LOGIC_IDENTITY
226 }
227 if name[3] == 50 { // '2'
228 return NX_AX_LOGIC_NONCONTRADICTION
229 }
230 if name[3] == 51 { // '3'
231 return NX_AX_LOGIC_EXCLUDED_MIDDLE
232 }
233 }
234 }
235 }
236 // peano-style: pa1..pa5
237 if name[0] == 112 { // 'p'
238 if name[1] == 97 { // 'a'
239 if name[2] == 49 { return NX_AX_PEANO_PA1_ZERO_EXISTS }
240 if name[2] == 50 { return NX_AX_PEANO_PA2_SUCCESSOR }
241 if name[2] == 51 { return NX_AX_PEANO_PA3_ZERO_NOT_SUCC }
242 if name[2] == 52 { return NX_AX_PEANO_PA4_SUCC_INJECTIVE }
243 if name[2] == 53 { return NX_AX_PEANO_PA5_INDUCTION }
244 }
245 }
246 // zfc: zf-ext (extensionality), zf-pair, etc.
247 if name[0] == 122 { // 'z'
248 if name[1] == 102 { // 'f'
249 if name[2] == 45 { // '-'
250 if name[3] == 101 { return NX_AX_ZFC_EXTENSIONALITY } // 'e'
251 if name[3] == 112 { return NX_AX_ZFC_PAIRING } // 'p'
252 if name[3] == 117 { return NX_AX_ZFC_UNION } // 'u'
253 if name[3] == 99 { return NX_AX_ZFC_CHOICE } // 'c'
254 }
255 }
256 }
257 return 0 // unknown
258}
259
260// ===== minimal ingest driver ==========================================
261//
262// Tokenize the corpus. For each top-level $a or $p / $e statement,
263// pick the label (precedes the $-keyword) and either:
264// - register the labeled axiom ($a) into the database;
265// - for $p, run the proof through nx_derive_verify by translating
266// each proof token to either an axiom citation (if mapped) or
267// a reference to a previously-ingested theorem.
268//
269// The proof translation: every proof token is either
270// - a $a label (axiom citation -> nx_deriv_add_axiom)
271// - a previously-ingested $p label (theorem reference; here we
272// model it as another axiom citation since our verifier doesn't
273// distinguish axiom-cited leaves from theorem-cited leaves --
274// both are leaves in the local chain)
275//
276// Returns the database with n_passed / n_rejected counts populated.
277
278func nx_ingest_corpus(buf: *u8, len: i64) -> *IngestDb {
279 let db: *IngestDb = nx_ingest_db_alloc()
280 let pos: *i64 = (sys_mmap(8)) as *i64
281 pos[0] = 0
282 let label_buf: *u8 = sys_mmap(NX_INGEST_MAX_LABEL_LEN)
283 let pending: *u8 = sys_mmap(NX_INGEST_MAX_LABEL_LEN)
284 pending[0] = 0
285
286 while pos[0] < len {
287 let tok: i64 = nx_mm_next_token(buf, pos, len, label_buf)
288 if tok == NX_MM_TOK_NONE { return db }
289 if tok == NX_MM_TOK_LABEL {
290 // Remember this label as a potential statement name.
291 var i: i64 = 0
292 while i < NX_INGEST_MAX_LABEL_LEN {
293 pending[i] = label_buf[i]
294 if label_buf[i] == 0 { i = NX_INGEST_MAX_LABEL_LEN }
295 if i < NX_INGEST_MAX_LABEL_LEN { i = i + 1 }
296 }
297 }
298 if tok == NX_MM_TOK_DOLLAR_A {
299 // Register pending label as an axiom.
300 if db.n_theorems < db.capacity {
301 let th: *IngestTheorem = nx_ingest_th_at(db, db.n_theorems)
302 th.label = pending
303 th.kind = NX_MM_TOK_DOLLAR_A
304 th.n_proof = 0
305 th.chain = (0 as *DerivationChain)
306 db.n_theorems = db.n_theorems + 1
307 }
308 // Skip everything until $. -- bound by file length.
309 let lp_a: *NxLoopFrame = nx_loop_begin(len + 1)
310 while nx_loop_step(lp_a) == 1 {
311 let t2: i64 = nx_mm_next_token(buf, pos, len, label_buf)
312 if t2 == NX_MM_TOK_DOLLAR_DOT { nx_loop_break(lp_a) }
313 if t2 == NX_MM_TOK_NONE { nx_loop_break(lp_a) }
314 }
315 }
316 if tok == NX_MM_TOK_DOLLAR_P {
317 // Provable statement. Skip term until $=, then collect
318 // proof tokens until $.; translate each into the chain.
319 let lp_eq: *NxLoopFrame = nx_loop_begin(len + 1)
320 while nx_loop_step(lp_eq) == 1 {
321 let t3: i64 = nx_mm_next_token(buf, pos, len, label_buf)
322 if t3 == NX_MM_TOK_DOLLAR_EQ { nx_loop_break(lp_eq) }
323 if t3 == NX_MM_TOK_NONE { return db }
324 }
325 // Collect proof tokens. Chain capacity = 64 tokens.
326 let chain: *DerivationChain = nx_deriv_chain_alloc(64)
327 var n_tokens: i64 = 0
328 var ok: i64 = 1
329 let lp_p: *NxLoopFrame = nx_loop_begin(64)
330 while nx_loop_step(lp_p) == 1 {
331 let t4: i64 = nx_mm_next_token(buf, pos, len, label_buf)
332 if t4 == NX_MM_TOK_DOLLAR_DOT { nx_loop_break(lp_p) }
333 if t4 == NX_MM_TOK_NONE { ok = 0; nx_loop_break(lp_p) }
334 if t4 == NX_MM_TOK_LABEL {
335 let ax_code: i64 = nx_ingest_axiom_lookup(label_buf)
336 if ax_code != 0 {
337 nx_deriv_add_axiom(chain, n_tokens, ax_code)
338 n_tokens = n_tokens + 1
339 }
340 if ax_code == 0 {
341 // Try as substitution step from an earlier leaf.
342 if n_tokens >= 1 {
343 nx_deriv_add_step(chain, n_tokens,
344 NX_DRULE_SUBSTITUTION,
345 n_tokens - 1, -1)
346 n_tokens = n_tokens + 1
347 }
348 }
349 }
350 }
351 if n_tokens > 0 { nx_deriv_mark_theorem(chain) }
352 let verdict: i64 = nx_deriv_verify(chain)
353 if verdict == NX_DERIV_VERIFY_OK {
354 if db.n_theorems < db.capacity {
355 let th: *IngestTheorem = nx_ingest_th_at(db, db.n_theorems)
356 th.label = pending
357 th.kind = NX_MM_TOK_DOLLAR_P
358 th.n_proof = n_tokens
359 th.chain = chain
360 db.n_theorems = db.n_theorems + 1
361 }
362 db.n_passed = db.n_passed + 1
363 }
364 if verdict != NX_DERIV_VERIFY_OK {
365 db.n_rejected = db.n_rejected + 1
366 }
367 }
368 if tok == NX_MM_TOK_DOLLAR_E {
369 // Logical hypothesis -- skip to $.
370 let lp_e: *NxLoopFrame = nx_loop_begin(len + 1)
371 while nx_loop_step(lp_e) == 1 {
372 let t5: i64 = nx_mm_next_token(buf, pos, len, label_buf)
373 if t5 == NX_MM_TOK_DOLLAR_DOT { nx_loop_break(lp_e) }
374 if t5 == NX_MM_TOK_NONE { nx_loop_break(lp_e) }
375 }
376 }
377 if tok == NX_MM_TOK_DOLLAR_F {
378 // Variable-type hypothesis -- skip to $.
379 let lp_f: *NxLoopFrame = nx_loop_begin(len + 1)
380 while nx_loop_step(lp_f) == 1 {
381 let t6: i64 = nx_mm_next_token(buf, pos, len, label_buf)
382 if t6 == NX_MM_TOK_DOLLAR_DOT { nx_loop_break(lp_f) }
383 if t6 == NX_MM_TOK_NONE { nx_loop_break(lp_f) }
384 }
385 }
386 if tok == NX_MM_TOK_DOLLAR_C {
387 let lp_cc: *NxLoopFrame = nx_loop_begin(len + 1)
388 while nx_loop_step(lp_cc) == 1 {
389 let t7: i64 = nx_mm_next_token(buf, pos, len, label_buf)
390 if t7 == NX_MM_TOK_DOLLAR_DOT { nx_loop_break(lp_cc) }
391 if t7 == NX_MM_TOK_NONE { nx_loop_break(lp_cc) }
392 }
393 }
394 if tok == NX_MM_TOK_DOLLAR_V {
395 let lp_v: *NxLoopFrame = nx_loop_begin(len + 1)
396 while nx_loop_step(lp_v) == 1 {
397 let t8: i64 = nx_mm_next_token(buf, pos, len, label_buf)
398 if t8 == NX_MM_TOK_DOLLAR_DOT { nx_loop_break(lp_v) }
399 if t8 == NX_MM_TOK_NONE { nx_loop_break(lp_v) }
400 }
401 }
402 }
403 return db
404}
405
406// Top-level entry point: read .mm file from disk, ingest it.
407func nx_ingest_file(path: *u8) -> *IngestDb {
408 let len_p: *i64 = (sys_mmap(8)) as *i64
409 len_p[0] = 0
410 let buf: *u8 = sys_read_file(path, len_p)
411 if buf == (0 as *u8) {
412 let empty: *IngestDb = nx_ingest_db_alloc()
413 return empty
414 }
415 return nx_ingest_corpus(buf, len_p[0])
416}