From 2eb59a1287c040a4d481294522cd6aec0b180fe8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 21 Aug 2026 14:17:01 +0200 Subject: [PATCH 1/2] =?UTF-8?q?rivet:=20promote=20FEAT-074/075=20to=20acce?= =?UTF-8?q?pted=20=E2=80=94=20v3.2.5=20is=20cuttable?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both features' acceptance criteria are met and verified on main, not merely implemented: FEAT-074 (#125) — measured before/after on the reporter's own sources. Both spec modules PANICKED at the pre-fix commit; after the fix unwind.wast analyses cleanly (49 functions, 100 program points) and func.wast returns a structured error instead of trapping the guest. FEAT-075 (#126) — mutation-checked: reverting the one-word change reproduces the reporter's exact string, so the oracle tests the fix and not the fixture. Both regression oracles were written RED FIRST and both reproduced the reported symptom before the fix existed. All 11 CI checks green on #127. `accepted` rather than `implemented`, per the release-gate semantics tested in rivet 0.22: `accepted` is cuttable, `implemented` means NOT yet verified. rivet release status v3.2.5: Cuttable. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc --- artifacts/roadmap-3.0.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index 881b529..570eb0f 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -1385,7 +1385,7 @@ artifacts: - id: FEAT-074 type: feature title: "v3.2.5 — A branch to the function label must not panic (scry#125)" - status: proposed + status: accepted release: v3.2.5 description: > `analyze` PANICKED with "index out of bounds: the len is 0 but the index @@ -1446,7 +1446,7 @@ artifacts: - id: FEAT-075 type: feature title: "v3.2.5 — Every unsoundness fallback names its operator (scry#126)" - status: proposed + status: accepted release: v3.2.5 description: > In avrabe's real-world corpus run (scry#126) the LARGEST bucket of From d554f5b2586b47621b26c4c67cff2eab2a8a312d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 21 Aug 2026 14:20:01 +0200 Subject: [PATCH 2/2] FEAT-075: fix the SECOND site, and measure FEAT-074's AC#3 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two gaps closed after review, both of the "asserted rather than measured" kind. 1. A SECOND defective op_name site. After fixing the interpreter's fallback I grepped every `op_name` call site instead of assuming the reported one was the only one. The taint pass has its own "operator not modelled" diagnostic whose TRIGGER is an unmodelled operator — so it printed `` for precisely the population it exists to describe: "taint: operator not modelled — taint state conservatively raised to High (sound, FEAT-009)" Same one-word fix, own red-first test. A third site (the write-set-havoc Info at a region opener) is SAFE and was left alone: `op_name` does cover `block`/`loop`/`if`, so it never reaches the placeholder. FEAT-075's AC is widened from "its unsoundness-fallback diagnostic" to ANY diagnostic naming an operator, since the original wording would have let this site through. 2. FEAT-074's AC#3 said a precision or soundness regression "must be excluded rather than assumed" — and then I promoted on a green unit suite, which is exactly the assumption the AC forbids. `checked_sub` changed behaviour for every branch whose depth reaches past its enclosing regions, and small fixtures are where that would NOT show. Measured properly: the same 8.2 MB compiler-emitted module through the pre-fix and post-fix analyzer. Identical — 8530 advisories, 6490 trap checks, 28 proven-safe, 6462 potential-trap, same class breakdown. Note this needed a different experiment than the self-history harness, which varies the MODULE; the question here was whether the ANALYZER change moved results, so the module had to be held fixed and the binary varied. 105 core tests pass; clippy -D warnings clean; rivet validate PASS. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc --- artifacts/roadmap-3.0.yaml | 4 +-- crates/scry-analyze-core/src/lib.rs | 49 ++++++++++++++++++++++++++++- 2 files changed, 50 insertions(+), 3 deletions(-) diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index 570eb0f..0769ab1 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -1427,7 +1427,7 @@ artifacts: acceptance-criteria: - "Given a module whose function branches to the function label (`br 0` / `br_if 0` at top level, or `br 1` out of a single block), When analyze runs, Then it returns normally instead of panicking." - "Given the two spec-suite sources the reporter named — test/core/func.wast and test/core/unwind.wast — When their first modules are analysed, Then neither traps. MEASURED before/after on the real sources: both PANICKED at HEAD; after the fix unwind.wast analyses cleanly (49 functions, 100 program points) and func.wast returns a STRUCTURED Internal error rather than a trap." - - "Given the fix, When the existing suite runs, Then no analyzer test regresses — the change alters which label a function-exiting branch records into, so a silent precision or soundness regression must be excluded rather than assumed." + - "Given the fix, When the existing suite runs, Then no analyzer test regresses — the change alters which label a function-exiting branch records into, so a silent precision or soundness regression must be excluded rather than assumed. MEASURED, because a unit suite of small fixtures is exactly where this would NOT show: the same 8.2 MB compiler-emitted module was analysed by the pre-fix and post-fix analyzer and the results are identical — 8530 advisories, 6490 trap checks, 28 proven-safe, 6462 potential-trap, and the same class breakdown (6463 unproven-obligation / 2039 precision-gap / 28 leverageable-fact). The AC is met on real code, not merely un-contradicted by fixtures." - "REGRESSION ORACLE, written RED FIRST: issue125_branch_to_the_function_label_does_not_panic reproduced the reporter's exact message (`index out of bounds: the len is 0 but the index is 0`) at the same site from a one-line module BEFORE the fix, and covers every branch form that resolves a label — a fix guarding only `br` would leave `br_if` live." residual: > Fixing the panic UNMASKED a separate, pre-existing defect that the crash @@ -1474,7 +1474,7 @@ artifacts: fields: phase: phase-3 acceptance-criteria: - - "Given a module containing an unmodelled operator, When analysis emits its unsoundness-fallback diagnostic, Then the message names the operator and never contains the literal ``." + - "Given a module containing an unmodelled operator, When analysis emits ANY diagnostic naming that operator, Then the message names it and never contains the literal ``. Scoped to ALL sites, not just the reported one: after fixing the interpreter's fallback, every `op_name` call site was grepped rather than assumed. A SECOND defective site was found — the taint pass has its own 'operator not modelled' diagnostic whose TRIGGER is an unmodelled operator, so it printed the placeholder for exactly the population it describes. A third site (the write-set-havoc Info) is safe, because `op_name` does cover `block`/`loop`/`if`." - "Given the same site, When a consumer correlates the diagnostic with the gap record, Then both name the SAME operator — the surfaces may not disagree about one event." - "MUTATION-CHECKED: reverting the one-word change reproduces the reporter's exact string, `unsupported operator at v0.2 AC#1: — locals degraded to top`, so the oracle is known to test the fix rather than the fixture." - "NON-VACUITY, learned the hard way: the first version of this test used AnalysisConfig::default(), where emit_diagnostics is FALSE, so it asserted on an empty diagnostic set and would have passed against no fix at all. The second version asserted on the wrong operator — `f64.const` is itself unmodelled and takes the fallback first, and only ONE fallback fires per function. The fixture now makes the operator under test the only unmodelled one." diff --git a/crates/scry-analyze-core/src/lib.rs b/crates/scry-analyze-core/src/lib.rs index 79179c2..dad3726 100644 --- a/crates/scry-analyze-core/src/lib.rs +++ b/crates/scry-analyze-core/src/lib.rs @@ -7023,9 +7023,13 @@ fn run_taint_analysis( func_index: func.abs_index, pc, message: format!( + // scry#126: `op_report_name`, NOT `op_name` — this + // diagnostic's TRIGGER is an unmodelled operator, so + // `op_name`'s `` fallback fired for + // exactly the population it exists to describe. "taint: operator {} not modelled — taint state conservatively \ raised to High (sound, FEAT-009)", - op_name(op) + op_report_name(op) ), }); } @@ -8918,6 +8922,49 @@ mod tests { ); } + /// scry#126, second site. The taint pass has its OWN "operator not + /// modelled" diagnostic, and it formatted `op_name` too — so it printed + /// `` for exactly the population it exists to describe. + /// + /// Found by grepping every `op_name` call site after fixing the first one, + /// rather than assuming the first was the only one. A third site (the + /// write-set-havoc Info at the `block`/`loop`/`if` opener) is safe, because + /// `op_name` does cover those three. + #[test] + fn issue126_taint_fallback_diagnostic_also_names_the_operator() { + let r = analyze( + wat::parse_str( + "(module (func (param f64) (result f64) local.get 0 local.get 0 f64.add))", + ) + .expect("assemble"), + AnalysisConfig { + emit_diagnostics: true, + taint_policy: Some(TaintPolicy { + high_params: alloc::vec![0], + low_results: alloc::vec![0], + }), + ..Default::default() + }, + ) + .expect("analyze"); + let taint: Vec<&Diagnostic> = r + .diagnostics + .iter() + .filter(|d| d.message.starts_with("taint: operator")) + .collect(); + assert!( + !taint.is_empty(), + "the taint pass must report the unmodelled f64.add" + ); + for d in &taint { + assert!( + !d.message.contains(""), + "the taint fallback must name its operator: {:?}", + d.message + ); + } + } + fn analyze_default(src: &str) -> AnalysisResult { analyze( wat::parse_str(src).expect("assemble"),