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}