code wiki / _hdl_build / nx_toolrun_trunc_gate.nx

nx_toolrun_trunc_gate.nx source

↩ module page · 135 lines · 6205 B

1// nx_toolrun_trunc_gate.nx -- BITE-PROOF for tr_run_capture_tr's truncation discriminator (2026-08-08). 2// 3// SUBJECT: tr_drain_tr / tr_run_capture_tr in runtime/nx_tool_run.nx, added for debt 1786235483 -- 4// the three legacy drain loops exit on `total >= cap` and return success with outlen[0] == cap, which 5// is byte-for-byte identical to a child that emitted EXACTLY cap bytes. 51+ call sites. 6// 7// ***WHY THE FIXTURE STRADDLES THE BOUNDARY.*** A test whose child output is smaller than the cap can 8// never reach the branch under test -- it would pass against a stub that hardcodes FIT. So the teeth 9// are cap=N-1 (must report CUT) and cap=N exactly (must report FIT). The second is the one that a 10// trivial wrong implementation -- "buffer full therefore truncated" -- CANNOT pass. 11// 12// THE CHILD IS THIS GATE ITSELF (`emit <n>` writes exactly n bytes), so the fixture is deterministic 13// and needs no sibling organ. If argv[0] does not resolve, the child exits 127 and the teeth FAIL 14// loudly rather than passing vacuously. 15// 16// nx_toolrun_trunc_gate -> run the teeth 17// nx_toolrun_trunc_gate emit <n> -> child fixture: emit exactly n bytes 18// license_tier: ORIGINAL expect_exit: 0 No hw writes (Rule 26). 19import "nx_syscalls.nx" 20import "nx_sovjson_lib.nx" 21import "nx_gate_verdict.nx" 22import "nx_tool_run.nx" 23 24const TG_N: i64 = 3000 25const TG_BUF: i64 = 65536 26const TG_TMO: i64 = 5000 27const TG_FILL: i64 = 65 28 29func tg_emit(n: i64) -> i64 { 30 let b: *u8 = sys_mmap(n + 64) 31 var i: i64 = 0 32 while i < n { b[i] = TG_FILL as u8; i = i + 1 } 33 sys_write(1, b, n) 34 return 0 35} 36 37// fork THIS elf as `emit <n>` and capture it under `cap`, reporting outlen + trunc. 38func tg_run(self: *u8, n: i64, cap: i64, outlen: *i64, trunc: *i64) -> i64 { 39 let nb: *u8 = sys_mmap(64) 40 let k: i64 = sj_catn(nb, 0, n) 41 nb[k] = 0 as u8 42 let av: *i64 = sys_mmap(64) as *i64 43 av[0] = self as i64 44 av[1] = "emit" as *u8 as i64 45 av[2] = nb as i64 46 av[3] = 0 47 let out: *u8 = sys_mmap(TG_BUF + 64) 48 return tr_run_capture_tr(self, av, out, cap, outlen, TG_TMO, trunc) 49} 50 51func tg_diag(label: *u8, rc: i64, got: i64, tr: i64) -> i64 { 52 let d: *u8 = sys_mmap(512) 53 var o: i64 = sj_cat(d, 0, label) 54 o = sj_cat(d, o, " rc=" as *u8) 55 o = sj_catn(d, o, rc) 56 o = sj_cat(d, o, " outlen=" as *u8) 57 o = sj_catn(d, o, got) 58 o = sj_cat(d, o, " trunc=" as *u8) 59 o = sj_catn(d, o, tr) 60 d[o] = 10 as u8 61 o = o + 1 62 d[o] = 0 as u8 63 sj_puts(d) 64 return 0 65} 66 67func main(argc: i64, argv: *i64) -> i64 { 68 let self: *u8 = argv[0] as *u8 69 if argc >= 3 { 70 let v: *u8 = argv[1] as *u8 71 if sj_lit_eq(v, 0, sj_vlen(v), "emit" as *u8) == 1 { 72 tg_emit(sj_atoi_z(argv[2] as *u8)) 73 sys_exit(0) 74 return 0 75 } 76 } 77 78 let ctr: *i64 = gv_ctr() 79 gv_head("nx_toolrun_trunc_gate -- tr_run_capture_tr must tell CUT from FIT at the cap boundary" as *u8) 80 81 let ol: *i64 = sys_mmap(64) as *i64 82 let tc: *i64 = sys_mmap(64) as *i64 83 84 // neg-control-fits: output far under cap. MUST be FIT. A guard that refused everything would 85 // fail HERE -- that is the point of carrying a positive control. 86 let r1: i64 = tg_run(self, TG_N, TG_BUF, ol, tc) 87 tg_diag("neg-control-fits" as *u8, r1, ol[0], tc[0]) 88 var ok1: i64 = 0 89 if r1 == 0 { if ol[0] == TG_N { if tc[0] == TR_FIT { ok1 = 1 } } } 90 gv_check("neg-control-fits: 3000B under a 65536B cap reports FIT and captured all 3000" as *u8, ok1, ctr) 91 92 // T2 CUT: cap one byte short. outlen==cap asserts THE FIXTURE ACTUALLY REACHED THE CONDITION 93 // before the outcome is asserted -- without it this tooth could pass on a short read. 94 let r2: i64 = tg_run(self, TG_N, TG_N - 1, ol, tc) 95 tg_diag("T2-cut" as *u8, r2, ol[0], tc[0]) 96 var ok2: i64 = 0 97 if r2 == 0 { if ol[0] == TG_N - 1 { if tc[0] == TR_CUT { ok2 = 1 } } } 98 gv_check("T2 cap=N-1 reports CUT with the buffer filled exactly (fixture PROVEN at the boundary)" as *u8, ok2, ctr) 99 100 // T3 THE ANTI-VACUITY TOOTH: cap EXACTLY the output length. A full buffer is NOT truncation. 101 // The trivial wrong implementation (total>=cap => CUT) passes T2 and FAILS THIS. 102 let r3: i64 = tg_run(self, TG_N, TG_N, ol, tc) 103 tg_diag("T3-exact" as *u8, r3, ol[0], tc[0]) 104 var ok3: i64 = 0 105 if r3 == 0 { if ol[0] == TG_N { if tc[0] == TR_FIT { ok3 = 1 } } } 106 gv_check("T3 cap==N reports FIT -- a FULL buffer is not evidence of truncation" as *u8, ok3, ctr) 107 108 // T4 the legacy-caller shape: 51 existing sites pass no trunc pointer. A null must not fault. 109 let r4: i64 = tg_run(self, TG_N, TG_N - 1, ol, 0 as *i64) 110 tg_diag("T4-null-trunc" as *u8, r4, ol[0], 0 - 1) 111 var ok4: i64 = 0 112 if r4 == 0 { if ol[0] == TG_N - 1 { ok4 = 1 } } 113 gv_check("T4 null trunc pointer accepted (legacy shape) and capture still bounded at cap" as *u8, ok4, ctr) 114 115 // T5 MULTI-READ DRAIN: output 8x the cap, so the loop makes MANY read() calls before filling. 116 // The measured defect (nx_debtmine: 1048576 captured of a 4921787-byte plane) is THIS shape -- 117 // far past the cap -- not the tight boundary, so the gate must cover it explicitly. 118 let r5: i64 = tg_run(self, TG_N * 8, TG_BUF / 16, ol, tc) 119 tg_diag("T5-multiread" as *u8, r5, ol[0], tc[0]) 120 var ok5: i64 = 0 121 if r5 == 0 { if ol[0] == TG_BUF / 16 { if tc[0] == TR_CUT { ok5 = 1 } } } 122 gv_check("T5 output 8x cap reports CUT after a multi-read drain (the real-world shape)" as *u8, ok5, ctr) 123 124 // T6 EMPTY CHILD: zero bytes is not truncation. total(0) < cap, so the probe must NOT run -- 125 // an always-probing implementation would block here on a child that never writes. 126 let r6: i64 = tg_run(self, TG_N - TG_N, TG_FILL, ol, tc) 127 tg_diag("T6-empty" as *u8, r6, ol[0], tc[0]) 128 var ok6: i64 = 0 129 if r6 == 0 { if ol[0] == 0 { if tc[0] == TR_FIT { ok6 = 1 } } } 130 gv_check("T6 empty child reports FIT with outlen 0 -- silence is not truncation" as *u8, ok6, ctr) 131 132 let rc: i64 = gv_verdict("TOOLRUN-TRUNC-GATE" as *u8, ctr, "cap-boundary truncation signal proven in BOTH directions; null-trunc legacy shape safe" as *u8) 133 sys_exit(rc) 134 return rc 135}