code wiki / _hdl_build / nx_reader_census_gate.nx

nx_reader_census_gate.nx source

↩ module page · 74 lines · 3992 B

1import "nx_gate_gn.nx" 2// nx_reader_census_gate.nx -- liar-kill gate: the reader census lives in the SOVEREIGN seg-store (NO TSV), proven 3// by reading the STORE directly (not the .tsv). Walks rc:ids, reads every rc:<id>, checks each has a valid status 4// field, asserts a known cell (rc:SC59 = the zero-JS reader, must be HAVE), and a NEGATIVE CONTROL: a bogus key is 5// ABSENT (the store never fabricates). Independent of the .tsv -> safe to delete the tsv after this is GREEN. 6// expect_exit: 0 7import "nx_reader_census_store.nx" // rc_get / rc_field 8import "nx_seg_store.nx" 9import "nx_syscalls.nx" 10import "nx_gate_verdict.nx" 11 12func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 13func gstreq(a: *u8, b: *u8) -> i64 { var i: i64=0; while a[i]!=(0 as u8){ if a[i]!=b[i]{return 0} i=i+1 } if b[i]!=(0 as u8){return 0} return 1 } 14 15func main() -> i64 { 16 gp("=== nx_reader_census_gate: census in the sovereign seg-store, read from the STORE (no tsv) ===\n" as *u8) 17 var pass: i64 = 0; var fail: i64 = 0 18 19 let pq: *i64 = sys_mmap(16) as *i64 20 let lq: *i64 = sys_mmap(16) as *i64 21 if rc_get("rc:ids" as *u8, pq, lq) == 1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL no-index\n" as *u8); gp("READER-CENSUS-GATE verdict=RED\n" as *u8); sys_exit(1); return 1 } 22 let ids: *u8 = pq[0] as *u8 23 let idn: i64 = lq[0] 24 25 let idbuf: *u8 = sys_mmap(64) 26 let keybuf: *u8 = sys_mmap(128) 27 let stbuf: *u8 = sys_mmap(64) 28 let rq: *i64 = sys_mmap(16) as *i64 29 let rl: *i64 = sys_mmap(16) as *i64 30 31 var cells: i64 = 0 32 var valid_status: i64 = 0 33 var i: i64 = 0 34 while i < idn { 35 var o: i64 = 0 36 while i < idn { if ids[i] == (9 as u8) { break } idbuf[o] = ids[i]; o = o + 1; i = i + 1 } 37 if i < idn { i = i + 1 } 38 idbuf[o] = 0 as u8 39 if o > 0 { 40 keybuf[0]=114 as u8; keybuf[1]=99 as u8; keybuf[2]=58 as u8 41 var k: i64=0; while k<o { keybuf[3+k]=idbuf[k]; k=k+1 } keybuf[3+o]=0 as u8 42 if rc_get(keybuf, rq, rl) == 1 { 43 cells = cells + 1 44 rc_field(rq[0] as *u8, rl[0], 5, stbuf) 45 if gstreq(stbuf,"HAVE" as *u8)==1 { valid_status=valid_status+1 } 46 else { if gstreq(stbuf,"PARTIAL" as *u8)==1 { valid_status=valid_status+1 } 47 else { if gstreq(stbuf,"MISSING" as *u8)==1 { valid_status=valid_status+1 } } } 48 } 49 } 50 } 51 gp(" cells_in_store=" as *u8); gn(cells); gp(" valid_status=" as *u8); gn(valid_status); gp("\n" as *u8) 52 if cells >= 60 { pass=pass+1 } else { fail=fail+1; gp(" FAIL too-few-cells\n" as *u8) } 53 if valid_status == cells { pass=pass+1 } else { fail=fail+1; gp(" FAIL bad-status-field\n" as *u8) } 54 55 // a known cell: rc:SC59 (the ZERO-JS reader capability) must be present + HAVE 56 if rc_get("rc:SC59" as *u8, rq, rl) == 1 { 57 let st: *u8 = sys_mmap(64); rc_field(rq[0] as *u8, rl[0], 5, st) 58 if gstreq(st, "HAVE" as *u8) == 1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL SC59-not-HAVE\n" as *u8) } 59 } else { fail=fail+1; gp(" FAIL SC59-absent\n" as *u8) } 60 61 // NEGATIVE CONTROL: a bogus key must be ABSENT (the store never fabricates) 62 if rc_get("rc:SC_BOGUS_XYZ" as *u8, rq, rl) != 1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL bogus-fabricated\n" as *u8) } 63 64 gp("READER-CENSUS-GATE pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail) 65 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 66 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 67 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 68 let ctr__dry: *i64 = gv_ctr() 69 ctr__dry[0] = pass 70 ctr__dry[1] = pass + fail 71 let rc__dry: i64 = gv_verdict("READER-CENSUS-GATE" as *u8, ctr__dry, "census served from the sovereign seg-store; no tsv needed)" as *u8) 72 sys_exit(rc__dry) 73 return rc__dry 74}