From 2e6efbbf832f5ac5c14dfa0e69d2ac899abaf9cf Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 15 Jul 2026 23:12:54 +0200 Subject: [PATCH] docs(337): make the verification claim accurate (relabel + narrow) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The flat always-green `Formally_Verified` badge and the "every transformation carries mechanized proofs covering parsing, resolution, merging, and adapter correctness" tagline overstated the actual evidence (grounded in proofs/STATUS.md + abi_proofs.rs): - Kani harnesses (abi/resolver/merger) are VERIFICATION SUCCESSFUL LOCALLY (SR-40) but NOT gated in CI (shared runners lack the Kani toolchain); some ABI size/align + aggregate-padding contracts fell back to unit tests. - Rocq: 350 closed proofs on resolver/merger/adapter/spec (real, substantial), but parser/rewriter/segments/attestation are placeholders, orchestration is unproven, semantic preservation is a FORWARD simulation only, and one FACT adapter lemma is Admitted — so "every transformation … behaves identically" overstates. Fix (claim-verification relabel): - Badge → linked `Formal_Methods: Rocq + Kani (partial)` pointing at the Formal Verification section (informational, not a false CI-gate claim). - Tagline → narrowed to the core stages actually proven + a scope caveat. - Formal Verification section → rewritten to state the 350-proof coverage honestly (what's proved vs placeholder, forward-only simulation, the one Admitted lemma, Kani local-not-CI), linking proofs/STATUS.md. Not addressed here (infra): #337(b) gating the converging Kani harnesses in CI needs the Kani toolchain on the shared runners — a smithy-infra change. Refs #337. Co-Authored-By: Claude Opus 4.8 (1M context) --- README.md | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index 70418ce..fd78154 100644 --- a/README.md +++ b/README.md @@ -12,7 +12,7 @@ ![Rust](https://img.shields.io/badge/Rust-CE422B?style=flat-square&logo=rust&logoColor=white&labelColor=1a1b27) ![WebAssembly](https://img.shields.io/badge/WebAssembly-654FF0?style=flat-square&logo=webassembly&logoColor=white&labelColor=1a1b27) ![Component Model](https://img.shields.io/badge/Component_Model-654FF0?style=flat-square&logoColor=white&labelColor=1a1b27) -![Formally Verified](https://img.shields.io/badge/Formally_Verified-00C853?style=flat-square&logoColor=white&labelColor=1a1b27) +[![Formal Methods](https://img.shields.io/badge/Formal_Methods-Rocq_%2B_Kani_(partial)-2962FF?style=flat-square&logoColor=white&labelColor=1a1b27)](#formal-verification) ![License: Apache-2.0](https://img.shields.io/badge/License-Apache--2.0-blue?style=flat-square&labelColor=1a1b27)   @@ -35,7 +35,7 @@ Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals. -Meld statically fuses multiple WebAssembly components into a single core module, eliminating the need for runtime linking. Import resolution, index-space merging, and canonical ABI adapter generation happen at build time. Every transformation carries mechanized proofs covering parsing, resolution, merging, and adapter correctness. +Meld statically fuses multiple WebAssembly components into a single core module, eliminating the need for runtime linking. Import resolution, index-space merging, and canonical ABI adapter generation happen at build time. The core transformations — resolution, index-space merging, and adapter generation — carry mechanized Rocq proofs, plus local Kani bounded-model-checking harnesses on the Canonical-ABI layout invariants; see [Formal Verification](#formal-verification) for the per-stage coverage (some stages are specified but not yet proved, and the Kani harnesses are run locally, not gated in CI). Unlike composition tools that produce linked-but-separate component graphs, Meld produces a single monolithic module suitable for whole-program optimization by Loom and native transpilation by Synth. @@ -158,13 +158,15 @@ Step 2 proves the checksum file came from this repo's `release.yml`; step 3 ties ## Formal Verification -Meld's core transformations are formally verified using Rocq. The proofs establish that fusion preserves program semantics — the fused module behaves identically to the original composed components. +Meld's **core** transformations carry mechanized Rocq proofs — 350 closed proofs (`Qed`) across the resolver, merger, adapter, and specification layers (see [`proofs/STATUS.md`](proofs/STATUS.md) for the per-stage coverage matrix). This is real, substantial verification on the core; it is **not** yet a whole-pipeline proof: the parser, rewriter, segments, and attestation stages are specified but their proofs are placeholders, orchestration (`lib.rs`) is unproven, and the semantic-preservation result is a **forward** simulation (the fused module simulates the original graph step-by-step; the reverse direction and the backward half of trap-equivalence are not yet proved). -Key verified properties: -- **Merge correctness** — Index remapping preserves function/memory/table references -- **Resolve correctness** — Topological sort produces valid instantiation order; cycle detection terminates -- **Adapter correctness** — Generated trampolines preserve call semantics -- **Forward simulation** — Fused module simulates the original component graph step-by-step +Proven properties (Rocq): +- **Merge correctness** — Index remapping preserves function/memory/table references (injectivity, completeness, boundedness); memory-layout disjointness. +- **Resolve correctness** — Topological sort produces a valid instantiation order; cycle detection terminates. +- **Adapter correctness** — Canonical-ABI lift/lower roundtrip and crossing-adapter semantics (one FACT parameter-match lemma remains `Admitted`). +- **Forward simulation** — The fused module simulates the original component graph step-by-step (forward direction; fully proved). + +In addition, the Canonical-ABI layout invariants (size/alignment saturating arithmetic, the #141 stream ring model) carry **Kani** bounded-model-checking harnesses (`abi_proofs.rs`, `resolver.rs`, `merger.rs`) that were `VERIFICATION SUCCESSFUL` locally (SR-40); these are **not gated in CI** (the shared runners do not ship the Kani toolchain), and the ABI size/alignment and aggregate-padding contracts that did not converge in CBMC fall back to unit tests. Proofs are built via Bazel using [`rules_rocq_rust`](https://github.com/pulseengine/rules_rocq_rust):