From a7e3b77cda762e03a846df380bcc47e1534c79b9 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 16 Jul 2026 07:02:50 +0200 Subject: [PATCH] =?UTF-8?q?docs(readme):=20fix=20stale=20status=20block=20?= =?UTF-8?q?=E2=80=94=20v0.1.0=20'no=20real=20logic'=20=E2=86=92=20v3.0.0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The status section still described the v0.1.0 structural scaffold ('no real abstract-interpretation logic yet') while scry is on v3.0.0: real sound domains (interval, IEEE-754 float, Component-Model handle-lifetime) with admit-free Rocq soundness for specific properties (WrapAdd.v proves i32.add sound vs the official wrapping Wasm semantics). Surfaced by a cross-repo doc-drift audit; the stale block made scry look far less mature than it is (and would embarrass in review). Keeps the honest scope caveat: soundness is mechanized for named properties, not the whole analyzer. Co-Authored-By: Claude Opus 4.8 (1M context) --- README.md | 37 +++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/README.md b/README.md index 1532c26..b13aa2f 100644 --- a/README.md +++ b/README.md @@ -60,24 +60,25 @@ deductive-proof and bounded-model-checking layers do not staff. ## status -**v0.1.0 shipped 2026-05-27** — -[release page](https://github.com/pulseengine/scry/releases/tag/v0.1.0) -with cosign-signed `scry-0.1.0-wasm32-wasip2.wasm` + per-crate -CycloneDX SBOMs + SHA256SUMS + SLSA v1 provenance. The full -PulseEngine Wasm-component toolchain runs end-to-end on scry's own -build (the dogfood gate for [[DD-008]]). v0.1.0 ships the -**structural scaffold**: no real abstract-interpretation logic yet. - -The implementation work — interval-domain fixpoint on a parsed Wasm -module, host wasmtime test harness, Verus + Rocq proof targets, -region-memory domain — lands progressively from v0.2. Follow the -[release plan](#release-plan) below; each numbered version closes a -specific verified-evidence increment. - -`rivet validate` here is PASS with 0 warnings; 64 artifacts span 11 -types across `common + dev + research + research-ext + safety-case`. -Everything in this README that isn't tagged "v0.1.0" is still a -*requirements artifact* awaiting the labelled version. +**v3.0.0 shipped 2026-07-01** — "Qualifiable + differentiated" +(see [CHANGELOG](CHANGELOG.md)). scry is a **sound abstract interpreter for +WebAssembly**: it over-approximates, so it never misses a behaviour that can +occur — the DO-333 static-analysis leg of the PulseEngine pipeline. Artifacts +are cosign-signed with CycloneDX SBOMs + SLSA provenance, and the full +Wasm-component toolchain runs end-to-end on scry's own build (the dogfood gate +for [[DD-008]]). + +What ships today — not scaffold — includes an interval-domain fixpoint over a +parsed Wasm module, an IEEE-754 float domain, and Component-Model +handle-lifetime analysis, with **mechanized, admit-free Rocq** soundness for +specific properties: `proofs/rocq/WrapAdd.v` proves the shipped `i32.add` sound +against the *official* wrapping Wasm semantics, alongside per-domain lattice +proofs. A tool-qualification dossier ships for assessors. + +Scope, honestly: soundness is mechanized for named properties and domains, not +for the whole analyzer — see the per-feature proof targets and the honesty +ledger. Sections of this README still tagged `status: proposed` remain +requirements artifacts awaiting their labelled version. ## is this for you?