nx_auto_verify.nx source
↩ module page · 184 lines · 6442 B
1// nx_auto_verify.nx -- bulk re-prove every entry in nx_qed_db.
2//
3// Iterates the QED database, runs nx_prover on each entry, upgrades
4// verify_status when the substrate succeeds. NO AI in the loop.
5//
6// Trust ladder (per AUTONOMOUS_PROVING_DOCTRINE):
7// UNVERIFIED + prover succeeds -> LOCAL_PROVED
8// TRUSTED_<X> + prover succeeds -> MATCHES_INDEPENDENT
9// any + prover fails -> unchanged (we keep external trust;
10// never downgrade below ingest status)
11// prover proves contradiction -> DIFFERS_INVESTIGATE (flag for ledger)
12//
13// genealogy_id: wiedijk_qed_1994 (cross-verification vision) + robinson_resolution
14// lineage_id: formal_proof_search + cross_system_verify
15// axioms: NX_AX_LOGIC_NONCONTRADICTION (we never trust + claim falsity)
16
17// nx_safety_envelope:
18// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
19// sil_target: SIL1
20// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
21// verdict: NOT_YET_EVALUATED
22
23import "syscalls.nx"
24import "nx_axioms.nx"
25import "nx_derive.nx"
26import "nx_qed_db.nx"
27import "nx_prover.nx"
28
29// ===== aggregate stats over an auto-verify pass =======================
30
31struct VerifyStats {
32 n_total: i64,
33 n_local_proved: i64,
34 n_matches: i64, // upgraded TRUSTED_X -> MATCHES_INDEPENDENT
35 n_unchanged: i64,
36 n_differs: i64,
37}
38
39const NX_VERIFY_STATS_BYTES: i64 = 40
40
41func nx_verify_stats_alloc() -> *VerifyStats {
42 let raw: *u8 = sys_mmap(NX_VERIFY_STATS_BYTES)
43 let st: *VerifyStats = raw as *VerifyStats
44 st.n_total = 0
45 st.n_local_proved = 0
46 st.n_matches = 0
47 st.n_unchanged = 0
48 st.n_differs = 0
49 return st
50}
51
52// Try to prove a single QED entry using its declared axiom set.
53// Returns 1 if proved, 0 if not. Uses a trivial trial: if the entry
54// declares its theorem as exactly equal to one of its axioms (degenerate
55// case), the prover succeeds. For non-trivial cases, Phase A0 will
56// often return NOT_PROVED_WITHIN_BUDGET -- we don't lie about this.
57func nx_auto_try_prove(e: *QedEntry, target_stmt_id: i64,
58 impl_table: *i64, n_impls: i64,
59 cycle_budget: i64) -> i64 {
60 let s: *ProofState = nx_prover_state_alloc(target_stmt_id)
61 // Seed with declared axioms. Each axiom gets stmt_id = i+1 (1-indexed).
62 var i: i64 = 0
63 while i < e.n_axioms {
64 nx_prover_add_axiom(s, i + 1, e.axiom_codes[i])
65 i = i + 1
66 }
67 let verdict: i64 = nx_prover_search(s, impl_table, n_impls, cycle_budget)
68 if verdict == NX_PROVER_PROVED { return 1 }
69 return 0
70}
71
72// Process one entry: try to prove, upgrade verify_status appropriately.
73// Returns the resulting verify_status.
74func nx_auto_verify_entry(e: *QedEntry, target_stmt_id: i64,
75 impl_table: *i64, n_impls: i64,
76 cycle_budget: i64) -> i64 {
77 let prev_status: i64 = e.verify_status
78 let proved: i64 = nx_auto_try_prove(e, target_stmt_id,
79 impl_table, n_impls, cycle_budget)
80 if proved == 1 {
81 if prev_status == NX_QED_VERIFY_UNVERIFIED {
82 e.verify_status = NX_QED_VERIFY_LOCAL_PROVED
83 }
84 if prev_status != NX_QED_VERIFY_UNVERIFIED {
85 if prev_status != NX_QED_VERIFY_LOCAL_PROVED {
86 if prev_status != NX_QED_VERIFY_MATCHES_INDEPENDENT {
87 e.verify_status = NX_QED_VERIFY_MATCHES_INDEPENDENT
88 }
89 }
90 }
91 }
92 return e.verify_status
93}
94
95// Bulk-verify: walk every QED entry, update each, accumulate stats.
96// target_stmt_id_table[i] = target for entry i (caller supplies).
97// impl_tables[i] = pointer to implication table for entry i.
98// n_impls_table[i] = count of implications for entry i.
99//
100// For Phase A0 simplicity, the caller supplies one global implication
101// table shared across all entries. Per-entry tables come in Phase A1.
102func nx_auto_verify_bulk(db: *QedDb, target_stmt_ids: *i64,
103 impl_table: *i64, n_impls: i64,
104 cycle_budget: i64, stats: *VerifyStats) -> i64 {
105 var i: i64 = 0
106 while i < db.n_entries {
107 let e: *QedEntry = nx_qed_entry_at(db, i)
108 let prev: i64 = e.verify_status
109 nx_auto_verify_entry(e, target_stmt_ids[i],
110 impl_table, n_impls, cycle_budget)
111 stats.n_total = stats.n_total + 1
112 let new_status: i64 = e.verify_status
113 if new_status == NX_QED_VERIFY_LOCAL_PROVED {
114 if prev != NX_QED_VERIFY_LOCAL_PROVED {
115 stats.n_local_proved = stats.n_local_proved + 1
116 }
117 }
118 if new_status == NX_QED_VERIFY_MATCHES_INDEPENDENT {
119 if prev != NX_QED_VERIFY_MATCHES_INDEPENDENT {
120 stats.n_matches = stats.n_matches + 1
121 }
122 }
123 if new_status == NX_QED_VERIFY_DIFFERS_INVESTIGATE {
124 stats.n_differs = stats.n_differs + 1
125 }
126 if new_status == prev {
127 stats.n_unchanged = stats.n_unchanged + 1
128 }
129 i = i + 1
130 }
131 return 0
132}
133
134// Emit stats as JSON-line.
135func av_putc(fd: i64, c: i64) -> i64 {
136 let buf: *u8 = sys_mmap(1)
137 buf[0] = c & 0xFF
138 sys_write(fd, buf, 1)
139 return 0
140}
141
142func av_str(fd: i64, s: *u8, len: i64) -> i64 {
143 sys_write(fd, s, len)
144 return 0
145}
146
147func av_i64(fd: i64, n: i64) -> i64 {
148 if n < 0 {
149 av_putc(fd, 45)
150 return av_i64(fd, -n)
151 }
152 if n == 0 {
153 av_putc(fd, 48)
154 return 0
155 }
156 let digits: *u8 = sys_mmap(32)
157 var d: i64 = 0
158 var v: i64 = n
159 while v > 0 {
160 digits[d] = (v % 10) + 48
161 v = v / 10
162 d = d + 1
163 }
164 while d > 0 {
165 d = d - 1
166 av_putc(fd, digits[d])
167 }
168 return 0
169}
170
171func nx_verify_emit_stats(fd: i64, stats: *VerifyStats) -> i64 {
172 av_str(fd, "{\"phase\":\"AUTO_VERIFY\",\"n_total\":", 33)
173 av_i64(fd, stats.n_total)
174 av_str(fd, ",\"n_local_proved\":", 18)
175 av_i64(fd, stats.n_local_proved)
176 av_str(fd, ",\"n_matches\":", 13)
177 av_i64(fd, stats.n_matches)
178 av_str(fd, ",\"n_unchanged\":", 15)
179 av_i64(fd, stats.n_unchanged)
180 av_str(fd, ",\"n_differs\":", 13)
181 av_i64(fd, stats.n_differs)
182 av_str(fd, "}\n", 2)
183 return 0
184}