Skip to content

Tool: witness — MC/DC for the WebAssembly component model (+ announcement post) #29

@avrabe

Description

@avrabe

What

witness is a proposed small tool that executes MC/DC-style coverage measurement on WebAssembly modules (including composed components post-meld and optimized Wasm post-loom), with source mapping back to rivet requirements when DWARF or the Wasm name section is available.

Name rationale: ties to the attestation frame the blog arc is built around — "you cannot attest to what you did not observe." witness is the instrument that makes the observation, so the attestation isn't hollow. Fits the active-verb cadence of the other tools (sigil signs, rivet validates, spar analyses).

Why

Follow-up to two posts in the arc:

Those posts argue:

  • MC/DC at the Wasm level bypasses the hardest part of MC/DC-for-Rust (pattern-matching mapping)
  • Variant management makes MC/DC scope tractable
  • The C-macro / post-preprocessor precedent makes post-Wasm measurement structurally uncontroversial
  • Multi-level measurement across the PulseEngine pipeline (Rust source → Wasm → meld → loom → synth) is the strongest evidence chain DO-178C was designed to accept

witness is the concrete instrument that makes those arguments empirical rather than theoretical. Without it, the posts are an argument; with it, the posts are an argument with a reference tool.

Scope (incremental)

Version Capability
v0.1 Instrument a .wasm module with branch counters; run a test harness; emit a branch-coverage report at the decision level. Strict-interpretation (per-br_if) coverage. No MC/DC condition decomposition yet.
v0.2 MC/DC decomposition — group br_if / br_table sequences back into source-level decisions when DWARF is present; strict-per-br_if fallback when not.
v0.3 rivet integration — link coverage back to requirements via the rivet schema; emit as an in-toto predicate that sigil bundles can carry.
v0.4 Variant-aware scope — post-cfg, post-meld, post-loom as selectable measurement points. Integrates with loom's translation-validation output.
v1.0 Check-It pattern qualification artifact — emit a checkable coverage attestation that a small, qualified checker can validate under DO-330.

Relationship to Rust-level MC/DC (Ferrous / DLR)

Complementary, not competitive. When the Ferrous/DLR MC/DC tool for Rust lands via the Safety-Critical Rust Consortium's 2026 Rust Project Goal, witness does not become obsolete. Different measurement points have different blind spots:

  • Rust-level MC/DC measures source-level decisions (what the human wrote)
  • witness measures post-compile Wasm (what actually ships)
  • Translation validation (loom's Z3 TV) bridges proofs across the two levels
  • Coverage at both levels is additive evidence — the multi-level discipline DO-178C was designed to accept

The overdo principle applies here too: we adopt both tools, not one. Resistance is futile. Each catches what the other misses, and the assessor-legibility of the combined dossier is stronger than either alone.

Hard technical problem

Decision-granularity at the Wasm level. Short-circuit evaluation at Rust source (a && b && c) compiles to multiple br_if instructions; MC/DC requires grouping them back into the source-level decision. The defensible pick is DWARF-informed reconstruction with strict-per-br_if as the always-available fallback. The definition deserves a short paper once v0.2 ships.

Ecosystem integration

  • Depends on kiln or another Wasm runtime to execute instrumented modules
  • Reads loom's translation-validation output to know the post-optimization CFG
  • Reports to rivet as requirement-to-coverage evidence
  • Feeds sigil attestation bundles as an in-toto coverage predicate (once sigil composes upstream predicates)
  • Composes with meld output for multi-component modules

Repo

Not yet created. Reserve github.com/pulseengine/witness (or similar) when v0.1 code exists.

Blog post

Draft file: content/blog/2026-04-25-witness-wasm-mcdc.md (draft = true). Bones in place, iterate as v0.1 ships. Announcement post written in the same style as the variant-pruning post — argument first, tool second, roadmap as honest "shipping today vs. in the pipe" split.

Related

  • Closes the argument opened in the variant-pruning draft
  • Provides empirical grounding for the SDD post's MBSE and oracle-gated claims
  • Candidate future post: "The compilation pipeline as an evidence structure" — multi-level coverage measurement across meld/loom/synth with TV bridging the layers. Deferred until witness v0.1 + loom TV are both shipping.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions