code wiki / _hdl_build / _drv_proto_gate.nx

_drv_proto_gate.nx source

↩ module page · 343 lines · 24218 B

1// _drv_proto_gate.nx -- the gate for DRIVER-PROTOCOL-FROM-SPEC (X-DRV-W1). NO mocks. 2// 3// Drives the GENERIC emitter end to end: runs the REAL nx_drv_proto_emit on TWO different driver 4// SPECS (op-lists), runs EACH emitted image on the SOVEREIGN rv64 emulator (nx_boot_run_sov, with 5// the legacy virtio-MMIO blk @0x10001000 + net @0x10002000 device models attached), and asserts: 6// 7// (1) BLK -- spec A (virtio-blk, DeviceID=2) drives the FULL register/ring/irq transaction 8// (handshake -> queue config -> descriptor lay -> avail/used ring -> status writeback -> 9// sector-data round-trip): the captured serial CONTAINS golden A + the emu reports a clean 10// SiFive-finisher halt. The device genuinely DMA-walked the ring the driver laid (the driver 11// verifies QueueDescPeek/UsedIdxPeek/StatPeek/SectPeek read-backs), so a stuck device cannot 12// fake it. 13// (2) NET -- spec B (virtio-net, DeviceID=1) drives a DIFFERENT op-list against a DIFFERENT 14// device class: serial CONTAINS golden B + clean halt. 15// (3) DISTINCT -- golden A != golden B AND both non-empty, BOTH authored by the SAME emitter 16// binary. Two different op-lists -> two different working drivers proves the protocol STATE 17// MACHINE is synthesized FROM THE SPEC, not a fixed virtio-blk template (the no-false-green 18// keystone: a fixed template could not produce two distinct device-class drivers). 19// (4) TAMPER -- two independent corruptions of the BLK image, each must drop golden A: 20// t1: bump the device-base lui immediate (byte 7) -> all MMIO reads target a non-device 21// address -> the identity verify fails -> the whole transcript collapses (proves the 22// driver REALLY talks to the device at the spec's base; a no-op driver would be immune). 23// t2: bump the magic-EXPECTED constant (byte 15, the first verify's li high byte) -> the 24// identity verify mismatches -> transcript collapses (proves the VERIFY logic is real, 25// not a rubber stamp). 26// 27// Evidence -> knowledge/status/driver_spec.log (DRVPROTOGATE row; the queue row's ||MARK= reads 28// it). Sovereign orchestration (fork/dup3/execve/wait4), no gcc/.sh. license_tier: ORIGINAL 29import "nx_syscalls.nx" 30 31import "nx_gate_verdict.nx" 32// ct_admit_now(): the shared "can this host afford the work" question. Imported rather than re-derived -- 33// the parse, the threshold and the fail-closed policy are all proven in nx_ctxtop_lib's own gate. 34import "nx_ctxtop_lib.nx" 35 36const EMIT_ELF: *u8 = "_offc/nx_drv_proto_emit.elf" 37const SOV_ELF: *u8 = "_offc/nx_boot_run_sov.elf" 38 39func g_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 40func g_fp(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 } 41func g_fn(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 } 42 43// run prog with one arg (a1, may be null); serial/stdout -> outpath; return WEXITSTATUS (or 128+sig). 44func g_run1(prog: *u8, a1: *u8, outpath: *u8) -> i64 { 45 let pid: i64 = sys_fork() 46 if pid == 0 { 47 let ofd: i64 = sys_openat_wr(outpath, 0x1a4) 48 if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } 49 let argv: *i64 = sys_mmap(32) as *i64 50 argv[0] = prog as i64 51 var k: i64 = 1 52 if a1 != (0 as *u8) { argv[k] = a1 as i64; k = k + 1 } 53 argv[k] = 0 54 let envp: *i64 = sys_mmap(16) as *i64 55 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0 56 sys_execve(prog, argv, envp) 57 sys_exit(127) 58 } 59 let st: *i64 = sys_mmap(16) as *i64 60 sys_wait4(pid, st, 0) 61 let sig: i64 = st[0] & 0x7f 62 if sig != 0 { return 128 + sig } 63 return (st[0] >> 8) & 0xff 64} 65 66// read whole file into buf (cap-1 max); return byte count (0 if absent). 67func g_read(path: *u8, buf: *u8, cap: i64) -> i64 { 68 let fd: i64 = sys_openat_rd(path) 69 if fd < 0 { return 0 } 70 var n: i64 = 0 71 var go: i64 = 1 72 while go == 1 { let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, cap - 1 - n); if r <= 0 { go = 0 } else { n = n + r } if n >= cap - 1 { go = 0 } } 73 sys_close(fd) 74 return n 75} 76 77// offset of pat in buf[0,n), or -1. ONE finder; g_buf_has composes it rather than repeating the scan. 78func g_find(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 79 if pl <= 0 { return 0 - 1 } 80 var i: i64 = 0 81 while i + pl <= n { 82 var k: i64 = 0; var hit: i64 = 1 83 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } 84 if hit == 1 { return i } 85 i = i + 1 86 } 87 return 0 - 1 88} 89// does buf[0,n) contain pat (length pl)? 1/0 90func g_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 { 91 if g_find(buf, n, pat, pl) >= 0 { return 1 } 92 return 0 93} 94// ★★★★★★ANCHOR THE PARSE. nx_boot_run_sov's FAILURE MESSAGE QUOTES THE GOLDEN VERBATIM 95// (`expected=[VIOACKDRVFEATOKVQDESCUSEDSTATSECT] got=[VIOACKDRVFEATOKVQ]`), so searching the WHOLE serial 96// finds the golden INSIDE THE DIAGNOSTIC THAT SAYS THE GOLDEN WAS ABSENT. Measured on this gate: a run 97// whose device transcript stopped at VQ was reported as "golden present, no clean halt", i.e. strictly 98// BETTER than the truth, and the tamper axis flipped to BITE-PROVEN off the same contamination. 99// ★A PARSER THAT READS THE DATA AS THE ANSWER FLATTERS EXACTLY THE RUN THAT FAILED. 100// The DEVICE transcript is everything before the emulator's verdict line; search only that. 101func g_device_len(buf: *u8, n: i64) -> i64 { 102 let v: i64 = g_find(buf, n, "BOOTSOV verdict=" as *u8, 16) 103 if v >= 0 { return v } 104 return n 105} 106 107func g_strlen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n } 108 109// are two NUL-terminated strings equal? 1/0 110func g_streq(a: *u8, b: *u8) -> i64 { 111 var i: i64 = 0 112 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 } 113 if b[i] != (0 as u8) { return 0 } 114 return 1 115} 116 117// emit a driver from spec, run it on the sovereign emu; return 1 iff serial CONTAINS golden + 118// clean SiFive halt. golden read from <out>.gold; out path passed in. serialpath = scratch. 119// ★★★★★★A COMPOUND ASSERTION THAT WILL NOT NAME ITS FAILING CONJUNCT IS A FALSE-ALARM GENERATOR, AND THE 120// READER ALWAYS GUESSES THE ALARMING ONE. g_emit_run used to return a bare 0/1 for FIVE distinct 121// failures, so `blk_full_txn=RED` could equally mean: the emitter crashed, the spec produced no golden, 122// the emulator rejected the image before a single instruction ran, the driver ran and produced the WRONG 123// transcript, or it produced the RIGHT transcript and never halted. Five causes, five different remedies, 124// one indistinguishable word. A verdict is not a diagnosis. 125func g_er_reason(c: i64) -> *u8 { 126 if c == 0 { return "ok" as *u8 } 127 if c == 1 { return "EMITTER-FAILED (nx_drv_proto_emit exited nonzero -- spec unreadable, or an emit bug; the driver was never built)" as *u8 } 128 if c == 2 { return "GOLDEN-ABSENT (the emitter wrote no .gold -- there is nothing to look for, so this run CANNOT be judged)" as *u8 } 129 if c == 3 { return "EMU-NO-SERIAL (the emulator produced no transcript at all -- the image really was rejected before any instruction ran)" as *u8 } 130 if c == 4 { return "TRANSCRIPT-SHORT-OR-WRONG (the driver RAN but its serial does not contain the golden -- READ THE SERIAL: nx_boot_run_sov prints expected=[..] got=[..] and the divergence point NAMES the protocol stage that stopped)" as *u8 } 131 if c == 5 { return "NO-CLEAN-HALT (golden present but no SiFive finisher halt -- the driver did the work and did not finish)" as *u8 } 132 if c == 6 { return "EMU-NONZERO-DESPITE-MATCHING-TRANSCRIPT (golden present AND clean halt, yet the emulator still exited nonzero -- suspect the emulator or the harness, NOT the driver)" as *u8 } 133 if c == 7 { return "EMU-DID-NOT-FINISH (a partial transcript with NO `BOOTSOV verdict=` line -- the emulator was cut off before it could judge, so this run says NOTHING about the driver. Check /proc/loadavg and re-run. The LONGEST transcript is always the first to be cut, which is why blk shows this and the short net handshake does not)" as *u8 } 134 return "UNRECOGNISED CODE -- that is a defect in THIS GATE, not in the subject" as *u8 135} 136// returns 0 on success, otherwise a NUMBERED reason named by g_er_reason 137// ⚠emitlog is PER-SPEC. Both emit runs used to share /tmp/_drvproto_emit.out, so the NET run overwrote 138// the BLK emitter's own report every single time -- the one artifact that says how many ops the emitter 139// actually walked for the failing spec was destroyed by the passing one, on every run, silently. 140// ★★★★★TWO PRODUCERS SHARING ONE OUTPUT PATH IS NOT A COLLISION YOU NOTICE -- IT IS EVIDENCE THAT SIMPLY 141// IS NEVER THERE, AND THE READER BLAMES THE PRODUCER THAT RAN FIRST. 142func g_emit_run(spec: *u8, out: *u8, goldout: *u8, gbuf: *u8, gcap: i64, serialpath: *u8, emitlog: *u8) -> i64 { 143 let est: i64 = g_run1(EMIT_ELF, spec, emitlog) 144 if est != 0 { return 1 } 145 let gn: i64 = g_read(goldout, gbuf, gcap) 146 if gn <= 0 { return 2 } 147 gbuf[gn] = 0 as u8 148 let rst: i64 = g_run1(SOV_ELF, out, serialpath) 149 let sbuf: *u8 = sys_mmap(65536) 150 let sbn: i64 = g_read(serialpath, sbuf, 65536) 151 // ★★★★★★ORDER THE CHECKS BY WHAT THEY CAN DISTINGUISH, NOT BY WHAT IS CHEAPEST TO TEST. Testing the 152 // emulator's EXIT CODE first made code 4 UNREACHABLE: nx_boot_run_sov signals a transcript mismatch 153 // BY exiting nonzero, so every real protocol failure was being reported as "the image was rejected 154 // before the driver ran" -- the opposite of the truth, and it sends the reader to the loader when the 155 // bug is in the driver. ★A REASON CODE THAT CAN NEVER BE RETURNED IS A DIAGNOSIS THE GATE CANNOT GIVE. 156 // An EMPTY serial is the only thing that actually means "nothing ran"; everything else is evidence. 157 if sbn <= 0 { return 3 } 158 let dn: i64 = g_device_len(sbuf, sbn) 159 let has: i64 = g_buf_has(sbuf, dn, gbuf, gn) 160 let halt: i64 = g_buf_has(sbuf, sbn, "BOOTSOV verdict=GREEN" as *u8, 21) 161 // A TRUNCATED RUN AND A DIVERGENT DRIVER SHOW THE SAME SYMPTOM -- an absent golden -- AND THEY DEMAND 162 // OPPOSITE RESPONSES: one is "re-run when the box is quiet", the other is "the driver is wrong". 163 // MEASURED 2026-08-15: under host saturation (load 11.6-15.1, nx_ctxtop itself refusing to run at 164 // load_centi=1375 vs max=800) the long blk transcript stopped early while the short net handshake 165 // completed, so this gate reported the blk DRIVER as broken. It was not: the same binary, same 166 // caller, returned 4/4 GREEN once load fell to ~6, and the serial held the golden exactly. 167 // nx_boot_run_sov ALWAYS renders a `BOOTSOV verdict=` line once it reaches its own conclusion, so 168 // the absence of that line is a statement about the HOST, never about the driver. 169 // ★AN AXIS THAT CANNOT SEE MUST ABSTAIN, NOT CONVICT -- and this one was convicting. 170 // Checked BEFORE the golden test on purpose: whichever check runs first owns the diagnosis, and the 171 // narrower, more specific cause has to win or it is invisible behind the broader one. 172 let rendered: i64 = g_buf_has(sbuf, sbn, "BOOTSOV verdict=" as *u8, 16) 173 if rendered == 0 { return 7 } 174 if has == 0 { return 4 } 175 if halt == 0 { return 5 } 176 if rst != 0 { return 6 } 177 return 0 178} 179 180// run the BLK image with byte[pos] bumped by 1; return 1 iff golden A is now ABSENT (tamper bites). 181func g_tamper(srcbin: *u8, pos: i64, golden: *u8, gn: i64, tampbin: *u8, serialpath: *u8) -> i64 { 182 let ibuf: *u8 = sys_mmap(16384) 183 let ibn: i64 = g_read(srcbin, ibuf, 16384) 184 if ibn <= pos { return 0 } 185 ibuf[pos] = (ibuf[pos] + 1) as u8 186 let tfd: i64 = sys_openat_wr(tampbin, 0x1a4) 187 if tfd < 0 { return 0 } 188 sys_write(tfd, ibuf, ibn); sys_close(tfd) 189 let rst: i64 = g_run1(SOV_ELF, tampbin, serialpath) 190 let sbuf: *u8 = sys_mmap(65536) 191 let sbn: i64 = g_read(serialpath, sbuf, 65536) 192 // SAME CONTAMINATION, SAME FIX: a tampered run whose emulator prints `expected=[<golden>]` would 193 // otherwise read as "golden still present" and the tamper would score as NOT biting. 194 let dn: i64 = g_device_len(sbuf, sbn) 195 let has: i64 = g_buf_has(sbuf, dn, golden, gn) 196 if has == 0 { return 1 } // golden gone from the DEVICE transcript -> tamper bites 197 return 0 198} 199 200// PRINT THE EVIDENCE, DO NOT CITE IT. Reason code 4 literally instructs the reader to "READ THE SERIAL" 201// -- a transcript this gate has already read into memory once and then dropped. Measured 2026-08-15: 202// diagnosing one blk RED cost a manual hunt through /tmp for a 164-byte file that answered the question 203// instantly, and by the time it was found a later run had overwritten it. An instruction to go look is 204// not a diagnosis; the bytes are. 205// ★THE ARTEFACT THAT NAMES THE FAILURE IS WORTHLESS IF IT IS GONE BEFORE ANYONE READS IT. 206func g_dump_serial(label: *u8, path: *u8) -> i64 { 207 let sb: *u8 = sys_mmap(65536) 208 let sn: i64 = g_read(path, sb, 65536) 209 g_p(" " as *u8); g_p(label); g_p(" serial follows:\n " as *u8) 210 if sn > 0 { sys_write(1, sb, sn) } else { g_p("(EMPTY -- the emulator produced no transcript at all)\n" as *u8) } 211 return 0 212} 213 214func main() -> i64 { 215 g_p("=== driver-protocol-from-spec gate (X-DRV-W1: op-list spec -> emitted rv64 driver -> real virtio device on sovereign emu) ===\n" as *u8) 216 // ★A DIAGNOSTIC THAT CANNOT REFUSE TO RUN IS A LOAD GENERATOR WITH GOOD INTENTIONS. That law was 217 // written for a /proc walk; this gate forks a full rv64 EMULATOR twice plus two tamper runs, so it is 218 // far heavier and had no admission check at all. MEASURED 2026-08-15: under host saturation the long 219 // virtio-blk transcript was cut short and this gate reported the blk DRIVER as broken -- the same 220 // binary returns 4/4 GREEN on a quiet box. Refusing here is not caution; it is the difference between 221 // a verdict and a coin flip, and a fleet metric that flips with load is one everyone learns to ignore. 222 // Composed from nx_ctxtop_lib: ONE admission sequence, ONE operator-tunable threshold 223 // (knowledge/status/procchurn.conf, admit-max-load-centi), shared with every other heavy organ. 224 // Refused BEFORE the log is opened, on purpose: nothing was measured, so there is no domain row to 225 // write, and a row of zeros would read as a failure. gv_verdict still records the harness.jrnl frame, 226 // so the abstention is audited without inventing a second row shape. 227 if ct_admit_now() == 0 { 228 let ctrA: *i64 = gv_ctr() 229 gv_need("a host quiet enough to trust an emulator run (threshold: knowledge/status/procchurn.conf admit-max-load-centi)" as *u8, 0, ctrA) 230 let rcA: i64 = gv_verdict("DRVPROTOGATE", ctrA, "driver-protocol-from-spec -- abstained, the host was too loaded to measure") 231 sys_exit(rcA) 232 return rcA 233 } 234 let lfd: i64 = sys_openat_append("knowledge/status/driver_spec.log" as *u8, 0x1a4) 235 236 let blk_out: *u8 = "runtime/_hdl_build/_drv_proto_blk.bin" as *u8 237 let blk_gold: *u8 = "runtime/_hdl_build/_drv_proto_blk.bin.gold" as *u8 238 let net_out: *u8 = "runtime/_hdl_build/_drv_proto_net.bin" as *u8 239 let net_gold: *u8 = "runtime/_hdl_build/_drv_proto_net.bin.gold" as *u8 240 241 let gA: *u8 = sys_mmap(2048) 242 let gB: *u8 = sys_mmap(2048) 243 244 // (1) BLK full register/ring/irq transaction on the sovereign emu. 245 let blk_rc: i64 = g_emit_run("knowledge/specs/drv_proto_blk_virt.spec" as *u8, blk_out, blk_gold, gA, 2048, "/tmp/_drvproto_blk_serial.txt" as *u8, "/tmp/_drvproto_blk_emit.out" as *u8) 246 // (2) NET handshake (different device class, DeviceID=1) on the sovereign emu. 247 let net_rc: i64 = g_emit_run("knowledge/specs/drv_proto_net_virt.spec" as *u8, net_out, net_gold, gB, 2048, "/tmp/_drvproto_net_serial.txt" as *u8, "/tmp/_drvproto_net_emit.out" as *u8) 248 var blk_ok: i64 = 0 249 if blk_rc == 0 { blk_ok = 1 } 250 var net_ok: i64 = 0 251 if net_rc == 0 { net_ok = 1 } 252 // NAME THE FAILING CONJUNCT IMMEDIATELY, on its own line, before any aggregate is printed. 253 if blk_ok == 0 { g_p(" blk FAILED: " as *u8); g_p(g_er_reason(blk_rc)); g_p("\n" as *u8); g_dump_serial("blk" as *u8, "/tmp/_drvproto_blk_serial.txt" as *u8) } 254 if net_ok == 0 { g_p(" net FAILED: " as *u8); g_p(g_er_reason(net_rc)); g_p("\n" as *u8); g_dump_serial("net" as *u8, "/tmp/_drvproto_net_serial.txt" as *u8) } 255 256 // (3) DISTINCT: two op-lists -> two different drivers (same emitter binary). 257 var distinct: i64 = 0 258 if g_strlen(gA) > 0 { if g_strlen(gB) > 0 { if g_streq(gA, gB) == 0 { distinct = 1 } } } 259 260 // (4) TAMPER x2 on the BLK image: device-base lui imm (byte 7) + magic-expected li high (byte 15). 261 let gAn: i64 = g_strlen(gA) 262 let t1: i64 = g_tamper(blk_out, 7, gA, gAn, "/tmp/_drvproto_t1.bin" as *u8, "/tmp/_drvproto_t1.txt" as *u8) 263 let t2: i64 = g_tamper(blk_out, 15, gA, gAn, "/tmp/_drvproto_t2.bin" as *u8, "/tmp/_drvproto_t2.txt" as *u8) 264 // ★★★★★★A TAMPER TEST ASSERTS "GOLDEN IS ABSENT AFTER CORRUPTION" -- WHICH PROVES NOTHING IF THE GOLDEN 265 // WAS ALREADY ABSENT BEFORE IT. With blk_ok==0 both tampers return "bites" FOR FREE, and this gate was 266 // printing `tamper_bites=yes`: an UNEARNED GREEN SUB-CLAIM sitting inside a RED verdict, which is the 267 // most misleading thing a gate can emit -- the reader trusts the parts that say yes. 268 // ★★★★★AN AXIS THAT CANNOT SEE MUST ABSTAIN, NOT ACQUIT. blk_ok IS this axis's positive control: the 269 // untampered run must produce the golden before its disappearance can mean anything. 270 // ★COMPOSE THE BASE CLASS, NEVER ADD A SECOND RULER -- I nearly hand-rolled a third state right beside 271 // the primitive built for it. gv_bite(name, fired_on_bad, fired_on_good, ctr) IS "fires on bad, silent 272 // on good", and it prints [VACUOUS] / [FALSE-POSITIVE] itself. Here "firing" = the golden DISAPPEARS: 273 // bad = both corruptions dropped golden A -> the detector MUST fire 274 // good = the UNTAMPERED image ALSO lacks golden A -> the detector MUST NOT fire 275 // With blk broken, `good` is 1 and gv_bite reports FALSE-POSITIVE, which is the honest reading: a 276 // tamper check whose golden was already missing discriminates nothing. 277 var tamper_both: i64 = 0 278 if t1 == 1 { if t2 == 1 { tamper_both = 1 } } 279 // blk_rc 0 and 5 are EXACTLY the codes where the golden WAS present in the untampered serial (5 = 280 // present but no clean halt). Deriving the positive control from the reason code is the direct payoff 281 // for decomposing the compound assertion above -- before that, this control was not expressible. 282 // ⚠WHEN A PARTITION GAINS A CLASS, EVERY DERIVED SET MUST BE REVISITED: code 6 also means the golden 283 // WAS present, so omitting it here would silently disarm the tamper control for that case. 284 var blk_golden_seen: i64 = 0 285 if blk_rc == 0 { blk_golden_seen = 1 } 286 if blk_rc == 5 { blk_golden_seen = 1 } 287 if blk_rc == 6 { blk_golden_seen = 1 } 288 var tamper_fires_on_good: i64 = 1 289 if blk_golden_seen == 1 { tamper_fires_on_good = 0 } 290 291 // ---- MIGRATED ONTO THE BASE CLASS (D001), BY HAND ---------------------------------------------- 292 // /api/promote refused this gate for rolling its own verdict, and the record is explicit that the 293 // `allow_own_verdict=yes` escape SHIPS AN UNREADABLE GATE -- nx_gate_green cannot judge it and it 294 // records no harness.jrnl frame, so flake and erosion stay invisible for it. The record is equally 295 // explicit that the ASSISTED migration collapses N teeth into ONE boolean (ctr[0]=green; ctr[1]=1), 296 // the very defect gv_ctr exists to prevent -- so this is the HAND migration onto per-tooth gv_check. 297 // ★DECLARED == EXECUTED BY CONSTRUCTION: the denominator now moves by itself when a tooth is added, 298 // where the hand-rolled 4-way `pass` conjunction below it would have gone on saying 4 forever. 299 let ctr: *i64 = gv_ctr() 300 // CODE 7 IS NOT A FAILING TOOTH, IT IS AN UNOBSERVABLE ONE, AND THE TWO MUST NOT SHARE A COUNTER. 301 // If the emulator never rendered its verdict line the run was cut off, and NOTHING here was measured 302 // -- convicting the driver on that evidence is the false-alarm this gate spent a whole investigation 303 // being. Abstaining as a BRANCH rather than an early return is deliberate: this gate's own law is 304 // ONE LOG ROW, ALWAYS, and a return here would skip the row and take the reasons with it -- the 305 // exact branch-dependent-field-set defect the log comment below was written to kill. 306 var emu_cut: i64 = 0 307 if blk_rc == 7 { emu_cut = 1 } 308 if net_rc == 7 { emu_cut = 1 } 309 if emu_cut == 1 { 310 gv_need("a COMPLETED emulator run -- the transcript carries no `BOOTSOV verdict=` line, so the emulator was cut off before it could judge. That is a statement about the host (check /proc/loadavg and re-run), not about the driver" as *u8, 0, ctr) 311 } else { 312 gv_check("blk_full_txn: virtio-blk handshake + queue config + descriptor lay + avail/used ring + status writeback + sector roundtrip, clean halt", blk_ok, ctr) 313 gv_check("net_handshake: virtio-net DeviceID=1 at 0x10002000, a DIFFERENT device class, clean halt", net_ok, ctr) 314 gv_check("distinct: goldenA != goldenB and both non-empty, authored by the SAME emitter binary (the protocol state machine is synthesized FROM THE SPEC, not a fixed virtio-blk template)", distinct, ctr) 315 gv_bite("tamper-bite-blk: base-imm and magic-const corruption each drop golden A, while the untampered image KEEPS it", tamper_both, tamper_fires_on_good, ctr) 316 } 317 318 // ONE LOG ROW, ALWAYS -- not one row per verdict branch. The old shape wrote a GREEN row from one 319 // branch and a RED row from another, and the two had DRIFTED: only the GREEN branch recorded the 320 // goldens, only the RED branch recorded the reasons. ★★★★★A ROW WHOSE FIELD SET CHANGES WITH ITS 321 // VERDICT CANNOT BE READ BY ONE PARSER, AND THE FIELD YOU MOST NEED IS ALWAYS IN THE OTHER BRANCH. 322 if lfd >= 0 { 323 g_fp(lfd, "DRVPROTOGATE keystone=driver-protocol-from-spec composes=emitter-of-emitters+HWMAP runtime=sovereign-emu transport=legacy-virtio-mmio blk_ok=" as *u8); g_fn(lfd, blk_ok) 324 // the LOG carries the named reason too -- a row that only records 0/1 sends the next reader 325 // through the same five-way investigation this gate just did for them. 326 g_fp(lfd, " blk_reason=" as *u8); g_fp(lfd, g_er_reason(blk_rc)) 327 g_fp(lfd, " net_reason=" as *u8); g_fp(lfd, g_er_reason(net_rc)) 328 g_fp(lfd, " tamper_control_fires_on_good=" as *u8); g_fn(lfd, tamper_fires_on_good) 329 g_fp(lfd, " net_ok=" as *u8); g_fn(lfd, net_ok) 330 g_fp(lfd, " distinct=" as *u8); g_fn(lfd, distinct) 331 g_fp(lfd, " t1=" as *u8); g_fn(lfd, t1); g_fp(lfd, " t2=" as *u8); g_fn(lfd, t2) 332 g_fp(lfd, " goldenA=" as *u8); g_fp(lfd, gA) 333 g_fp(lfd, " goldenB=" as *u8); g_fp(lfd, gB) 334 g_fp(lfd, " epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()) 335 g_fp(lfd, "\n" as *u8); sys_close(lfd) 336 } 337 // THE EXIT CODE NOW CARRIES THE VERDICT (and gv_verdict writes the harness.jrnl frame), which is the 338 // whole point of the D001 migration: /api/gate_run derives GREEN/RED/SKIP from rc, so a gate that 339 // printed RED and returned 0 was being SERVED AS GREEN. 340 let rc: i64 = gv_verdict("DRVPROTOGATE", ctr, "the GENERIC nx_drv_proto_emit synthesized a full virtio-blk register/ring/irq driver AND a virtio-net handshake driver from two op-list SPECS; both completed against the real device models on the sovereign rv64 emu with clean halts; the state machine is DATA-driven; and two independent BLK tampers bite against a LIVE positive control -- driver-from-spec, author=emitter") 341 sys_exit(rc) 342 return rc 343}