nx_workstream_registry_neg.nx source

1// nx_workstream_registry_neg.nx -- NEGATIVE-CONTROL PROOF for WMS-R1 (companion to the gate). 2// Proves the gate's audit/neg-control machinery can ACTUALLY detect failure -- a GREEN with no 3// working neg-control is INVALID (no-false-green law). It exercises ws_audit_complete + ws_get on 4// two CONTRASTING hermetic stores and asserts they give DIFFERENT, correct answers: 5// 6// N1 complete-store-audits-0 : a store whose ws:ids ids ALL have committed segments -> audit==0. 7// (If the audit were a constant non-zero, this FAILS -> proves the 8// gate's T3/T5 contrast is real, not a rigged constant.) 9// N2 missing-store-audits-1 : the SAME store + one id appended to ws:ids with NO segment -> 10// audit==1 and that id is reported. (If the audit were a constant 0, 11// this FAILS -> proves a lost segment is genuinely caught.) 12// N3 false-hit-would-fail : ws_get of a never-registered id returns WS_UNKNOWN, and a 13// committed id returns WS_FOUND -> the two are DISTINGUISHED (a 14// ws_get that always returned 1 would collapse them). 15// GREEN only if N1 .. N3 hold: audit returns DIFFERENT answers for complete vs missing, and get 16// distinguishes present vs absent. Evidence -> knowledge/status/workstream_registry_gate.log. 17// license_tier: ORIGINAL 18import "nx_workstream_store.nx" 19import "nx_seg_store.nx" 20import "nx_syscalls.nx" 21 22const WRN_LOG: *u8 = "knowledge/status/workstream_registry_gate.log" 23const NEGC_PREFIX: *u8 = "knowledge/store/wsnegc-" // complete store (every id has a segment) 24const NEGM_PREFIX: *u8 = "knowledge/store/wsnegm-" // missing store (one id has NO segment) 25 26func wrn_w(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 } 27func wrn_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 28 29func wrn_streq(a: *u8, b: *u8) -> i64 { 30 var i: i64 = 0 31 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 } 32 if b[i] != (0 as u8) { return 0 } 33 return 1 34} 35 36func wrn_streq_store(prefix: *u8, key: *u8, val: *u8) -> i64 { 37 let pq: *i64 = sys_mmap(16) as *i64 38 let lq: *i64 = sys_mmap(16) as *i64 39 if ss_get(prefix, key, pq, lq) != 1 { return 0 } 40 let b: *u8 = pq[0] as *u8 41 let n: i64 = lq[0] 42 let vl: i64 = wrn_len(val) 43 if n != vl { return 0 } 44 var i: i64 = 0 45 while i < n { if b[i] != val[i] { return 0 } i = i + 1 } 46 return 1 47} 48 49func wrn_seed_one(prefix: *u8, key: *u8, val: *u8) -> i64 { 50 if wrn_streq_store(prefix, key, val) == 1 { return 1 } 51 let w: *i64 = ss_begin() 52 ss_add(w, 1, key, val, wrn_len(val)) 53 let segid: i64 = ws_seg_next(prefix) 54 return ss_commit(prefix, w, segid) 55} 56 57func wrn_in_ids(ids_out: *i64, cnt: i64, tok: *u8) -> i64 { 58 var i: i64 = 0 59 while i < cnt { if wrn_streq(ids_out[i] as *u8, tok) == 1 { return 1 } i = i + 1 } 60 return 0 61} 62 63func wrn_row(fd: i64, name: *u8, pass: i64) -> i64 { 64 wrn_w(fd, " "); wrn_w(fd, name) 65 if pass == 1 { wrn_w(fd, " PASS\n" as *u8) } else { wrn_w(fd, " FAIL\n" as *u8) } 66 return 0 67} 68 69func main() -> i64 { 70 let missing: *i64 = sys_mmap(8 * 32) as *i64 71 let pq: *i64 = sys_mmap(16) as *i64 72 let lq: *i64 = sys_mmap(16) as *i64 73 74 // ---- COMPLETE store: ws:ids = {N-A,N-B}, BOTH segments committed ---- 75 wrn_seed_one(NEGC_PREFIX, "ws:empires" as *u8, "E-CORE\tE-GAME" as *u8) 76 wrn_seed_one(NEGC_PREFIX, "ws:ids" as *u8, "N-A\tN-B" as *u8) 77 wrn_seed_one(NEGC_PREFIX, "ws:N-A" as *u8, "N-A\tE-CORE\tDONE\t0\t-\t-\t-" as *u8) 78 wrn_seed_one(NEGC_PREFIX, "ws:N-B" as *u8, "N-B\tE-GAME\tACTIVE\t0\t-\t-\t-" as *u8) 79 80 // ---- MISSING store: ws:ids = {N-A,N-GONE}, only N-A committed (N-GONE = lost segment) ---- 81 wrn_seed_one(NEGM_PREFIX, "ws:empires" as *u8, "E-CORE\tE-GAME" as *u8) 82 wrn_seed_one(NEGM_PREFIX, "ws:ids" as *u8, "N-A\tN-GONE" as *u8) 83 wrn_seed_one(NEGM_PREFIX, "ws:N-A" as *u8, "N-A\tE-CORE\tDONE\t0\t-\t-\t-" as *u8) 84 // ws:N-GONE intentionally NOT committed. 85 86 // N1: complete store audits to 0 (proves audit is NOT a constant non-zero). 87 let mc: i64 = ws_audit_complete_p(NEGC_PREFIX, missing, 32) 88 var n1: i64 = 0 89 if mc == 0 { n1 = 1 } 90 91 // N2: missing store audits to >=1 with N-GONE reported (proves audit is NOT a constant 0). 92 let mm: i64 = ws_audit_complete_p(NEGM_PREFIX, missing, 32) 93 var n2: i64 = 0 94 if mm >= 1 { if wrn_in_ids(missing, mm, "N-GONE" as *u8) == 1 { n2 = 1 } } 95 96 // N3: ws_get distinguishes present (WS_FOUND) from never-registered (WS_UNKNOWN). 97 let rp: i64 = ws_get_p(NEGC_PREFIX, "ws:N-A" as *u8, pq, lq) 98 let rn: i64 = ws_get_p(NEGC_PREFIX, "ws:N-NEVER" as *u8, pq, lq) 99 var n3: i64 = 0 100 if rp == WS_FOUND { if rn == WS_UNKNOWN { n3 = 1 } } 101 102 var passes: i64 = 0 103 if n1 == 1 { passes = passes + 1 } 104 if n2 == 1 { passes = passes + 1 } 105 if n3 == 1 { passes = passes + 1 } 106 var ok: i64 = 0 107 if passes == 3 { ok = 1 } 108 109 wrn_w(1, "WMS-R1 NEG-CONTROL proof (audit/get genuinely detect failure)\n" as *u8) 110 wrn_row(1, "N1 complete-store-audits-0 " as *u8, n1) 111 wrn_row(1, "N2 missing-store-audits>=1 " as *u8, n2) 112 wrn_row(1, "N3 get-distinguishes-pres " as *u8, n3) 113 if ok == 1 { wrn_w(1, "verdict=GREEN\n" as *u8) } else { wrn_w(1, "verdict=RED\n" as *u8) } 114 115 let lf: i64 = sys_openat_append(WRN_LOG, 420) 116 if lf >= 0 { 117 wrn_w(lf, "WMS-R1-NEGC authored=organ " as *u8) 118 if ok == 1 { wrn_w(lf, "N1complete=0 N2missing>=1 N3get-distinguishes verdict=GREEN\n" as *u8) } else { wrn_w(lf, "verdict=RED\n" as *u8) } 119 sys_close(lf) 120 } 121 122 if ok == 1 { return 0 } 123 return 1 124}