From 20316f94741f6e6339dc250869dbf3379c255321 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 11 Aug 2026 21:39:56 +0200 Subject: [PATCH] test(witness): close verify-core's coverable MC/DC gap; baseline 5->3 (#128) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The scoped witness gate had SRC_BASELINE_GAP=5 across two Partial decisions. On inspection only ONE is verify-core's own logic — the header-compare decision in Module::init_from_reader (`header != WASM_HEADER && header != WASM_COMPONENT_HEADER`, misreported at varint.rs by witness line attribution). Add a scenario for the WASM_COMPONENT_HEADER accept path (`00 61 73 6d 0d 00 01 00`) — the missing unique-cause row — driving that decision to FULL MC/DC (0->1 fully-covered). Add fixed-arity short-buffer exports (decode_varint_0..4) exercising get32's `read_exact(...)?` EOF error-propagation. Fixed arity is deliberate: a length- parameterised export would inject an `if`/`.min()` branch that witness attributes to src/lib.rs, a phantom "verify-core" decision — this keeps every branch inside get32. Baseline 5->3 (a tightening, backed by the closure). The residual 3 gaps are the INLINED `<&[u8] as Read>::read_exact` decision's copy branches (vary only with buffer length; verify-core reads at lengths 1 and 8 only) — infeasible to cover without gaming; documented, and the scoping-heuristic imprecision filed separately. Gate potency re-verified: baseline 2 -> red; deleting header reads -> gap 4>3 -> red. verify-core src/ untouched. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH --- verification/witness-harness/README.md | 29 ++++---- verification/witness-harness/src/lib.rs | 56 +++++++++++++++ verification/witness-harness/witness-gate.sh | 74 ++++++++++++++++---- 3 files changed, 132 insertions(+), 27 deletions(-) diff --git a/verification/witness-harness/README.md b/verification/witness-harness/README.md index 1ac0ed3..f85ff7a 100644 --- a/verification/witness-harness/README.md +++ b/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) diff --git a/verification/witness-harness/src/lib.rs b/verification/witness-harness/src/lib.rs index d5b010a..280edfd 100644 --- a/verification/witness-harness/src/lib.rs +++ b/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`. /// diff --git a/verification/witness-harness/witness-gate.sh b/verification/witness-harness/witness-gate.sh index 70f0e95..c1809ce 100755 --- a/verification/witness-harness/witness-gate.sh +++ b/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' \