nx_mmbench_lib.nx source

1// nx_mmbench_lib.nx -- the TESTABLE CORE of the media-manager + companion ruler. 2// 3// Shared by nx_mmbench (the shipping tool) AND nx_mmbench_gate (the proof), so the gate's negative 4// control exercises THE CODE THAT ACTUALLY SHIPS rather than a copy of it (rule 15 / refbench shape). 5// The whole honesty claim of the ruler rests on aud() below: if aud() does not really downgrade an 6// unbacked claim, every coverage number the tool prints is decoration. The gate mutation-tests it. 7// license_tier: ORIGINAL expect_exit: 0 8import "nx_syscalls.nx" 9 10const V_HAVE: i64 = 2 11const V_PART: i64 = 1 12const V_GAP: i64 = 0 13const MMB_SCRATCH: i64 = 32 14 15func sw(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 16func sn(v: i64) -> i64 { 17 let bb: *u8 = sys_mmap(MMB_SCRATCH) 18 var m: i64 = v 19 if m<0 { sys_write(1,"-" as *u8,1); m=0-m } 20 let t: *u8 = sys_mmap(MMB_SCRATCH) 21 var k: i64 = 0 22 if m==0 { t[0]=48 as u8; k=1 } 23 while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 } 24 var i: i64 = 0 25 while i<k { bb[i]=t[k-1-i]; i=i+1 } 26 sys_write(1,bb,k) 27 return 0 28} 29// EXISTENCE PROBE: does this evidence artifact exist RIGHT NOW on the machine we are grading? 30func have(path: *u8) -> i64 { let fd: i64 = sys_openat_rd(path); if fd<0 { return 0 } sys_close(fd); return 1 } 31 32// PURE, TESTABLE EVIDENCE AUDIT -- the single decision point of the whole ruler. 33// ev==0 : no artifact was ever named. A HAVE is UNGROUNDED -> capped to PARTIAL (flag 2). 34// You may not assert a win you never pointed at anything for. 35// artifact absent : a SPECIFIC claim that is FALSE -> LIAR-KILLED to GAP (flag 1). Harsher than 36// ungrounded on purpose: naming a file that is not there is worse than silence. 37// artifact present : the declared verdict stands (flag 0). 38// returns verdict*10 + flag 39func aud(v: i64, ev: i64) -> i64 { 40 if ev==0 { 41 if v==V_HAVE { return V_PART*10+2 } 42 return v*10 43 } 44 if have(ev as *u8)==0 { return V_GAP*10+1 } 45 return v*10 46} 47// WIRED AUDIT -- the second dimension, added 2026-07-25 after finding nx_media_extract: a complete, 48// 6/6-gate-proven media extraction orchestrator with 8 importers, deployed NOWHERE. The ruler could 49// only say HAVE/PARTIAL/GAP, so it had no way to express "built and correct but unreachable" -- which 50// is the MOST COMMON state in this ecosystem (measured: 5020 dead organs). A capability the product 51// cannot reach is not a capability the user has. 52// wire==0 : no deployment artifact named -> DARK 53// artifact absent: implementation lives only in the build tree -> DARK 54// artifact present: deployed on the live host -> WIRED 55// DECLARED FLOOR (law L011, stated not implied): this probes DEPLOYED, not CALLED. A deployed binary 56// no running daemon invokes still scores WIRED, so wired-coverage is an UPPER bound on usability and 57// the true number can only be lower. It is never an over-count of DARK. 58func wired(wire: i64) -> i64 { 59 if wire==0 { return 0 } 60 if have(wire as *u8)==0 { return 0 } 61 return 1 62} 63const MMB_BINCAP: i64 = 4194304 // 4 MiB scan cap -- DECLARED (law L011), never a silent partial 64 65// ---- THE STRONG WIRING TEST, adopted from nx_reader_liveness rather than invented ---- 66// That organ exists because mobi/azw/azw3 decoders were BUILT and gated GREEN but ms_handle_open never 67// routed to them, so ~390 books dead-ended at /file. Its insight: presence on disk proves nothing; 68// what proves reachability is that THE LIVE SERVING BINARY REFERENCES THE ORGAN. Verified on our own 69// stack before adopting: nx_gallery_serve.elf really does contain the literal 70// "/volume1/ai/galx/nx_ts_index.elf" (the path it forks). 71// returns 1 = referenced, 0 = fully scanned and ABSENT, -1 = unreadable or over cap = UNKNOWN. 72// UNKNOWN is deliberately distinct from ABSENT: a binary too big to scan must never masquerade as dark. 73func bin_ref(binpath: *u8, needle: *u8) -> i64 { 74 var nl: i64 = 0 75 while needle[nl]!=(0 as u8) { nl = nl + 1 } 76 if nl == 0 { return 0-1 } 77 let fd: i64 = sys_openat_rd(binpath) 78 if fd < 0 { return 0-1 } 79 let buf: *u8 = sys_mmap(MMB_BINCAP) 80 var total: i64 = 0 81 var go: i64 = 1 82 while go == 1 { 83 if total >= MMB_BINCAP { go = 0 } 84 else { 85 let n: i64 = sys_read(fd, (buf as i64 + total) as *u8, MMB_BINCAP - total) 86 if n > 0 { total = total + n } else { go = 0 } 87 } 88 } 89 sys_close(fd) 90 if total >= MMB_BINCAP { return 0-1 } 91 var i: i64 = 0 92 while i + nl <= total { 93 var j: i64 = 0 94 var hit: i64 = 1 95 while j < nl { 96 if buf[i+j] != needle[j] { hit = 0; j = nl } else { j = j + 1 } 97 } 98 if hit == 1 { return 1 } 99 i = i + 1 100 } 101 return 0 102} 103 104// WIRING VERDICT with the strong test when a serving binary is named. 105// sb==0 -> fall back to artifact existence (the weaker, declared floor) 106// referenced -> WIRED 107// scanned, absent -> DARK, even though the artifact is deployed. THIS is the strengthening. 108// UNKNOWN -> fall back rather than assert either way 109func wired_ref(wire: i64, sb: i64, needle: i64) -> i64 { 110 if sb==0 { return wired(wire) } 111 let r: i64 = bin_ref(sb as *u8, needle as *u8) 112 if r==1 { return 1 } 113 if r==0 { return 0 } 114 return wired(wire) 115} 116 117// A dark capability scores GAP for coverage purposes no matter how good its code is. 118func usable(built_v: i64, wire: i64) -> i64 { 119 if wired(wire)==0 { return V_GAP } 120 return built_v 121} 122// Same collapse, but using the STRONG reference test when a serving binary is named. 123func usable_ref(built_v: i64, wire: i64, sb: i64, needle: i64) -> i64 { 124 if wired_ref(wire, sb, needle)==0 { return V_GAP } 125 return built_v 126} 127func vstr(v: i64) -> *u8 { if v==2 { return "HAVE" as *u8 } if v==1 { return "PARTIAL" as *u8 } return "GAP" as *u8 } 128func streq(a: *u8, b: *u8) -> i64 { 129 var i: i64 = 0 130 while a[i]!=(0 as u8) { if a[i]!=b[i] { return 0 } i=i+1 } 131 if b[i]!=(0 as u8) { return 0 } 132 return 1 133}