nx_validation_cycle.nx source
↩ module page · 201 lines · 7376 B
1// nx_validation_cycle.nx -- monthly validation cycle orchestrator.
2//
3// Runs nx_auto_verify across the entire QED database on a fixed
4// cadence (default monthly). Uses sharded parallelism via nx_shard.
5// Tracks last_run_ns + cycle_id; emits structured monthly report.
6//
7// Per user mandate 2026-05-13: 'we want NishiLang where we can
8// validate its math monthly as it ingests more theorems quickly so
9// parallelism etc are required so we can address the catalog'.
10//
11// genealogy_id: continuous_integration + ci_cd + parallel_validation
12// lineage_id: periodic_orchestration + shard_dispatch
13// axioms: NX_AX_ALG_ASSOCIATIVITY (shard aggregation is associative)
14
15// nx_safety_envelope:
16// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
17// sil_target: SIL1
18// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
19// verdict: NOT_YET_EVALUATED
20
21import "syscalls.nx"
22import "nx_axioms.nx"
23import "nx_clock.nx"
24import "nx_qed_db.nx"
25import "nx_prover.nx"
26import "nx_auto_verify.nx"
27import "nx_shard.nx"
28
29// ===== cadence constants ===============================================
30
31const NX_VC_MONTH_NS: i64 = 2592000000000000 // 30 days in ns
32
33// ===== cycle state =====================================================
34
35struct ValidationCycle {
36 cycle_id: i64, // monotonic counter
37 last_run_ns: i64, // when last full validation
38 n_shards: i64, // configured shard count
39 cycle_budget: i64, // per-entry prover budget
40 next_run_ns: i64, // next scheduled
41}
42
43const NX_VC_BYTES: i64 = 40
44
45func nx_vc_alloc(n_shards: i64, cycle_budget: i64) -> *ValidationCycle {
46 let raw: *u8 = sys_mmap(NX_VC_BYTES)
47 let v: *ValidationCycle = raw as *ValidationCycle
48 v.cycle_id = 0
49 v.last_run_ns = 0
50 v.n_shards = n_shards
51 v.cycle_budget = cycle_budget
52 v.next_run_ns = 0
53 return v
54}
55
56// ===== run-decision ====================================================
57//
58// Returns 1 if the cycle should run now (cadence elapsed); 0 otherwise.
59// Useful as a guard in long-running services / CI hooks.
60
61func nx_vc_should_run(v: *ValidationCycle, now_ns: i64) -> i64 {
62 if v.last_run_ns == 0 { return 1 } // first run always
63 if now_ns >= v.next_run_ns { return 1 }
64 return 0
65}
66
67// ===== monthly report ==================================================
68
69struct MonthlyReport {
70 cycle_id: i64,
71 started_ns: i64,
72 completed_ns: i64,
73 elapsed_ns: i64,
74 qed_entries: i64,
75 n_shards_used: i64,
76 stats: *VerifyStats,
77 aggregate_status_local_proved: i64, // total LOCAL_PROVED in DB after cycle
78 aggregate_status_matches_independent: i64,
79 aggregate_status_trusted_external: i64,
80 aggregate_status_unverified: i64,
81}
82
83const NX_MONTHLY_REPORT_BYTES: i64 = 80
84
85func nx_monthly_report_alloc() -> *MonthlyReport {
86 let raw: *u8 = sys_mmap(NX_MONTHLY_REPORT_BYTES)
87 let r: *MonthlyReport = raw as *MonthlyReport
88 r.cycle_id = 0
89 r.started_ns = 0
90 r.completed_ns = 0
91 r.elapsed_ns = 0
92 r.qed_entries = 0
93 r.n_shards_used = 0
94 r.stats = nx_verify_stats_alloc()
95 r.aggregate_status_local_proved = 0
96 r.aggregate_status_matches_independent = 0
97 r.aggregate_status_trusted_external = 0
98 r.aggregate_status_unverified = 0
99 return r
100}
101
102// ===== run a full cycle =================================================
103
104func nx_vc_run(v: *ValidationCycle, db: *QedDb, targets: *i64,
105 impl_table: *i64, n_impls: i64,
106 now_ns: i64, out: *MonthlyReport) -> i64 {
107 out.cycle_id = v.cycle_id + 1
108 out.started_ns = now_ns
109 out.qed_entries = db.n_entries
110 out.n_shards_used = v.n_shards
111
112 // Build shard plan + dispatch.
113 let plan: *ShardPlan = nx_shard_plan_build(db, v.n_shards)
114 nx_shard_run_all(db, plan, targets, impl_table, n_impls, v.cycle_budget)
115
116 // Aggregate per-shard stats.
117 nx_shard_aggregate(plan, out.stats)
118
119 // Tally aggregate DB-level status counts.
120 out.aggregate_status_local_proved = nx_qed_count_by_verify(db, NX_QED_VERIFY_LOCAL_PROVED)
121 out.aggregate_status_matches_independent = nx_qed_count_by_verify(db, NX_QED_VERIFY_MATCHES_INDEPENDENT)
122 out.aggregate_status_unverified = nx_qed_count_by_verify(db, NX_QED_VERIFY_UNVERIFIED)
123 out.aggregate_status_trusted_external = 0
124 out.aggregate_status_trusted_external = out.aggregate_status_trusted_external + nx_qed_count_by_verify(db, NX_QED_VERIFY_TRUSTED_LEAN)
125 out.aggregate_status_trusted_external = out.aggregate_status_trusted_external + nx_qed_count_by_verify(db, NX_QED_VERIFY_TRUSTED_MIZAR)
126 out.aggregate_status_trusted_external = out.aggregate_status_trusted_external + nx_qed_count_by_verify(db, NX_QED_VERIFY_TRUSTED_COQ)
127 out.aggregate_status_trusted_external = out.aggregate_status_trusted_external + nx_qed_count_by_verify(db, NX_QED_VERIFY_TRUSTED_METAMATH)
128 out.aggregate_status_trusted_external = out.aggregate_status_trusted_external + nx_qed_count_by_verify(db, NX_QED_VERIFY_TRUSTED_HOL_LIGHT)
129 out.aggregate_status_trusted_external = out.aggregate_status_trusted_external + nx_qed_count_by_verify(db, NX_QED_VERIFY_TRUSTED_ISABELLE)
130
131 // Update cycle state.
132 v.cycle_id = out.cycle_id
133 v.last_run_ns = now_ns
134 v.next_run_ns = now_ns + NX_VC_MONTH_NS
135 out.completed_ns = now_ns // sim placeholder
136 out.elapsed_ns = 0
137 return 0
138}
139
140// ===== JSON-line monthly report ========================================
141
142func vr_putc(fd: i64, c: i64) -> i64 {
143 let buf: *u8 = sys_mmap(1)
144 buf[0] = c & 0xFF
145 sys_write(fd, buf, 1)
146 return 0
147}
148
149func vr_str(fd: i64, s: *u8, n: i64) -> i64 {
150 sys_write(fd, s, n)
151 return 0
152}
153
154func vr_i64(fd: i64, n: i64) -> i64 {
155 if n < 0 {
156 vr_putc(fd, 45)
157 return vr_i64(fd, -n)
158 }
159 if n == 0 {
160 vr_putc(fd, 48)
161 return 0
162 }
163 let digits: *u8 = sys_mmap(32)
164 var d: i64 = 0
165 var v: i64 = n
166 while v > 0 {
167 digits[d] = (v % 10) + 48
168 v = v / 10
169 d = d + 1
170 }
171 while d > 0 {
172 d = d - 1
173 vr_putc(fd, digits[d])
174 }
175 return 0
176}
177
178func nx_vc_emit_report(fd: i64, r: *MonthlyReport) -> i64 {
179 vr_str(fd, "{\"phase\":\"MONTHLY_VALIDATION\",\"cycle\":", 39)
180 vr_i64(fd, r.cycle_id)
181 vr_str(fd, ",\"entries\":", 11)
182 vr_i64(fd, r.qed_entries)
183 vr_str(fd, ",\"shards\":", 10)
184 vr_i64(fd, r.n_shards_used)
185 vr_str(fd, ",\"newly_proved\":", 16)
186 vr_i64(fd, r.stats.n_local_proved)
187 vr_str(fd, ",\"newly_matched\":", 17)
188 vr_i64(fd, r.stats.n_matches)
189 vr_str(fd, ",\"differs\":", 11)
190 vr_i64(fd, r.stats.n_differs)
191 vr_str(fd, ",\"total_local_proved\":", 22)
192 vr_i64(fd, r.aggregate_status_local_proved)
193 vr_str(fd, ",\"total_matches\":", 17)
194 vr_i64(fd, r.aggregate_status_matches_independent)
195 vr_str(fd, ",\"total_trusted\":", 17)
196 vr_i64(fd, r.aggregate_status_trusted_external)
197 vr_str(fd, ",\"total_unverified\":", 20)
198 vr_i64(fd, r.aggregate_status_unverified)
199 vr_str(fd, "}\n", 2)
200 return 0
201}