nx_validation_cycle_test.nx source
↩ module page · 132 lines · 5076 B
1// nx_validation_cycle_test.nx -- monthly cycle smoke (parallel shards).
2
3import "syscalls.nx"
4import "nx_axioms.nx"
5import "nx_qed_db.nx"
6import "nx_auto_verify.nx"
7import "nx_shard.nx"
8import "nx_validation_cycle.nx"
9
10func main() -> i64 {
11 let db: *QedDb = nx_qed_db_alloc()
12
13 // Populate 20 entries from various source systems, mixed statuses.
14 let ax: *i64 = (sys_mmap(8)) as *i64
15 ax[0] = NX_AX_PEANO_PA1_ZERO_EXISTS
16 var i: i64 = 0
17 while i < 20 {
18 let src: i64 = (i - (i / 4) * 4) // i mod 4: cycle 4 sources
19 let init_status: i64 = (i - (i / 3) * 3) + 1 // mix UNVERIFIED / LOCAL / MATCHES / TRUSTED
20 nx_qed_insert(db, "thm" as *u8, src, ax, 1, i, init_status)
21 i = i + 1
22 }
23 if db.n_entries != 20 { return 1 }
24
25 // Build target table: each entry's target = stmt_id 1 (trivial).
26 let targets: *i64 = (sys_mmap(20 * 8)) as *i64
27 var k: i64 = 0
28 while k < 20 {
29 targets[k] = 1
30 k = k + 1
31 }
32 let impl: *i64 = (sys_mmap(8)) as *i64
33
34 // === Test 1: 4-shard plan covers all 20 entries ===
35 let plan4: *ShardPlan = nx_shard_plan_build(db, 4)
36 if plan4.n_shards != 4 { return 10 }
37 if plan4.total_entries != 20 { return 11 }
38 let s0: *Shard = nx_shard_at(plan4, 0)
39 let s3: *Shard = nx_shard_at(plan4, 3)
40 if s0.start_idx != 0 { return 12 }
41 if s3.end_idx != 20 { return 13 }
42 // Each shard should cover ~5 entries.
43 if s0.end_idx - s0.start_idx != 5 { return 14 }
44
45 // === Test 2: run shards sequentially produces same as direct auto-verify ===
46 nx_shard_run_all(db, plan4, targets, impl, 0, 10)
47 let agg: *VerifyStats = nx_verify_stats_alloc()
48 nx_shard_aggregate(plan4, agg)
49 if agg.n_total != 20 { return 20 }
50
51 // === Test 3: cycle should-run logic ===
52 let cycle: *ValidationCycle = nx_vc_alloc(4, 10)
53 // First run: always 1.
54 if nx_vc_should_run(cycle, 1000000) != 1 { return 30 }
55 // Simulate run: set last_run + next_run.
56 cycle.last_run_ns = 1000000
57 cycle.next_run_ns = 1000000 + NX_VC_MONTH_NS
58 // Before next_run: should not run.
59 if nx_vc_should_run(cycle, 1500000) != 0 { return 31 }
60 // At/after next_run: should run.
61 if nx_vc_should_run(cycle, cycle.next_run_ns) != 1 { return 32 }
62 if nx_vc_should_run(cycle, cycle.next_run_ns + 1) != 1 { return 33 }
63
64 // === Test 4: full run produces monthly report ===
65 let db2: *QedDb = nx_qed_db_alloc()
66 var j: i64 = 0
67 while j < 15 {
68 let src: i64 = (j - (j / 3) * 3) + 1 // sources 1..3
69 nx_qed_insert(db2, "x" as *u8, src, ax, 1, j,
70 NX_QED_VERIFY_TRUSTED_LEAN)
71 j = j + 1
72 }
73 let tgt: *i64 = (sys_mmap(15 * 8)) as *i64
74 j = 0
75 while j < 15 { tgt[j] = 1; j = j + 1 }
76
77 let cyc: *ValidationCycle = nx_vc_alloc(3, 10)
78 let report: *MonthlyReport = nx_monthly_report_alloc()
79 nx_vc_run(cyc, db2, tgt, impl, 0, 2000000000, report)
80
81 if report.cycle_id != 1 { return 40 }
82 if report.qed_entries != 15 { return 41 }
83 if report.n_shards_used != 3 { return 42 }
84 // After cycle: all 15 TRUSTED_LEAN entries upgraded to MATCHES_INDEPENDENT.
85 if report.aggregate_status_matches_independent != 15 { return 43 }
86 if report.aggregate_status_trusted_external != 0 { return 44 }
87 // Cycle state updated.
88 if cyc.cycle_id != 1 { return 45 }
89 if cyc.last_run_ns != 2000000000 { return 46 }
90 if cyc.next_run_ns != 2000000000 + NX_VC_MONTH_NS { return 47 }
91
92 // Emit report to stderr.
93 nx_vc_emit_report(2, report)
94
95 // === Test 5: parallelism-readiness -- sharded results equal direct ===
96 let db3: *QedDb = nx_qed_db_alloc()
97 var m: i64 = 0
98 while m < 12 {
99 nx_qed_insert(db3, "y" as *u8, NX_QED_SYS_LEAN_MATHLIB, ax, 1, m,
100 NX_QED_VERIFY_UNVERIFIED)
101 m = m + 1
102 }
103 let tgt2: *i64 = (sys_mmap(12 * 8)) as *i64
104 m = 0
105 while m < 12 { tgt2[m] = 1; m = m + 1 }
106
107 // Run with 2 shards
108 let p2: *ShardPlan = nx_shard_plan_build(db3, 2)
109 nx_shard_run_all(db3, p2, tgt2, impl, 0, 10)
110 let agg2: *VerifyStats = nx_verify_stats_alloc()
111 nx_shard_aggregate(p2, agg2)
112 let final_proved_2: i64 = nx_qed_count_by_verify(db3, NX_QED_VERIFY_LOCAL_PROVED)
113 if final_proved_2 != 12 { return 50 }
114
115 // Reset + run with 4 shards on a fresh DB
116 let db4: *QedDb = nx_qed_db_alloc()
117 m = 0
118 while m < 12 {
119 nx_qed_insert(db4, "y" as *u8, NX_QED_SYS_LEAN_MATHLIB, ax, 1, m,
120 NX_QED_VERIFY_UNVERIFIED)
121 m = m + 1
122 }
123 let p4: *ShardPlan = nx_shard_plan_build(db4, 4)
124 nx_shard_run_all(db4, p4, tgt2, impl, 0, 10)
125 let final_proved_4: i64 = nx_qed_count_by_verify(db4, NX_QED_VERIFY_LOCAL_PROVED)
126 if final_proved_4 != 12 { return 51 }
127
128 // Same result for 2 vs 4 shards -- associativity verified.
129 if final_proved_2 != final_proved_4 { return 52 }
130
131 return 0
132}