From 6905bad930118787238dad8b2ab47f9100394b3a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 15 Jul 2026 05:11:31 +0200 Subject: [PATCH] =?UTF-8?q?release:=20v3.2.2=20=E2=80=94=20readable=20dash?= =?UTF-8?q?board=20redesign=20(FEAT-063)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Version 3.2.1 → 3.2.2 (workspace + SCRY_VERSION + Cargo.lock). CHANGELOG 3.2.2. FEAT-063 (accepted, release v3.2.2): the scry-viz dashboard redesign from the four-persona review — capped program points (18.8 MB → <1 MB), collapsed guidance boilerplate, structured guidance.json feed, retitle + honest Scope & limitations block. No analyzer change. rivet release status v3.2.2 = ✓ Cuttable. Co-Authored-By: Claude Opus 4.8 --- CHANGELOG.md | 38 ++++++++++++++++++++++++++++ Cargo.lock | 30 +++++++++++----------- Cargo.toml | 2 +- artifacts/roadmap-3.0.yaml | 39 +++++++++++++++++++++++++++++ crates/scry-analyze-core/Cargo.toml | 18 ++++++------- crates/scry-analyze-core/src/lib.rs | 2 +- crates/scry-segment/Cargo.toml | 2 +- crates/scry-viz/Cargo.toml | 2 +- 8 files changed, 105 insertions(+), 28 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ab8b124..5845721 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,44 @@ Versioning: [SemVer 2.0](https://semver.org/spec/v2.0.0.html). ## [Unreleased] +## [3.2.2] — 2026-07-15 + +Headline: **make the dashboard readable.** A four-persona review of the deployed +GitHub Pages dashboard (assessor, AI-agent, skeptic, first-time engineer) found +it unusable — an 18.8 MB self-analysis page, an inverted pyramid, no structured +feed, and no legible scope. This release fixes the `scry-viz` output. No analyzer +change. + +### Changed — scry-viz dashboard + +- **Capped the Program points section** — was ~90% of the page bytes (the 18.8 MB + culprit). Each function now shows a summary + the first 20 points + a pointer to + the JSON feed; the whole HTML stays well under 1 MB (test-enforced). +- **Collapsed the Guidance boilerplate** — every DefiniteFault in full (proven + bugs are never elided), other classes capped with a "… and N more" pointer, so + the real fixes no longer drown under thousands of identical rows. +- **Retitled** from "verification dashboard" to **"scry — a sound static analyzer + for WebAssembly"**, with a lead that states what it catches and the soundness + caveat: **⊤ / POTENTIAL-TRAP mean "unknown", never "safe".** +- **New Scope & limitations block** — the mechanized-vs-γ-sweep-validated evidence + distinction, and what scry does NOT prove (no WasmCert-Coq import yet; + official-semantics proof covers `i32.add` only; memory content singleton-i32 + only; not a qualified tool — no TQL/TCL claim). + +### Added — structured guidance feed + +- **`scry-viz::render_guidance_json`** + a `.guidance.json` written alongside + the HTML (and emitted + sanity-checked in `release.yml`): the full, un-capped + advisories + trap verdicts as machine-consumable JSON — the structured-primary + feed an AI agent should consume instead of scraping HTML. + +### Notes + +- FEAT-057 slice-2 reframed (rivet): a straight-line polyhedra pass is near-vacuous + over Wasm's wrapping i32 (general-coefficient facts need no-wrap → bounds → + guards → the fixpoint), so the polyhedra body is scoped to a fixpoint-integration + arc, tracked honestly rather than shipped vacuous. + ## [3.2.1] — 2026-07-11 Headline: **make the new memory tracking visible.** FEAT-062 surfaces FEAT-058's diff --git a/Cargo.lock b/Cargo.lock index 34f225b..809118e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1834,7 +1834,7 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "scry-host-tests" -version = "3.2.1" +version = "3.2.2" dependencies = [ "anyhow", "jsonschema", @@ -1851,18 +1851,18 @@ dependencies = [ [[package]] name = "scry-sai-analyzer" -version = "3.2.1" +version = "3.2.2" dependencies = [ "scry-sai-core", ] [[package]] name = "scry-sai-bits" -version = "3.2.1" +version = "3.2.2" [[package]] name = "scry-sai-core" -version = "3.2.1" +version = "3.2.2" dependencies = [ "scry-sai-bits", "scry-sai-float", @@ -1880,19 +1880,19 @@ dependencies = [ [[package]] name = "scry-sai-float" -version = "3.2.1" +version = "3.2.2" [[package]] name = "scry-sai-handle" -version = "3.2.1" +version = "3.2.2" [[package]] name = "scry-sai-interval" -version = "3.2.1" +version = "3.2.2" [[package]] name = "scry-sai-lattice" -version = "3.2.1" +version = "3.2.2" dependencies = [ "bitflags", "scry-sai-octagon", @@ -1901,34 +1901,34 @@ dependencies = [ [[package]] name = "scry-sai-octagon" -version = "3.2.1" +version = "3.2.2" [[package]] name = "scry-sai-pentagon" -version = "3.2.1" +version = "3.2.2" [[package]] name = "scry-sai-poly" -version = "3.2.1" +version = "3.2.2" [[package]] name = "scry-sai-provenance" -version = "3.2.1" +version = "3.2.2" [[package]] name = "scry-sai-segment" -version = "3.2.1" +version = "3.2.2" dependencies = [ "scry-sai-interval", ] [[package]] name = "scry-sai-taint" -version = "3.2.1" +version = "3.2.2" [[package]] name = "scry-sai-viz" -version = "3.2.1" +version = "3.2.2" dependencies = [ "cpp_demangle 0.5.1", "rustc-demangle", diff --git a/Cargo.toml b/Cargo.toml index 55f742e..302c2a3 100644 --- a/Cargo.toml +++ b/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.1" +version = "3.2.2" edition = "2024" license = "MIT OR Apache-2.0" repository = "https://github.com/pulseengine/scry" diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index 13a18aa..a77370f 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -829,3 +829,42 @@ artifacts: target: REQ-013 - type: traces-to target: REQ-019 + + # ── Dashboard usability (four-persona review) ───────────────────────── + + - id: FEAT-063 + type: feature + title: "v3.2.2 — Readable dashboard redesign + structured guidance feed" + status: accepted + release: v3.2.2 + description: > + A four-persona review of the deployed Pages dashboard (DO-178C assessor, + AI-agent consumer, skeptical Wasm academic, first-time engineer) found it + unusable: an 18.8 MB self-analysis page (the un-capped program-points dump + was ~90% of the bytes), an inverted pyramid (thin landing, bottomless + dump), no structured/machine-consumable feed, and no legible soundness + scope. This redesigns the scry-viz OUTPUT (no analyzer change): + - cap the program-points section (summary + first N per function + a + pointer to the JSON feed) so the HTML stays < 1 MB; + - collapse the guidance boilerplate (every DefiniteFault in full; other + classes capped) so real fixes are not drowned; + - emit a structured `guidance.json` (advisories + trap verdicts, full/ + un-capped) alongside the HTML — the structured-primary feed (TE-011) + an AI agent consumes instead of scraping HTML; + - retitle to a precise scoped claim + a Scope & limitations block making + the mechanized-vs-γ-swept evidence distinction and the honest + not-proven list legible (skeptic + assessor asks). + tags: [viz, dashboard, observability, ai-agent, ux, v3.2] + fields: + phase: phase-3 + acceptance-criteria: + - "Given scry's self-analysis, When scry-viz renders it, Then the HTML stays under 1 MB (program points capped) instead of the 18.8 MB dump. (Shipped: points_section_is_capped_and_page_stays_small.)" + - "Given the AnalysisResult, When scry-viz emits the guidance feed, Then a well-formed guidance.json carries the full advisories + trap verdicts for machine consumption. (Shipped: guidance_json_is_well_formed_and_carries_advisories.)" + - "Given the dashboard, When a reader loads it, Then it states scry is a SOUND analyzer (⊤ = unknown, never safe) and distinguishes mechanized from γ-sweep-validated evidence. (Shipped: hero_and_scope_copy_finalized.)" + links: + - type: traces-to + target: REQ-013 + - type: traces-to + target: REQ-017 + - type: evaluates-tech + target: TE-011 diff --git a/crates/scry-analyze-core/Cargo.toml b/crates/scry-analyze-core/Cargo.toml index 7e4cb8a..e6d88dc 100644 --- a/crates/scry-analyze-core/Cargo.toml +++ b/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.1" } +scry-sai-interval = { path = "../scry-interval", version = "3.2.2" } # 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.1" } -scry-sai-provenance = { path = "../scry-provenance", version = "3.2.1" } +scry-sai-taint = { path = "../scry-taint", version = "3.2.2" } +scry-sai-provenance = { path = "../scry-provenance", version = "3.2.2" } # 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.1" } +scry-sai-octagon = { path = "../scry-octagon", version = "3.2.2" } # 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.1" } +scry-sai-bits = { path = "../scry-bits", version = "3.2.2" } # 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.1" } +scry-sai-pentagon = { path = "../scry-pentagon", version = "3.2.2" } # 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.1" } +scry-sai-float = { path = "../scry-float", version = "3.2.2" } # 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.1" } +scry-sai-handle = { path = "../scry-handle", version = "3.2.2" } # 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.1" } +scry-sai-segment = { path = "../scry-segment", version = "3.2.2" } [dev-dependencies] # Test-only (the crate is otherwise dep-light + no_std): assemble the .wat diff --git a/crates/scry-analyze-core/src/lib.rs b/crates/scry-analyze-core/src/lib.rs index 68cac25..2fe9229 100644 --- a/crates/scry-analyze-core/src/lib.rs +++ b/crates/scry-analyze-core/src/lib.rs @@ -856,7 +856,7 @@ mod domain { scry_taint::join(a, b) } } -const SCRY_VERSION: &str = "3.2.1"; +const SCRY_VERSION: &str = "3.2.2"; const INVARIANT_SCHEMA_URL: &str = "https://pulseengine.eu/scry-invariants/v1"; /// Default Wasm linear-memory page size (64 KiB). diff --git a/crates/scry-segment/Cargo.toml b/crates/scry-segment/Cargo.toml index 055206a..d9c5ae2 100644 --- a/crates/scry-segment/Cargo.toml +++ b/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.1" } +scry-sai-interval = { path = "../scry-interval", version = "3.2.2" } diff --git a/crates/scry-viz/Cargo.toml b/crates/scry-viz/Cargo.toml index 9552907..84c6a7c 100644 --- a/crates/scry-viz/Cargo.toml +++ b/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.1" } +scry-sai-core = { path = "../scry-analyze-core", version = "3.2.2" } # 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 }