nx_theorem_registry.nx source
↩ module page · 207 lines · 6730 B
1// nx_theorem_registry.nx -- substrate-native primitive registry.
2//
3// Per user 2026-05-14: "we should be able to build from the hardware
4// up and shift this correctly much faster". The L0->L2.5 promotion:
5// each catalog entry becomes a SUBSTRATE-REGISTERED ENTITY (queryable
6// by name + iterable + countable + composable) without per-entry code
7// generation. Machine speed: O(N) load over JSONL.
8//
9// After loading the 42,469-row shard:
10// - each name is a first-class substrate primitive id
11// - nx_thm_lookup(name) -> row or null
12// - nx_thm_at(idx) -> row by index
13// - nx_thm_count_by_kind(kind) -> aggregate
14//
15// genealogy_id: substrate_thm_registry_2026_05_14
16// lineage_id: l0_to_l2_5_bulk_promotion
17
18// nx_safety_envelope:
19// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
20// sil_target: SIL1
21// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
22// verdict: NOT_YET_EVALUATED
23
24import "nx_syscalls.nx"
25import "nx_runtime.nx"
26import "nx_tier.nx"
27import "nx_str.nx"
28
29// Sized for 50k+ headroom over today's 42,469.
30const NX_THM_REG_CAP: nx_int = 262144 // bumped from 65536 to fit 145k+ mathlib4 ingestion
31const NX_THM_NAME_MAX: nx_size = 128
32
33// Source enum.
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
41
42struct NxThmRow {
43 name: *u8,
44 kind: nx_int,
45 source: nx_int,
46}
47
48const NX_THM_ROW_BYTES: nx_size = 24
49
50struct NxThmRegistry {
51 rows: *NxThmRow,
52 n: nx_int,
53 capacity: nx_int,
54}
55
56// ----- shard line parser ------------------------------------------------
57
58// Scan forward from p in buf[lo..hi] for pat (length pat_len).
59// Returns position of first match, or -1.
60func nx_thm_find(buf: *u8, p: nx_int, end: nx_int, pat: *u8, pat_len: nx_int) -> nx_int {
61 var i: nx_int = p
62 while i + pat_len <= end {
63 var j: nx_int = 0
64 var ok: nx_int = 1
65 while j < pat_len {
66 if buf[i + j] != pat[j] { ok = 0; j = pat_len }
67 j = j + 1
68 }
69 if ok == 1 { return i }
70 i = i + 1
71 }
72 return -1
73}
74
75func nx_thm_src_from_str(buf: *u8, p: nx_int, end: nx_int) -> nx_int {
76 if nx_thm_find(buf, p, end, "\"source\":\"lean\"" as *u8, 15) >= 0 { return NX_THM_SRC_LEAN }
77 if nx_thm_find(buf, p, end, "\"source\":\"coq\"" as *u8, 14) >= 0 { return NX_THM_SRC_COQ }
78 if nx_thm_find(buf, p, end, "\"source\":\"isabelle\"" as *u8, 19) >= 0 { return NX_THM_SRC_ISABELLE }
79 if nx_thm_find(buf, p, end, "\"source\":\"hol\"" as *u8, 14) >= 0 { return NX_THM_SRC_HOL }
80 if nx_thm_find(buf, p, end, "\"source\":\"mizar\"" as *u8, 16) >= 0 { return NX_THM_SRC_MIZAR }
81 if nx_thm_find(buf, p, end, "\"source\":\"rfc\"" as *u8, 14) >= 0 { return NX_THM_SRC_RFC }
82 return NX_THM_SRC_UNKNOWN
83}
84
85// Parse one JSONL row from buf[lo..hi] into out. Returns 1 on success.
86func nx_thm_parse_row(buf: *u8, lo: nx_int, hi: nx_int, name_buf: *u8, out: *NxThmRow) -> nx_int {
87 if hi <= lo + 2 { return 0 }
88 if buf[lo] != 123 { return 0 }
89
90 // source
91 out.source = nx_thm_src_from_str(buf, lo, hi)
92
93 // kind: first digit after "kind":
94 let p_kind: nx_int = nx_thm_find(buf, lo, hi, "\"kind\":" as *u8, 7)
95 if p_kind < 0 { return 0 }
96 let kc: nx_int = buf[p_kind + 7] as nx_int
97 if kc < 48 { return 0 }
98 if kc > 57 { return 0 }
99 out.kind = kc - 48
100
101 // name
102 let p_name: nx_int = nx_thm_find(buf, lo, hi, "\"name\":\"" as *u8, 8)
103 if p_name < 0 { return 0 }
104 let ns: nx_int = p_name + 8
105 var ne: nx_int = ns
106 var de: nx_int = 0
107 while de == 0 {
108 if ne >= hi { de = 1 }
109 if de == 0 {
110 if buf[ne] == 34 { de = 1 }
111 if de == 0 { ne = ne + 1 }
112 }
113 }
114 let name_len: nx_int = ne - ns
115 if name_len <= 0 { return 0 }
116 if name_len >= (NX_THM_NAME_MAX as nx_int) { return 0 }
117 var i: nx_int = 0
118 while i < name_len {
119 name_buf[i] = buf[ns + i]
120 i = i + 1
121 }
122 name_buf[name_len] = 0
123
124 let owned: *u8 = sys_mmap((name_len + 1) as nx_size)
125 nx_str_cpy(owned, name_buf)
126 out.name = owned
127 return 1
128}
129
130// ----- public API -------------------------------------------------------
131
132func nx_thm_load(path: *u8) -> *NxThmRegistry {
133 let raw: *u8 = sys_mmap(24)
134 let r: *NxThmRegistry = raw as *NxThmRegistry
135 r.rows = (sys_mmap((NX_THM_REG_CAP as nx_size) * NX_THM_ROW_BYTES)) as *NxThmRow
136 r.n = 0
137 r.capacity = NX_THM_REG_CAP
138
139 let len_p: *nx_int = (sys_mmap(8)) as *nx_int
140 len_p[0] = 0
141 let buf: *u8 = sys_read_file(path, len_p)
142 if (buf as nx_int) == 0 { return r }
143 let n: nx_int = len_p[0]
144
145 let name_buf: *u8 = sys_mmap(NX_THM_NAME_MAX)
146 var p: nx_int = 0
147 while p < n {
148 var eol: nx_int = p
149 var de: nx_int = 0
150 while de == 0 {
151 if eol >= n { de = 1 }
152 if de == 0 {
153 if buf[eol] == 10 { de = 1 }
154 if de == 0 { eol = eol + 1 }
155 }
156 }
157 if r.n < r.capacity {
158 let raw_row: *u8 = ((r.rows as nx_int) + (r.n as nx_int) * (NX_THM_ROW_BYTES as nx_int)) as *u8
159 let row: *NxThmRow = raw_row as *NxThmRow
160 let ok: nx_int = nx_thm_parse_row(buf, p, eol, name_buf, row)
161 if ok == 1 { r.n = r.n + 1 }
162 }
163 p = eol + 1
164 }
165 return r
166}
167
168func nx_thm_n(r: *NxThmRegistry) -> nx_int { return r.n }
169
170func nx_thm_at(r: *NxThmRegistry, idx: nx_int) -> *NxThmRow {
171 if idx < 0 { return 0 as *NxThmRow }
172 if idx >= r.n { return 0 as *NxThmRow }
173 let raw: *u8 = ((r.rows as nx_int) + (idx as nx_int) * (NX_THM_ROW_BYTES as nx_int)) as *u8
174 return raw as *NxThmRow
175}
176
177func nx_thm_lookup(r: *NxThmRegistry, name: *u8) -> *NxThmRow {
178 var i: nx_int = 0
179 while i < r.n {
180 let row: *NxThmRow = nx_thm_at(r, i)
181 if nx_str_eq(row.name, name) == 1 { return row }
182 i = i + 1
183 }
184 return 0 as *NxThmRow
185}
186
187func nx_thm_count_by_kind(r: *NxThmRegistry, kind: nx_int) -> nx_int {
188 var c: nx_int = 0
189 var i: nx_int = 0
190 while i < r.n {
191 let row: *NxThmRow = nx_thm_at(r, i)
192 if row.kind == kind { c = c + 1 }
193 i = i + 1
194 }
195 return c
196}
197
198func nx_thm_count_by_source(r: *NxThmRegistry, source: nx_int) -> nx_int {
199 var c: nx_int = 0
200 var i: nx_int = 0
201 while i < r.n {
202 let row: *NxThmRow = nx_thm_at(r, i)
203 if row.source == source { c = c + 1 }
204 i = i + 1
205 }
206 return c
207}