nx_sts_bulkload_gate.nx source

1// nx_sts_bulkload_gate.nx -- GATE for the seq356 sts_load bulk path (5 teeth incl an anti-vacuity 2// negative). ORACLE = sts_load_slow (the verbatim pre-fix body): the new open-once path must be 3// BYTE-IDENTICAL to the old per-row path on every plane shape. No forks; imports the lib directly. 4// T1 single-segment plane identical + exact rows | T2 superseded plane (re-seed) identical AND 5// equals the NEWEST snapshot | T3 shrink plane (5 rows -> 3) identical, stale q:3/q:4 invisible | 6// T4 absent plane -> both 0 | T5 anti-vacuity: newest snapshot differs from the OLD snapshot 7// (proves the byte-compare tooth can fail). Mutation (manual): flip ss_hget's newest-first walk 8// -> T2/T3 RED. Verdict exit 0 iff 5/5. 9// license_tier: ORIGINAL No hw writes (Rule 26). 10import "nx_store_seed_lib.nx" 11import "nx_seg_store.nx" 12import "nx_syscalls.nx" 13import "nx_gate_verdict.nx" 14 15const BG_CAP: i64 = 65536 16 17func bg_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 18func bg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 19 20func bg_eq(a: *u8, an: i64, b: *u8, bn: i64) -> i64 { 21 if an != bn { return 0 } 22 var i: i64 = 0 23 while i < an { if a[i] != b[i] { return 0 } i = i + 1 } 24 return 1 25} 26 27func main(argc: i64, argv: *i64) -> i64 { 28 var pass: i64 = 0 29 let outa: *u8 = sys_mmap(BG_CAP) 30 let outb: *u8 = sys_mmap(BG_CAP) 31 32 // T1: single-segment plane 33 let p1: *u8 = "/tmp/bgate1-" as *u8 34 let s1: *u8 = "alpha\tone\nbravo\ttwo\ncharlie\tthree\n" as *u8 35 sts_seed(p1, s1, bg_len(s1)) 36 let a1: i64 = sts_load(p1, outa, BG_CAP) 37 let b1: i64 = sts_load_slow(p1, outb, BG_CAP) 38 var t1: i64 = 0 39 if bg_eq(outa, a1, outb, b1) == 1 { if a1 > 0 { t1 = 1 } } 40 if t1 == 1 { bg_w("T1 single-seg-identical PASS\n" as *u8); pass = pass + 1 } else { bg_w("T1 single-seg-identical FAIL\n" as *u8) } 41 42 // T2: superseded plane -- second seed commits a NEW full snapshot; newest must win, both paths 43 let p2: *u8 = "/tmp/bgate2-" as *u8 44 let s2a: *u8 = "old1\nold2\nold3\n" as *u8 45 sts_seed(p2, s2a, bg_len(s2a)) 46 let s2b: *u8 = "new1\nnew2\nnew3\nnew4\n" as *u8 47 sts_seed(p2, s2b, bg_len(s2b)) 48 let a2: i64 = sts_load(p2, outa, BG_CAP) 49 let b2: i64 = sts_load_slow(p2, outb, BG_CAP) 50 var t2: i64 = 0 51 if bg_eq(outa, a2, outb, b2) == 1 { if bg_eq(outa, a2, s2b, bg_len(s2b)) == 1 { t2 = 1 } } 52 if t2 == 1 { bg_w("T2 supersede-newest-wins PASS\n" as *u8); pass = pass + 1 } else { bg_w("T2 supersede-newest-wins FAIL\n" as *u8) } 53 54 // T3: shrink plane -- 5 rows then 3; stale q:3/q:4 from the old segment must stay invisible 55 let p3: *u8 = "/tmp/bgate3-" as *u8 56 let s3a: *u8 = "r0\nr1\nr2\nr3\nr4\n" as *u8 57 sts_seed(p3, s3a, bg_len(s3a)) 58 let s3b: *u8 = "k0\nk1\nk2\n" as *u8 59 sts_seed(p3, s3b, bg_len(s3b)) 60 let a3: i64 = sts_load(p3, outa, BG_CAP) 61 let b3: i64 = sts_load_slow(p3, outb, BG_CAP) 62 var t3: i64 = 0 63 if bg_eq(outa, a3, outb, b3) == 1 { if bg_eq(outa, a3, s3b, bg_len(s3b)) == 1 { t3 = 1 } } 64 if t3 == 1 { bg_w("T3 shrink-stale-invisible PASS\n" as *u8); pass = pass + 1 } else { bg_w("T3 shrink-stale-invisible FAIL\n" as *u8) } 65 66 // T4: absent plane -> both paths return 0 67 let p4: *u8 = "/tmp/bgate4-absent-" as *u8 68 let a4: i64 = sts_load(p4, outa, BG_CAP) 69 let b4: i64 = sts_load_slow(p4, outb, BG_CAP) 70 var t4: i64 = 0 71 if a4 == 0 { if b4 == 0 { t4 = 1 } } 72 if t4 == 1 { bg_w("T4 absent-plane-zero PASS\n" as *u8); pass = pass + 1 } else { bg_w("T4 absent-plane-zero FAIL\n" as *u8) } 73 74 // T5: anti-vacuity -- the p2 result must DIFFER from the OLD snapshot (the compare can fail) 75 var t5: i64 = 0 76 if bg_eq(outa, a3, s3a, bg_len(s3a)) == 0 { t5 = 1 } 77 if t5 == 1 { bg_w("T5 compare-non-vacuous PASS\n" as *u8); pass = pass + 1 } else { bg_w("T5 compare-non-vacuous FAIL\n" as *u8) } 78 79 // T6: HONEST-LOADER POSITIVE -- p3 IS the shrink plane (q:n=3 while q:3/q:4 stay reachable from 80 // the older segment), byte-for-byte the debt- plane corruption that made nx_debt list report 81 // total=125 as fact. T3 proves sts_load LOADS correctly here; it reports NOTHING. sts_load_honest 82 // must DECLARE the 2 unreachable rows. Fails RED on the pre-fix lib (the symbol does not exist). 83 let fl: *i64 = sys_mmap(BG_CAP) as *i64 84 let a6: i64 = sts_load_honest(p3, outa, BG_CAP, fl) 85 var t6: i64 = 0 86 if bg_eq(outa, a6, s3b, bg_len(s3b)) == 1 { if fl[0] == 3 { if fl[1] == 3 { if fl[2] == 2 { t6 = 1 } } } } 87 if t6 == 1 { bg_w("T6 honest-detects-unreachable PASS\n" as *u8); pass = pass + 1 } else { bg_w("T6 honest-detects-unreachable FAIL\n" as *u8) } 88 89 // T7: ANTI-VACUITY for the detector -- p1 was never shrunk, so a HEALTHY plane must report ZERO 90 // unreachable. Without this tooth an always-on detector would still pass T6. 91 let fl2: *i64 = sys_mmap(BG_CAP) as *i64 92 let a7: i64 = sts_load_honest(p1, outa, BG_CAP, fl2) 93 var t7: i64 = 0 94 if a7 > 0 { if fl2[2] == 0 { t7 = 1 } } 95 if t7 == 1 { bg_w("T7 honest-no-false-positive PASS\n" as *u8); pass = pass + 1 } else { bg_w("T7 honest-no-false-positive FAIL\n" as *u8) } 96 97 bg_w("NX-STS-BULKLOAD-GATE pass=" as *u8) 98 let pb: *u8 = sys_mmap(8) 99 pb[0] = (48 + pass) as u8 100 pb[1] = 0 as u8 101 bg_w(pb) 102 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 103 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 104 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 105 let ctr__dry: *i64 = gv_ctr() 106 ctr__dry[0] = pass 107 ctr__dry[1] = 7 108 let rc__dry: i64 = gv_verdict("STS-BULKLOAD-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 109 sys_exit(rc__dry) 110 return rc__dry 111}