nx_theorem_registry_test.nx source
↩ module page · 79 lines · 3015 B
1// nx_theorem_registry_test.nx -- smoke for the L0->L2.5 bulk registry.
2//
3// Loads the 42k+ mathlib4 shard and verifies:
4// - n_records >= 10000 (rock-solid threshold)
5// - lookup by name works (sample known theorem)
6// - kind aggregates are non-zero
7// - source aggregates show all lean
8
9import "nx_syscalls.nx"
10import "nx_runtime.nx"
11import "nx_tier.nx"
12import "nx_str.nx"
13import "nx_theorem_registry.nx"
14
15const NX_THM_T_THRESHOLD: nx_int = 10000
16
17func main() -> nx_exit {
18 let path: *u8 = "/tmp/nx_ingest_lean-shard-0000.jsonl" as *u8
19 let t0: nx_int = 0 // (no clock here -- bench wrapper measures)
20
21 let r: *NxThmRegistry = nx_thm_load(path)
22 if (r as nx_int) == 0 {
23 println("FAIL: registry load failed" as *u8)
24 return 100
25 }
26
27 let n: nx_int = nx_thm_n(r)
28 print("thm_registry_loaded=" as *u8); print_i64(n); println("" as *u8)
29
30 if n < NX_THM_T_THRESHOLD {
31 print("FAIL: loaded " as *u8); print_i64(n); println(" below 10000 threshold" as *u8)
32 return 1
33 }
34
35 // Aggregate counts
36 let n_kind_1: nx_int = nx_thm_count_by_kind(r, 1)
37 let n_kind_2: nx_int = nx_thm_count_by_kind(r, 2)
38 let n_lean: nx_int = nx_thm_count_by_source(r, NX_THM_SRC_LEAN)
39 print("kind_1_theorems=" as *u8); print_i64(n_kind_1); println("" as *u8)
40 print("kind_2_other=" as *u8); print_i64(n_kind_2); println("" as *u8)
41 print("source_lean=" as *u8); print_i64(n_lean); println("" as *u8)
42
43 if n_kind_1 == 0 { return 10 }
44 if n_kind_2 == 0 { return 11 }
45 if n_lean != n { return 12 } // all should be lean for this shard
46
47 // Sample lookups: 5 indexes, verify each row is well-formed
48 var i: nx_int = 0
49 var samples_checked: nx_int = 0
50 while i < 5 {
51 let idx: nx_int = i * (n / 5)
52 let row: *NxThmRow = nx_thm_at(r, idx)
53 if (row as nx_int) == 0 { return 20 + i }
54 if (row.name as nx_int) == 0 { return 30 + i }
55 // Name should be non-empty
56 if row.name[0] == 0 { return 40 + i }
57 samples_checked = samples_checked + 1
58 i = i + 1
59 }
60 print("samples_well_formed=" as *u8); print_i64(samples_checked); println("/5" as *u8)
61
62 // Test name->row lookup: get the first row's name + look it up
63 let first: *NxThmRow = nx_thm_at(r, 0)
64 let found: *NxThmRow = nx_thm_lookup(r, first.name)
65 if (found as nx_int) == 0 { return 50 }
66 if nx_str_eq(found.name, first.name) != 1 { return 51 }
67 println("lookup_by_name=PASS" as *u8)
68
69 // Negative case: lookup an obviously-non-existent name
70 let missing: *NxThmRow = nx_thm_lookup(r, "definitely_not_a_real_theorem_xyz123" as *u8)
71 if (missing as nx_int) != 0 { return 60 }
72 println("lookup_negative_case=PASS" as *u8)
73
74 println("" as *u8)
75 println("=== L0 -> L2.5 PROMOTION VERIFIED ===" as *u8)
76 print("substrate-registered primitives: " as *u8); print_i64(n); println("" as *u8)
77 println("each entry queryable by name, iterable by index, kind-aggregable" as *u8)
78 return 0
79}