nx_ss_verify_gate.nx source

1import "nx_gate_verdict.nx" 2import "nx_seg_store.nx" 3import "nx_syscalls.nx" 4// nx_ss_verify_gate.nx -- BITE gate for ss_verify_merged (verify-then-commit, 2026-08-07). 5// 6// WHY THIS EXISTS. ss_verify_merged was added so the compactor re-reads the segment it just wrote and 7// proves it reproduces the merged table BEFORE the manifest swap. Running the compaction gate with it 8// active showed 9/9 GREEN -- but an ss_verify_merged that unconditionally returned 0 would produce 9// byte-identical output. ★A GUARD THAT HAS ONLY EVER PASSED IS UNVERIFIED. So every tooth below is a 10// gv_bite: the verifier must FIRE on a crafted disagreement AND stay SILENT on the exact match. A 11// green here means the check is real, not merely present. 12// 13// CONSTRUCTION. A segment is written from a table this gate builds itself, so the table and the 14// artifact are known to agree by construction; each bite then perturbs ONE field, runs the verifier, 15// restores the field, and runs it again. The restore-and-re-pass is what proves the RED came from the 16// mutation and not from state the previous tooth damaged -- the failure mode that made 17// _ss_compact_cap_gate green exactly once. 18// 19// Verdict emission INHERITS nx_gate_verdict (D001): this gate does not roll its own, so nx_gate_green 20// can judge it and it records a harness frame. 21// license_tier: ORIGINAL No hw writes (Rule 26). 22 23const SSV_K: i64 = 64 24const SSV_SEGID: i64 = 700001 25const SSV_ABSENT_SEGID: i64 = 700999 26const SSV_KLEN: i64 = 6 27const SSV_VLEN: i64 = 5 28const SSV_DIRMODE: i64 = 0x1ed 29const SSV_PROBE_I: i64 = 7 30const SSV_KIND_I: i64 = 9 31const SSV_KLEN_I: i64 = 13 32 33// "vk:NNN" -- 6 bytes, null-terminated 34func ssv_kbuf(n: i64, out: *u8) -> i64 { 35 out[0] = 118 as u8 36 out[1] = 107 as u8 37 out[2] = 58 as u8 38 out[3] = (48 + (n / 100) % 10) as u8 39 out[4] = (48 + (n / 10) % 10) as u8 40 out[5] = (48 + n % 10) as u8 41 out[6] = 0 as u8 42 return SSV_KLEN 43} 44// "vvNNN" -- 5 bytes, null-terminated 45func ssv_vbuf(n: i64, out: *u8) -> i64 { 46 out[0] = 118 as u8 47 out[1] = 118 as u8 48 out[2] = (48 + (n / 100) % 10) as u8 49 out[3] = (48 + (n / 10) % 10) as u8 50 out[4] = (48 + n % 10) as u8 51 out[5] = 0 as u8 52 return SSV_VLEN 53} 54 55// run the verifier against the CURRENT table state; 1 = it fired (disagreed), 0 = it was silent 56func ssv_fired(prefix: *u8, segid: i64, tkp: *i64, tkl: *i64, tkind: *i64, tvp: *i64, tvl: *i64, nk: i64, hidx: *i64, hcap: i64) -> i64 { 57 if ss_verify_merged(prefix, segid, tkp, tkl, tkind, tvp, tvl, nk, hidx, hcap) != 0 { return 1 } 58 return 0 59} 60 61func main() -> i64 { 62 let ctr: *i64 = gv_ctr() 63 gv_head("nx_ss_verify_gate -- ss_verify_merged must FIRE on a segment that disagrees with the merged table, and stay SILENT on one that agrees" as *u8) 64 65 sys_mkdir("/tmp/ssvgate\x00" as *u8, SSV_DIRMODE) 66 let prefix: *u8 = "/tmp/ssvgate/_ssv-" as *u8 67 68 let tkp: *i64 = sys_mmap(8 * SSV_K) as *i64 69 let tkl: *i64 = sys_mmap(8 * SSV_K) as *i64 70 let tkind: *i64 = sys_mmap(8 * SSV_K) as *i64 71 let tvp: *i64 = sys_mmap(8 * SSV_K) as *i64 72 let tvl: *i64 = sys_mmap(8 * SSV_K) as *i64 73 var hcap: i64 = 16 74 while hcap < SSV_K * 2 { hcap = hcap * 2 } 75 let hidx: *i64 = sys_mmap(8 * hcap) as *i64 76 77 // build the table AND the segment from the same source, so they agree by construction 78 let w: *i64 = ss_begin() 79 var i: i64 = 0 80 while i < SSV_K { 81 let kb: *u8 = sys_mmap(16) 82 let vb: *u8 = sys_mmap(16) 83 ssv_kbuf(i, kb) 84 ssv_vbuf(i, vb) 85 tkp[i] = kb as i64 86 tkl[i] = SSV_KLEN 87 tkind[i] = 1 88 tvp[i] = vb as i64 89 tvl[i] = SSV_VLEN 90 var probe: i64 = ss_khash(kb, SSV_KLEN) & (hcap - 1) 91 while hidx[probe] != 0 { probe = (probe + 1) & (hcap - 1) } 92 hidx[probe] = i + 1 93 ss_add2(w, 1, kb, SSV_KLEN, vb, SSV_VLEN) 94 i = i + 1 95 } 96 if ss_write_seg(prefix, w, SSV_SEGID) != 0 { 97 gv_puts("SETUP FAIL: cannot write the fixture segment\ 98" as *u8) 99 sys_exit(1) 100 return 1 101 } 102 103 // ---- T1: the exact match must be accepted (the control every bite below is measured against) 104 var t1: i64 = 0 105 if ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) == 0 { t1 = 1 } 106 gv_check("T1 accepts a segment that matches its table exactly" as *u8, t1, ctr) 107 108 // ---- T2: key COUNT too high == a key vanished from the output. This is the tooth a per-record 109 // check cannot have: every record present still verifies, so only the count sees the loss. 110 let b2: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K + 1, hidx, hcap) 111 let g2: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) 112 gv_bite("T2 fires when a key is MISSING from the output (count too high)" as *u8, b2, g2, ctr) 113 114 // ---- T3: key COUNT too low == the writer emitted a key twice 115 let b3: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K - 1, hidx, hcap) 116 let g3: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) 117 gv_bite("T3 fires when a key is DUPLICATED in the output (count too low)" as *u8, b3, g3, ctr) 118 119 // ---- T4: one VALUE byte differs. Size-preserving by construction -- a byte count cannot see it. 120 let vb4: *u8 = tvp[SSV_PROBE_I] as *u8 121 let sv4: i64 = vb4[2] as i64 122 vb4[2] = (sv4 + 1) as u8 123 let b4: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) 124 vb4[2] = sv4 as u8 125 let g4: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) 126 gv_bite("T4 fires on a single differing VALUE byte (same length)" as *u8, b4, g4, ctr) 127 128 // ---- T5: KIND differs (a put recorded where a tombstone belongs, or the reverse) 129 let sv5: i64 = tkind[SSV_KIND_I] 130 tkind[SSV_KIND_I] = 2 131 let b5: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) 132 tkind[SSV_KIND_I] = sv5 133 let g5: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) 134 gv_bite("T5 fires when a record KIND disagrees (put vs tombstone)" as *u8, b5, g5, ctr) 135 136 // ---- T6: a key in the output is not findable in the table (key length corrupted so ss_kcmp 137 // misses). Proves the probe REFUSES rather than silently accepting an unmatched record. 138 let sv6: i64 = tkl[SSV_KLEN_I] 139 tkl[SSV_KLEN_I] = SSV_KLEN - 1 140 let b6: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) 141 tkl[SSV_KLEN_I] = sv6 142 let g6: i64 = ssv_fired(prefix, SSV_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) 143 gv_bite("T6 fires when an output key is UNFINDABLE in the table" as *u8, b6, g6, ctr) 144 145 // ---- T7: a missing artifact must REFUSE, never pass by vacuous absence. This is the tooth that 146 // catches the whole class where nothing ran at all and the check reported success. 147 var t7: i64 = 0 148 if ssv_fired(prefix, SSV_ABSENT_SEGID, tkp, tkl, tkind, tvp, tvl, SSV_K, hidx, hcap) == 1 { t7 = 1 } 149 gv_check("T7 refuses when the segment file is ABSENT (no vacuous pass)" as *u8, t7, ctr) 150 151 let rc: i64 = gv_verdict("SS-VERIFY-GATE" as *u8, ctr, "ss_verify_merged fires on missing/duplicated keys, a differing value byte, a wrong kind, an unfindable key and an absent artifact -- and is silent on the exact match" as *u8) 152 sys_exit(rc) 153 return rc 154}