nx_wiedijk_100_test.nx source
↩ module page · 76 lines · 3833 B
1// nx_wiedijk_100_test.nx -- exercise the Wiedijk Top 100 corpus
2// registration + audit per source + verification debt.
3
4import "nx_wiedijk_100.nx"
5
6func main() -> nx_exit {
7 println("=== Wiedijk Top 100 corpus -- mass ingestion via v2 kernel ===" as *u8)
8
9 let lib: *LemmaLib = nx_lemma_lib_new(128)
10 let ch: *K2Chain = nx_k2_chain_new(128)
11 let n: nx_int = nx_wiedijk_100_register(lib, ch)
12 print("Registered " as *u8); print_i64(n); println(" Wiedijk entries" as *u8)
13 if n != 100 {
14 println("FAIL: expected 100 entries" as *u8)
15 return 1
16 }
17
18 println("" as *u8)
19 println("--- Per-source breakdown ---" as *u8)
20 let n_native: nx_int = nx_lemma_count_by_src(lib, NX_LEMMA_SRC_NATIVE)
21 print(" NATIVE NishiLang : " as *u8); print_i64(n_native); println("" as *u8)
22 let n_hl: nx_int = nx_lemma_count_by_src(lib, NX_LEMMA_SRC_HOL_LIGHT)
23 print(" HOL Light : " as *u8); print_i64(n_hl); println("" as *u8)
24 let n_co: nx_int = nx_lemma_count_by_src(lib, NX_LEMMA_SRC_COQ)
25 print(" Coq : " as *u8); print_i64(n_co); println("" as *u8)
26 let n_le: nx_int = nx_lemma_count_by_src(lib, NX_LEMMA_SRC_LEAN)
27 print(" Lean Mathlib : " as *u8); print_i64(n_le); println("" as *u8)
28 let n_is: nx_int = nx_lemma_count_by_src(lib, NX_LEMMA_SRC_ISABELLE)
29 print(" Isabelle/HOL : " as *u8); print_i64(n_is); println("" as *u8)
30 let n_mz: nx_int = nx_lemma_count_by_src(lib, NX_LEMMA_SRC_MIZAR)
31 print(" Mizar : " as *u8); print_i64(n_mz); println("" as *u8)
32
33 println("" as *u8)
34 println("--- Per-status breakdown (3-status native-or-nothing) ---" as *u8)
35 let n_proved: nx_int = nx_lemma_count_by_status(lib, NX_LEMMA_PROVED_NATIVE)
36 print(" PROVED_NATIVE : " as *u8); print_i64(n_proved); println("" as *u8)
37 let n_replayed: nx_int = nx_lemma_count_by_status(lib, NX_LEMMA_PROVED_NATIVE_REPLAYED)
38 print(" PROVED_NATIVE_REPLAYED : " as *u8); print_i64(n_replayed); println("" as *u8)
39 let n_pending: nx_int = nx_lemma_count_by_status(lib, NX_LEMMA_PENDING)
40 print(" PENDING : " as *u8); print_i64(n_pending); println("" as *u8)
41
42 println("" as *u8)
43 let debt: nx_int = nx_lemma_pending_count(lib)
44 print("VERIFICATION DEBT (PENDING entries needing native chains): " as *u8)
45 print_i64(debt); println("" as *u8)
46 println("This number must drop to 0 for full kernel-checked parity." as *u8)
47 println("Each PROVED_NATIVE is a milestone toward that goal." as *u8)
48
49 println("" as *u8)
50 println("HONEST CARDINAL VERDICT:" as *u8)
51 println(" + WIN: 100 statements registered with provenance + content-hash" as *u8)
52 println(" + WIN: each becomes a v2 kernel axiom callable in any proof" as *u8)
53 println(" + WIN: audit table separates PROVED_NATIVE from PENDING" as *u8)
54 println(" - LOSE_BIG: 1 PROVED_NATIVE vs ~99 PENDING (cardinal-honest accounting)" as *u8)
55 println(" - named_improvement: ship one new PROVED_NATIVE per session;" as *u8)
56 println(" target ~100 over coming sessions to close the verification debt" as *u8)
57 println("" as *u8)
58
59 // ===== Per-entry kernel checks: every imported axiom must appear =====
60 // in the chain at the recorded chain_idx.
61 var i: nx_int = 0
62 var bad: nx_int = 0
63 while i < lib.n {
64 let item: *ImportedLemma = nx_lemma_lib_at(lib, i)
65 if item.chain_idx < 0 { bad = bad + 1 }
66 if item.chain_idx >= ch.n { bad = bad + 1 }
67 i = i + 1
68 }
69 if bad > 0 {
70 print("FAIL: " as *u8); print_i64(bad)
71 println(" entries had bad chain_idx" as *u8)
72 return 1
73 }
74 println("All 100 entries have valid v2 chain indices." as *u8)
75 return 0
76}