feat(witness): Phase 2 — instrument Module::init_from_reader

verification/witness-harness/README.md

@@ -1,8 +1,14 @@
 # witness MC/DC harness for `wsc-verify-core`
 
-Phase-1 proof-of-concept harness for running
-[`pulseengine/witness`](https://github.com/pulseengine/witness) — an MC/DC
-branch-coverage tool for WebAssembly — against sigil's verification core.
+Harness for running [`pulseengine/witness`](https://github.com/pulseengine/witness)
+— an MC/DC branch-coverage tool for WebAssembly — against sigil's
+verification core.
+
+| Phase | Target | Status |
+|---|---|---|
+| 1 | `varint::get32` (LEB128 decoder) | done |
+| 2 | `Module::init_from_reader` (WASM header parser) | done |
+| 3 | `PublicKey::verify_multi` (full verification with signed-module fixtures) | tracked on #128 |
 
 This crate is **excluded from the main workspace** (`workspace.exclude` in
 the root `Cargo.toml`) because it builds for a wasm target and would
@@ -39,35 +45,45 @@ WASM=target/wasm32-wasip1/debug/wsc_witness_harness.wasm
 mkdir -p out
 witness instrument "$WASM" -o out/instrumented.wasm
 witness run out/instrumented.wasm \
+    # Phase 1: varint decoder scenarios — continuation-bit at each position
     --invoke-with-args 'decode_varint_5:1,0,0,0,0' \
     --invoke-with-args 'decode_varint_5:128,1,0,0,0' \
     --invoke-with-args 'decode_varint_5:128,128,1,0,0' \
     --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' \
+    # Phase 2: WASM-header parser scenarios — valid + flip each magic/version byte
+    --invoke-with-args 'try_parse_wasm:0,97,115,109,1,0,0,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' \
+    --invoke-with-args 'try_parse_wasm:0,97,115,255,1,0,0,0' \
+    --invoke-with-args 'try_parse_wasm:0,97,115,109,255,0,0,0' \
+    --invoke-with-args 'try_parse_wasm:0,0,0,0,0,0,0,0' \
     -o out/run.json
 witness report --input out/run.json --format mcdc
 ```
 
-## Observed output (Phase 1)
+## Observed output (Phases 1 + 2)
 
 ```
-decisions: 0/162 full MC/DC; conditions: 1 proved, 13 gap, 582 dead
+decisions: 0/164 full MC/DC; conditions: 2 proved, 19 gap, 583 dead
 
-decision #1 varint.rs:28: NoWitness
-  truth table:
-    row 1:  {c0=F, c1=T, c2=T} -> T
-    row 10: {c0=F, c1=T, c2=T} -> T
-    ...
+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 path
 ```
 
-`varint.rs:28` is sigil's actual LEB128 decoder — that decision is being
-instrumented through the carved `wsc-verify-core`. The high "dead" count
-(582) is mostly `std::result`/formatting machinery reachable from the
-harness; what matters for Phase 1 is that witness can *see* sigil-core
-decisions at all. Phase 2 will design scenarios that drive the
-`decode_varint_5` and (later) `verify_multi` decisions to **full MC/DC**
-rather than just demonstrating reachability.
+`varint.rs:26` and `mod.rs:456` are sigil's own code — instrumented through
+the carved `wsc-verify-core`. The high "dead" count (583) is mostly
+`std::result` / formatting / panic-runtime machinery reachable from the
+harness; what matters for Phases 1 + 2 is that witness can *see* multiple
+sigil-core decisions at all.
+
+Phase 3 (#128) will design scenarios that drive `verify_multi` to full MC/DC
+with crafted signed-module fixtures — that is the test-corpus design work
+the [curl-comparison writeup](../../audit/witness-wasm-inspection.md) called
+out as the actual cost of MC/DC adoption (the tool is the cheap part).
 
 ## Notes on target choice
 

verification/witness-harness/src/lib.rs

@@ -1,24 +1,30 @@
-//! Witness MC/DC harness for `wsc-verify-core` — Phase 1.
+//! Witness MC/DC harness for `wsc-verify-core` — Phases 1 + 2.
 //!
-//! This crate compiles to a `wasm32-unknown-unknown` cdylib that the
+//! This crate compiles to a `wasm32-wasip1` cdylib that the
 //! [`pulseengine/witness`](https://github.com/pulseengine/witness) tool
 //! instruments to reconstruct **Modified Condition / Decision Coverage**
 //! truth tables for the verification core.
 //!
-//! # Phase 1 — toolchain end-to-end
+//! # Phase 1 — varint decoder (`varint::get32`)
 //!
-//! The scenario here drives `wasm_module::varint::get32` — sigil's LEB128
-//! decoder, the only sigil-core hot loop whose conditions a witness truth
-//! table can render cleanly. Five symbolic input bytes flip the
-//! continuation bit at each varint position; witness reports MC/DC over the
-//! decoder's loop.
+//! `decode_varint_5` drives sigil's LEB128 decoder. Five symbolic input
+//! bytes flip the continuation bit at each varint position; witness
+//! reports MC/DC over the decoder's loop.
 //!
-//! Phase 2 (#128) adds scenarios over `PublicKey::verify_multi` with
-//! crafted signed-module fixtures.
+//! # Phase 2 — WASM module parser (`Module::init_from_reader`)
+//!
+//! `try_parse_wasm` drives `Module::init_from_reader` on an 8-byte
+//! symbolic input. The WASM module format requires the magic bytes
+//! `[0x00, 0x61, 0x73, 0x6D]` followed by the version `[0x01, 0, 0, 0]`;
+//! flipping any one of those bytes hits a different parser-decision branch.
+//! This covers more of `wsc-verify-core`'s surface than Phase 1, while
+//! staying small enough that the truth tables remain legible. Phase 3
+//! (#128) will add scenarios over `PublicKey::verify_multi` with crafted
+//! signed-module fixtures.
 
 #![allow(clippy::missing_safety_doc)]
 
-use wsc_verify_core::wasm_module::varint;
+use wsc_verify_core::wasm_module::{Module, varint};
 
 /// Decode the LEB128 varint encoded in `[b0, b1, b2, b3, b4]`.
 ///
@@ -32,3 +38,31 @@ pub extern "C" fn decode_varint_5(b0: u8, b1: u8, b2: u8, b3: u8, b4: u8) -> u32
     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`.
+///
+/// Returns `0` on parse success, a nonzero discriminant on parse error
+/// (the specific value is informational; witness measures the branch
+/// coverage, not the return value). Each invocation flips one or more
+/// of the 8 header bytes — scenarios that flip exactly one byte at a
+/// time give MC/DC rows for the magic / version field decisions inside
+/// the parser.
+#[unsafe(no_mangle)]
+pub extern "C" fn try_parse_wasm(
+    b0: u8,
+    b1: u8,
+    b2: u8,
+    b3: u8,
+    b4: u8,
+    b5: u8,
+    b6: u8,
+    b7: u8,
+) -> u32 {
+    let bytes = [b0, b1, b2, b3, b4, b5, b6, b7];
+    let mut slice = &bytes[..];
+    match Module::init_from_reader(&mut slice) {
+        Ok(_stream) => 0,
+        Err(_) => 1,
+    }
+}