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" 13 14const BG_CAP: i64 = 65536 15 16func 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 } 17func bg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 18 19func bg_eq(a: *u8, an: i64, b: *u8, bn: i64) -> i64 { 20 if an != bn { return 0 } 21 var i: i64 = 0 22 while i < an { if a[i] != b[i] { return 0 } i = i + 1 } 23 return 1 24} 25 26func main(argc: i64, argv: *i64) -> i64 { 27 var pass: i64 = 0 28 let outa: *u8 = sys_mmap(BG_CAP) 29 let outb: *u8 = sys_mmap(BG_CAP) 30 31 // T1: single-segment plane 32 let p1: *u8 = "/tmp/bgate1-" as *u8 33 let s1: *u8 = "alpha\tone\nbravo\ttwo\ncharlie\tthree\n" as *u8 34 sts_seed(p1, s1, bg_len(s1)) 35 let a1: i64 = sts_load(p1, outa, BG_CAP) 36 let b1: i64 = sts_load_slow(p1, outb, BG_CAP) 37 var t1: i64 = 0 38 if bg_eq(outa, a1, outb, b1) == 1 { if a1 > 0 { t1 = 1 } } 39 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) } 40 41 // T2: superseded plane -- second seed commits a NEW full snapshot; newest must win, both paths 42 let p2: *u8 = "/tmp/bgate2-" as *u8 43 let s2a: *u8 = "old1\nold2\nold3\n" as *u8 44 sts_seed(p2, s2a, bg_len(s2a)) 45 let s2b: *u8 = "new1\nnew2\nnew3\nnew4\n" as *u8 46 sts_seed(p2, s2b, bg_len(s2b)) 47 let a2: i64 = sts_load(p2, outa, BG_CAP) 48 let b2: i64 = sts_load_slow(p2, outb, BG_CAP) 49 var t2: i64 = 0 50 if bg_eq(outa, a2, outb, b2) == 1 { if bg_eq(outa, a2, s2b, bg_len(s2b)) == 1 { t2 = 1 } } 51 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) } 52 53 // T3: shrink plane -- 5 rows then 3; stale q:3/q:4 from the old segment must stay invisible 54 let p3: *u8 = "/tmp/bgate3-" as *u8 55 let s3a: *u8 = "r0\nr1\nr2\nr3\nr4\n" as *u8 56 sts_seed(p3, s3a, bg_len(s3a)) 57 let s3b: *u8 = "k0\nk1\nk2\n" as *u8 58 sts_seed(p3, s3b, bg_len(s3b)) 59 let a3: i64 = sts_load(p3, outa, BG_CAP) 60 let b3: i64 = sts_load_slow(p3, outb, BG_CAP) 61 var t3: i64 = 0 62 if bg_eq(outa, a3, outb, b3) == 1 { if bg_eq(outa, a3, s3b, bg_len(s3b)) == 1 { t3 = 1 } } 63 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) } 64 65 // T4: absent plane -> both paths return 0 66 let p4: *u8 = "/tmp/bgate4-absent-" as *u8 67 let a4: i64 = sts_load(p4, outa, BG_CAP) 68 let b4: i64 = sts_load_slow(p4, outb, BG_CAP) 69 var t4: i64 = 0 70 if a4 == 0 { if b4 == 0 { t4 = 1 } } 71 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) } 72 73 // T5: anti-vacuity -- the p2 result must DIFFER from the OLD snapshot (the compare can fail) 74 var t5: i64 = 0 75 if bg_eq(outa, a3, s3a, bg_len(s3a)) == 0 { t5 = 1 } 76 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) } 77 78 // T6: HONEST-LOADER POSITIVE -- p3 IS the shrink plane (q:n=3 while q:3/q:4 stay reachable from 79 // the older segment), byte-for-byte the debt- plane corruption that made nx_debt list report 80 // total=125 as fact. T3 proves sts_load LOADS correctly here; it reports NOTHING. sts_load_honest 81 // must DECLARE the 2 unreachable rows. Fails RED on the pre-fix lib (the symbol does not exist). 82 let fl: *i64 = sys_mmap(BG_CAP) as *i64 83 let a6: i64 = sts_load_honest(p3, outa, BG_CAP, fl) 84 var t6: i64 = 0 85 if bg_eq(outa, a6, s3b, bg_len(s3b)) == 1 { if fl[0] == 3 { if fl[1] == 3 { if fl[2] == 2 { t6 = 1 } } } } 86 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) } 87 88 // T7: ANTI-VACUITY for the detector -- p1 was never shrunk, so a HEALTHY plane must report ZERO 89 // unreachable. Without this tooth an always-on detector would still pass T6. 90 let fl2: *i64 = sys_mmap(BG_CAP) as *i64 91 let a7: i64 = sts_load_honest(p1, outa, BG_CAP, fl2) 92 var t7: i64 = 0 93 if a7 > 0 { if fl2[2] == 0 { t7 = 1 } } 94 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) } 95 96 bg_w("NX-STS-BULKLOAD-GATE pass=" as *u8) 97 let pb: *u8 = sys_mmap(8) 98 pb[0] = (48 + pass) as u8 99 pb[1] = 0 as u8 100 bg_w(pb) 101 if pass == 7 { 102 bg_w("/7 verdict=GREEN\n" as *u8) 103 sys_exit(0) 104 return 0 105 } 106 bg_w("/7 verdict=RED\n" as *u8) 107 sys_exit(1) 108 return 1 109}