v1.2.0 (FEAT-014 / DD-012): witness MC/DC on the real analyzer core

CHANGELOG.md

@@ -7,6 +7,69 @@ Versioning: [SemVer 2.0](https://semver.org/spec/v2.0.0.html).
 
 ## [Unreleased]
 
+## [1.2.0] — 2026-05-31
+
+Headline: **the analyzer's real decisions now carry MC/DC coverage
+evidence.** v1.2 closes the witness step of the original feature loop,
+blocked since v0.1 by the composition gap (v1.1 made `analyze()` runnable;
+v1.2 makes it *instrumentable*). Per DD-012, the analyzer's decision logic
+is extracted into a pure, bindgen-free core so witness can reconstruct an
+MC/DC truth table over the **real** transfer functions driven by the
+**real** corpus — not a synthetic proxy.
+
+### Added / Changed
+
+- **`crates/scry-analyze-core` (FEAT-014 / DD-012).** The analyzer's full
+  pipeline — wasmparser parse, the interval + region-memory fixpoint, the
+  call-graph / SCC / summary machinery, and the taint (noninterference)
+  walk, with ~40 helpers — moves out of `scry-analyzer` into a pure
+  `#![no_std]` crate with plain-Rust result types mirroring the WIT. Same
+  dual-compile pattern as scry-interval: it builds natively, to
+  `wasm32-unknown-unknown` (witness instruments it), and into the shipped
+  `wasm32-wasip2` component. The soundness-critical transfer functions now
+  run on pure types with no per-op WIT marshalling.
+- **`scry-analyzer` is now a thin canonical-ABI wrapper.** It keeps only
+  `struct Component`, the `Guest` impl, the field-by-field WIT⇄core
+  conversions (pure boilerplate, no analysis), and the `export!` macro;
+  `analyze()` delegates to `scry_analyze_core::analyze`. Its deps slim to
+  `scry-analyze-core`. `bazel build //:scry` and the host-test soundness
+  oracles stay green — the move is behaviour-identical.
+- **`crates/scry-mcdc` — witness MC/DC over the real analyzer.** A harness
+  whose 16 no-arg `run_*` exports drive `analyze()` over the corpus
+  fixtures (5 fixtures × config variants: taint on/off, diagnostics on/off,
+  widening 1 vs 3, plus an overflow fixture). `witness run --invoke-all`
+  accumulates per-branch counters across all executions so MC/DC
+  independence pairs exist. witness reconstructs **662 source-level
+  decisions** and proves **119 conditions under MC/DC** (4 full-MC/DC),
+  including conditions in the soundness-critical interval transfer
+  functions — versus **0** proved by the discarded synthetic-domain spike.
+- **`#[inline(never)]` on the scry-interval transfer functions** (per
+  DD-012) so each keeps a standalone DWARF decision cluster for witness's
+  reconstruction. The MC/DC predicate body (`witness-mcdc/v3`) is produced
+  by `witness predicate --kind mcdc` for sigil to sign at release; the
+  canonical truth table ships at `crates/scry-mcdc/evidence/report.json`.
+
+### Known limitations
+
+- MC/DC coverage is **partial-with-named-gaps**, not zero-gap. Some
+  transfer-fn straddle→TOP decisions remain `no_witness`/`gap` (a witness
+  multi-instance-attribution effect); each residual gap is named with its
+  closing approach in `crates/scry-mcdc/README.md` (FEAT-014 AC#1's
+  name-the-gap escape hatch). REQ-010 thus has initial structural-coverage
+  evidence; full closure is tracked for v1.2.x.
+
+### Falsification statement
+
+What v1.2 claims, made falsifiable: **the witness MC/DC pipeline runs over
+the analyzer's real decision logic and proves conditions inside the shipped
+soundness-critical transfer functions.** Falsifier: rebuild
+`crates/scry-mcdc` to `wasm32-wasip1` and run `witness instrument → run
+--invoke-all → report --format mcdc-json`; if `report.json` does not show
+proved (`full_mcdc`) conditions attributed to the interval transfer
+functions' source lines, the claim is false. What v1.2 does **not** claim:
+zero unresolved gap rows — the residual safety-relevant gaps are named, not
+proved closed.
+
 ## [1.1.0] — 2026-05-30
 
 Headline: **the shipped artifact is finally the real one.** v1.1 closes

Cargo.toml

@@ -27,6 +27,7 @@ members = [
     "crates/scry-taint",
     "crates/scry-octagon",
     "crates/scry-interval",
+    "crates/scry-analyze-core",
     "crates/scry-host-tests",
 ]
 

artifacts/roadmap-2.0.yaml

@@ -362,7 +362,7 @@ artifacts:
   - id: FEAT-014
     type: feature
     title: "v1.2 — witness MC/DC on the analyzer (closes the long-standing structural-coverage gap)"
-    status: proposed
+    status: implemented
     description: >
       With the analyzer executable (FEAT-013), measure modified-condition/
       decision coverage on its real decision logic with witness, driven by
@@ -395,6 +395,24 @@ artifacts:
       via `witness run --invoke-with-args`. Until that extraction lands,
       REQ-010 is NOT satisfied; this feature is the extraction + the
       corpus-driven MC/DC run together.
+
+      EVIDENCE (v1.2.0, implemented): the DD-012 extraction landed —
+      crates/scry-analyze-core is the pure bindgen-free core, scry-analyzer
+      is a thin canonical-ABI wrapper, and `bazel build //:scry` + the
+      host-test soundness oracles stay green (behaviour-identical move).
+      crates/scry-mcdc drives the REAL analyze() over the corpus fixtures
+      (16 no-arg run_* exports = fixture×config pairs; `witness run
+      --invoke-all` rather than --invoke-with-args, which sidesteps the
+      canonical-ABI list<u8> marshalling problem). witness reconstructs 662
+      source-level decisions and proves 119 conditions under MC/DC (4 full),
+      including conditions in the soundness-critical interval transfer
+      functions — the decisive break from the spike's 0-proved. AC#1 is met
+      via its name-the-gap escape hatch: residual transfer-fn straddle gaps
+      are NAMED in crates/scry-mcdc/README.md with their closing approach
+      (per-instance vectors / OR-guard split). AC#2: the signable in-toto
+      MC/DC predicate body (witness-mcdc/v3) is produced by `witness
+      predicate --kind mcdc`; sigil wraps+signs it at release time. The
+      canonical truth table ships at crates/scry-mcdc/evidence/report.json.
     tags: [reality, structural-coverage, mcdc, witness, v1.2]
     fields:
       phase: phase-2

crates/scry-analyze-core/BUILD.bazel

@@ -0,0 +1,36 @@
+load("@rules_rust//rust:defs.bzl", "rust_library", "rust_test")
+
+# scry-analyze-core — the pure, bindgen-free analyzer core (FEAT-014 /
+# DD-012): the wasmparser parse + interval/region fixpoint + call-graph /
+# SCC / summary machinery + taint walk, plus the plain-Rust result types
+# mirroring the analyzer's WIT. Extracted from scry-analyzer so the real
+# analyzer decisions can be instrumented for witness MC/DC (witness wants a
+# core module) and so the component becomes a thin canonical-ABI wrapper.
+#
+# Same dual-compile pattern as scry-interval / scry-taint / scry-provenance:
+# cross-compiled to wasm32-wasip2 (linked into the scry-analyzer component
+# so analyze() runs standalone) AND native (scry-host-tests + the witness
+# MC/DC harness drive it). Unlike those leaf crates it has deps, so they are
+# wired here; the component then depends only on this target.
+rust_library(
+    name = "scry_analyze_core",
+    srcs = ["src/lib.rs"],
+    crate_name = "scry_analyze_core",
+    edition = "2024",
+    visibility = ["//visibility:public"],
+    tags = ["feat-014"],
+    deps = [
+        "@scry_crates//:sha2",
+        "@scry_crates//:wasmparser",
+        "//crates/scry-interval:scry_interval",
+        "//crates/scry-provenance:scry_provenance",
+        "//crates/scry-taint:scry_taint",
+    ],
+)
+
+rust_test(
+    name = "scry_analyze_core_test",
+    crate = ":scry_analyze_core",
+    edition = "2024",
+    tags = ["feat-014"],
+)

crates/scry-analyze-core/Cargo.toml

@@ -0,0 +1,43 @@
+[package]
+name = "scry-analyze-core"
+description = "Pure, bindgen-free analyzer core for scry (FEAT-014 / DD-012): the wasmparser + fixpoint + transfer logic and its plain-Rust result types, extracted from scry-analyzer so the analyzer's real decisions can be instrumented for witness MC/DC and the component becomes a thin canonical-ABI wrapper."
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+repository.workspace = true
+authors.workspace = true
+
+# Pure library — same dual-compile pattern as scry-interval / scry-taint /
+# scry-octagon / scry-provenance: `#![no_std]` + `extern crate alloc`, no
+# wit-bindgen. It compiles natively (scry-host-tests + the witness MC/DC
+# harness drive it) AND to wasm32-unknown-unknown (a core module witness
+# instruments) AND, once the component wrapper lands, into the shipped
+# wasm32-wasip2 analyzer component. DD-012: this is the lever that makes
+# MC/DC land on the real shipped analyzer decisions, not a copy.
+#
+# Step 1 (this commit) defines the plain-Rust result-type surface mirroring
+# the analyzer's WIT (`crates/scry-analyzer/wit/scry.wit`). Later steps move
+# the analyze body + helpers here (adding wasmparser / sha2 / scry-taint /
+# scry-octagon / scry-provenance deps) and rewire the component as a thin
+# Guest wrapper that converts between these types and the WIT bindings.
+[lib]
+path = "src/lib.rs"
+
+[dependencies]
+# Interval + Region are field-identical to the WIT `interval` /
+# `region-pointer-payload`, so the core reuses the pure types directly
+# (the analyzer's region transfer ops then need no conversion).
+scry-interval = { path = "../scry-interval" }
+
+# Step 2 (DD-012): the analyze body + helpers moved here. wasmparser parses
+# the input Wasm Core Model module; sha2 digests the module bytes for
+# `invariant-bundle.module-sha256`. Both `default-features = false` (set in
+# the workspace dep table) so the crate stays `#![no_std]` and compiles to
+# wasm32-unknown-unknown / wasm32-wasip2.
+wasmparser = { workspace = true }
+sha2 = { workspace = true }
+
+# Security-label (taint) lattice for the noninterference analysis (FEAT-009)
+# and the pure meld<->scry provenance boundary crate (FEAT-002 / DD-002).
+scry-taint = { path = "../scry-taint" }
+scry-provenance = { path = "../scry-provenance" }