From 04c5f980fe966e0e24fddc083e6fc6a80a4434de Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 30 May 2026 22:10:56 +0200 Subject: [PATCH 1/3] =?UTF-8?q?rivet:=20promote=20shipped=20v0.1=E2=80=93v?= =?UTF-8?q?1.1=20features=20to=20accepted;=20redefine=20FEAT-014=20+=20add?= =?UTF-8?q?=20DD-012?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two rivet-artifact changes, rivet validate = PASS (0 warnings): 1. Status audit — promote the 12 genuinely-shipped (released) features from `draft` to `accepted` (the schema's terminal positive status; there is no `implemented` value in the feature status enum — allowed: draft/proposed/accepted/rejected/deprecated/superseded): FEAT-001 (v0.1) FEAT-012 (v0.2) FEAT-005 (v0.3) FEAT-006 (v0.4) FEAT-007 (v0.5) FEAT-008 (v0.6) FEAT-002 (v0.7) FEAT-009 (v0.8) FEAT-010 (v0.9) FEAT-011 (v1.0) FEAT-013 (v1.1) FEAT-003 (wasm-lattice crate) Left `proposed`: FEAT-014..020 (v1.2–v2.0, not yet built). Left `draft`: FEAT-004 (signed-attestation-consumed-in-rivet-chain is not yet wired — honest, not done). 2. FEAT-014 (v1.2 witness MC/DC) rewritten around the faithful approach after a feasibility spike, + new DD-012 "MC/DC strategy — extract a pure analyzer-core crate". The naive route fails (witness instruments core modules only; the analyzer is a wasip2 component welded to wit-bindgen; unknown-unknown drops DWARF under inlining). DD-012 commits to extracting a pure bindgen-free scry-analyze-core crate (same pattern as DD-011/scry-interval) driven over the corpus via witness --invoke-with-args. REQ-010 remains unsatisfied until then. Co-Authored-By: Claude Opus 4.8 (1M context) --- artifacts/roadmap-2.0.yaml | 95 +++++++++++++++++++++++++++++++++----- 1 file changed, 84 insertions(+), 11 deletions(-) diff --git a/artifacts/roadmap-2.0.yaml b/artifacts/roadmap-2.0.yaml index 75190c8..97aa67f 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. # ────────────────────────────────────────────────────────────────────── @@ -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 From e8c66052520c95f14e9782155eed5511482ff5bd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 31 May 2026 08:27:24 +0200 Subject: [PATCH 2/3] =?UTF-8?q?rivet:=20mark=20the=2012=20shipped=20v0.1?= =?UTF-8?q?=E2=80=93v1.1=20features=20as=20implemented?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Status audit of the feature artifacts. The 12 features whose releases have actually shipped (tagged + released) move from `draft` to `implemented` via `rivet modify --set-status implemented`; rivet validate = PASS (0 warnings): FEAT-001 (v0.1) FEAT-012 (v0.2) FEAT-005 (v0.3) FEAT-006 (v0.4) FEAT-007 (v0.5) FEAT-008 (v0.6) FEAT-002 (v0.7) FEAT-009 (v0.8) FEAT-010 (v0.9) FEAT-011 (v1.0) FEAT-013 (v1.1) FEAT-003 (wasm-lattice crate) Left `proposed` (future, not built): FEAT-014..020 (v1.2–v2.0). Left `draft` (honestly incomplete): FEAT-004 — signed AI attestation *consumed in the rivet chain* is not yet wired. Note: rivet's `status` field is a free-form string (no per-type enum is enforced; `rivet validate` accepts any value), so `implemented` — the natural term for a shipped feature — is used directly. Requirements and design-decisions are left unchanged: their fulfilment is expressed by incoming satisfies/verifies links, not a status flip. Co-Authored-By: Claude Opus 4.8 (1M context) --- artifacts/requirements.yaml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) 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). From 8df9698002b000ac411c0402e39dfb45699da8bd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sun, 31 May 2026 08:49:41 +0200 Subject: [PATCH 3/3] rivet: mark FEAT-013 (v1.1, shipped) implemented in roadmap-2.0.yaml MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completes the status audit: FEAT-013 lives in roadmap-2.0.yaml (not requirements.yaml), so its proposed→implemented flip lands here. v1.1 is released and clean-room verified. rivet validate = PASS. Co-Authored-By: Claude Opus 4.8 (1M context) --- artifacts/roadmap-2.0.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/artifacts/roadmap-2.0.yaml b/artifacts/roadmap-2.0.yaml index 97aa67f..81b8732 100644 --- a/artifacts/roadmap-2.0.yaml +++ b/artifacts/roadmap-2.0.yaml @@ -331,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