nx_auto_verify_test.nx source
↩ module page · 80 lines · 3095 B
1// nx_auto_verify_test.nx -- smoke for autonomous bulk verification.
2
3import "syscalls.nx"
4import "nx_axioms.nx"
5import "nx_qed_db.nx"
6import "nx_prover.nx"
7import "nx_auto_verify.nx"
8
9func main() -> i64 {
10 let db: *QedDb = nx_qed_db_alloc()
11
12 // Insert 3 entries with different starting statuses.
13 let ax1: *i64 = (sys_mmap(8)) as *i64
14 ax1[0] = NX_AX_PEANO_PA1_ZERO_EXISTS
15 nx_qed_insert(db, "local_unverified",
16 NX_QED_SYS_NISHILANG_LOCAL,
17 ax1, 1, 100, NX_QED_VERIFY_UNVERIFIED)
18
19 let ax2: *i64 = (sys_mmap(8)) as *i64
20 ax2[0] = NX_AX_LOGIC_MODUS_PONENS_RULE
21 nx_qed_insert(db, "lean_trusted",
22 NX_QED_SYS_LEAN_MATHLIB,
23 ax2, 1, 200, NX_QED_VERIFY_TRUSTED_LEAN)
24
25 let ax3: *i64 = (sys_mmap(8)) as *i64
26 ax3[0] = NX_AX_PEANO_PA5_INDUCTION
27 nx_qed_insert(db, "metamath_trusted",
28 NX_QED_SYS_METAMATH_SETMM,
29 ax3, 1, 300, NX_QED_VERIFY_TRUSTED_METAMATH)
30
31 if db.n_entries != 3 { return 1 }
32
33 // Build target table: for entry i, the target stmt_id is stmt_id=1
34 // (which matches the first axiom we seed in the prover state, so
35 // each entry is trivially provable: target == axiom).
36 let targets: *i64 = (sys_mmap(24)) as *i64
37 targets[0] = 1
38 targets[1] = 1
39 targets[2] = 1
40
41 // Empty implication table -- the targets are already in axioms.
42 let impl: *i64 = (sys_mmap(8)) as *i64
43
44 let stats: *VerifyStats = nx_verify_stats_alloc()
45 nx_auto_verify_bulk(db, targets, impl, 0, 10, stats)
46
47 if stats.n_total != 3 { return 10 }
48 // Entry 0 (UNVERIFIED) -> LOCAL_PROVED
49 let e0: *QedEntry = nx_qed_entry_at(db, 0)
50 if e0.verify_status != NX_QED_VERIFY_LOCAL_PROVED { return 11 }
51 // Entries 1, 2 (TRUSTED_X) -> MATCHES_INDEPENDENT
52 let e1: *QedEntry = nx_qed_entry_at(db, 1)
53 if e1.verify_status != NX_QED_VERIFY_MATCHES_INDEPENDENT { return 12 }
54 let e2: *QedEntry = nx_qed_entry_at(db, 2)
55 if e2.verify_status != NX_QED_VERIFY_MATCHES_INDEPENDENT { return 13 }
56
57 if stats.n_local_proved != 1 { return 20 }
58 if stats.n_matches != 2 { return 21 }
59 if stats.n_unchanged != 0 { return 22 }
60 if stats.n_differs != 0 { return 23 }
61
62 // Emit stats for inspection.
63 nx_verify_emit_stats(2, stats)
64
65 // === negative: target unreachable -- status unchanged ===
66 let db2: *QedDb = nx_qed_db_alloc()
67 nx_qed_insert(db2, "unreachable",
68 NX_QED_SYS_LEAN_MATHLIB,
69 ax2, 1, 999, NX_QED_VERIFY_TRUSTED_LEAN)
70 let targets2: *i64 = (sys_mmap(8)) as *i64
71 targets2[0] = 42 // not in axioms
72 let stats2: *VerifyStats = nx_verify_stats_alloc()
73 nx_auto_verify_bulk(db2, targets2, impl, 0, 10, stats2)
74 let eu: *QedEntry = nx_qed_entry_at(db2, 0)
75 if eu.verify_status != NX_QED_VERIFY_TRUSTED_LEAN { return 30 }
76 if stats2.n_unchanged != 1 { return 31 }
77 if stats2.n_matches != 0 { return 32 }
78
79 return 0
80}