release: v3.2.5

CHANGELOG.md

@@ -7,6 +7,71 @@ Versioning: [SemVer 2.0](https://semver.org/spec/v2.0.0.html).
 
 ## [Unreleased]
 
+## [3.2.5] — 2026-08-21
+
+Issue-driven patch, cut ahead of v3.3.0. Both defects were reported by a user
+running the RELEASED 3.2.4 artifact over a 468-module real-world corpus — not
+found by the fixture suite. Both turned out to be a correct helper existing and
+the call site not using it.
+
+### Fixed — scry-sai-core
+
+- **`analyze` no longer panics on a branch to the function label** (#125,
+  FEAT-074). `Interp::target()` resolved a branch's label with
+  `saturating_sub` and then INDEXED; the label stack is pushed only on
+  *entering* a block/loop/if, so the function body's own implicit label is
+  never on it and `br 0` at function top level indexed an empty slice. A panic
+  inside the component traps the guest, so the host received neither arm of
+  `result<analysis-result, analyze-error>` — bypassing the interface's own
+  channel for "I could not analyse this". 2 of 281 analysed corpus modules hit
+  this deterministically.
+
+  The same line held a second defect: when the clamp did *not* panic it sent a
+  branch that exits the function into the OUTERMOST region's label, recording a
+  state that never arrives there. `checked_sub` fixes both — reaching past every
+  enclosing region means the function label, which is a return.
+
+  Verified before/after on the two spec-suite sources the reporter named: both
+  panicked before; after, `unwind.wast` analyses cleanly (49 functions, 100
+  program points) and `func.wast` returns a structured error. No precision or
+  soundness change on real code — the same 8.2 MB compiler-emitted module gives
+  identical results through both analyzers (8530 advisories, 6490 trap checks,
+  28 proven-safe, 6462 potential-trap).
+
+- **Every diagnostic that names an operator now names it** (#126, FEAT-075).
+  579 fallbacks in the corpus said only `<unsupported>` — the largest bucket,
+  larger than any named operator. `op_report_name()` already falls back to the
+  operator's Debug variant name and was already wired into the *gap* records;
+  the *diagnostics* used the lower-level `op_name()`, so the two surfaces
+  disagreed about the same event at the same pc. Fixed at both defective sites:
+  the interpreter's unsoundness fallback and the taint pass's "operator not
+  modelled" (whose trigger *is* an unmodelled operator, so it printed the
+  placeholder for exactly the population it describes).
+
+  Treated as a REQ-017 defect rather than a cosmetic one: "no silent ⊤" is not
+  met by a record that announces a degradation without identifying its cause,
+  and an unnameable fallback is *worse* than silence for an agent, which cannot
+  ask a follow-up question.
+
+  This NAMES the operators; it does not MODEL any of them. The operator ranking
+  behind #126 (nop/drop/unreachable, the bitwise/shift family, select) is
+  precision work for a later release.
+
+### Known issues
+
+- #128 — fixing the panic unmasked a pre-existing operand-stack defect in
+  `func.wast` that the crash was hiding: `Internal("i32 binop with single
+  operand")`. It takes the `analyze-error` channel correctly, so it is a defect
+  rather than a crash. Two hypotheses were tested and refuted, so its cause is
+  recorded as uncharacterised rather than guessed at.
+
+### Falsification
+
+This release is wrong if a module that analysed successfully under 3.2.4 now
+returns an error or a different verdict set. The A/B above tested exactly one
+module; a corpus-wide before/after would falsify it properly, and #126's
+reporter has offered to re-run theirs.
+
 ## [3.2.4] — 2026-07-15
 
 Fix (final page-size pass): after v3.2.3 the deployed `self-analysis.html` was

Cargo.toml

@@ -69,7 +69,7 @@ default-members = [
 # on crates.io matches the release artifacts. The crates.io publish workflow
 # asserts the pushed `v*` tag equals this version, so a release bump must move
 # both in lockstep (and the internal path-dep `version = "..."` fields below).
-version = "3.2.4"
+version = "3.2.5"
 edition = "2024"
 license = "MIT OR Apache-2.0"
 repository = "https://github.com/pulseengine/scry"

README.md

@@ -63,7 +63,7 @@ deductive-proof and bounded-model-checking layers do not staff.
 <!-- claim id=version: "scry-sai-core" crates.io max_version == workspace version -->
 <!-- claim id=crates: publish.rs lists 12 scry-sai-* crates -->
 <!-- claim id=admit-free: 0 Admitted/admit/Axiom across proofs/rocq/*.v -->
-**v3.2.4 shipped** — the full v0.1 → v3.2 arc is done; scry is a working **sound
+**v3.2.5 shipped** — the full v0.1 → v3.2 arc is done; scry is a working **sound
 abstract interpreter**, not a scaffold. Shipped and on crates.io: **12 pure
 `scry-sai-*` crates** (10 abstract domains — interval, region-memory, call-graph
 + reachability, octagon, pentagon, known-bits/congruence, IEEE-754 float,

claims.yaml

@@ -21,10 +21,10 @@ claims:
   # Cargo.toml + this pattern together — exactly the point.)
   - id: STATUS-VERSION
     doc: README.md
-    text: "**v3.2.4 shipped**"
+    text: "**v3.2.5 shipped**"
     evidence:
       - kind: count-min
-        pattern: 'version = "3\.2\.4"'
+        pattern: 'version = "3\.2\.5"'
         glob: ['Cargo.toml']
         min: 1
 

crates/scry-analyze-core/Cargo.toml

@@ -31,7 +31,7 @@ path = "src/lib.rs"
 # Path deps carry `version` so `cargo publish` rewrites them to the crates.io
 # coordinate (crates.io rejects path-only deps). The version equals the
 # workspace version and must be bumped in lockstep with it.
-scry-sai-interval = { path = "../scry-interval", version = "3.2.4" }
+scry-sai-interval = { path = "../scry-interval", version = "3.2.5" }
 
 # Step 2 (DD-012): the analyze body + helpers moved here. wasmparser parses
 # the input Wasm Core Model module; sha2 digests the module bytes for
@@ -43,44 +43,44 @@ 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-sai-taint = { path = "../scry-taint", version = "3.2.4" }
-scry-sai-provenance = { path = "../scry-provenance", version = "3.2.4" }
+scry-sai-taint = { path = "../scry-taint", version = "3.2.5" }
+scry-sai-provenance = { path = "../scry-provenance", version = "3.2.5" }
 
 # Octagon relational domain (FEAT-016 slice-2b-ii): carried alongside the
 # intervals through the structured-CFG fixpoint so a loop counter bounded by a
 # VARIABLE relation (`i < n`) stays bounded where the interval domain alone
 # widens it to ⊤. Same pure `#![no_std]` dual-compile crate as scry-interval.
-scry-sai-octagon = { path = "../scry-octagon", version = "3.2.4" }
+scry-sai-octagon = { path = "../scry-octagon", version = "3.2.5" }
 
 # Known-bits × interval-guarded congruence reduced product (FEAT-037 / DD-017):
 # an additive bit/alignment/stride companion computed in a straight-line-sound
 # pass, surfaced library-only on `AnalysisResult.bit_facts`. Same pure
 # `#![no_std]` dual-compile crate as the other domains.
-scry-sai-bits = { path = "../scry-bits", version = "3.2.4" }
+scry-sai-bits = { path = "../scry-bits", version = "3.2.5" }
 
 # Pentagons weakly-relational domain (FEAT-044 / AC-014): intervals + strict
 # `x < y` facts, the cheap relational layer behind sound out-of-bounds-trap
 # detection (FEAT-046). An additive guard-recording pass surfaces proven
 # strict relations library-only on `AnalysisResult.pentagon_facts`. Same pure
 # `#![no_std]` dual-compile crate as the other domains.
-scry-sai-pentagon = { path = "../scry-pentagon", version = "3.2.4" }
+scry-sai-pentagon = { path = "../scry-pentagon", version = "3.2.5" }
 
 # IEEE-754 float-interval domain (FEAT-047 / AC-022): sound f32/f64 abstraction
 # with NaN/±inf tracking + round-to-nearest-aware widening. An additive
 # straight-line pass surfaces sound float intervals library-only on
 # `AnalysisResult.float_facts`. Same pure `#![no_std]` dual-compile crate.
-scry-sai-float = { path = "../scry-float", version = "3.2.4" }
+scry-sai-float = { path = "../scry-float", version = "3.2.5" }
 
 # Affine Component-Model handle-state lattice (FEAT-049 / MF-007): tracks
 # own/borrow resource-handle state to flag use-after-drop / double-drop. A
 # straight-line pass over the canonical-ABI `[resource-drop]` call sites
 # surfaces findings library-only on `AnalysisResult.handle_findings`.
-scry-sai-handle = { path = "../scry-handle", version = "3.2.4" }
+scry-sai-handle = { path = "../scry-handle", version = "3.2.5" }
 
 # FEAT-058: the linear-memory segmentation domain (content-sensitive memory).
 # The interpreter tracks per-offset interval content for i32 loads/stores
 # instead of degrading every load to ⊤.
-scry-sai-segment = { path = "../scry-segment", version = "3.2.4" }
+scry-sai-segment = { path = "../scry-segment", version = "3.2.5" }
 
 [dev-dependencies]
 # Test-only (the crate is otherwise dep-light + no_std): assemble the .wat

crates/scry-segment/Cargo.toml

@@ -20,4 +20,4 @@ path = "src/lib.rs"
 # The per-segment content domain. Path dep carries `version` so `cargo publish`
 # rewrites it to the crates.io coordinate; the version equals the workspace
 # version and is bumped in lockstep.
-scry-sai-interval = { path = "../scry-interval", version = "3.2.4" }
+scry-sai-interval = { path = "../scry-interval", version = "3.2.5" }

crates/scry-viz/Cargo.toml

@@ -22,7 +22,7 @@ path = "src/main.rs"
 # The only dependency: the published analyzer library. scry-viz is a plain
 # `std` host tool, so it can read the `AnalysisResult` plain-Rust types and
 # render them — no WIT, no component, no wasmtime.
-scry-sai-core = { path = "../scry-analyze-core", version = "3.2.4" }
+scry-sai-core = { path = "../scry-analyze-core", version = "3.2.5" }
 # Assemble `.wat` inputs to module bytes (so the CLI accepts both .wat and
 # .wasm); host-only, same dep the test harness uses.
 wat = { workspace = true }