nx_lean_ingest.nx source
↩ module page · 292 lines · 11211 B
1// nx_lean_ingest.nx -- ingest Lean 4 theorem STATEMENTS (L0 phase).
2//
3// We do not implement a Lean kernel. Instead we parse the
4// statement-level structure of .lean files (theorem / lemma / def /
5// axiom declarations) and emit them into the QED database with
6// verification_status = TRUSTED_LEAN_KERNEL.
7//
8// L1+ phases add statement-to-card mapping, local-proof cross-check,
9// and reverse export.
10//
11// genealogy_id: de_moura_lean_2013 + lean4_2021 + scholze_liquid_tensor + tao_pfr
12// lineage_id: dependent_type_theory + formal_statement_parsing
13// axioms: NX_AX_ZFC_SEPARATION
14
15// nx_safety_envelope:
16// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
17// sil_target: SIL1
18// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
19// verdict: NOT_YET_EVALUATED
20
21import "nx_syscalls.nx"
22import "nx_axioms.nx"
23import "nx_lex.nx"
24import "nx_ascii.nx"
25
26// ===== Lean keyword tokens (sealed) ====================================
27
28const NX_LEAN_TOK_NONE: i64 = 0
29const NX_LEAN_TOK_THEOREM: i64 = 1
30const NX_LEAN_TOK_LEMMA: i64 = 2
31const NX_LEAN_TOK_DEF: i64 = 3
32const NX_LEAN_TOK_AXIOM: i64 = 4
33const NX_LEAN_TOK_COLON: i64 = 5
34const NX_LEAN_TOK_ASSIGN: i64 = 6 // :=
35const NX_LEAN_TOK_LBRACE: i64 = 7 // { for tactic block
36const NX_LEAN_TOK_RBRACE: i64 = 8
37const NX_LEAN_TOK_BY: i64 = 9 // by-block proof
38const NX_LEAN_TOK_IDENT: i64 = 10
39const NX_LEAN_TOK_NEWLINE: i64 = 11
40const NX_LEAN_TOK_COMMENT: i64 = 12
41
42// ===== ingest entry =====================================================
43
44const NX_LEAN_MAX_NAME_LEN: i64 = 256
45const NX_LEAN_MAX_STATEMENT_LEN: i64 = 4096
46
47struct LeanDecl {
48 kind: i64, // THEOREM / LEMMA / DEF / AXIOM
49 name: *u8, // null-terminated, up to MAX_NAME_LEN
50 statement: *u8, // raw type text, up to MAX_STATEMENT_LEN
51 n_refs: i64, // count of theorem-references in proof
52}
53
54const NX_LEAN_DECL_BYTES: i64 = 32
55
56struct LeanDb {
57 decls: *LeanDecl,
58 n_decls: i64,
59 capacity: i64,
60}
61
62// Sized to hold the largest single-file mathlib4 module's worth of
63// top-level decls. Mathlib/Data/Nat has ~85 files yielding ~3k decls,
64// and a tight clone-ingest pipeline streams one file at a time so this
65// cap bounds the per-call working set, not the per-corpus output.
66const NX_LEAN_MAX_DECLS: i64 = 262144 // bumped from 65536 to fit full mathlib4 (~194k raw)
67
68func nx_lean_db_alloc() -> *LeanDb {
69 let raw: *u8 = sys_mmap(24)
70 let db: *LeanDb = raw as *LeanDb
71 db.decls = (sys_mmap(NX_LEAN_MAX_DECLS * NX_LEAN_DECL_BYTES)) as *LeanDecl
72 db.n_decls = 0
73 db.capacity = NX_LEAN_MAX_DECLS
74 return db
75}
76
77func nx_lean_decl_at(db: *LeanDb, i: i64) -> *LeanDecl {
78 return (((db.decls as i64) + i * NX_LEAN_DECL_BYTES) as *LeanDecl)
79}
80
81// ===== tokenizer ========================================================
82
83// is_ws canonical in nx_lex.nx.
84
85// is_alpha (is_id_start) canonical in nx_ascii.nx.
86
87// is_alnum (alpha + _ + digit + ' + .) canonical in nx_lex (nx_lex_is_id_cont_qualified).
88
89// Skip whitespace + line comments (-- ...) + block comments (/- ... -/).
90func nx_lean_skip_ws(buf: *u8, pos: *i64, len: i64) -> i64 {
91 var progress: i64 = 1
92 while progress == 1 {
93 progress = 0
94 while pos[0] < len {
95 let c: i64 = buf[pos[0]]
96 if nx_lex_is_ws(c) == 1 {
97 pos[0] = pos[0] + 1
98 progress = 1
99 }
100 if nx_lex_is_ws(c) == 0 {
101 if c != 45 { return 0 } // not '-'
102 // -- comment?
103 if pos[0] + 1 < len {
104 if buf[pos[0] + 1] == 45 {
105 pos[0] = pos[0] + 2
106 while pos[0] < len {
107 if buf[pos[0]] == 10 { pos[0] = pos[0] + 1; pos[0] = pos[0] - 1 ; progress = 1 }
108 pos[0] = pos[0] + 1
109 if buf[pos[0] - 1] == 10 { pos[0] = pos[0] - 0; pos[0] = pos[0]; }
110 if pos[0] > 0 {
111 if buf[pos[0] - 1] == 10 { progress = 1 }
112 if buf[pos[0] - 1] == 10 { pos[0] = pos[0]; }
113 }
114 if buf[pos[0] - 1] == 10 { pos[0] = pos[0]; }
115 }
116 }
117 }
118 return 0
119 }
120 }
121 }
122 return 0
123}
124
125// Read a single token starting at pos[0]; writes label into out_label (null-term).
126// Returns one of NX_LEAN_TOK_*.
127func nx_lean_next_token(buf: *u8, pos: *i64, len: i64, out_label: *u8) -> i64 {
128 nx_lean_skip_ws(buf, pos, len)
129 if pos[0] >= len { return NX_LEAN_TOK_NONE }
130 let c0: i64 = buf[pos[0]]
131
132 // := -- assign-proof start
133 if c0 == 58 {
134 if pos[0] + 1 < len {
135 if buf[pos[0] + 1] == 61 {
136 pos[0] = pos[0] + 2
137 return NX_LEAN_TOK_ASSIGN
138 }
139 }
140 pos[0] = pos[0] + 1
141 return NX_LEAN_TOK_COLON
142 }
143 if c0 == 123 { pos[0] = pos[0] + 1; return NX_LEAN_TOK_LBRACE }
144 if c0 == 125 { pos[0] = pos[0] + 1; return NX_LEAN_TOK_RBRACE }
145
146 // Identifier or keyword.
147 if nx_ascii_is_id_start(c0) == 1 {
148 var i: i64 = 0
149 while pos[0] < len {
150 let c: i64 = buf[pos[0]]
151 if nx_lex_is_id_cont_qualified(c) == 0 {
152 out_label[i] = 0
153 // Check keywords
154 if i == 7 {
155 if out_label[0] == 116 { // 't'
156 if out_label[1] == 104 { return NX_LEAN_TOK_THEOREM }
157 }
158 }
159 if i == 5 {
160 if out_label[0] == 108 { // 'l'
161 if out_label[1] == 101 {
162 if out_label[2] == 109 { return NX_LEAN_TOK_LEMMA }
163 }
164 }
165 if out_label[0] == 97 { // 'a'
166 if out_label[1] == 120 { return NX_LEAN_TOK_AXIOM }
167 }
168 }
169 if i == 3 {
170 if out_label[0] == 100 { return NX_LEAN_TOK_DEF } // 'def'
171 }
172 if i == 2 {
173 if out_label[0] == 98 { // 'b'
174 if out_label[1] == 121 { return NX_LEAN_TOK_BY } // 'by'
175 }
176 }
177 return NX_LEAN_TOK_IDENT
178 }
179 if i < NX_LEAN_MAX_NAME_LEN - 1 {
180 out_label[i] = c
181 i = i + 1
182 }
183 pos[0] = pos[0] + 1
184 }
185 out_label[i] = 0
186 return NX_LEAN_TOK_IDENT
187 }
188
189 // Other punctuation -- treat as ident-terminator.
190 pos[0] = pos[0] + 1
191 return NX_LEAN_TOK_NONE
192}
193
194// ===== ingest driver ===================================================
195//
196// Walks the file looking for `theorem NAME` / `lemma NAME` / `axiom NAME`
197// patterns. For each decl found, records (kind, name, statement-text,
198// n_refs). Statement text is read raw between : and := tokens.
199// Proof body (after :=) is scanned for theorem-references (counts only;
200// future work tracks per-name).
201
202func nx_lean_ingest_corpus(buf: *u8, len: i64) -> *LeanDb {
203 let db: *LeanDb = nx_lean_db_alloc()
204 let pos: *i64 = (sys_mmap(8)) as *i64
205 pos[0] = 0
206 let label: *u8 = sys_mmap(NX_LEAN_MAX_NAME_LEN)
207
208 while pos[0] < len {
209 let tok: i64 = nx_lean_next_token(buf, pos, len, label)
210 // Unknown punctuation (e.g., Lean attribute brackets `@[...]`) -- skip,
211 // don't abort. next_token already advanced pos past the offending byte.
212 if tok == NX_LEAN_TOK_NONE {
213 if pos[0] >= len { pos[0] = len }
214 }
215 if tok == NX_LEAN_TOK_THEOREM {
216 // Next ident = name.
217 let t2: i64 = nx_lean_next_token(buf, pos, len, label)
218 if t2 == NX_LEAN_TOK_IDENT {
219 if db.n_decls < db.capacity {
220 let d: *LeanDecl = nx_lean_decl_at(db, db.n_decls)
221 d.kind = NX_LEAN_TOK_THEOREM
222 let name_copy: *u8 = sys_mmap(NX_LEAN_MAX_NAME_LEN)
223 var i: i64 = 0
224 while i < NX_LEAN_MAX_NAME_LEN {
225 name_copy[i] = label[i]
226 if label[i] == 0 { i = NX_LEAN_MAX_NAME_LEN }
227 if i < NX_LEAN_MAX_NAME_LEN { i = i + 1 }
228 }
229 d.name = name_copy
230 d.statement = (0 as *u8)
231 d.n_refs = 0
232 db.n_decls = db.n_decls + 1
233 }
234 // Skip to next theorem/lemma keyword (we don't deeply
235 // parse types in L0).
236 }
237 }
238 if tok == NX_LEAN_TOK_LEMMA {
239 let t2: i64 = nx_lean_next_token(buf, pos, len, label)
240 if t2 == NX_LEAN_TOK_IDENT {
241 if db.n_decls < db.capacity {
242 let d: *LeanDecl = nx_lean_decl_at(db, db.n_decls)
243 d.kind = NX_LEAN_TOK_LEMMA
244 let name_copy: *u8 = sys_mmap(NX_LEAN_MAX_NAME_LEN)
245 var i: i64 = 0
246 while i < NX_LEAN_MAX_NAME_LEN {
247 name_copy[i] = label[i]
248 if label[i] == 0 { i = NX_LEAN_MAX_NAME_LEN }
249 if i < NX_LEAN_MAX_NAME_LEN { i = i + 1 }
250 }
251 d.name = name_copy
252 d.statement = (0 as *u8)
253 d.n_refs = 0
254 db.n_decls = db.n_decls + 1
255 }
256 }
257 }
258 if tok == NX_LEAN_TOK_AXIOM {
259 let t2: i64 = nx_lean_next_token(buf, pos, len, label)
260 if t2 == NX_LEAN_TOK_IDENT {
261 if db.n_decls < db.capacity {
262 let d: *LeanDecl = nx_lean_decl_at(db, db.n_decls)
263 d.kind = NX_LEAN_TOK_AXIOM
264 let name_copy: *u8 = sys_mmap(NX_LEAN_MAX_NAME_LEN)
265 var i: i64 = 0
266 while i < NX_LEAN_MAX_NAME_LEN {
267 name_copy[i] = label[i]
268 if label[i] == 0 { i = NX_LEAN_MAX_NAME_LEN }
269 if i < NX_LEAN_MAX_NAME_LEN { i = i + 1 }
270 }
271 d.name = name_copy
272 d.statement = (0 as *u8)
273 d.n_refs = 0
274 db.n_decls = db.n_decls + 1
275 }
276 }
277 }
278 }
279 return db
280}
281
282// Count declarations by kind.
283func nx_lean_count_kind(db: *LeanDb, kind: i64) -> i64 {
284 var count: i64 = 0
285 var i: i64 = 0
286 while i < db.n_decls {
287 let d: *LeanDecl = nx_lean_decl_at(db, i)
288 if d.kind == kind { count = count + 1 }
289 i = i + 1
290 }
291 return count
292}