Skip to content

viz redesign: readable dashboard (cap points, guidance.json, scope block) + honest copy - #107

Merged
avrabe merged 2 commits into
mainfrom
viz-redesign
Jul 15, 2026
Merged

viz redesign: readable dashboard (cap points, guidance.json, scope block) + honest copy#107
avrabe merged 2 commits into
mainfrom
viz-redesign

Conversation

@avrabe

@avrabe avrabe commented Jul 14, 2026

Copy link
Copy Markdown
Contributor

Acts on the unanimous persona review of the deployed dashboard (a DO-178C assessor, an AI-agent consumer, a skeptical Wasm academic, and a busy first-time engineer). The problem wasn't verbosity — it was an inverted pyramid with a broken page.

Structural fixes (from the redesign subagent)

  • Capped the Program points section — the 18.8 MB culprit. Each function shows a summary + first 20 points + "… showing 20 of M; full data in guidance.json". Whole HTML now well under 1 MB (test-enforced).
  • Collapsed the Guidance boilerplate — every DefiniteFault in full (proven bugs, never elided), other classes capped at 10 + "… and N more (see JSON)". The ~14 real fixes no longer drown under 6,191 identical rows.
  • render_guidance_json — a structured, machine-consumable feed ({advisories[], trap_checks[]}, full/un-capped), written alongside the HTML and emitted+checked in release.yml. Matches scry's structured-primary ethos (the AI-agent persona's top ask).

Honest copy (finalized by me — honesty-sensitive)

  • Retitled from bare "verification dashboard" → "scry — a sound static analyzer for WebAssembly"; landing lead says what it catches + "⊤ means unknown, never safe."
  • Scope & limitations block: the mechanized-vs-γ-swept evidence distinction (Rocq admit-free lattices + WrapAdd.v vs γ-swept FM/float/known-bits-w32/64 → issue Machine-check scry-bits transfer soundness at w=32/64 with ordeal certificates (DO-333) #105), 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). Directly answers the skeptic + assessor.

Verification

24 viz tests (5 new: points-cap + <1 MB page-size, guidance.json well-formedness + escaping, guidance-collapse-keeps-faults, panels regression); clippy -D warnings + fmt clean. Additive — scry-analyze-core untouched.

Ships as the next dashboard release (v3.2.2). 🤖 Generated with Claude Code

avrabe and others added 2 commits July 14, 2026 20:52
…e, JSON feed, scope block)

Persona reviews of the deployed dashboard converged on: self-analysis.html is
18.8 MB (unopenable); Guidance drowns ~14 real items in ~6k identical rows; no
machine-consumable output; no scope block. Structural, additive fixes:

- Cap Program points at POINTS_PER_FN_CAP (20) per function; render a
  per-function summary (#points, up-to #locals) + a "showing N of M; full data
  in the JSON feed" note. Whole page now well under 1 MB.
- Collapse Guidance boilerplate: keep the tally, render every DefiniteFault in
  full, cap each other class at ADVISORY_PER_CLASS_CAP (10) with a "… and N
  more <class> (see the JSON feed)" line.
- Add pub fn render_guidance_json: hand-rolled JSON (no serde dep) with proper
  string escaping (json_esc), emitting the FULL advisories + trap verdicts.
  CLI writes <stem>.guidance.json alongside the HTML; release.yml emits and
  sanity-checks dist/self-analysis.guidance.json.
- Add render_scope() emitting <section id="scope"> with a
  SCOPE_COPY_PLACEHOLDER comment (maintainer writes the soundness copy).
- Retitle to neutral HERO_TITLE placeholder (SCOPE_TAGLINE_PLACEHOLDER) on the
  page and landing lead.

Tests added: points cap + <1 MB page-size sanity, guidance.json
well-formedness + expected advisory, JSON escaping, Guidance collapse keeps
faults, existing-panels regression. cargo test/clippy/fmt clean.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Fills the two placeholders the redesign left for me, with precise, Watt-defensible
copy:
- Hero/title: "scry — a sound static analyzer for WebAssembly" (retitled away from
  bare "verification dashboard"); landing lead states what it catches + "⊤ means
  unknown, never safe".
- Scope & limitations block: the mechanized-vs-γ-swept evidence-kind distinction
  (Rocq admit-free lattices/WrapAdd.v vs γ-swept FM/float/known-bits-w32/64,
  issue #105), 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).

Guard test updated to assert the finalized copy (no placeholders, retitled,
evidence-kinds + soundness caveat legible). Addresses the skeptic + assessor
persona findings. 24 viz tests pass; clippy + fmt clean.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@avrabe
avrabe merged commit e4ec042 into main Jul 15, 2026
9 checks passed
@avrabe
avrabe deleted the viz-redesign branch July 15, 2026 03:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant