Conversation
This was referenced May 1, 2026
Closes audit S5 by giving callers a way to distinguish "Z3 proved equivalence" from "verifier silently bailed because input was unverifiable." The existing VerificationResult enum already had the variants; this PR adds the predicates and a strict-mode revert helper so passes can opt into "skip = unsafe to optimize." verify.rs additions: - VerificationResult::is_skip() — true for SkippedLoop / SkippedMemory / SkippedUnknown; false for Verified / Failed / Error. - VerificationResult::skip_reason() — human-readable skip cause. - TranslationValidator::verify_or_revert_strict() — strict counterpart to verify_or_revert. Reverts on Skipped*, Failed, or Error; only Verified is accepted. Recorded under "<pass>:strict-skip" stat key for skip-induced reverts so they're separable from genuine counterexamples. - Stub for non-verification builds returns false (REQ-5 conservative- over-fast: when Z3 isn't available we don't hoist). - Doc comments on existing is_equivalent() / is_verified() now name the lenient/strict semantics explicitly. Tests added (4) for the lenient/strict/is_skip/skip_reason behavior. Research artifact: docs/research/gale-v0.4.0/measurement-report.md copied from scripts/mythos/gale_measure/. The report measures LOOM v0.4.0 vs wasm-opt -O3 on a Verus-verified kernel-scheduler FFI. Headline finding: LOOM regresses code-section size by +6.3% on this workload while wasm-opt reduces by -2.0%, primarily because LOOM's CSE pass deduplicates trivially-cheap small constants into local.tee/local.get pairs that grow function headers. Critical finding: CSE produces an UNSOUND transformation in gale_sem_count_take, hoisting an i32.store above its null-pointer guard — the function uses 'if + return' (early-exit) which the v0.4.0 has_dataflow_unsafe_control_flow guard does not flag (it only checks BrIf/BrTable). Addressed in v0.5.0 PR-B. Trace: REQ-3, REQ-5
avrabe
force-pushed
the
release/v0.5.0-pr-a-verification-outcome
branch
from
64d71b2 to
75857d3
Compare
avrabe
added a commit
that referenced
this pull request
May 2, 2026
Bump workspace version 0.4.0 → 0.5.0 and add CHANGELOG section. This release ships the v0.5.0 audit follow-ups across five PRs: - #88 PR-A: VerificationResult strict-mode helpers (is_skip, skip_reason, verify_or_revert_strict) + gale v0.4.0 measurement report documenting the CSE soundness bug on production kernel-scheduler code. - #89 PR-B: Close hoist hole on early-exit (Return/Br) patterns. Per-pass tracing showed reordering happens in constant_folding's terms-IR roundtrip; the function ends up with the if-guard moved to the function tail and the load/store sequence hoisted to the function head. Fix: extend has_dataflow_unsafe_control_flow to flag nested Return/Br; constant_folding and optimize_advanced_instructions skip such functions entirely. Defense-in-depth guards on simplify_locals, remove_unused_branches, optimize_added_constants. Regression test pinned. - #90 PR-C: 8 minimal post-MVP wasm fixtures + spec_features.rs test harness. Pins the "parser must never panic" contract for SIMD, ref types, bulk memory, tail calls, exception handling, multi-memory, sign-extension, saturating-trunc. - #91 PR-D: FusedOptimization.v wired into BUILD.bazel. Closes audit D1; the 7 axioms remain (discharge is future work). - #92 chore: top-level concurrency: block on every workflow. Closes the org-wide CI queue backlog; superseded PR runs now cancelled in ~30s, runs on main / tags / releases / scheduled events never cancelled. CHANGELOG.md adds a v0.5.0 section documenting all of the above plus the deferred work for the next release. Trace: REQ-1, REQ-3, REQ-5, REQ-7, REQ-9, REQ-12, REQ-14
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
First PR of the v0.5.0 release. Two parts:
Closes audit S5 — gives passes a way to distinguish "Z3 proved equivalence" from "verifier silently bailed because input was unverifiable." The existing
VerificationResultenum already carried the variants; this PR adds the predicates and a strict-mode revert helper so callers opt into "skip = unsafe to optimize."Documents v0.4.0 gale measurement in `docs/research/gale-v0.4.0/measurement-report.md`. Critical finding: CSE produces an UNSOUND store-hoist on `gale_sem_count_take` because the v0.4.0 hoist guard only checks BrIf/BrTable, not Return/Br. Fixed in v0.5.0 PR-B.
verify.rs additions
4 unit tests covering lenient/strict/is_skip/skip_reason.
Test plan
v0.5.0 release sequence
🤖 Generated with Claude Code