nx_qed_db.nx

buildroot/runtime/nx_qed_db.nx

6741 B223 linesdepth 3pulls 4 transitivereach 10 importersview sourcekind library

docs dependencies structs consts functions

about

nx_qed_db.nx -- QED-compatible theorem database. Implements the QED manifesto's schema for a unified machine-readable mathematics database. Per Wiedijk + Mizar QED pages, each theorem gets: qed_id stable cross-system identifier (i64) name source-system name (e.g., "Nat.add_comm") source_system_code sealed enum: LEAN / MIZAR / COQ / METAMATH / HOL_LIGHT / NISHILANG_LOCAL axioms[] transitive axiom dependencies proof_hash stable hash of the proof (for caching) verify_status sealed enum: TRUSTED_<SYSTEM> / LOCAL_PROVED / MATCHES_INDEPENDENT / UNVERIFIED genealogy_id: bundy_qed_manifesto_1994 + wiedijk_qed_page + mizar_qed_attempt lineage_id: formal_database + unified_math + provenance axioms: NX_AX_ZFC_SEPARATION

dependencies 2 imports · 10 importers

imports: syscalls.nxnx_axioms.nx

imported by: nx_auto_verify.nxnx_auto_verify_test.nxnx_help.nxnx_help_test.nxnx_ingest_pipeline.nxnx_ingest_pipeline_test.nxnx_qed_db_test.nxnx_shard.nxnx_validation_cycle.nxnx_validation_cycle_test.nx

structs

53	struct QedEntry
65	struct QedDb

consts

31	const NX_QED_SYS_NISHILANG_LOCAL: i64 = 0
32	const NX_QED_SYS_LEAN_MATHLIB: i64 = 1
33	const NX_QED_SYS_MIZAR_MML: i64 = 2
34	const NX_QED_SYS_COQ_STDLIB: i64 = 3
35	const NX_QED_SYS_METAMATH_SETMM: i64 = 4
36	const NX_QED_SYS_HOL_LIGHT: i64 = 5
37	const NX_QED_SYS_ISABELLE_HOL: i64 = 6
38	const NX_QED_SYS_PROOFPOWER: i64 = 7
40	const NX_QED_VERIFY_UNVERIFIED: i64 = 0
41	const NX_QED_VERIFY_LOCAL_PROVED: i64 = 1
42	const NX_QED_VERIFY_TRUSTED_LEAN: i64 = 2
43	const NX_QED_VERIFY_TRUSTED_MIZAR: i64 = 3
44	const NX_QED_VERIFY_TRUSTED_COQ: i64 = 4
45	const NX_QED_VERIFY_TRUSTED_METAMATH: i64 = 5
46	const NX_QED_VERIFY_TRUSTED_HOL_LIGHT: i64 = 6
47	const NX_QED_VERIFY_TRUSTED_ISABELLE: i64 = 7
48	const NX_QED_VERIFY_MATCHES_INDEPENDENT: i64 = 8
49	const NX_QED_VERIFY_DIFFERS_INVESTIGATE: i64 = 9
63	const NX_QED_ENTRY_BYTES: i64 = 56
72	const NX_QED_MAX_ENTRIES: i64 = 4096
73	const NX_QED_MAX_NAME_LEN: i64 = 256

functions

75	func nx_qed_db_alloc() -> *QedDb called by 5: main main main main main
85	func nx_qed_entry_at(db: QedDb, i: i64) -> QedEntry called by 9: nx_auto_verify_bulk main nx_help_search_qed nx_qed_insert nx_qed_find_by_name nx_qed_count_by_system+3
90	func nx_qed_insert(db: QedDb, name: u8, source_system: i64, called by 7: main main nx_pipe_run_metamath nx_pipe_run_lean nx_pipe_run_mizar main+1 calls 1: nx_qed_entry_at
108	func nx_qed_find_by_name(db: QedDb, name: u8) -> i64 called by 2: nx_help_search_qed main calls 1: nx_qed_entry_at
129	func nx_qed_count_by_system(db: *QedDb, sys: i64) -> i64 called by 2: main main calls 1: nx_qed_entry_at
141	func nx_qed_count_by_verify(db: *QedDb, status: i64) -> i64 called by 4: main main nx_vc_run main calls 1: nx_qed_entry_at
154	func qe_putc(fd: i64, c: i64) -> i64 called by 1: qe_i64
161	func qe_str(fd: i64, s: *u8, len: i64) -> i64 called by 1: nx_qed_emit_entry
166	func qe_strz(fd: i64, s: *u8) -> i64 called by 1: nx_qed_emit_entry
173	func qe_i64(fd: i64, n: i64) -> i64 called by 2: qe_i64 nx_qed_emit_entry calls 2: qe_putc qe_i64
198	func nx_qed_emit_entry(fd: i64, e: *QedEntry) -> i64 called by 1: nx_qed_emit_all calls 3: qe_str qe_i64 qe_strz
216	func nx_qed_emit_all(fd: i64, db: *QedDb) -> i64 called by 1: main calls 2: nx_qed_emit_entry nx_qed_entry_at