rivet: promote shipped v0.1–v1.1 features to accepted; FEAT-014 redefine + DD-012

artifacts/requirements.yaml

@@ -177,7 +177,7 @@ artifacts:
   - id: FEAT-001
     type: feature
     title: Sound abstract-interpretation pass for the Wasm Core Model (v0.1 — Wasm component dogfood)
-    status: draft
+    status: implemented
     description: >
       The scry analyzer, shipping as a wasm32-wasip2 Component Model
       component (per DD-008). Exports the `analyzer.analyze` function
@@ -240,7 +240,7 @@ artifacts:
   - id: FEAT-002
     type: feature
     title: Component-Model AI extension — handles, capability flow, host effects
-    status: draft
+    status: implemented
     description: >
       A second-phase extension lifting the AI to the Wasm Component
       Model. Per DD-002, the analysis runs on the original component
@@ -301,7 +301,7 @@ artifacts:
   - id: FEAT-003
     type: feature
     title: Reusable wasm-lattice crate
-    status: draft
+    status: implemented
     description: >
       A standalone Rust crate providing the abstract domain library
       (interval, octagon, region-memory, reachability, taint, capability,
@@ -347,7 +347,7 @@ artifacts:
   - id: FEAT-012
     type: feature
     title: "v0.2 — Wire rules_verus + rules_rocq_rust into the Bazel build"
-    status: proposed
+    status: implemented
     description: >
       Add the PulseEngine-canonical proof toolchains to scry's Bazel
       workspace alongside `rules_wasm_component`. Mirrors the
@@ -385,7 +385,7 @@ artifacts:
   - id: FEAT-005
     type: feature
     title: "v0.3 — Region-based linear-memory model (CRAB-style)"
-    status: draft
+    status: implemented
     description: >
       Add a region-based memory abstraction to the wasm-lattice
       component and use it from scry-analyzer. Wasm linear memory is
@@ -439,7 +439,7 @@ artifacts:
   - id: FEAT-006
     type: feature
     title: "v0.4 — Sound call_indirect resolution (value-domain call graph)"
-    status: draft
+    status: implemented
     description: >
       Implement the Paccamiccio et al. 2024 technique (AC-008): track
       the operand stack with the interval domain (collapsing to a
@@ -495,7 +495,7 @@ artifacts:
   - id: FEAT-007
     type: feature
     title: "v0.5 — Compositional summary-based interprocedural AI"
-    status: draft
+    status: implemented
     description: >
       Implement per-function abstract summaries in the Stiévenart-De
       Roover 2020 style (AC-010): each function gets a summary
@@ -557,7 +557,7 @@ artifacts:
   - id: FEAT-008
     type: feature
     title: "v0.6 — loom contract: published invariant JSON schema (v1)"
-    status: draft
+    status: implemented
     description: >
       Publish a stable, versioned JSON schema (v1) for scry's per-
       instruction and per-function abstract invariants so the loom
@@ -612,7 +612,7 @@ artifacts:
   - id: FEAT-009
     type: feature
     title: "v0.8 — Taint / noninterference domain (Wanilla-class)"
-    status: draft
+    status: implemented
     description: >
       Add a security-label lattice (Low ⊑ High) lifted pointwise over
       values and memory; lift to a relational analysis sufficient for
@@ -676,7 +676,7 @@ artifacts:
   - id: FEAT-010
     type: feature
     title: "v0.9 — Octagon domain + mechanized soundness for interval domain"
-    status: draft
+    status: implemented
     description: >
       Add the octagon abstract domain (Miné HOSC 2006, AC-011) for
       relational reasoning over Wasm memory offsets and call-table
@@ -758,7 +758,7 @@ artifacts:
   - id: FEAT-011
     type: feature
     title: "v1.0 — Six-domain credit dossier + SpecTec backend prototype"
-    status: draft
+    status: implemented
     description: >
       The v1.0 capstone, in three legs, closing the top-level safety
       goal G-001 (all three DO-333 technique classes staffed).

artifacts/roadmap-2.0.yaml

@@ -216,6 +216,57 @@ artifacts:
       - type: traces-to
         target: FEAT-013
 
+  - id: DD-012
+    type: design-decision
+    title: "MC/DC strategy — extract a pure analyzer-core crate to make the real decisions instrumentable"
+    status: accepted
+    description: >
+      Structural (MC/DC) coverage of the analyzer (REQ-010, FEAT-014) must
+      be measured on the analyzer's REAL decision logic, driven by the real
+      corpus, not on a proxy. A v1.2 feasibility spike established the
+      constraints: (1) witness instruments core Wasm MODULES only and
+      rejects wasip2 components; (2) the shipped analyzer is a component
+      whose analyze() is reachable only via the canonical ABI; (3) the
+      analyzer's decision logic is welded to wit-bindgen (types from
+      scry_analyzer_component_bindings, entry is a `Guest` impl), so it does
+      not compile to a plain core module as-is; (4) at opt-level>=1 the
+      wasm32-unknown-unknown linker drops DWARF line rows for inlined
+      functions, which defeats witness's decision reconstruction. A
+      throwaway harness instrumenting the pure scry-interval crate with
+      synthetic inputs was built and rejected as measuring domain arithmetic
+      in isolation rather than the analyzer over the corpus.
+    fields:
+      decision: >
+        Extract the analyzer's wasmparser + fixpoint + transfer logic into a
+        pure, bindgen-free `scry-analyze-core` crate (the same pure-crate
+        pattern DD-011 used for scry-interval), leaving the component as a
+        thin canonical-ABI wrapper over it. Build the core to wasm32-wasip1
+        with debug=2 and #[inline(never)] on measured decisions so DWARF
+        line rows survive, then drive its analyze() over the corpus fixtures
+        via `witness run --invoke-with-args`.
+      rationale: >
+        Same lever as DD-011: a pure no_std core crate is both the shipped
+        execution path (the component wraps it) and the verifiable artifact
+        (witness instruments it, host tests falsify it). It makes the MC/DC
+        evidence land on shipped code, not a copy, and keeps the component a
+        thin marshalling shell.
+      alternatives: >
+        (a) instrument the pure domain crates with synthetic inputs
+            (prototyped, rejected — not the analyzer, not the corpus);
+        (b) teach witness to instrument components / unbundle then drive
+            analyze() through a bespoke canonical-ABI wasmtime harness
+            (high wiring cost, measures marshalling noise alongside logic);
+        (c) extract analyzer-core (chosen) — the honest, reusable shape.
+    links:
+      - type: satisfies
+        target: REQ-010
+      - type: traces-to
+        target: REQ-009
+      - type: traces-to
+        target: DD-011
+      - type: traces-to
+        target: FEAT-014
+
   # ──────────────────────────────────────────────────────────────────────
   # Requirements added for the 2.0 line.
   # ──────────────────────────────────────────────────────────────────────
@@ -280,7 +331,7 @@ artifacts:
   - id: FEAT-013
     type: feature
     title: "v1.1 — Composition-gap fix: shipped artifact embeds and runs the analyzer"
-    status: proposed
+    status: implemented
     description: >
       Resolve DD-011: make the distributable scry artifact contain the
       analyzer and execute end-to-end. Audit why wac_compose //:scry does
@@ -314,27 +365,49 @@ artifacts:
     status: proposed
     description: >
       With the analyzer executable (FEAT-013), measure modified-condition/
-      decision coverage on it with witness: instrument the analyzer Wasm,
-      drive it with the existing scry-host-tests fixtures as a
-      witness harness (witness's --harness subprocess mode, or its
-      embedded wasmtime runner), and emit the MC/DC truth-table report +
-      a signed coverage predicate consumed by rivet. This finally
-      discharges the structural-coverage requirement (REQ-010) and closes
-      the witness step of the original feature loop that has been blocked
-      since v0.1 by the composition gap. Gap rows in the truth table drive
-      new analyzer unit tests until the safety-relevant transfer-function
-      decisions are proved.
+      decision coverage on its real decision logic with witness, driven by
+      the existing scry-host-tests corpus fixtures, and emit the MC/DC
+      truth-table report + a signed coverage predicate consumed by rivet.
+      This discharges the structural-coverage requirement (REQ-010) and
+      closes the witness step of the original feature loop, blocked since
+      v0.1 by the composition gap. Gap rows in the truth table drive new
+      analyzer test inputs until the safety-relevant transfer-function and
+      fixpoint decisions are proved (or each residual gap is named with its
+      closing row vector).
+
+      SCOPE NOTE (2026-05-30, from a v1.2 feasibility spike — see DD-012):
+      a naive route fails. witness instruments CORE modules only, but the
+      analyzer ships as a wasip2 COMPONENT whose analyze() is reachable only
+      through the canonical ABI; and the analyzer's decision logic is welded
+      to the wit-bindgen layer (its types come from
+      scry_analyzer_component_bindings; the entry is a `Guest` impl). A
+      one-off harness that instruments the pure scry-interval crate with
+      synthetic inputs was prototyped and DISCARDED: it measures the domain
+      arithmetic in isolation, not "the analyzer over the corpus", so it
+      does not honestly satisfy this AC. The faithful route (DD-012) is to
+      extract the analyzer's wasmparser+fixpoint+transfer logic into a pure,
+      bindgen-free `scry-analyze-core` crate (the same pure-crate pattern as
+      FEAT-013's scry-interval), make the component a thin canonical-ABI
+      wrapper over it, build that core to wasm32-wasip1 with debug=2 and
+      #[inline(never)] on measured decisions (so DWARF line rows survive for
+      witness's decision reconstruction — the unknown-unknown linker drops
+      them under inlining), and drive its analyze() over the corpus fixtures
+      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.
     tags: [reality, structural-coverage, mcdc, witness, v1.2]
     fields:
       phase: phase-2
       acceptance-criteria:
-        - "Given the executable analyzer Wasm and the host-test fixtures as a harness, When witness runs, Then it emits an MC/DC truth table over the analyzer's decisions with zero unresolved gap rows on the safety-relevant transfer functions (or each remaining gap is named with its closing row vector)."
+        - "Given the analyzer's decision logic extracted into a pure core crate built as an instrumentable core module, and the host-test corpus fixtures as inputs, When witness runs, Then it emits an MC/DC truth table over the analyzer's real decisions with zero unresolved gap rows on the safety-relevant transfer functions (or each remaining gap is named with its closing row vector)."
         - "Given the witness run, When it completes, Then a signed coverage predicate is produced and validated by rivet as requirement-to-test evidence for REQ-010."
     links:
       - type: satisfies
         target: REQ-010
       - type: depends-on
         target: FEAT-013
+      - type: depends-on
+        target: DD-012
 
   - id: FEAT-015
     type: feature