nx_ingest_pipeline.nx source
↩ module page · 243 lines · 8164 B
1// nx_ingest_pipeline.nx -- orchestrate: ingest -> QED-db -> auto-verify.
2//
3// Wraps the per-source ingesters (MetaMath, Lean, Mizar) with a common
4// pipeline that:
5// 1. Runs the appropriate ingester on raw corpus bytes
6// 2. Inserts each parsed declaration into nx_qed_db with the right
7// source_system code and initial verify_status
8// 3. Runs nx_auto_verify over the inserted entries
9// 4. Emits an aggregate JSON-line stats record
10//
11// Substrate-native, no AI, no external network.
12//
13// genealogy_id: wiedijk_qed_1994 (unified pipeline vision)
14// lineage_id: theorem_ingestion + autonomous_proving + qed_database
15
16// nx_safety_envelope:
17// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
18// sil_target: SIL1
19// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
20// verdict: NOT_YET_EVALUATED
21
22import "syscalls.nx"
23import "nx_axioms.nx"
24import "nx_qed_db.nx"
25import "nx_prover.nx"
26import "nx_auto_verify.nx"
27import "nx_theorem_ingest.nx"
28import "nx_lean_ingest.nx"
29import "nx_mizar_ingest.nx"
30
31// ===== sealed source codes ============================================
32
33const NX_PIPE_SRC_METAMATH: i64 = 0
34const NX_PIPE_SRC_LEAN: i64 = 1
35const NX_PIPE_SRC_MIZAR: i64 = 2
36
37// ===== pipeline run result ============================================
38
39struct PipelineResult {
40 src_code: i64,
41 n_ingested: i64,
42 n_inserted: i64,
43 n_local_proved: i64,
44 n_matches: i64,
45 n_unchanged: i64,
46 n_differs: i64,
47}
48
49const NX_PIPE_RESULT_BYTES: i64 = 56
50
51func nx_pipe_result_alloc() -> *PipelineResult {
52 let raw: *u8 = sys_mmap(NX_PIPE_RESULT_BYTES)
53 let r: *PipelineResult = raw as *PipelineResult
54 r.src_code = 0
55 r.n_ingested = 0
56 r.n_inserted = 0
57 r.n_local_proved = 0
58 r.n_matches = 0
59 r.n_unchanged = 0
60 r.n_differs = 0
61 return r
62}
63
64// ===== per-source pipelines ==========================================
65//
66// Each takes raw corpus bytes + length, plus a shared QED database to
67// insert into, plus a shared axiom-map array. Returns a result struct.
68
69func nx_pipe_run_metamath(buf: *u8, len: i64, qed: *QedDb,
70 axiom_map: *i64, n_axioms_per_entry: i64,
71 cycle_budget: i64, out: *PipelineResult) -> i64 {
72 out.src_code = NX_PIPE_SRC_METAMATH
73 let ingest_db: *IngestDb = nx_ingest_corpus(buf, len)
74 out.n_ingested = ingest_db.n_theorems
75 // Insert each ingested theorem into QED-db.
76 var i: i64 = 0
77 while i < ingest_db.n_theorems {
78 let th: *IngestTheorem = nx_ingest_th_at(ingest_db, i)
79 let verify_init: i64 = NX_QED_VERIFY_TRUSTED_METAMATH
80 if th.kind == NX_MM_TOK_DOLLAR_A {
81 // axioms stay as axiomatic citation; treat as TRUSTED_METAMATH
82 }
83 nx_qed_insert(qed, th.label, NX_QED_SYS_METAMATH_SETMM,
84 axiom_map, n_axioms_per_entry, i, verify_init)
85 out.n_inserted = out.n_inserted + 1
86 i = i + 1
87 }
88 // Auto-verify the entries just inserted (trivial target = first axiom).
89 let stats: *VerifyStats = nx_verify_stats_alloc()
90 let targets: *i64 = (sys_mmap(qed.n_entries * 8)) as *i64
91 var k: i64 = 0
92 while k < qed.n_entries {
93 targets[k] = 1
94 k = k + 1
95 }
96 let impl: *i64 = (sys_mmap(8)) as *i64
97 nx_auto_verify_bulk(qed, targets, impl, 0, cycle_budget, stats)
98 out.n_local_proved = stats.n_local_proved
99 out.n_matches = stats.n_matches
100 out.n_unchanged = stats.n_unchanged
101 out.n_differs = stats.n_differs
102 return 0
103}
104
105func nx_pipe_run_lean(buf: *u8, len: i64, qed: *QedDb,
106 axiom_map: *i64, n_axioms_per_entry: i64,
107 cycle_budget: i64, out: *PipelineResult) -> i64 {
108 out.src_code = NX_PIPE_SRC_LEAN
109 let ld: *LeanDb = nx_lean_ingest_corpus(buf, len)
110 out.n_ingested = ld.n_decls
111 var i: i64 = 0
112 while i < ld.n_decls {
113 let d: *LeanDecl = nx_lean_decl_at(ld, i)
114 let verify_init: i64 = NX_QED_VERIFY_TRUSTED_LEAN
115 nx_qed_insert(qed, d.name, NX_QED_SYS_LEAN_MATHLIB,
116 axiom_map, n_axioms_per_entry, i, verify_init)
117 out.n_inserted = out.n_inserted + 1
118 i = i + 1
119 }
120 let stats: *VerifyStats = nx_verify_stats_alloc()
121 let targets: *i64 = (sys_mmap(qed.n_entries * 8)) as *i64
122 var k: i64 = 0
123 while k < qed.n_entries {
124 targets[k] = 1
125 k = k + 1
126 }
127 let impl: *i64 = (sys_mmap(8)) as *i64
128 nx_auto_verify_bulk(qed, targets, impl, 0, cycle_budget, stats)
129 out.n_local_proved = stats.n_local_proved
130 out.n_matches = stats.n_matches
131 out.n_unchanged = stats.n_unchanged
132 out.n_differs = stats.n_differs
133 return 0
134}
135
136func nx_pipe_run_mizar(buf: *u8, len: i64, qed: *QedDb,
137 axiom_map: *i64, n_axioms_per_entry: i64,
138 cycle_budget: i64, out: *PipelineResult) -> i64 {
139 out.src_code = NX_PIPE_SRC_MIZAR
140 let md: *MizarDb = nx_mizar_ingest_corpus(buf, len)
141 out.n_ingested = md.n_decls
142 var i: i64 = 0
143 while i < md.n_decls {
144 let d: *MizarDecl = nx_mizar_decl_at(md, i)
145 let verify_init: i64 = NX_QED_VERIFY_TRUSTED_MIZAR
146 nx_qed_insert(qed, d.article, NX_QED_SYS_MIZAR_MML,
147 axiom_map, n_axioms_per_entry, d.number, verify_init)
148 out.n_inserted = out.n_inserted + 1
149 i = i + 1
150 }
151 let stats: *VerifyStats = nx_verify_stats_alloc()
152 let targets: *i64 = (sys_mmap(qed.n_entries * 8)) as *i64
153 var k: i64 = 0
154 while k < qed.n_entries {
155 targets[k] = 1
156 k = k + 1
157 }
158 let impl: *i64 = (sys_mmap(8)) as *i64
159 nx_auto_verify_bulk(qed, targets, impl, 0, cycle_budget, stats)
160 out.n_local_proved = stats.n_local_proved
161 out.n_matches = stats.n_matches
162 out.n_unchanged = stats.n_unchanged
163 out.n_differs = stats.n_differs
164 return 0
165}
166
167// ===== unified entry: dispatch on src_code ============================
168
169func nx_ingest_pipeline_run(src_code: i64, buf: *u8, len: i64, qed: *QedDb,
170 axiom_map: *i64, n_axioms_per_entry: i64,
171 cycle_budget: i64,
172 out: *PipelineResult) -> i64 {
173 if src_code == NX_PIPE_SRC_METAMATH {
174 return nx_pipe_run_metamath(buf, len, qed, axiom_map,
175 n_axioms_per_entry, cycle_budget, out)
176 }
177 if src_code == NX_PIPE_SRC_LEAN {
178 return nx_pipe_run_lean(buf, len, qed, axiom_map,
179 n_axioms_per_entry, cycle_budget, out)
180 }
181 if src_code == NX_PIPE_SRC_MIZAR {
182 return nx_pipe_run_mizar(buf, len, qed, axiom_map,
183 n_axioms_per_entry, cycle_budget, out)
184 }
185 return -1
186}
187
188// ===== JSON-line emission =============================================
189
190func pp_putc(fd: i64, c: i64) -> i64 {
191 let buf: *u8 = sys_mmap(1)
192 buf[0] = c & 0xFF
193 sys_write(fd, buf, 1)
194 return 0
195}
196
197func pp_str(fd: i64, s: *u8, n: i64) -> i64 {
198 sys_write(fd, s, n)
199 return 0
200}
201
202func pp_i64(fd: i64, n: i64) -> i64 {
203 if n < 0 {
204 pp_putc(fd, 45)
205 return pp_i64(fd, -n)
206 }
207 if n == 0 {
208 pp_putc(fd, 48)
209 return 0
210 }
211 let digits: *u8 = sys_mmap(32)
212 var d: i64 = 0
213 var v: i64 = n
214 while v > 0 {
215 digits[d] = (v % 10) + 48
216 v = v / 10
217 d = d + 1
218 }
219 while d > 0 {
220 d = d - 1
221 pp_putc(fd, digits[d])
222 }
223 return 0
224}
225
226func nx_pipe_emit_result(fd: i64, r: *PipelineResult) -> i64 {
227 pp_str(fd, "{\"phase\":\"INGEST_PIPELINE\",\"src\":", 33)
228 pp_i64(fd, r.src_code)
229 pp_str(fd, ",\"n_ingested\":", 14)
230 pp_i64(fd, r.n_ingested)
231 pp_str(fd, ",\"n_inserted\":", 14)
232 pp_i64(fd, r.n_inserted)
233 pp_str(fd, ",\"n_local_proved\":", 18)
234 pp_i64(fd, r.n_local_proved)
235 pp_str(fd, ",\"n_matches\":", 13)
236 pp_i64(fd, r.n_matches)
237 pp_str(fd, ",\"n_unchanged\":", 15)
238 pp_i64(fd, r.n_unchanged)
239 pp_str(fd, ",\"n_differs\":", 13)
240 pp_i64(fd, r.n_differs)
241 pp_str(fd, "}\n", 2)
242 return 0
243}