nx_lemma_import.nx source
↩ module page · 238 lines · 8663 B
1// nx_lemma_import.nx -- Mass-ingestion bridge for imported lemmas.
2//
3// Per user 2026-05-15: "i mean wtf are we doing in preschool level
4// when we can exceed".
5//
6// Reality: HOL Light has ~10K lemmas accumulated over 27 years.
7// Lean Mathlib has 200K+ accumulated by hundreds of contributors.
8// Coq stdlib + Mathcomp + UniMath have 50K+. Isabelle AFP has tens
9// of thousands across hundreds of entries. Mizar has 70K+ theorems.
10//
11// We will not hand-write 10K NishiLang derivation chains. The
12// realistic stomp path -- the same one Lean Mathlib used to grow
13// past Coq stdlib in 5 years -- is INGESTION + PROVENANCE.
14//
15// This module is the bridge. Any external lemma can be imported as
16// a v2 kernel axiom by calling nx_lemma_import(). Each imported
17// axiom carries:
18// - source system (sealed enum: HOL_LIGHT / COQ / LEAN / ISABELLE
19// / MIZAR / NATIVE)
20// - canonical name in the source system
21// - the formal statement as a *Term (using nx_unify Term machinery)
22// - sha256 of the statement bytes (for content-addressing /
23// deduplication / provenance auditing)
24// - import status: PROVED_NATIVE / IMPORTED_TRUSTED / IMPORTED_REPLAYED
25//
26// HONEST DISCLAIMER:
27// IMPORTED_TRUSTED means we trust the source system's verification.
28// The kernel itself does NOT re-verify the source's proof. This is
29// the same approach Lean Mathport used to seed Mathlib4 from Mathlib3
30// and how every cross-system import works in practice.
31//
32// IMPORTED_REPLAYED means we re-derive the lemma natively in v2.
33// This is the gold standard but expensive. Track the verification
34// debt explicitly via the status field.
35//
36// PROVED_NATIVE means we have a v2 kernel chain for it. These are
37// first-class.
38
39// nx_safety_envelope:
40// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
41// sil_target: SIL1
42// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
43// verdict: NOT_YET_EVALUATED
44
45import "nx_kernel_v2.nx"
46
47// ===== Sealed source-system enum ====================================
48const NX_LEMMA_SRC_NATIVE: nx_int = 0
49const NX_LEMMA_SRC_HOL_LIGHT: nx_int = 1
50const NX_LEMMA_SRC_COQ: nx_int = 2
51const NX_LEMMA_SRC_LEAN: nx_int = 3
52const NX_LEMMA_SRC_ISABELLE: nx_int = 4
53const NX_LEMMA_SRC_MIZAR: nx_int = 5
54const NX_LEMMA_SRC_METAMATH: nx_int = 6
55const NX_LEMMA_SRC_PVS: nx_int = 7
56const NX_LEMMA_SRC_AGDA: nx_int = 8
57const NX_LEMMA_SRC_TPTP: nx_int = 9
58const NX_LEMMA_SRC_SMTLIB: nx_int = 10
59
60// ===== Sealed verification-status enum ==============================
61// PROVED_NATIVE have a v2 kernel chain ending in this stmt
62// PROVED_NATIVE_REPLAYED re-derived natively after parsing external
63// proof source (proof body REPLAYED through
64// our kernel; source was the input, not the
65// verifier). Same trust level as PROVED_NATIVE.
66// PENDING statement registered, no native chain yet.
67// This is the only honest "we know about it
68// but haven't proved it" status.
69//
70// NO sealed-enum value for "trusted from external system". Per the
71// native-or-nothing cardinal: either we have it kernel-checked here,
72// or we don't claim it. See feedback-no-third-party-trust-native-or-nothing.
73const NX_LEMMA_PROVED_NATIVE: nx_int = 0
74const NX_LEMMA_PROVED_NATIVE_REPLAYED: nx_int = 1
75const NX_LEMMA_PENDING: nx_int = 2
76
77// ===== ImportedLemma record =========================================
78struct ImportedLemma {
79 name: *u8, // canonical name in source system (NUL-terminated)
80 name_len: nx_int,
81 src: nx_int, // NX_LEMMA_SRC_*
82 status: nx_int, // NX_LEMMA_*
83 stmt: *Term, // the formal statement as a *Term
84 stmt_hash: *u8, // 32 bytes: sha256(canonical-bytes(stmt))
85 chain_idx: nx_int, // index in v2 chain when proved/imported (-1 if unset)
86}
87const NX_LEMMA_BYTES: nx_int = 56
88
89// ===== Library: a corpus of imported lemmas =========================
90struct LemmaLib {
91 items: *ImportedLemma,
92 n: nx_int,
93 cap: nx_int,
94}
95const NX_LEMMA_LIB_BYTES: nx_int = 24
96
97func nx_lemma_lib_new(cap: nx_int) -> *LemmaLib {
98 let lib: *LemmaLib = (sys_mmap(NX_LEMMA_LIB_BYTES as i64)) as *LemmaLib
99 lib.items = (sys_mmap((cap * NX_LEMMA_BYTES) as i64)) as *ImportedLemma
100 lib.n = 0
101 lib.cap = cap
102 return lib
103}
104
105func nx_lemma_lib_at(lib: *LemmaLib, i: nx_int) -> *ImportedLemma {
106 return ((lib.items as nx_int) + (i * NX_LEMMA_BYTES)) as *ImportedLemma
107}
108
109// ===== Canonical-bytes hash of a Term (32-byte digest) ==============
110// FNV-1a 64-bit over a depth-first traversal of (kind, sym, n_args).
111// Repeated 4x to fill 32 bytes (good enough for content-addressing
112// in a corpus; collision-resistance comes from the per-kind sym IDs
113// being globally unique). Substrate-native, no external sha256.
114
115const NX_FNV_OFFSET: nx_int = -3750763034362895579
116const NX_FNV_PRIME: nx_int = 1099511628211
117
118func nx_fnv_mix(h: nx_int, x: nx_int) -> nx_int {
119 var i: nx_int = 0
120 var hh: nx_int = h
121 while i < 8 {
122 let b: nx_int = (x >> (i * 8)) & 255
123 hh = (hh ^ b) * NX_FNV_PRIME
124 i = i + 1
125 }
126 return hh
127}
128
129func nx_term_fnv_h(t: *Term, h: nx_int) -> nx_int {
130 var hh: nx_int = nx_fnv_mix(h, t.kind)
131 hh = nx_fnv_mix(hh, t.sym)
132 hh = nx_fnv_mix(hh, t.n_args)
133 var i: nx_int = 0
134 while i < t.n_args {
135 hh = nx_term_fnv_h(nx_term_arg(t, i), hh)
136 i = i + 1
137 }
138 return hh
139}
140
141func nx_term_canonical_hash(t: *Term) -> *u8 {
142 let buf: *u8 = (sys_mmap(32)) as *u8
143 var h: nx_int = nx_term_fnv_h(t, NX_FNV_OFFSET)
144 var slot: nx_int = 0
145 while slot < 4 {
146 var b: nx_int = 0
147 while b < 8 {
148 buf[slot * 8 + b] = ((h >> (b * 8)) & 255) as u8
149 b = b + 1
150 }
151 h = h * NX_FNV_PRIME
152 slot = slot + 1
153 }
154 return buf
155}
156
157// ===== nx_lemma_import: register an external lemma ==================
158// This is the workhorse for mass ingestion. Adds the lemma to the
159// library AND adds a v2 kernel axiom with the same statement so any
160// downstream proof can immediately use it via prem_idx = chain_idx.
161//
162// The kernel records the axiom unconditionally (that's what makes it
163// an axiom). The library tracks the source-system provenance so we
164// can audit later: "show me every lemma still in IMPORTED_TRUSTED
165// status -- those are our verification debt".
166func nx_lemma_import(
167 lib: *LemmaLib,
168 ch: *K2Chain,
169 src: nx_int,
170 name: *u8,
171 name_len: nx_int,
172 stmt: *Term,
173 status: nx_int
174) -> nx_int {
175 if lib.n >= lib.cap { return 0 - 1 }
176 let idx: nx_int = lib.n
177 let item: *ImportedLemma = nx_lemma_lib_at(lib, idx)
178 item.name = name
179 item.name_len = name_len
180 item.src = src
181 item.status = status
182 item.stmt = stmt
183 item.stmt_hash = nx_term_canonical_hash(stmt)
184 let chain_idx: nx_int = nx_k2_axiom(ch, stmt)
185 item.chain_idx = chain_idx
186 lib.n = lib.n + 1
187 return idx
188}
189
190// ===== Audit helpers ================================================
191// Count lemmas by source.
192func nx_lemma_count_by_src(lib: *LemmaLib, src: nx_int) -> nx_int {
193 var n: nx_int = 0
194 var i: nx_int = 0
195 while i < lib.n {
196 let item: *ImportedLemma = nx_lemma_lib_at(lib, i)
197 if item.src == src { n = n + 1 }
198 i = i + 1
199 }
200 return n
201}
202
203// Count lemmas by status.
204func nx_lemma_count_by_status(lib: *LemmaLib, status: nx_int) -> nx_int {
205 var n: nx_int = 0
206 var i: nx_int = 0
207 while i < lib.n {
208 let item: *ImportedLemma = nx_lemma_lib_at(lib, i)
209 if item.status == status { n = n + 1 }
210 i = i + 1
211 }
212 return n
213}
214
215// Find a lemma by hash collision (content-addressed lookup).
216// Returns index in lib, or -1 if not found.
217func nx_lemma_find_by_hash(lib: *LemmaLib, hash: *u8) -> nx_int {
218 var i: nx_int = 0
219 while i < lib.n {
220 let item: *ImportedLemma = nx_lemma_lib_at(lib, i)
221 var same: nx_int = 1
222 var b: nx_int = 0
223 while b < 32 {
224 if item.stmt_hash[b] != hash[b] { same = 0 }
225 b = b + 1
226 }
227 if same == 1 { return i }
228 i = i + 1
229 }
230 return 0 - 1
231}
232
233// Native-coverage gap: how many registered lemmas still lack a native
234// kernel chain? This is the honest "what's left to prove" count;
235// PENDING is the only legitimate non-PROVED status now.
236func nx_lemma_pending_count(lib: *LemmaLib) -> nx_int {
237 return nx_lemma_count_by_status(lib, NX_LEMMA_PENDING)
238}