code wiki / (root) / nx_theorem_registry.nx

nx_theorem_registry.nx

buildroot/runtime/nx_theorem_registry.nx

6730 B207 linesdepth 4pulls 5 transitivereach 1 importersview sourcekind librarytopic theorem
docsdependenciesstructsconstsfunctions

about

nx_theorem_registry.nx -- substrate-native primitive registry. Per user 2026-05-14: "we should be able to build from the hardware up and shift this correctly much faster". The L0->L2.5 promotion: each catalog entry becomes a SUBSTRATE-REGISTERED ENTITY (queryable by name + iterable + countable + composable) without per-entry code generation. Machine speed: O(N) load over JSONL. After loading the 42,469-row shard: - each name is a first-class substrate primitive id - nx_thm_lookup(name) -> row or null - nx_thm_at(idx) -> row by index - nx_thm_count_by_kind(kind) -> aggregate genealogy_id: substrate_thm_registry_2026_05_14 lineage_id: l0_to_l2_5_bulk_promotion

dependencies 4 imports · 1 importers

nx_syscalls.nx nx_runtime.nx nx_tier.nx nx_str.nx nx_theorem_registry.nx nx_theorem_registry_test.nx

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_str.nx

imported by: nx_theorem_registry_test.nx

structs

42struct NxThmRow
50struct NxThmRegistry

consts

30const NX_THM_REG_CAP: nx_int = 262144 // bumped from 65536 to fit 145k+ mathlib4 ingestion
31const NX_THM_NAME_MAX: nx_size = 128
34const NX_THM_SRC_UNKNOWN: nx_int = 0
35const NX_THM_SRC_LEAN: nx_int = 1
36const NX_THM_SRC_COQ: nx_int = 2
37const NX_THM_SRC_ISABELLE: nx_int = 3
38const NX_THM_SRC_HOL: nx_int = 4
39const NX_THM_SRC_MIZAR: nx_int = 5
40const NX_THM_SRC_RFC: nx_int = 6
48const NX_THM_ROW_BYTES: nx_size = 24

functions

60func nx_thm_find(buf: *u8, p: nx_int, end: nx_int, pat: *u8, pat_len: nx_int) -> nx_int
called by 2: nx_thm_src_from_strnx_thm_parse_row
75func nx_thm_src_from_str(buf: *u8, p: nx_int, end: nx_int) -> nx_int
called by 1: nx_thm_parse_row calls 1: nx_thm_find
86func nx_thm_parse_row(buf: *u8, lo: nx_int, hi: nx_int, name_buf: *u8, out: *NxThmRow) -> nx_int
called by 1: nx_thm_load calls 4: nx_thm_src_from_strnx_thm_findsys_mmapnx_str_cpy
132func nx_thm_load(path: *u8) -> *NxThmRegistry
called by 1: main calls 3: sys_mmapsys_read_filenx_thm_parse_row
168func nx_thm_n(r: *NxThmRegistry) -> nx_int { return r.n }
called by 1: main
170func nx_thm_at(r: *NxThmRegistry, idx: nx_int) -> *NxThmRow
called by 4: nx_thm_lookupnx_thm_count_by_kindnx_thm_count_by_sourcemain
177func nx_thm_lookup(r: *NxThmRegistry, name: *u8) -> *NxThmRow
called by 1: main calls 2: nx_thm_atnx_str_eq
187func nx_thm_count_by_kind(r: *NxThmRegistry, kind: nx_int) -> nx_int
called by 1: main calls 1: nx_thm_at
198func nx_thm_count_by_source(r: *NxThmRegistry, source: nx_int) -> nx_int
called by 1: main calls 1: nx_thm_at