nx_qed_db.nx source
↩ module page · 223 lines · 6741 B
1// nx_qed_db.nx -- QED-compatible theorem database.
2//
3// Implements the QED manifesto's schema for a unified machine-readable
4// mathematics database. Per Wiedijk + Mizar QED pages, each theorem
5// gets:
6//
7// qed_id stable cross-system identifier (i64)
8// name source-system name (e.g., "Nat.add_comm")
9// source_system_code sealed enum: LEAN / MIZAR / COQ / METAMATH /
10// HOL_LIGHT / NISHILANG_LOCAL
11// axioms[] transitive axiom dependencies
12// proof_hash stable hash of the proof (for caching)
13// verify_status sealed enum: TRUSTED_<SYSTEM> / LOCAL_PROVED /
14// MATCHES_INDEPENDENT / UNVERIFIED
15//
16// genealogy_id: bundy_qed_manifesto_1994 + wiedijk_qed_page + mizar_qed_attempt
17// lineage_id: formal_database + unified_math + provenance
18// axioms: NX_AX_ZFC_SEPARATION
19
20// nx_safety_envelope:
21// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
22// sil_target: SIL1
23// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
24// verdict: NOT_YET_EVALUATED
25
26import "syscalls.nx"
27import "nx_axioms.nx"
28
29// ===== sealed enums =====================================================
30
31const NX_QED_SYS_NISHILANG_LOCAL: i64 = 0
32const NX_QED_SYS_LEAN_MATHLIB: i64 = 1
33const NX_QED_SYS_MIZAR_MML: i64 = 2
34const NX_QED_SYS_COQ_STDLIB: i64 = 3
35const NX_QED_SYS_METAMATH_SETMM: i64 = 4
36const NX_QED_SYS_HOL_LIGHT: i64 = 5
37const NX_QED_SYS_ISABELLE_HOL: i64 = 6
38const NX_QED_SYS_PROOFPOWER: i64 = 7
39
40const NX_QED_VERIFY_UNVERIFIED: i64 = 0
41const NX_QED_VERIFY_LOCAL_PROVED: i64 = 1
42const NX_QED_VERIFY_TRUSTED_LEAN: i64 = 2
43const NX_QED_VERIFY_TRUSTED_MIZAR: i64 = 3
44const NX_QED_VERIFY_TRUSTED_COQ: i64 = 4
45const NX_QED_VERIFY_TRUSTED_METAMATH: i64 = 5
46const NX_QED_VERIFY_TRUSTED_HOL_LIGHT: i64 = 6
47const NX_QED_VERIFY_TRUSTED_ISABELLE: i64 = 7
48const NX_QED_VERIFY_MATCHES_INDEPENDENT: i64 = 8
49const NX_QED_VERIFY_DIFFERS_INVESTIGATE: i64 = 9
50
51// ===== entry structure =================================================
52
53struct QedEntry {
54 qed_id: i64,
55 name: *u8,
56 source_system: i64, // sealed NX_QED_SYS_*
57 proof_hash: i64,
58 verify_status: i64, // sealed NX_QED_VERIFY_*
59 n_axioms: i64,
60 axiom_codes: *i64, // pointer to array
61}
62
63const NX_QED_ENTRY_BYTES: i64 = 56
64
65struct QedDb {
66 entries: *QedEntry,
67 n_entries: i64,
68 capacity: i64,
69 next_id: i64,
70}
71
72const NX_QED_MAX_ENTRIES: i64 = 4096
73const NX_QED_MAX_NAME_LEN: i64 = 256
74
75func nx_qed_db_alloc() -> *QedDb {
76 let raw: *u8 = sys_mmap(32)
77 let db: *QedDb = raw as *QedDb
78 db.entries = (sys_mmap(NX_QED_MAX_ENTRIES * NX_QED_ENTRY_BYTES)) as *QedEntry
79 db.n_entries = 0
80 db.capacity = NX_QED_MAX_ENTRIES
81 db.next_id = 1
82 return db
83}
84
85func nx_qed_entry_at(db: *QedDb, i: i64) -> *QedEntry {
86 return (((db.entries as i64) + i * NX_QED_ENTRY_BYTES) as *QedEntry)
87}
88
89// Insert a new theorem entry. Returns the assigned qed_id, or -1 if full.
90func nx_qed_insert(db: *QedDb, name: *u8, source_system: i64,
91 axiom_codes: *i64, n_axioms: i64,
92 proof_hash: i64, verify_status: i64) -> i64 {
93 if db.n_entries >= db.capacity { return -1 }
94 let e: *QedEntry = nx_qed_entry_at(db, db.n_entries)
95 e.qed_id = db.next_id
96 db.next_id = db.next_id + 1
97 e.name = name
98 e.source_system = source_system
99 e.proof_hash = proof_hash
100 e.verify_status = verify_status
101 e.n_axioms = n_axioms
102 e.axiom_codes = axiom_codes
103 db.n_entries = db.n_entries + 1
104 return e.qed_id
105}
106
107// Find an entry by name (linear scan in P0; index for P1).
108func nx_qed_find_by_name(db: *QedDb, name: *u8) -> i64 {
109 var i: i64 = 0
110 while i < db.n_entries {
111 let e: *QedEntry = nx_qed_entry_at(db, i)
112 var k: i64 = 0
113 var eq: i64 = 1
114 while k < NX_QED_MAX_NAME_LEN {
115 if e.name[k] != name[k] { eq = 0; k = NX_QED_MAX_NAME_LEN }
116 if e.name[k] == 0 {
117 if name[k] != 0 { eq = 0 }
118 k = NX_QED_MAX_NAME_LEN
119 }
120 if k < NX_QED_MAX_NAME_LEN { k = k + 1 }
121 }
122 if eq == 1 { return e.qed_id }
123 i = i + 1
124 }
125 return -1
126}
127
128// Count by source system.
129func nx_qed_count_by_system(db: *QedDb, sys: i64) -> i64 {
130 var count: i64 = 0
131 var i: i64 = 0
132 while i < db.n_entries {
133 let e: *QedEntry = nx_qed_entry_at(db, i)
134 if e.source_system == sys { count = count + 1 }
135 i = i + 1
136 }
137 return count
138}
139
140// Count by verification status.
141func nx_qed_count_by_verify(db: *QedDb, status: i64) -> i64 {
142 var count: i64 = 0
143 var i: i64 = 0
144 while i < db.n_entries {
145 let e: *QedEntry = nx_qed_entry_at(db, i)
146 if e.verify_status == status { count = count + 1 }
147 i = i + 1
148 }
149 return count
150}
151
152// ===== JSON-line emission =============================================
153
154func qe_putc(fd: i64, c: i64) -> i64 {
155 let buf: *u8 = sys_mmap(1)
156 buf[0] = c & 0xFF
157 sys_write(fd, buf, 1)
158 return 0
159}
160
161func qe_str(fd: i64, s: *u8, len: i64) -> i64 {
162 sys_write(fd, s, len)
163 return 0
164}
165
166func qe_strz(fd: i64, s: *u8) -> i64 {
167 var i: i64 = 0
168 while s[i] != 0 { i = i + 1 }
169 sys_write(fd, s, i)
170 return i
171}
172
173func qe_i64(fd: i64, n: i64) -> i64 {
174 if n < 0 {
175 qe_putc(fd, 45)
176 return qe_i64(fd, -n)
177 }
178 if n == 0 {
179 qe_putc(fd, 48)
180 return 0
181 }
182 let digits: *u8 = sys_mmap(32)
183 var d: i64 = 0
184 var v: i64 = n
185 while v > 0 {
186 digits[d] = (v % 10) + 48
187 v = v / 10
188 d = d + 1
189 }
190 while d > 0 {
191 d = d - 1
192 qe_putc(fd, digits[d])
193 }
194 return 0
195}
196
197// Emit one entry to fd as JSON-line.
198func nx_qed_emit_entry(fd: i64, e: *QedEntry) -> i64 {
199 qe_str(fd, "{\"qed_id\":", 10)
200 qe_i64(fd, e.qed_id)
201 qe_str(fd, ",\"name\":\"", 9)
202 if e.name != (0 as *u8) { qe_strz(fd, e.name) }
203 qe_str(fd, "\",\"source\":", 11)
204 qe_i64(fd, e.source_system)
205 qe_str(fd, ",\"hash\":", 8)
206 qe_i64(fd, e.proof_hash)
207 qe_str(fd, ",\"verify\":", 10)
208 qe_i64(fd, e.verify_status)
209 qe_str(fd, ",\"n_axioms\":", 12)
210 qe_i64(fd, e.n_axioms)
211 qe_str(fd, "}\n", 2)
212 return 0
213}
214
215// Emit entire db.
216func nx_qed_emit_all(fd: i64, db: *QedDb) -> i64 {
217 var i: i64 = 0
218 while i < db.n_entries {
219 nx_qed_emit_entry(fd, nx_qed_entry_at(db, i))
220 i = i + 1
221 }
222 return 0
223}