test(witness): close verify-core's coverable MC/DC gap; baseline 5->3 (#128, REQ-25) - #242
Merged
Conversation
…#128) 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes the closeable half of #128 (REQ-25). The scoped witness gate had
SRC_BASELINE_GAP=5over twoPartialdecisions; this drives verify-core's one genuinely-coverable decision to full MC/DC and tightens the baseline to 3.What
Partialdecisions is verify-core's own logic: the header compare inModule::init_from_reader(header != WASM_HEADER && header != WASM_COMPONENT_HEADER; witness misattributes its line tovarint.rs). Added a scenario for theWASM_COMPONENT_HEADERaccept path (00 61 73 6d 0d 00 01 00) — the missing unique-cause row. Result:0/142 → 1/152fully-covered decisions.decode_varint_0..4exerciseget32'sread_exact(...)?EOF error-propagation. Fixed-arity on purpose — a length-parameterised export would inject anif/.min()branch witness attributes tosrc/lib.rs, a phantom "verify-core" decision. This keeps every branch insideget32.The residual 3 (documented, not faked)
All in the inlined
<&[u8] as Read>::read_exactdecision — copy branches that vary only with buffer length (verify-core reads at lengths 1 and 8 only), so no honest verify-core input flips them. This is the DO-178C "masked/unreachable — document, don't cover" case. The underlying cause — the^src/heuristic counting inlined-std decisions — is filed as #241.Potency (verified empirically, not reasoned)
SRC_BASELINE_GAP=2→ RED (exit 1)3 → 4 > 3→ RED (catches a genuine verify-core coverage regression)SRC_GAP=3, baseline 3, gate OKverify-core/src/is untouched (scenarios + harness exports only — no logic edits to make coverage easier).🤖 Generated with Claude Code