FEAT-049 (v3.0): Component-Model handle-state / use-after-drop (REQ-003, MF-007)#88
Merged
Conversation
…03, MF-007)
The uncontested green field (MF-007): scry becomes the first sound analyzer to
model Component-Model resource-handle lifetimes.
New zero-dep #![no_std] crate scry-sai-handle: an affine handle-state lattice
(Alive/Dropped/Top over concrete {alive,dropped}) with drop/use transitions.
γ-sweep asserts the lattice laws + transition soundness; admit-free Rocq
proofs/rocq/Handle.v mechanizes join/order/transition soundness (verified
locally with coqc — no Stdlib deps).
Analyzer: compute_handle_findings tracks each local's handle state across the
canonical-ABI call sites (imports named `[resource-drop]` = drop,
`[method]`/`[resource-rep]` = use — the ABI's own convention, read from
import_func_meta) and reports DEFINITE use-after-drop / double-drop faults,
surfaced library-only on AnalysisResult.handle_findings. Straight-line and
conservative at control flow (all locals widen to Top = "maybe dropped" at any
branch/merge, so a definite fault is never reported across paths) — sound in
the "no false report" direction the AC requires. scry-viz handle-faults panel.
New-crate wiring: workspace members+default-members, BUILD.bazel + dep in
scry-analyze-core, proofs/rocq/BUILD.bazel target, scripts/publish.rs
leaf-before-core. handle 6 / core 86 / viz 17 green, clippy + fmt clean,
rivet PASS.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #88 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
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.
The moat — scry becomes the first sound analyzer to model Component-Model
resource-handle lifetimes (MF-007, the uncontested green field).
What lands
scry-sai-handle(zero-dep,#![no_std]) — an affinehandle-state lattice (
Alive/Dropped/Topover concrete{alive,dropped})with drop/use transitions. γ-sweep asserts the lattice laws + transition
soundness; admit-free Rocq
proofs/rocq/Handle.v(verified locally withcoqc— no Stdlib deps).compute_handle_findings: tracks each local's handle state acrossthe canonical-ABI call sites — imports named
[resource-drop](drop),[method]/[resource-rep](use) — and reports definite use-after-drop /double-drop faults on
AnalysisResult.handle_findings. Straight-line andconservative at control flow (locals widen to
Top= "maybe dropped" at anybranch/merge, so a definite fault is never reported across paths).
Soundness claim (falsifiable)
A reported use-after-drop / double-drop is a DEFINITE fault: on the reported
path the handle is provably
Droppedat the site. Correct owned/borrowedlifetimes raise no finding (no false report). FALSE if any finding is
emitted for a handle that is not provably dropped at the site, or if a
straight-line drop-then-use goes unreported.
handle 6 / core 86 / viz 17 tests green; clippy + fmt clean;
rivet validatePASS. WIT mirror + frozen v1 JSON contract unchanged.
🤖 Generated with Claude Code