feat(witness): Phase 2 — instrument Module::init_from_reader#133
Open
avrabe wants to merge 1 commit into
Open
Conversation
Adds a second scenario export, `try_parse_wasm(b0..b7) -> u32`, that drives `Module::init_from_reader` on an 8-byte symbolic input. The existing `decode_varint_5` scenario remains for Phase 1 (LEB128 decoder) coverage. Result with 7 scenarios across both exports: decisions: 0/164 full MC/DC; conditions: 2 proved, 19 gap, 583 dead decision #0 mod.rs:456: NoWitness ← Module::init_from_reader decision #2 varint.rs:26: Partial ← LEB128 decoder decision #3 mod.rs:387: Unreached ← wasm_module parser Witness now instruments multiple sigil-core decisions (varint + WASM parser), not just the single one from Phase 1. The toolchain is demonstrated end-to-end on a second target with zero changes to verify-core's public API. Symmetry note: `Module::init_from_reader` is also the function the torture-runner exercises against I/O fault injection — the same parser surface, measured two ways (witness for branch distinction, torture for error-path reachability). Phase 3 — full MC/DC scenarios over `PublicKey::verify_multi` with crafted signed-module fixtures — remains tracked on #128. That work is the test-corpus design effort the curl-comparison flagged as the actual cost of MC/DC adoption (the tool is the cheap part). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
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.
Summary
Extends the witness MC/DC harness with a second scenario export, `try_parse_wasm(b0..b7) -> u32`, driving `Module::init_from_reader` on an 8-byte symbolic input. Phase 1's `decode_varint_5` scenario remains for LEB128 coverage. Witness now instruments two sigil-core decisions, not just one.
Result
With 7 scenarios across both exports (6 continuation-bit positions for the decoder + 7 magic/version-flip variations for the parser):
```
decisions: 0/164 full MC/DC; conditions: 2 proved, 19 gap, 583 dead
decision #0 mod.rs:456: NoWitness ← Module::init_from_reader (Phase 2)
decision #2 varint.rs:26: Partial ← LEB128 decoder (Phase 1)
decision #3 mod.rs:387: Unreached ← wasm_module parser
```
The 583 "dead" conditions are mostly `std::result` / formatting / panic-runtime machinery reachable from the harness; the meaningful signal is that witness now sees multiple sigil-core decisions through the carved verify-core.
Symmetry with the torture runner
`Module::init_from_reader` is also the function the torture-runner (PR #131) exercises against I/O fault injection. Same parser surface, measured two ways: witness for branch distinction, torture for error-path reachability. Together they form the curl-comparison rigor triangle: mutation testing (cargo-mutants, already gated) + MC/DC (witness, advancing here) + fault injection (torture-runner, PR #131).
Phase 3 — out of scope
Full MC/DC scenarios over `PublicKey::verify_multi` with crafted signed-module fixtures remain tracked on #128. That work is the test-corpus design effort the curl-comparison writeup flagged as the actual cost of MC/DC adoption — the tool is the cheap part.
Test plan
🤖 Generated with Claude Code