diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index e78eb14..b17f04f 100644 --- a/artifacts/requirements.yaml +++ b/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). diff --git a/artifacts/roadmap-2.0.yaml b/artifacts/roadmap-2.0.yaml index 75190c8..81b8732 100644 --- a/artifacts/roadmap-2.0.yaml +++ b/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