code wiki / _hdl_build / nx_papers_index_gate.nx

nx_papers_index_gate.nx source

↩ module page · 138 lines · 6221 B

1// nx_papers_index_gate.nx -- proves the repository index is DATA-DRIVEN and FAIL-CLOSED (F1130). 2// The organ used to bake one hardcoded call per paper, so the list went stale and adding a 3// paper meant recompiling. These checks pin the fix: the same binary must emit a different 4// page when only the DATA changes (T2 -- that is what "data-driven" means and nothing else), 5// access must gate the hyperlink (T4, because /wiki/ is auth-gated and a link a reader cannot 6// follow is worse than an honest label), and a missing registry must REFUSE rather than 7// publish an empty repository over a real one (T3). 8// Runs the real CLI by fork+exec on a throwaway CWD. license_tier: ORIGINAL expect_exit: 0 9import "nx_syscalls.nx" 10 11const PG_ELF: i64 = 0 12 13func gw(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 14func gn(v: i64) -> i64 { let t: *u8=sys_mmap(24); var m: i64=v; var k: i64=0; if m<0{m=0-m} if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} let b: *u8=sys_mmap(24); var j: i64=0; while j<k{b[j]=t[k-1-j];j=j+1} sys_write(1,b,k); return 0 } 15func gchk(name: *u8, ok: i64, pass: *i64) -> i64 { 16 gw("T " as *u8); gw(name); gw(" -> " as *u8) 17 if ok == 1 { gw("PASS\n" as *u8); pass[0] = pass[0] + 1 } else { gw("FAIL\n" as *u8) } 18 return 0 19} 20func gslen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n } 21func gwrite(path: *u8, body: *u8) -> i64 { 22 let fd: i64 = sys_openat_wr(path, 0x1a4) 23 if fd < 0 { return 0 - 1 } 24 sys_write(fd, body, gslen(body)) 25 sys_close(fd) 26 return 0 27} 28func gread(path: *u8, buf: *u8, cap: i64) -> i64 { 29 let fd: i64 = sys_openat_rd(path) 30 if fd < 0 { return 0 - 1 } 31 var n: i64 = 0 32 var go: i64 = 1 33 while go == 1 { 34 let base: i64 = buf as i64 35 let r: i64 = sys_read(fd, (base + n) as *u8, cap - n) 36 if r <= 0 { go = 0 } else { n = n + r } 37 if n >= cap { go = 0 } 38 } 39 sys_close(fd) 40 return n 41} 42func gcount(hay: *u8, n: i64, pat: *u8) -> i64 { 43 let pl: i64 = gslen(pat) 44 if pl == 0 { return 0 } 45 var c: i64 = 0 46 var i: i64 = 0 47 while i + pl <= n { 48 var k: i64 = 0 49 var hit: i64 = 1 50 while k < pl { if hay[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } 51 if hit == 1 { c = c + 1 } 52 i = i + 1 53 } 54 return c 55} 56func grun(elf: *u8, a1: *u8, a2: *u8) -> i64 { 57 let pid: i64 = sys_fork() 58 if pid == 0 { 59 let argv: *i64 = sys_mmap(32) as *i64 60 argv[0]=elf as i64; argv[1]=a1 as i64; argv[2]=a2 as i64; argv[3]=0 61 let envp: *i64 = sys_mmap(16) as *i64 62 envp[0]=0 63 sys_execve(elf, argv, envp) 64 sys_exit(127) 65 } 66 let st: *i64 = sys_mmap(16) as *i64 67 sys_wait4(pid, st, 0) 68 let sig: i64 = st[0] & 0x7f 69 if sig != 0 { return 128 + sig } 70 return (st[0] >> 8) & 0xff 71} 72 73func main() -> i64 { 74 let pass: *i64 = sys_mmap(16) as *i64 75 pass[0] = 0 76 let elf: *u8 = "_offc/nx_papers_index.elf" as *u8 77 let buf: *u8 = sys_mmap(524288) 78 79 // two-row fixture: one public, one internal 80 gwrite("/tmp/pg_two.tsv" as *u8, "A-1\tpublic\t/a.html\tAlpha Title\tabs a\tres a\tgate a\nB-2\tinternal\t/wiki/b.html\tBeta Title\tabs b\tres b\tgate b\n" as *u8) 81 // three-row fixture: SAME binary, one extra DATA row 82 gwrite("/tmp/pg_three.tsv" as *u8, "A-1\tpublic\t/a.html\tAlpha Title\tabs a\tres a\tgate a\nB-2\tinternal\t/wiki/b.html\tBeta Title\tabs b\tres b\tgate b\nC-3\tpublic\t/c.html\tGamma Title\tabs c\tres c\tgate c\n" as *u8) 83 84 // T1 two data rows -> two sections 85 var ok1: i64 = 0 86 var n2: i64 = 0 87 if grun(elf, "/tmp/pg_two.tsv" as *u8, "/tmp/pg_two.html" as *u8) == 0 { 88 n2 = gread("/tmp/pg_two.html" as *u8, buf, 524280) 89 if gcount(buf, n2, "<section class=\"p\">" as *u8) == 2 { ok1 = 1 } 90 } 91 gchk("two-data-rows-two-sections" as *u8, ok1, pass) 92 93 // T2 ***THE DATA-DRIVEN PROOF***: the SAME binary emits THREE sections when only the 94 // registry changed. A hardcoded index cannot pass this test. 95 var ok2: i64 = 0 96 if grun(elf, "/tmp/pg_three.tsv" as *u8, "/tmp/pg_three.html" as *u8) == 0 { 97 let n3: i64 = gread("/tmp/pg_three.html" as *u8, buf, 524280) 98 if gcount(buf, n3, "<section class=\"p\">" as *u8) == 3 { 99 if gcount(buf, n3, "Gamma Title" as *u8) == 1 { ok2 = 1 } 100 } 101 } 102 gchk("same-binary-new-data-new-page" as *u8, ok2, pass) 103 104 // T3 ***NEG-CONTROL*** fail-closed: a missing registry REFUSES (exit 3) and writes nothing 105 var ok3: i64 = 0 106 if grun(elf, "/tmp/pg_absent.tsv" as *u8, "/tmp/pg_absent.html" as *u8) == 3 { 107 if gread("/tmp/pg_absent.html" as *u8, buf, 1024) < 0 { ok3 = 1 } 108 } 109 gchk("missing-registry-refuses-writes-nothing" as *u8, ok3, pass) 110 111 // T4 ACCESS gates the hyperlink: the public row is a link, the internal row is labelled 112 // and NOT linked (a link a reader cannot follow is worse than an honest label) 113 var ok4: i64 = 0 114 let n4: i64 = gread("/tmp/pg_two.html" as *u8, buf, 524280) 115 // ⚠the needle must be the TAG, not the bare phrase: "access-controlled" also appears in 116 // the footer prose explaining what the tag means, so a bare-phrase count is 2 and the 117 // assertion silently measures the wrong thing. Caught by this gate failing on its own 118 // first run -- the same imprecise-matching class as counting a citation token as a claim. 119 if gcount(buf, n4, "href=\"/a.html\"" as *u8) == 1 { 120 if gcount(buf, n4, "href=\"/wiki/b.html\"" as *u8) == 0 { 121 if gcount(buf, n4, "class=\"tag\">access-controlled" as *u8) == 1 { ok4 = 1 } 122 } 123 } 124 gchk("access-gates-the-hyperlink" as *u8, ok4, pass) 125 126 // T5 NON-VACUITY: real registry content reaches the page (not an empty shell) 127 var ok5: i64 = 0 128 if gcount(buf, n4, "Alpha Title" as *u8) >= 1 { 129 if gcount(buf, n4, "Beta Title" as *u8) >= 1 { ok5 = 1 } 130 } 131 gchk("non-vacuity-registry-content-reaches-page" as *u8, ok5, pass) 132 133 gw("PAPERS-INDEX-GATE pass=" as *u8); gn(pass[0]); gw("/5 verdict=" as *u8) 134 if pass[0] == 5 { gw("GREEN\n" as *u8); sys_exit(0); return 0 } 135 gw("RED\n" as *u8) 136 sys_exit(1) 137 return 1 138}