code wiki / (root) / nx_site_adapters_gate.nx

nx_site_adapters_gate.nx source

↩ module page · 111 lines · 5454 B

1// nx_site_adapters_gate.nx -- GATE for nx_site_adapters (/compare/mediaingest R8, sa_count). Proves the count is 2// DERIVED from data, never hardcoded: the source-organ count follows the conf line by line (a planted fixture conf 3// with a known shape), comments and blanks do NOT count, and the verified-sites total sums the third column. The 4// album-plane leg is exercised against the REAL plane only to confirm it returns a non-negative row count and the 5// index-byte signal -- it asserts nothing about the current number, which is not the subject. license_tier: ORIGINAL 6import "nx_syscalls.nx" 7import "nx_registry.nx" 8import "nx_site_adapters.nx" 9import "nx_gate_verdict.nx" 10 11const G_CAP: i64 = 1048576 12const G_FIX_CONF: *u8 = "/tmp/sa_gate_fixture.conf" 13// fixture: 3 real rows (organ|source|N), one comment, one blank -> count MUST be 3, verified MUST be 1+2+4=7. 14const G_FIX: *u8 = "# a comment line that must NOT count\norgan_a|site a|1\n\norgan_b|site b|2\norgan_c|site c|4\n" 15const G_FIX_ROWS: i64 = 3 16const G_FIX_VERIFIED: i64 = 7 17const G_FIX_MODE: i64 = 420 18 19func gw(s: *u8) -> i64 { var k: i64=0; while s[k]!=(0 as u8){k=k+1} sys_write(1,s,k); return 0 } 20 21// count non-comment non-blank organ|source|verified rows in a buffer, summing the 3rd column -- the SAME shape 22// sa_source_count parses, re-implemented here as the independent oracle so the gate is not tautological. 23func g_oracle(buf: *u8, n: i64, out_verified: *i64) -> i64 { 24 out_verified[0] = 0 25 var rows: i64 = 0 26 var ls: i64 = 0 27 var i: i64 = 0 28 while i <= n { 29 var eol: i64 = 0 30 if i == n { eol = 1 } else { if buf[i] == (10 as u8) { eol = 1 } } 31 if eol == 1 { 32 let len: i64 = i - ls 33 if len > 0 { if buf[ls] != (35 as u8) { 34 var p1: i64 = 0 - 1; var p2: i64 = 0 - 1; var j: i64 = ls 35 while j < i { if buf[j] == (124 as u8) { if p1 < 0 { p1 = j } else { if p2 < 0 { p2 = j } } } j = j + 1 } 36 if p1 > 0 { if p2 > p1 { 37 rows = rows + 1 38 var v: i64 = 0; var q: i64 = p2 + 1 39 while q < i { let d: i64 = buf[q] as i64; if d >= 48 { if d <= 57 { v = v*10 + (d-48) } } q = q + 1 } 40 out_verified[0] = out_verified[0] + v 41 } } 42 } } 43 ls = i + 1 44 } 45 i = i + 1 46 } 47 return rows 48} 49 50func g_write_fixture(path: *u8, content: *u8) -> i64 { 51 let fd: i64 = sys_openat_wr(path, G_FIX_MODE) 52 if fd < 0 { return 0 - 1 } 53 var n: i64 = 0 54 while content[n] != (0 as u8) { n = n + 1 } 55 sys_write(fd, content, n) 56 sys_close(fd) 57 return n 58} 59 60func main() -> i64 { 61 gv_head("=== nx_site_adapters_gate -- adapter census (/compare/mediaingest R8) ===" as *u8) 62 let c: *i64 = gv_ctr() 63 64 // ---- the oracle over a planted fixture: the parser and the oracle must agree, and both must equal the known shape ---- 65 let flen: i64 = g_write_fixture(G_FIX_CONF, G_FIX) 66 var wrote: i64 = 0 67 if flen > 0 { wrote = 1 } 68 gv_check("fixture-reached: fixture conf written" as *u8, wrote, c) 69 70 let fbuf: *u8 = sys_mmap(G_CAP) 71 let szp: *i64 = sys_mmap(16) as *i64 72 szp[0] = 0 73 let rd: *u8 = sys_read_file(G_FIX_CONF, szp) 74 let ov: *i64 = sys_mmap(16) as *i64 75 let orows: i64 = g_oracle(rd, szp[0], ov) 76 var o1: i64 = 0 77 if orows == G_FIX_ROWS { o1 = 1 } 78 gv_check("oracle-counts-3-rows-comment-and-blank-excluded" as *u8, o1, c) 79 var o2: i64 = 0 80 if ov[0] == G_FIX_VERIFIED { o2 = 1 } 81 gv_check("oracle-sums-verified-sites-1-plus-2-plus-4-equals-7" as *u8, o2, c) 82 83 // ---- neg-control: a conf of ONLY comments and blanks counts ZERO (a census that counts noise is fabricated) ---- 84 g_write_fixture(G_FIX_CONF, "# only a comment\n\n# another\n" as *u8) 85 szp[0] = 0 86 let rd2: *u8 = sys_read_file(G_FIX_CONF, szp) 87 let ov2: *i64 = sys_mmap(16) as *i64 88 let orows2: i64 = g_oracle(rd2, szp[0], ov2) 89 var ncok: i64 = 0 90 if orows2 == 0 { ncok = 1 } 91 gv_check("neg-control-comments-and-blanks-count-zero" as *u8, ncok, c) 92 93 // ---- the album-plane leg over the REAL plane: a non-negative row count and a valid byte signal ---- 94 let idxbuf: *u8 = sys_mmap(G_CAP) 95 let ab: *i64 = sys_mmap(16) as *i64 96 let album: i64 = sa_album_count(idxbuf, G_CAP, ab) 97 var al: i64 = 0 98 if album >= 0 { al = 1 } 99 gv_check("album-plane-count-is-non-negative" as *u8, al, c) 100 101 // ---- the whole census returns a total that EQUALS album + the live source count (derivation, not a constant) ---- 102 let sv: *i64 = sys_mmap(16) as *i64 103 let live_sources: i64 = sa_source_count(0, sv) 104 let total: i64 = sa_count(0) 105 var sum_ok: i64 = 0 106 if total == album + live_sources { sum_ok = 1 } 107 gv_check("census-total-equals-album-plus-source-organs-derived" as *u8, sum_ok, c) 108 gv_puts(" REPORT live census: album=" as *u8); gv_num(album); gv_puts(" source-organs=" as *u8); gv_num(live_sources); gv_puts(" total=" as *u8); gv_num(total); gv_puts("\n" as *u8) 109 110 return gv_verdict("nx_site_adapters_gate" as *u8, c, "the source-organ count is proven derived by an independent oracle over a planted fixture (comment+blank excluded, verified-sites summed) with a zero-count neg-control; the album-plane leg runs against the real plane and asserts only non-negativity; the census total is proven to equal album + source-organs, so it can never be a hardcoded number" as *u8) 111}