code wiki / (root) / nx_plane_check.nx

nx_plane_check.nx source

↩ module page · 180 lines · 9026 B

1// nx_plane_check.nx -- VERIFY the TSV<->NXR1 bridge against REAL production plane data, READ-ONLY. 2// 3// WHY THIS EXISTS AND WHY IT COMES BEFORE ANY WRITE: seq1369 shipped the bridge with a gate built on 4// SYNTHETIC fixtures. Fixtures prove the code does what I thought; they cannot prove real rows survive it. 5// Before a single production plane is rewritten, every row of that plane must be shown to make the round 6// trip tsv -> NXR1 -> tsv BYTE-IDENTICAL. This organ does exactly that and WRITES NOTHING. 7// 8// FAIL-CLOSED, and specifically against the VACUOUS-VERIFY TRAP: an empty or unreadable plane exits 4 9// rather than reporting "0 mismatches, all good". Zero rows checked is not a pass. This is the same trap 10// the TSV-retirement law already warns about (rowset-identical AND NON-EMPTY). 11// 12// COVERAGE IS REPORTED, NOT ASSUMED: it loads via sts_load_honest, whose flags expose that the q:n count 13// key can be LOWER than the rows actually present (measured on debt-: q:n said 125 while 629 segments held 14// 734+ rows). If rows exist beyond the declared count, this exits 5 -- the rows it checked were fine, but 15// the plane was not fully SEEN, and a partial check must never be presented as a complete one. 16// 17// EXIT: 0 all rows byte-identical and plane fully seen · 2 usage · 3 mismatch · 4 empty/unreadable 18// 5 clean so far but coverage incomplete (rows beyond the declared count) 19// license_tier: ORIGINAL No hw writes (Rule 26). 20import "nx_record_tsv.nx" 21import "nx_store_seed_lib.nx" 22 23const PC_CAP: i64 = 16777216 // 16MiB. NOT a fix -- a postponement, and deliberately far above the 24 // largest live plane so the TRUNCATION detector is exercised by a real 25 // ceiling rather than by a cap tuned to just barely pass. The real fix is 26 // streaming/paged plane reads (seq1326 rung); this only buys headroom. 27const PC_RECCAP: i64 = 131072 28const PC_OUTCAP: i64 = 131072 29const PC_MSGCAP: i64 = 4096 30const PC_TYPECAP: i64 = 512 31const PC_FLAGS: i64 = 64 32const PC_NL: i64 = 10 33const PC_CH_I: i64 = 105 // 'i' in a typespec means this column is an integer 34const PC_STDOUT: i64 = 1 35const PC_EXIT_USAGE: i64 = 2 36const PC_EXIT_MISMATCH: i64 = 3 37const PC_EXIT_EMPTY: i64 = 4 38const PC_EXIT_COVERAGE: i64 = 5 39const PC_EXIT_TRUNCATED: i64 = 6 40const PC_MAXSHOW: i64 = 5 // per-row detail lines shown before summarising 41 42func pc_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 43func pc_cat(d: *u8, off: i64, s: *u8) -> i64 { 44 var i: i64 = 0 45 while s[i] != (0 as u8) { d[off + i] = s[i]; i = i + 1 } 46 return off + i 47} 48func pc_emit(b: *u8, n: i64) -> i64 { sys_write(PC_STDOUT, b, n); return 0 } 49 50func main(argc: i64, argv: *i64) -> i64 { 51 let msg: *u8 = sys_mmap(PC_MSGCAP) 52 if argc < 2 { 53 var u: i64 = pc_cat(msg, 0, "usage: nx_plane_check <knowledge/store/prefix-> [typespec]\n typespec: one char per column, 'i'=integer, anything else=bytes (default: all bytes)\n" as *u8) 54 pc_emit(msg, u) 55 return PC_EXIT_USAGE 56 } 57 let prefix: *u8 = argv[1] as *u8 58 59 // typespec -> per-column NXR type codes. Absent typespec = every column stays raw bytes, which is 60 // the LOSSLESS default: never guess that a column is an integer, because guessing wrong is exactly 61 // how a migration silently rewrites data. 62 let types: *u8 = sys_mmap(PC_TYPECAP) 63 var ntypes: i64 = 0 64 if argc >= 3 { 65 let ts: *u8 = argv[2] as *u8 66 let tn: i64 = pc_len(ts) 67 var i: i64 = 0 68 while i < tn { 69 if i < PC_TYPECAP { 70 if ts[i] == (PC_CH_I as u8) { types[i] = NXR_T_I64 as u8 } else { types[i] = NXR_T_STR as u8 } 71 } 72 i = i + 1 73 } 74 ntypes = tn 75 if ntypes > PC_TYPECAP { ntypes = PC_TYPECAP } 76 } 77 78 let buf: *u8 = sys_mmap(PC_CAP) 79 let flags: *i64 = sys_mmap(PC_FLAGS) as *i64 80 let n: i64 = sts_load_honest(prefix, buf, PC_CAP, flags) 81 82 var rows: i64 = 0 83 var ok: i64 = 0 84 var mism: i64 = 0 85 var refused: i64 = 0 86 var shown: i64 = 0 87 88 let rec: *u8 = sys_mmap(PC_RECCAP) 89 let out: *u8 = sys_mmap(PC_OUTCAP) 90 var start: i64 = 0 91 var i2: i64 = 0 92 while i2 <= n { 93 var atend: i64 = 0 94 if i2 == n { atend = 1 } else { if buf[i2] == (PC_NL as u8) { atend = 1 } } 95 if atend == 1 { 96 let llen: i64 = i2 - start 97 if llen > 0 { 98 rows = rows + 1 99 let lp: *u8 = (buf as i64 + start) as *u8 100 let rn: i64 = rtv_to_nxr(lp, llen, types, ntypes, rec) 101 let cols: i64 = nxr_count(rec) 102 let on: i64 = rtv_to_tsv(rec, rn, cols, out, PC_OUTCAP) 103 if on < 0 { refused = refused + 1 } else { 104 var same: i64 = 0 105 if on == llen { 106 same = 1 107 var k: i64 = 0 108 while k < llen { if out[k] != lp[k] { same = 0; k = llen } else { k = k + 1 } } 109 } 110 if same == 1 { ok = ok + 1 } else { 111 mism = mism + 1 112 // Name the offending row so the failure is ACTIONABLE, not just counted. 113 if shown < PC_MAXSHOW { 114 var m: i64 = pc_cat(msg, 0, " MISMATCH row=" as *u8) 115 m = rtv_itoa(msg, m, rows) 116 m = pc_cat(msg, m, " cols=" as *u8) 117 m = rtv_itoa(msg, m, cols) 118 m = pc_cat(msg, m, " srclen=" as *u8) 119 m = rtv_itoa(msg, m, llen) 120 m = pc_cat(msg, m, " outlen=" as *u8) 121 m = rtv_itoa(msg, m, on) 122 msg[m] = PC_NL as u8 123 m = m + 1 124 pc_emit(msg, m) 125 shown = shown + 1 126 } 127 } 128 } 129 } 130 start = i2 + 1 131 } 132 i2 = i2 + 1 133 } 134 135 var o: i64 = pc_cat(msg, 0, "NX-PLANE-CHECK prefix=" as *u8) 136 o = pc_cat(msg, o, prefix) 137 o = pc_cat(msg, o, " rows=" as *u8); o = rtv_itoa(msg, o, rows) 138 o = pc_cat(msg, o, " identical=" as *u8); o = rtv_itoa(msg, o, ok) 139 o = pc_cat(msg, o, " mismatch=" as *u8); o = rtv_itoa(msg, o, mism) 140 o = pc_cat(msg, o, " refused=" as *u8); o = rtv_itoa(msg, o, refused) 141 o = pc_cat(msg, o, " bytes=" as *u8); o = rtv_itoa(msg, o, n) 142 o = pc_cat(msg, o, " declared_qn=" as *u8); o = rtv_itoa(msg, o, flags[0]) 143 o = pc_cat(msg, o, " loaded_rows=" as *u8); o = rtv_itoa(msg, o, flags[1]) 144 o = pc_cat(msg, o, " beyond_qn=" as *u8); o = rtv_itoa(msg, o, flags[2]) 145 o = pc_cat(msg, o, " cap=" as *u8); o = rtv_itoa(msg, o, PC_CAP) 146 o = pc_cat(msg, o, " verdict=" as *u8) 147 148 // TRUNCATION IS A COVERAGE LIE, AND I SHIPPED ONE. The FIRST run of this organ reported 149 // verdict=GREEN-all-rows-byte-identical on the debt- plane while bytes==cap and the rows I actually 150 // parsed (1273) were FEWER than the rows the loader said it loaded (1377): 104 rows were never 151 // checked and it called that a pass. That is exactly the class this organ exists to catch, occurring 152 // inside the organ itself -- and it was visible ONLY because the envelope prints bytes and cap. 153 // TWO INDEPENDENT DETECTORS, because either alone can be fooled: the buffer filling exactly, and the 154 // loader's own row count disagreeing with the number of lines parsed out of it. 155 // ★This is also seq1326's whole-plane-load ceiling biting in person: sts_load* materialises the 156 // ENTIRE plane into ONE buffer, so every reader inherits a hard cap. Raising the cap postpones it; 157 // streaming/paged reads are the actual fix, and that is a rung, not a knob. 158 var trunc: i64 = 0 159 if n >= PC_CAP { trunc = 1 } 160 if rows != flags[1] { trunc = 1 } 161 var rc: i64 = 0 162 if rows == 0 { rc = PC_EXIT_EMPTY } else { 163 if mism > 0 { rc = PC_EXIT_MISMATCH } else { 164 if refused > 0 { rc = PC_EXIT_MISMATCH } else { 165 if flags[2] > 0 { rc = PC_EXIT_COVERAGE } 166 } 167 } 168 } 169 if trunc == 1 { if rc == 0 { rc = PC_EXIT_TRUNCATED } } 170 if trunc == 1 { if rc == PC_EXIT_COVERAGE { rc = PC_EXIT_TRUNCATED } } 171 if rc == PC_EXIT_TRUNCATED { o = pc_cat(msg, o, "RED-LOAD-TRUNCATED-rows-were-never-checked" as *u8) } 172 if rc == 0 { o = pc_cat(msg, o, "GREEN-all-rows-byte-identical" as *u8) } 173 if rc == PC_EXIT_EMPTY { o = pc_cat(msg, o, "RED-EMPTY-nothing-checked-this-is-not-a-pass" as *u8) } 174 if rc == PC_EXIT_MISMATCH { o = pc_cat(msg, o, "RED-rows-do-not-round-trip" as *u8) } 175 if rc == PC_EXIT_COVERAGE { o = pc_cat(msg, o, "AMBER-checked-rows-clean-but-plane-NOT-fully-seen" as *u8) } 176 msg[o] = PC_NL as u8 177 o = o + 1 178 pc_emit(msg, o) 179 return rc 180}