code wiki / (root) / nx_campaign_verify.nx

nx_campaign_verify.nx source

↩ module page · 374 lines · 17214 B

1// nx_campaign_verify.nx -- DID THAT CAMPAIGN ACTUALLY DO WHAT IT CLAIMED, FOR EVERY ROW? 2// 3// WHY IT EXISTS, and it is a defect I committed today rather than one I read about. On 2026-08-07 I ran 4// two convergence campaigns (139 files, then 228) and "verified" them like this: 5// - byte identity: checked ALL rows -> honest 6// - import resolution: checked THE FIRST 40 OF 228, reported "ALL IMPORTS RESOLVE" 7// - surplus-line clusters: read the TOP 22 of 1,119 distinct lines, called it the distribution 8// Every one of those numbers was true about the sample and asserted about the population. The operator 9// named it exactly: "sample size bullshit ... full ecosystem scope". 10// => ★★★★★★A VERIFICATION THAT DOES NOT PRINT ITS DENOMINATOR IS A SAMPLE WEARING A PROOF'S CLOTHES. 11// => ★★★★★★A CHECK I HAVE TO REMEMBER TO RUN IN FULL IS A CHECK THAT WILL BE RUN IN PART. The estate 12// already banked why: A CAPABILITY OFFERED AS ADVICE IS ADOPTED AT ADVICE RATES; THE SAME 13// CAPABILITY PLACED IN THE PATH IS ADOPTED AT 100%. So this is an ORGAN the campaign CALLS, not a 14// discipline the operator maintains. 15// 16// WHAT IT PROVES, over the WHOLE adopted list, never a prefix: 17// 1. EVERY adopted row is byte-identical to the source it was adopted from (the adopt really landed) 18// 2. EVERY import edge in EVERY adopted file resolves in the TARGET tree (the tree stays coherent) 19// and it prints checked/total for both, so a shortfall is visible rather than inferable. 20// 21// !!IT REFUSES AN EMPTY OR UNREADABLE LIST. A gate that reports "0 of 0 failed, GREEN" on a list it 22// could not open is the absence-tooth defect the estate has already paid for twice: A TOOTH THAT 23// ASSERTS AN ABSENCE PASSES LOUDEST WHEN NOTHING RAN AT ALL. rows==0 is RED, not GREEN. 24// 25// !!IT IS A VERIFIER, NOT A GATE, AND THE NAME NOW SAYS SO. /api/ship REFUSED the first version under 26// D001: "this gate rolls its own verdict instead of inheriting nx_gate_verdict, so nothing can read its 27// outcome -- nx_gate_green cannot judge it and it records no harness.jrnl frame, so flake and erosion 28// stay invisible for it." There is an allow_own_verdict=yes escape hatch and taking it would have been 29// exempting my own gate from the convention it exists to enforce. The deeper error was the NAME: gates 30// here are no-arg and sweep-run, and a thing that takes a population in argv is a tool. 31// => ★★★★★★THE CONVENTION-ENFORCING MECHANISM CAUGHT THE CONVENTION-ENFORCING TOOL. A GUARD YOU 32// EXEMPT YOURSELF FROM IS NOT A GUARD, IT IS A PREFERENCE. 33// => ★★★★★NAMING A TOOL `*_gate` MAKES A CLAIM ABOUT HOW IT IS RUN AND JUDGED -- MEET THE CLAIM OR 34// CHANGE THE NAME. 35// Verdict + journalling are inherited from nx_gate_verdict (gv_check / gv_verdict), so nx_gate_green 36// can judge this like anything else and each run leaves a harness.jrnl frame. 37// Exit: gv_verdict's rc (0 GREEN, 1 RED) | 2 usage | 3 IO. 38// DIALECT: plain-if, <=6 params, consts above use, mmap'd static POINTERS (a BSS static array crashes 39// the module at startup -- banked gotcha). 40// license_tier: ORIGINAL expect_exit: 0 No hw writes (Rule 26). 41import "nx_gate_verdict.nx" 42import "nx_syscalls.nx" 43import "nx_sha256.nx" 44 45const CG_LINE: i64 = 4096 46const CG_PATH: i64 = 8192 47const CG_LIST: i64 = 8388608 // adopted list; 8MB holds ~100k rows 48const CG_FILE: i64 = 16777216 // one source file 49const CG_NUM: i64 = 64 50const CG_LF: i64 = 10 51const CG_CR: i64 = 13 52const CG_SP: i64 = 32 53const CG_TAB: i64 = 9 54const CG_QUOTE: i64 = 34 55const CG_SLASH: i64 = 47 56const CG_EMPTY_RESERVE: i64 = 4096 // sys_read_file reserves this for an empty file; free exactly it 57 58static cg_num: *u8 59static cg_rev: *u8 60static cg_ha: *u8 61static cg_hb: *u8 62static cg_pa: *u8 63static cg_pb: *u8 64static cg_ip: *u8 65static cg_walk: *u8 // cg_resolve's OWN scratch; it TRUNCATES as it walks up 66static cg_n: *i64 // [0]rows [1]checked [2]identical [3]edges [4]resolved [5]missing [6]badfiles 67 68func cg_puts(s: *u8) -> i64 { 69 var n: i64 = 0 70 while s[n] != (0 as u8) { n = n + 1 } 71 sys_write(1, s, n) 72 return 0 73} 74func cg_putn(v: i64) -> i64 { 75 var m: i64 = v 76 if m == 0 { cg_num[0] = 48 as u8; sys_write(1, cg_num, 1); return 0 } 77 if m < 0 { cg_puts("-" as *u8); m = 0 - m } 78 var k: i64 = 0 79 while m > 0 { cg_rev[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 80 var i: i64 = 0 81 while i < k { cg_num[i] = cg_rev[k - 1 - i]; i = i + 1 } 82 sys_write(1, cg_num, k) 83 return 0 84} 85func cg_join(root: *u8, rel: *u8, out: *u8) -> i64 { 86 var o: i64 = 0 87 while root[o] != (0 as u8) { out[o] = root[o]; o = o + 1 } 88 if o > 0 { if out[o-1] != (CG_SLASH as u8) { out[o] = CG_SLASH as u8; o = o + 1 } } 89 var k: i64 = 0 90 while rel[k] != (0 as u8) { out[o] = rel[k]; o = o + 1; k = k + 1 } 91 out[o] = 0 as u8 92 return o 93} 94// dir(path) + "/" + name -> out 95func cg_join_dir(path: *u8, name: *u8, out: *u8) -> i64 { 96 var last: i64 = 0 - 1 97 var i: i64 = 0 98 while path[i] != (0 as u8) { 99 if path[i] == (CG_SLASH as u8) { last = i } 100 i = i + 1 101 } 102 var o: i64 = 0 103 if last >= 0 { while o <= last { out[o] = path[o]; o = o + 1 } } 104 var k: i64 = 0 105 while name[k] != (0 as u8) { out[o] = name[k]; o = o + 1; k = k + 1 } 106 out[o] = 0 as u8 107 return o 108} 109// sha256 of a file into out (32 raw bytes). -1 unreadable. 110// !!FREES THE EMPTY-FILE RESERVATION EXACTLY: sys_read_file maps CG_EMPTY_RESERVE for a zero-length 111// file, so munmap'ing n+16 there would leak the reservation on every empty row. 112func cg_hash(path: *u8, out: *u8) -> i64 { 113 let ln: *i64 = sys_mmap(16) as *i64 114 ln[0] = 0 115 let buf: *u8 = sys_read_file(path, ln) 116 if (buf as i64) == 0 { sys_munmap(ln as *u8, 16); return 0 - 1 } 117 let n: i64 = ln[0] 118 sha256_digest(buf, n, out) 119 if n > 0 { sys_munmap(buf, n + 16) } else { sys_munmap(buf, CG_EMPTY_RESERVE + 16) } 120 sys_munmap(ln as *u8, 16) 121 return n 122} 123func cg_eq32(a: *u8, b: *u8) -> i64 { 124 var i: i64 = 0 125 while i < 32 { if a[i] != b[i] { return 0 } i = i + 1 } 126 return 1 127} 128func cg_exists(p: *u8) -> i64 { 129 let st: *u8 = sys_mmap(160) 130 let r: i64 = sys_fstatat(p, st) 131 sys_munmap(st, 160) 132 if r == 0 { return 1 } 133 return 0 134} 135// RESOLVE AN IMPORT THE WAY THE ACTUAL EXPANDER DOES, not the way that seemed obvious. 136// `import.nx` is the sovereign import preprocessor. Its try_resolve_import walks PARENT DIRECTORIES 137// (16 hops) and at EACH LEVEL tries, in order: the dir itself, hub/, wiki/, bin/, kernel/, _hdl_build/. 138// !!ITS OWN COMMENT LISTS ONLY hub/wiki/bin/kernel AND OMITS _hdl_build -- which sits three lines below 139// the comment, added later under debt 1785608999 and marked "tried LAST". I built this resolver from 140// that comment and it produced a FALSE dangling report for nx_html_sanitize.nx, a module that resolves 141// fine at build time. ⇒ ★★★★★★A COMMENT IS A CLAIM ABOUT THE CODE AS IT WAS; ONLY THE CODE IS A CLAIM 142// ABOUT THE CODE AS IT IS -- and this estate already banked that a scanner reading prose measures the 143// documentation, not the system. 144// 145// I guessed this rule THREE TIMES today before reading it, and was wrong in both directions: 146// dirname+root only -> too NARROW: reported 39 dangling edges that all resolve fine 147// basename-anywhere-in-tree-> too WIDE: would resolve modules the expander never looks for 148// Both are instruments measuring something other than what ships. 149// => ★★★★★★AN INSTRUMENT THAT MODELS A RULE INSTEAD OF READING IT MEASURES YOUR GUESS, NOT THE 150// SYSTEM. The rule was written down, in the header of the organ that implements it. 151// => ★★★★★WHEN A RESOLVER DISAGREES WITH ANOTHER RESOLVER, NEITHER IS EVIDENCE -- GO READ THE ONE 152// THAT ACTUALLY RUNS AT BUILD TIME. 153func cg_try(dir: *u8, sub: *u8, imp: *u8) -> i64 { 154 var o: i64 = 0 155 while dir[o] != (0 as u8) { cg_pb[o] = dir[o]; o = o + 1 } 156 if o > 0 { if cg_pb[o-1] != (CG_SLASH as u8) { cg_pb[o] = CG_SLASH as u8; o = o + 1 } } 157 var k: i64 = 0 158 while sub[k] != (0 as u8) { cg_pb[o] = sub[k]; o = o + 1; k = k + 1 } 159 k = 0 160 while imp[k] != (0 as u8) { cg_pb[o] = imp[k]; o = o + 1; k = k + 1 } 161 cg_pb[o] = 0 as u8 162 return cg_exists(cg_pb) 163} 164// !!WALKS IN ITS OWN BUFFER. The first version copied fpath into cg_pa and then truncated it to climb 165// parent directories -- but the caller PASSES cg_pa as fpath, so the first import destroyed the path of 166// the file being checked: every later resolution ran against a shortened path and the error line printed 167// an empty filename. It reported nx_gate_base.nx as dangling while sitting in the same directory as it. 168// => ★★★★★★A HELPER THAT MUTATES A CALLER'S BUFFER IS A BUG THE CALLER CANNOT SEE. (Third instance 169// today of the same class -- committed here inside the very gate built to enforce the discipline. 170// ★A LAW YOU CAN RECITE IS NOT A LAW YOU HAVE MECHANISED.) 171func cg_resolve(fpath: *u8, imp: *u8, troot: *u8) -> i64 { 172 var n: i64 = 0 173 while fpath[n] != (0 as u8) { cg_walk[n] = fpath[n]; n = n + 1 } 174 cg_walk[n] = 0 as u8 175 var lvl: i64 = 0 176 while lvl < 16 { 177 // strip the last path component to get this level's directory 178 var last: i64 = 0 - 1 179 var i: i64 = 0 180 while cg_walk[i] != (0 as u8) { 181 if cg_walk[i] == (CG_SLASH as u8) { last = i } 182 i = i + 1 183 } 184 if last < 0 { lvl = 8 } else { 185 cg_walk[last] = 0 as u8 186 if cg_try(cg_walk, "" as *u8, imp) == 1 { return 1 } 187 if cg_try(cg_walk, "hub/" as *u8, imp) == 1 { return 1 } 188 if cg_try(cg_walk, "wiki/" as *u8, imp) == 1 { return 1 } 189 if cg_try(cg_walk, "bin/" as *u8, imp) == 1 { return 1 } 190 if cg_try(cg_walk, "kernel/" as *u8, imp) == 1 { return 1 } 191 if cg_try(cg_walk, "_hdl_build/" as *u8, imp) == 1 { return 1 } 192 lvl = lvl + 1 193 } 194 } 195 if cg_try(troot, "" as *u8, imp) == 1 { return 1 } 196 return 0 197} 198// Every import edge of one adopted file, resolved against the TARGET tree. Returns unresolved count. 199func cg_check_imports(fpath: *u8, troot: *u8) -> i64 { 200 let ln: *i64 = sys_mmap(16) as *i64 201 ln[0] = 0 202 let buf: *u8 = sys_read_file(fpath, ln) 203 if (buf as i64) == 0 { sys_munmap(ln as *u8, 16); return 0 - 1 } 204 let n: i64 = ln[0] 205 var bad: i64 = 0 206 var p: i64 = 0 207 while p < n { 208 var e: i64 = p 209 var go: i64 = 1 210 while go == 1 { 211 if e >= n { go = 0 } else { 212 if buf[e] == (CG_LF as u8) { go = 0 } else { e = e + 1 } 213 } 214 } 215 var i: i64 = p 216 var gw: i64 = 1 217 while gw == 1 { 218 if i >= e { gw = 0 } else { 219 var w: i64 = 0 220 if buf[i] == (CG_SP as u8) { w = 1 } 221 if buf[i] == (CG_TAB as u8) { w = 1 } 222 if w == 1 { i = i + 1 } else { gw = 0 } 223 } 224 } 225 var isi: i64 = 0 226 if i + 7 <= e { 227 if buf[i] == (105 as u8) { if buf[i+1] == (109 as u8) { if buf[i+2] == (112 as u8) { 228 if buf[i+3] == (111 as u8) { if buf[i+4] == (114 as u8) { if buf[i+5] == (116 as u8) { 229 isi = 1 230 } } } } } } 231 } 232 if isi == 1 { 233 var q: i64 = i + 6 234 var s0: i64 = 0 - 1 235 var gq: i64 = 1 236 while gq == 1 { 237 if q >= e { gq = 0 } else { 238 if buf[q] == (CG_QUOTE as u8) { s0 = q + 1; gq = 0 } else { q = q + 1 } 239 } 240 } 241 if s0 > 0 { 242 var q2: i64 = s0 243 var s1: i64 = 0 - 1 244 var g2: i64 = 1 245 while g2 == 1 { 246 if q2 >= e { g2 = 0 } else { 247 if buf[q2] == (CG_QUOTE as u8) { s1 = q2; g2 = 0 } else { q2 = q2 + 1 } 248 } 249 } 250 if s1 > s0 { 251 var k: i64 = 0 252 while k < (s1 - s0) { cg_ip[k] = buf[s0 + k]; k = k + 1 } 253 cg_ip[k] = 0 as u8 254 cg_n[3] = cg_n[3] + 1 255 let ok: i64 = cg_resolve(fpath, cg_ip, troot) 256 if ok == 1 { cg_n[4] = cg_n[4] + 1 } else { 257 bad = bad + 1 258 cg_puts(" DANGLING-IMPORT " as *u8); cg_puts(cg_ip) 259 cg_puts(" in " as *u8); cg_puts(fpath); cg_puts("\n" as *u8) 260 } 261 } 262 } 263 } 264 p = e + 1 265 } 266 if n > 0 { sys_munmap(buf, n + 16) } else { sys_munmap(buf, CG_EMPTY_RESERVE + 16) } 267 sys_munmap(ln as *u8, 16) 268 return bad 269} 270 271func main(argc: i64, argv: *i64) -> i64 { 272 cg_num = sys_mmap(CG_NUM) 273 cg_rev = sys_mmap(CG_NUM) 274 if argc < 4 { 275 cg_puts("usage: nx_campaign_verify <adopted.list> <source-root> <target-root>\n" as *u8) 276 cg_puts(" Proves, over the WHOLE list and never a prefix, that a convergence campaign did\n" as *u8) 277 cg_puts(" what it claimed: every adopted row byte-identical to its source, and every import\n" as *u8) 278 cg_puts(" edge in every adopted file resolving in the target tree.\n" as *u8) 279 cg_puts(" Prints checked/total for both -- a verification without a denominator is a sample.\n" as *u8) 280 cg_puts(" An empty or unreadable list is RED, never a comforting GREEN.\n" as *u8) 281 sys_exit(2) 282 return 2 283 } 284 cg_ha = sys_mmap(64) 285 cg_hb = sys_mmap(64) 286 cg_pa = sys_mmap(CG_PATH) 287 cg_pb = sys_mmap(CG_PATH) 288 cg_ip = sys_mmap(CG_PATH) 289 cg_walk = sys_mmap(CG_PATH) 290 cg_n = sys_mmap(128) as *i64 291 var z: i64 = 0 292 while z < 8 { cg_n[z] = 0; z = z + 1 } 293 294 let ln: *i64 = sys_mmap(16) as *i64 295 ln[0] = 0 296 let lb: *u8 = sys_read_file(argv[1] as *u8, ln) 297 if (lb as i64) == 0 { 298 cg_puts("# CAMPAIGN-GATE RED -- cannot read the adopted list. A gate that cannot see its\n" as *u8) 299 cg_puts("# population must not report on it.\n" as *u8) 300 sys_exit(3) 301 return 3 302 } 303 let n: i64 = ln[0] 304 cg_puts("=== nx_campaign_verify -- FULL-POPULATION campaign verification ===\n" as *u8) 305 306 var p: i64 = 0 307 while p < n { 308 let base: i64 = lb as i64 309 var e: i64 = p 310 var go: i64 = 1 311 while go == 1 { 312 if e >= n { go = 0 } else { 313 if lb[e] == (CG_LF as u8) { go = 0 } else { e = e + 1 } 314 } 315 } 316 var t: i64 = e 317 if t > p { if lb[t-1] == (CG_CR as u8) { t = t - 1 } } 318 lb[t] = 0 as u8 319 let rel: *u8 = (base + p) as *u8 320 if rel[0] != (0 as u8) { 321 cg_n[0] = cg_n[0] + 1 322 cg_join(argv[2] as *u8, rel, cg_pa) 323 let ra: i64 = cg_hash(cg_pa, cg_ha) 324 cg_join(argv[3] as *u8, rel, cg_pb) 325 let rb: i64 = cg_hash(cg_pb, cg_hb) 326 if ra < 0 { cg_n[5] = cg_n[5] + 1 } else { 327 if rb < 0 { cg_n[5] = cg_n[5] + 1 } else { 328 cg_n[1] = cg_n[1] + 1 329 if cg_eq32(cg_ha, cg_hb) == 1 { cg_n[2] = cg_n[2] + 1 } else { 330 cg_n[6] = cg_n[6] + 1 331 cg_puts(" NOT-IDENTICAL " as *u8); cg_puts(rel); cg_puts("\n" as *u8) 332 } 333 // import coherence is checked on the TARGET copy -- the tree we just mutated 334 cg_join(argv[3] as *u8, rel, cg_pa) 335 cg_check_imports(cg_pa, argv[3] as *u8) 336 } } 337 } 338 p = e + 1 339 } 340 341 let ctr: *i64 = gv_ctr() 342 gv_head("nx_campaign_verify -- full-population proof that a convergence campaign did what it claimed" as *u8) 343 cg_puts("# CAMPAIGN-VERIFY rows=" as *u8); cg_putn(cg_n[0]) 344 cg_puts(" checked=" as *u8); cg_putn(cg_n[1]) 345 cg_puts(" identical=" as *u8); cg_putn(cg_n[2]) 346 cg_puts(" unreadable=" as *u8); cg_putn(cg_n[5]) 347 cg_puts(" importEdges=" as *u8); cg_putn(cg_n[3]) 348 cg_puts(" importsResolved=" as *u8); cg_putn(cg_n[4]) 349 cg_puts(" 350" as *u8) 351 352 // Each clause is stated as a RATIO against the population, never as a bare boolean, so the 353 // denominator is in the transcript whether the clause passes or fails. 354 var nonempty: i64 = 0 355 if cg_n[0] > 0 { nonempty = 1 } 356 gv_check("T1 population NON-EMPTY (0 rows proves nothing; an empty list is RED)" as *u8, nonempty, ctr) 357 358 var allread: i64 = 0 359 if cg_n[0] > 0 { if cg_n[1] == cg_n[0] { allread = 1 } } 360 gv_check("T2 EVERY row readable -- checked == rows, no prefix, no sample" as *u8, allread, ctr) 361 362 var allident: i64 = 0 363 if cg_n[0] > 0 { if cg_n[2] == cg_n[0] { allident = 1 } } 364 gv_check("T3 EVERY adopted row byte-identical to the source it was adopted from" as *u8, allident, ctr) 365 366 var allimp: i64 = 0 367 if cg_n[4] == cg_n[3] { allimp = 1 } 368 gv_check("T4 EVERY import edge in EVERY adopted file resolves in the target tree" as *u8, allimp, ctr) 369 370 let rc: i64 = gv_verdict("CAMPAIGN-VERIFY" as *u8, ctr, 371 "full-population campaign proof: byte identity and import coherence over 100% of the rows, denominators stated" as *u8) 372 sys_exit(rc) 373 return rc 374}