test(witness): close verify-core's coverable MC/DC gap; baseline 5->3 (#128, REQ-25)

verification/witness-harness/README.md

@@ -26,18 +26,23 @@ the varint decoder.
 ## CI gate
 
 [`witness-gate.sh`](witness-gate.sh) runs the whole flow below and **fails
-if the MC/DC gap count rises past the committed baseline** (`BASELINE_GAP`,
-currently 17 on the CI host, witness `v0.37.0`; ~16 on macOS/aarch64 due
-to host-dependent wasm codegen — override `BASELINE_GAP` for local runs).
-**Known limitation (#128):** the count is over the *whole* instrumented
-wasm (std + allocator + crypto deps), so only ~1 of ~40 decisions is
-verify-core's own — the count drifts with dep/toolchain bumps (12→17 from
-07-11 to 08-05 was std/dep churn, not a coverage loss). The gate should be
-scoped to `src/` decisions; tracked in #128. It is wired as the gating `witness-mcdc`
-job in `.github/workflows/formal-verification.yml` (#165 Track C / #128) —
-a real gate (no `continue-on-error`), but a *regression* gate, so it cannot
-block on the still-incomplete Phase 3 coverage. Closing gaps lowers the
-count; then refresh `out/mcdc-report.txt` and `BASELINE_GAP`.
+if the MC/DC gap count rises past the committed baseline** (`SRC_BASELINE_GAP`,
+currently **3** on the CI host, witness `v0.37.0`). The gate counts gaps
+**only in `src/`-path decisions** — verify-core's own code — not the whole
+instrumented wasm (std + allocator + crypto deps drifted the old whole-wasm
+count with every toolchain bump; that total is now printed for information
+only). #128 / REQ-25 closed the feasible gaps: a `WASM_COMPONENT_HEADER`
+scenario drove `Module::init_from_reader`'s header decision to full MC/DC,
+and short-buffer `decode_varint_N` scenarios exercise `get32`'s `read_exact`
+EOF path. The residual 3 gaps are in an inlined `<&[u8] as Read>::read_exact`
+decision that witness misattributes to the `get32` source line (the `^src/`
+filter counts it via debug-line inheritance); its copy-path conditions are
+unreachable given verify-core's fixed 1-byte / 8-byte reads — infeasible,
+documented in `witness-gate.sh`, not silenced. The gate is wired as the
+gating `witness-mcdc` job in `.github/workflows/formal-verification.yml`
+(#165 Track C / #128) — a real gate (no `continue-on-error`), and a
+*regression* gate: closing a gap lowers the count, then refresh
+`SRC_BASELINE_GAP` (CI is the authoritative host).
 
 ```sh
 # One-shot: build + instrument + run + report + gate (auto-downloads witness)

verification/witness-harness/src/lib.rs

@@ -39,6 +39,62 @@ pub extern "C" fn decode_varint_5(b0: u8, b1: u8, b2: u8, b3: u8, b4: u8) -> u32
     varint::get32(&mut slice).unwrap_or(0xFFFFFFFF)
 }
 
+// --- short-buffer exports: drive `get32`'s `reader.read_exact(&mut byte)?`
+// EOF-error path (#128 / REQ-25). `decode_varint_5` always supplies 5 bytes,
+// so `read_exact` never returns `Err` — the `?` early-return in `get32` is
+// then never taken and witness reports the shared `read_exact` decision
+// (`varint.rs:24`) as Partial (conditions c2/c3 GAP). Feeding a buffer that
+// runs out mid-decode exercises that error propagation: `decode_varint_N`
+// gives get32 exactly N continuation-tagged bytes (0x80 set) so the loop
+// asks for byte N+1 and read_exact hits EOF.
+//
+// These are FIXED-ARITY (one export per length) on purpose: a single
+// length-parameterised export would need an `if`/`.min()` inside the harness,
+// and witness would attribute that branch to `src/lib.rs`, injecting a
+// phantom "verify-core" decision that the gate's `^src/` filter would count.
+// Fixed arity keeps every branch inside verify-core's own `get32`.
+
+/// Decode a zero-byte varint — `get32` EOFs on its first `read_exact`.
+#[unsafe(no_mangle)]
+pub extern "C" fn decode_varint_0() -> u32 {
+    let bytes: [u8; 0] = [];
+    let mut slice = &bytes[..];
+    varint::get32(&mut slice).unwrap_or(0xFFFFFFFF)
+}
+
+/// Decode a 1-byte varint whose continuation bit is set — `get32` consumes
+/// byte 0, loops, and EOFs on the second `read_exact`.
+#[unsafe(no_mangle)]
+pub extern "C" fn decode_varint_1(b0: u8) -> u32 {
+    let bytes = [b0];
+    let mut slice = &bytes[..];
+    varint::get32(&mut slice).unwrap_or(0xFFFFFFFF)
+}
+
+/// 2-byte buffer — EOF on the third `read_exact` when both bytes continue.
+#[unsafe(no_mangle)]
+pub extern "C" fn decode_varint_2(b0: u8, b1: u8) -> u32 {
+    let bytes = [b0, b1];
+    let mut slice = &bytes[..];
+    varint::get32(&mut slice).unwrap_or(0xFFFFFFFF)
+}
+
+/// 3-byte buffer — EOF on the fourth `read_exact` when all three continue.
+#[unsafe(no_mangle)]
+pub extern "C" fn decode_varint_3(b0: u8, b1: u8, b2: u8) -> u32 {
+    let bytes = [b0, b1, b2];
+    let mut slice = &bytes[..];
+    varint::get32(&mut slice).unwrap_or(0xFFFFFFFF)
+}
+
+/// 4-byte buffer — EOF on the fifth `read_exact` when all four continue.
+#[unsafe(no_mangle)]
+pub extern "C" fn decode_varint_4(b0: u8, b1: u8, b2: u8, b3: u8) -> u32 {
+    let bytes = [b0, b1, b2, b3];
+    let mut slice = &bytes[..];
+    varint::get32(&mut slice).unwrap_or(0xFFFFFFFF)
+}
+
 /// Try to parse the 8-byte WASM module header `[b0..b7]` via
 /// `Module::init_from_reader`.
 ///

verification/witness-harness/witness-gate.sh

@@ -4,7 +4,7 @@
 # Rebuilds the harness, instruments it with a pinned `witness` release, runs
 # the fixed scenario set, and fails if the number of MC/DC *gap* conditions
 # has INCREASED past the committed baseline. Improvements (fewer gaps) pass
-# and should be followed by refreshing out/mcdc-report.txt + BASELINE_GAP.
+# and should be followed by lowering SRC_BASELINE_GAP (see HOST CALIBRATION).
 #
 # Why gap-count and not a byte-diff of the report: wasm codegen / witness
 # row ordering can differ across hosts and witness versions; the gap count
@@ -30,21 +30,59 @@ WITNESS_VERSION="${WITNESS_VERSION:-v0.37.0}"
 # (the compiler still lays out our own branches differently per target). The
 # whole-wasm total is still printed, for information only.
 #
-# HOST CALIBRATION: the baseline is set on the CI host (ubuntu-latest / linux
-# x86_64) — the authoritative gate host — where the scoped count is 5:
-# varint.rs:29 (3 gaps: c0,c3,c4) + wasm_module/mod.rs:455 (2 gaps: c0,c1). A
-# local macOS/aarch64 run yields FEWER (measured: 3 — mod.rs:455 is fully covered
-# there), which PASSES under the same baseline (3 <= 5), so no local override is
-# ever needed to go green. The SRC_BASELINE_GAP env knob is for re-calibrating on
-# CI when a scenario closes a gap, NOT for silencing a red locally: a host that
-# yields MORE than the baseline is a real finding (a new uncovered branch), not
-# an override target. Only lower the committed baseline from the CI (linux) count.
+# HOST CALIBRATION: baseline set on the CI host (ubuntu-latest / linux x86_64) —
+# the authoritative gate host. The scoped count was 5 (varint decision 3 +
+# header decision 2). #128 / REQ-25 added two kinds of scenario that close the
+# feasible gaps:
 #
-# Both baseline decisions are `Partial`; CLOSING them (adding witness scenarios
-# that supply the missing unique-cause rows) is follow-up MC/DC work on #128 —
-# the gate's job here is to stop a REGRESSION (a NEW gap in verify-core's own
-# code) from landing.
-SRC_BASELINE_GAP="${SRC_BASELINE_GAP:-5}"
+#   (a) try_parse_wasm:0,97,115,109,13,0,1,0 — the WASM_COMPONENT_HEADER accept
+#       path of Module::init_from_reader (mod.rs:456). This is a genuine second
+#       accept branch of verify-core's own header decision; it supplied the
+#       missing unique-cause row for `header != WASM_COMPONENT_HEADER` and drove
+#       that decision to full MC/DC (was 2 gaps). Semantic, host-invariant — the
+#       -2 that lowers the committed baseline from 5 to 3.
+#
+#   (b) decode_varint_0..4 — short-buffer exports that make get32's
+#       `reader.read_exact(&mut byte)?` hit EOF at each loop iteration, covering
+#       get32's EOF error-propagation path. Locally this proves one of the
+#       read_exact conditions; whether that nets a -1 on linux is NOT banked
+#       (see below), so the committed baseline stays at 3. CI shows what it nets.
+#
+# WHY 3 AND NOT 0 — the residual is (inferred) misattributed inlined std, and
+# infeasible: the remaining ~3 gap conditions live in the decision witness labels
+# `src/wasm_module/varint.rs:24` (macOS) / `:29` (linux). Row-count arithmetic
+# indicates that decision is NOT verify-core logic — it is
+# `<&[u8] as Read>::read_exact` INLINED into get32 (its truth table is 20
+# length-1 rows matching the varint scenarios' iteration counts + N length-8 rows
+# matching the header scenarios; inferred from the table, not from witness's own
+# attribution). The `^src/` filter counts it only because inlined std inherits
+# get32's debug line.
+# Its residual conditions are the read_exact copy-path branches, which vary only
+# with buffer length. verify-core issues read_exact at exactly two lengths — 1
+# (get32, per byte) and 8 (init_from_reader, the header) — and every `c1=T`
+# (length-1) row has those copy branches invariant, so no honest input flips
+# them. They are INFEASIBLE without editing verify-core's own reads (which would
+# be gaming the metric) — the DO-178C "masked/unreachable condition, document
+# don't cover" case. NOTE: witness's `cN` condition indices are NOT stable across
+# runs/hosts (a decision re-derives when the row set changes); do not diff the
+# letters — e.g. macOS {c2,c3,c4} and linux {c0,c3,c4} are the same three
+# read_exact conditions relabeled, not a regression.
+#
+# So: linux 5 - 2 (header, banked) = 3, committed. Local macOS/aarch64 also
+# yields 3 (header covered by macOS codegen; three read_exact residuals), so it
+# PASSES without any override. If the short-buffer EOF scenarios ALSO net a read_exact
+# closure on linux without surfacing a replacement, the gate emits its own "lower
+# it" notice and CI tightens to 2 — that is the only sanctioned way to lower it
+# further. A host yielding MORE than the baseline is a real finding (a new
+# uncovered verify-core branch / a lost scenario), never an override target: only
+# ever lower from the CI (linux) count.
+#
+# GATE POTENCY (verified locally, macOS, this change): (1) SRC_BASELINE_GAP=2 ->
+# the gate ::errors and exits 1 (comparison + exit path bites). (2) deleting the
+# length-8 header reads (the try_parse_wasm scenarios) strips a read_exact
+# condition's unique-cause pair, SRC_GAP rises 3 -> 4 > baseline, exit 1 (a real
+# verify-core coverage regression is caught, not just a threshold trip).
+SRC_BASELINE_GAP="${SRC_BASELINE_GAP:-3}"
 HERE="$(cd "$(dirname "$0")" && pwd)"
 cd "$HERE"
 
@@ -82,7 +120,13 @@ mkdir -p out
   --invoke-with-args 'decode_varint_5:128,128,128,1,0' \
   --invoke-with-args 'decode_varint_5:128,128,128,128,1' \
   --invoke-with-args 'decode_varint_5:128,128,128,128,128' \
+  --invoke-with-args 'decode_varint_0:' \
+  --invoke-with-args 'decode_varint_1:128' \
+  --invoke-with-args 'decode_varint_2:128,128' \
+  --invoke-with-args 'decode_varint_3:128,128,128' \
+  --invoke-with-args 'decode_varint_4:128,128,128,128' \
   --invoke-with-args 'try_parse_wasm:0,97,115,109,1,0,0,0' \
+  --invoke-with-args 'try_parse_wasm:0,97,115,109,13,0,1,0' \
   --invoke-with-args 'try_parse_wasm:255,97,115,109,1,0,0,0' \
   --invoke-with-args 'try_parse_wasm:0,255,115,109,1,0,0,0' \
   --invoke-with-args 'try_parse_wasm:0,97,255,109,1,0,0,0' \