nx_portability_proof_census.nx source

1// nx_portability_proof_census.nx -- the EMIT-PROVEN tier of the HAL reach census. 2// 3// AUTHOR=ORGAN, measured, no-wave: nx_portability_census proves each backend FILE EXISTS (= reach, 4// 16/16). This sibling proves the stronger claim that census header itself flags as the gap -- that 5// the backend actually EMITS CORRECT NATIVE code, KAT-verified -- by COMPUTING, per ISA, whether a 6// real GREEN gate-log / parity-stamp exists. It reads portability_proof_sources.tsv (WHERE the proof 7// lives + WHICH token = GREEN) and VERIFIES the token actually occurs in that file (does NOT trust 8// the map's say-so): a row whose token is absent reads UNPROVEN. proven_permil <= reach_permil by 9// construction; the delta IS the rv64-only kernel-emitter foundation gap, now a tracked number that 10// ratchets UP as per-ISA emit KATs land (twin of nx_hal_purity_audit's ratchet). 11// Self-validating: a POS control (real GREEN token) MUST read proven; a NEG control (bogus token in 12// the same real file) MUST read unproven -- so the census cannot rubber-stamp. Writes 13// portability_proof_census.tsv + an honest PROOFGATE verdict to the log. license_tier: ORIGINAL 14import "nx_syscalls.nx" 15const PT_MAGIC_200000: i64 = 200000 16const PT_MAGIC_80000: i64 = 80000 17const PT_MAGIC_262144: i64 = 262144 18 19const PT_REF: *u8 = "knowledge/registry/portability_targets.tsv" 20const PS_REF: *u8 = "knowledge/registry/portability_proof_sources.tsv" 21const PC_OUT: *u8 = "knowledge/registry/portability_proof_census.tsv" 22const PC_LOG: *u8 = "knowledge/status/portability_proof_census.log" 23const PC_MAXF: i64 = 256 24 25func pc_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 } 26func pc_wn(fd: i64, v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64=v; if m<0 {m=0-m; sys_write(fd,"-" as *u8,1)}; let t: *u8 = sys_mmap(28); var k: i64=0; if m==0 {t[0]=48;k=1}; while m>0 {t[k]=(48+(m%10)) as u8; m=m/10; k=k+1}; var i: i64=0; while i<k {bb[i]=t[k-1-i]; i=i+1}; sys_write(fd, bb, k); return 0 } 27 28func pc_read_file(path: *u8, buf: *u8, cap: i64) -> i64 { 29 let fd: i64 = sys_openat_rd(path) 30 if fd < 0 { return 0 - 1 } 31 var tot: i64 = 0 32 var r: i64 = 1 33 while r > 0 { 34 let dst: *u8 = ((buf as i64) + tot) as *u8 35 r = sys_read(fd, dst, cap - tot) 36 if r > 0 { tot = tot + r } 37 } 38 sys_close(fd) 39 return tot 40} 41 42func pc_scan_to(buf: *u8, n: i64, start: i64, delim: i64) -> i64 { 43 var i: i64 = start 44 var s: i64 = 1 45 while s == 1 { if i >= n { s = 0 } else { if buf[i] == (delim as u8) { s = 0 } else { i = i + 1 } } } 46 return i 47} 48 49func pc_app(dst: *u8, off: i64, s: *u8) -> i64 { var i: i64 = 0; while s[i] != (0 as u8) { dst[off+i] = s[i]; i = i + 1 } return off + i } 50 51func pc_streq(a: *u8, b: *u8) -> i64 { 52 var i: i64 = 0 53 while i < 256 { 54 if a[i] != b[i] { return 0 } 55 if a[i] == (0 as u8) { return 1 } 56 i = i + 1 57 } 58 return 1 59} 60 61// substring present? scan haystack[0..n) for NUL-terminated needle. 62func pc_contains(buf: *u8, n: i64, needle: *u8) -> i64 { 63 var m: i64 = 0 64 while needle[m] != (0 as u8) { m = m + 1 } 65 if m == 0 { return 0 } 66 var i: i64 = 0 67 while i + m <= n { 68 var j: i64 = 0 69 var ok: i64 = 1 70 while j < m { 71 if buf[i+j] != needle[j] { ok = 0; j = m } else { j = j + 1 } 72 } 73 if ok == 1 { return 1 } 74 i = i + 1 75 } 76 return 0 77} 78 79// parse a 3-column tab/newline TSV (skipping # comments + blank lines) into three ptr arrays. 80func pc_parse3(buf: *u8, n: i64, c0: *i64, c1: *i64, c2: *i64) -> i64 { 81 var cnt: i64 = 0 82 var p: i64 = 0 83 while p < n { 84 if buf[p] == (35 as u8) { let e: i64 = pc_scan_to(buf, n, p, 10); p = e + 1 } 85 else { if buf[p] == (10 as u8) { p = p + 1 } 86 else { 87 let a0: i64 = p 88 let t1: i64 = pc_scan_to(buf, n, a0, 9); buf[t1] = 0 as u8 89 let a1: i64 = t1 + 1 90 let t2: i64 = pc_scan_to(buf, n, a1, 9); buf[t2] = 0 as u8 91 let a2: i64 = t2 + 1 92 let t3: i64 = pc_scan_to(buf, n, a2, 10); buf[t3] = 0 as u8 93 if cnt < PC_MAXF { c0[cnt] = (buf as i64) + a0; c1[cnt] = (buf as i64) + a1; c2[cnt] = (buf as i64) + a2; cnt = cnt + 1 } 94 p = t3 + 1 95 } } 96 } 97 return cnt 98} 99 100// proven iff isa has a source row whose green_token actually occurs in its evidence file. 101// writes the matched evidence-file ptr to ev[0] and token ptr to tk[0] (or "-" when no row). 102func pc_is_proven(isa: *u8, ns: i64, sisa: *i64, sevf: *i64, stok: *i64, evbuf: *u8, ev: *i64, tk: *i64) -> i64 { 103 ev[0] = "-" as *u8 as i64 104 tk[0] = "-" as *u8 as i64 105 var j: i64 = 0 106 while j < ns { 107 if pc_streq(isa, (sisa[j]) as *u8) == 1 { 108 ev[0] = sevf[j] 109 tk[0] = stok[j] 110 let m: i64 = pc_read_file((sevf[j]) as *u8, evbuf, PT_MAGIC_200000) 111 if m > 0 { if pc_contains(evbuf, m, (stok[j]) as *u8) == 1 { return 1 } } 112 return 0 113 } 114 j = j + 1 115 } 116 return 0 117} 118 119func pc_emit(fd: i64, nf: i64, proven: i64, cpos: i64, cneg: i64, cov: i64, ok: i64) -> i64 { 120 pc_w(fd, "PROOFGATE authored=organ layer=emit-proven-native source=portability_proof_sources.tsv targets=" as *u8); pc_wn(fd, nf) 121 pc_w(fd, " proven=" as *u8); pc_wn(fd, proven) 122 pc_w(fd, " unproven=" as *u8); pc_wn(fd, nf - proven) 123 pc_w(fd, " proven_permil=" as *u8); pc_wn(fd, cov) 124 pc_w(fd, " reach_permil=1000(file-exists/nx_portability_census)" as *u8) 125 pc_w(fd, " control_pos=" as *u8); pc_wn(fd, cpos) 126 pc_w(fd, " control_neg=" as *u8); pc_wn(fd, cneg) 127 if ok == 1 { pc_w(fd, " verdict=GREEN\n" as *u8) } else { pc_w(fd, " verdict=RED reason=control-or-empty\n" as *u8) } 128 return 0 129} 130 131func main() -> i64 { 132 // targets (the 16 ISAs; col0 = isa) 133 let tb: *u8 = sys_mmap(PT_MAGIC_80000) 134 let tbn: i64 = pc_read_file(PT_REF, tb, PT_MAGIC_80000) 135 if tbn <= 0 { pc_w(1, "PROOFGATE verdict=RED reason=targets-unreadable\n" as *u8); return 1 } 136 let tisa: *i64 = sys_mmap(8 * PC_MAXF) as *i64 137 let tbk: *i64 = sys_mmap(8 * PC_MAXF) as *i64 138 let tcl: *i64 = sys_mmap(8 * PC_MAXF) as *i64 139 let nf: i64 = pc_parse3(tb, tbn, tisa, tbk, tcl) 140 141 // proof sources (isa, evidence_file, green_token) 142 let sb: *u8 = sys_mmap(PT_MAGIC_80000) 143 let sbn: i64 = pc_read_file(PS_REF, sb, PT_MAGIC_80000) 144 let sisa: *i64 = sys_mmap(8 * PC_MAXF) as *i64 145 let sevf: *i64 = sys_mmap(8 * PC_MAXF) as *i64 146 let stok: *i64 = sys_mmap(8 * PC_MAXF) as *i64 147 var ns: i64 = 0 148 if sbn > 0 { ns = pc_parse3(sb, sbn, sisa, sevf, stok) } 149 150 let evbuf: *u8 = sys_mmap(PT_MAGIC_262144) 151 let ob: *u8 = sys_mmap(PT_MAGIC_200000) 152 var o: i64 = 0 153 o = pc_app(ob, o, "# AUTHORED BY nx_portability_proof_census -- the EMIT-PROVEN tier of HAL reach. Status COMPUTED: PROVEN iff a real GREEN gate-log/parity-stamp token (per portability_proof_sources.tsv) actually occurs in its evidence file (VERIFIED, not asserted). PROVEN<=PRESENT; the gap = rv64-only kernel emitters not yet riding each backend. Ratchets up as per-ISA emit KATs land.\n" as *u8) 154 o = pc_app(ob, o, "# columns: status\tisa\tevidence\tgreen_token\n" as *u8) 155 156 let ev: *i64 = sys_mmap(8) as *i64 157 let tk: *i64 = sys_mmap(8) as *i64 158 var proven: i64 = 0 159 var i: i64 = 0 160 while i < nf { 161 let pr: i64 = pc_is_proven((tisa[i]) as *u8, ns, sisa, sevf, stok, evbuf, ev, tk) 162 if pr == 1 { o = pc_app(ob, o, "PROVEN\t" as *u8); proven = proven + 1 } else { o = pc_app(ob, o, "UNPROVEN\t" as *u8) } 163 o = pc_app(ob, o, (tisa[i]) as *u8) 164 o = pc_app(ob, o, "\t" as *u8) 165 o = pc_app(ob, o, (ev[0]) as *u8) 166 o = pc_app(ob, o, "\t" as *u8) 167 o = pc_app(ob, o, (tk[0]) as *u8) 168 o = pc_app(ob, o, "\n" as *u8) 169 i = i + 1 170 } 171 let wfd: i64 = sys_openat_wr(PC_OUT, 420) 172 if wfd < 0 { pc_w(1, "PROOFGATE verdict=RED reason=out-unwritable\n" as *u8); return 1 } 173 sys_write(wfd, ob, o) 174 sys_close(wfd) 175 176 // self-validating controls: POS = a real GREEN token reads proven; NEG = a bogus token in the 177 // SAME real file reads unproven -> the contains-scan is validated in both directions. 178 let cm: i64 = pc_read_file("knowledge/status/spirv_gate.log" as *u8, evbuf, PT_MAGIC_262144) 179 var cpos: i64 = 0 180 var cneg: i64 = 0 181 if cm > 0 { 182 if pc_contains(evbuf, cm, "verdict=GREEN" as *u8) == 1 { cpos = 1 } 183 if pc_contains(evbuf, cm, "verdict=GREEN_NEVERMATCH" as *u8) == 1 { cneg = 1 } 184 } 185 var cov: i64 = 0 186 if nf > 0 { cov = (proven * 1000) / nf } 187 var ok: i64 = 1 188 if cpos != 1 { ok = 0 } 189 if cneg != 0 { ok = 0 } 190 if nf <= 0 { ok = 0 } 191 192 pc_emit(1, nf, proven, cpos, cneg, cov, ok) 193 let lf: i64 = sys_openat_append(PC_LOG, 420) 194 if lf >= 0 { pc_emit(lf, nf, proven, cpos, cneg, cov, ok); sys_close(lf) } 195 if ok == 1 { return 0 } 196 return 1 197}