nx_ingest_pipeline_test.nx source
↩ module page · 80 lines · 3279 B
1// nx_ingest_pipeline_test.nx -- end-to-end cross-corpus ingestion smoke.
2
3import "syscalls.nx"
4import "nx_axioms.nx"
5import "nx_qed_db.nx"
6import "nx_ingest_pipeline.nx"
7
8func main() -> i64 {
9 let qed: *QedDb = nx_qed_db_alloc()
10
11 // Shared axiom map: every inserted entry gets this axiom set.
12 let axioms: *i64 = (sys_mmap(8)) as *i64
13 axioms[0] = NX_AX_PEANO_PA1_ZERO_EXISTS
14
15 // === MetaMath corpus ===
16 // 3 axioms + 2 theorems = 5 declarations
17 let mm_corpus: *u8 = sys_mmap(512)
18 var i: i64 = 0
19 while i < 512 { mm_corpus[i] = 0; i = i + 1 }
20 let mm_src: *u8 = "ax-1 $a wff $. ax-2 $a wff $. pa1 $a wff $. thm1 $p wff $= ax-1 $. thm2 $p wff $= pa1 ax-2 $."
21 var k: i64 = 0
22 while mm_src[k] != 0 { mm_corpus[k] = mm_src[k]; k = k + 1 }
23 let mm_len: i64 = k
24
25 let mm_result: *PipelineResult = nx_pipe_result_alloc()
26 nx_ingest_pipeline_run(NX_PIPE_SRC_METAMATH, mm_corpus, mm_len, qed,
27 axioms, 1, 10, mm_result)
28 if mm_result.n_inserted < 3 { return 10 }
29
30 // === Lean corpus ===
31 let ln_corpus: *u8 = sys_mmap(256)
32 var i2: i64 = 0
33 while i2 < 256 { ln_corpus[i2] = 0; i2 = i2 + 1 }
34 let ln_src: *u8 = "axiom ax_choice theorem Nat_add_comm lemma helper theorem Nat_mul_comm"
35 var k2: i64 = 0
36 while ln_src[k2] != 0 { ln_corpus[k2] = ln_src[k2]; k2 = k2 + 1 }
37 let ln_len: i64 = k2
38
39 let ln_result: *PipelineResult = nx_pipe_result_alloc()
40 nx_ingest_pipeline_run(NX_PIPE_SRC_LEAN, ln_corpus, ln_len, qed,
41 axioms, 1, 10, ln_result)
42 if ln_result.n_inserted != 4 { return 20 }
43
44 // === Mizar corpus ===
45 let mz_corpus: *u8 = sys_mmap(256)
46 var i3: i64 = 0
47 while i3 < 256 { mz_corpus[i3] = 0; i3 = i3 + 1 }
48 let mz_src: *u8 = "theorem definition theorem scheme theorem lemma"
49 var k3: i64 = 0
50 while mz_src[k3] != 0 { mz_corpus[k3] = mz_src[k3]; k3 = k3 + 1 }
51 let mz_len: i64 = k3
52
53 let mz_result: *PipelineResult = nx_pipe_result_alloc()
54 nx_ingest_pipeline_run(NX_PIPE_SRC_MIZAR, mz_corpus, mz_len, qed,
55 axioms, 1, 10, mz_result)
56 if mz_result.n_inserted < 5 { return 30 }
57
58 // === Aggregate check ===
59 // After all three pipelines, the QED database should contain:
60 // ~5 from MetaMath + 4 from Lean + ~6 from Mizar = ~15 entries.
61 if qed.n_entries < 12 { return 40 }
62 // Per-system counts.
63 if nx_qed_count_by_system(qed, NX_QED_SYS_METAMATH_SETMM) < 3 { return 41 }
64 if nx_qed_count_by_system(qed, NX_QED_SYS_LEAN_MATHLIB) != 4 { return 42 }
65 if nx_qed_count_by_system(qed, NX_QED_SYS_MIZAR_MML) < 5 { return 43 }
66
67 // Verify-status counts: every entry should now be either
68 // MATCHES_INDEPENDENT (was TRUSTED_X with trivial target),
69 // LOCAL_PROVED (was UNVERIFIED), or unchanged.
70 let n_matches: i64 = nx_qed_count_by_verify(qed, NX_QED_VERIFY_MATCHES_INDEPENDENT)
71 let n_proved: i64 = nx_qed_count_by_verify(qed, NX_QED_VERIFY_LOCAL_PROVED)
72 if n_matches + n_proved < 5 { return 50 }
73
74 // Emit pipeline results.
75 nx_pipe_emit_result(2, mm_result)
76 nx_pipe_emit_result(2, ln_result)
77 nx_pipe_emit_result(2, mz_result)
78
79 return 0
80}