nx_auto_verify.nx
buildroot/runtime/nx_auto_verify.nx
about
nx_auto_verify.nx -- bulk re-prove every entry in nx_qed_db.
Iterates the QED database, runs nx_prover on each entry, upgrades
verify_status when the substrate succeeds. NO AI in the loop.
Trust ladder (per AUTONOMOUS_PROVING_DOCTRINE):
UNVERIFIED + prover succeeds -> LOCAL_PROVED
TRUSTED_<X> + prover succeeds -> MATCHES_INDEPENDENT
any + prover fails -> unchanged (we keep external trust;
never downgrade below ingest status)
prover proves contradiction -> DIFFERS_INVESTIGATE (flag for ledger)
genealogy_id: wiedijk_qed_1994 (cross-verification vision) + robinson_resolution
lineage_id: formal_proof_search + cross_system_verify
axioms: NX_AX_LOGIC_NONCONTRADICTION (we never trust + claim falsity)
dependencies 5 imports · 5 importers
imports: syscalls.nxnx_axioms.nxnx_derive.nxnx_qed_db.nxnx_prover.nx
imported by: nx_auto_verify_test.nxnx_ingest_pipeline.nxnx_shard.nxnx_validation_cycle.nxnx_validation_cycle_test.nx
structs
| 31 | struct VerifyStats |
consts
| 39 | const NX_VERIFY_STATS_BYTES: i64 = 40 |
functions
| 41 | func nx_verify_stats_alloc() -> *VerifyStats |
| 57 | func nx_auto_try_prove(e: *QedEntry, target_stmt_id: i64, |
| 74 | func nx_auto_verify_entry(e: *QedEntry, target_stmt_id: i64, |
| 102 | func nx_auto_verify_bulk(db: *QedDb, target_stmt_ids: *i64, called by 4: mainnx_pipe_run_metamathnx_pipe_run_leannx_pipe_run_mizar calls 2: nx_qed_entry_atnx_auto_verify_entry |
| 135 | func av_putc(fd: i64, c: i64) -> i64 called by 1: av_i64 |
| 142 | func av_str(fd: i64, s: *u8, len: i64) -> i64 called by 1: nx_verify_emit_stats |
| 147 | func av_i64(fd: i64, n: i64) -> i64 |
| 171 | func nx_verify_emit_stats(fd: i64, stats: *VerifyStats) -> i64 |