refactor: rework the vcgen frame procedure API around a commit callback - #14706
Draft
sgraf812 wants to merge 6 commits into
Draft
refactor: rework the vcgen frame procedure API around a commit callback#14706sgraf812 wants to merge 6 commits into
sgraf812 wants to merge 6 commits into
Conversation
Add `IsArray`, whose cells are reached by address arithmetic rather than by following pointers, and verify a loop that sums one. `IsArray_focus` splits the block at an index and hands back a wand to close it again, so `load_array` reads a cell without the index arithmetic reaching the loop invariant.
This PR restates the separation-logic demo's `append` specification in plain Hoare form, with the postcondition stated directly instead of received through a wand from a schematic postcondition. The loop invariant no longer carries a continuation wand, so the six entailment lemmas feeding it lose their `K` parameter. The frame procedure's branch for a precondition whose uncancelled atom is a wand, which existed to apply the ramified specification at `emp` frame, is removed along with its `emp`-framed trivial-wand lemmas: call sites now reach the specification through ordinary domain-difference cancellation.
This PR replaces the vcgen frame procedure protocol. A procedure now receives a `commit` callback that applies the frame rule and the spec rule eagerly and hands back the live subgoals (the frame `?F`, the split VC `pre ⊑ (op ?F specPre) s⃗`, the `WP.Frames` condition, and the spec's remaining goals); the procedure signals framing by calling it, in place of returning an `Option FrameSplit` that the solver replayed. Because the split VC carries the spec's real parameter metavariables, cancelling atoms against it pins spec parameters permanently, which the previous speculative-application protocol could not do (its `specPre?` reopened the metavariables as unrelated copies after rollback). The frame rule is restated as `WP.Frames.op_le_wp` with the footprint `P` as a parameter, so `commit` needs no proof surgery: applying the spec rule to the residual premise `?P ⊑ W` and fixing `?P` as the spec's precondition leaves the split VC in its final shape; when the spec rule does not fit the premise (its excess-argument count differs), `?P` is fixed as the weakest footprint `W` and the split VC re-enters `solve`, reproducing the deferred behavior of the meet and tick worlds. Procedures run in `GrindM`, return the subgoals they create, and `FrameInferenceProc.ofFrame?` recovers the plain frame-returning style for procedures that discharge nothing. `FrameSplit`, `FrameBackwardRule`, `specPre?`, `mkResidualPre`, and `mkSplitVCS` are deleted; `peekSpecPre` (a `Pattern.match?` instantiation, data only) informs the commit decision. The separation-logic demo's procedure now cancels partially: paired atoms are cancelled out of the split VC (pinning the paired spec parameters), and unmatched footprint atoms survive into a residual VC `rest ⊑ ?F ∗ unmatched` with the frame left schematic, surfaced as a hole the user fills. New tests exercise the partial-cancellation flow against an abstract-predicate mismatch.
This PR simplifies the frame commit plumbing. The solver detects a commit by the goal being assigned and collects the subgoals as the unassigned metavariables of the goal's proof term, so the `IO.Ref` channel, the `List MVarId` returned by every procedure, and the exception save/restore disappear; `FrameInferenceProc` returns `Unit` again. `commitFrameRule` closes the residual premise's precondition VC (or, without a spec application, the premise itself) through the existing `rfl?` rule, removing the hand-built reflexivity proofs, and `FrameGoals` shrinks to the three named handles `F`, `splitVC`, `frames`.
…lot indexing This PR reverts the `WP.Frames.op_le_wp` frame rule introduced earlier in this branch and returns to `op_wp_upperAdjoint_le_wp`. Parameterizing the rule by the footprint `P` put the residual premise `P ⊑ wp x (fun a => upperAdjoint (op F) (Q a)) E` in the lemma's hypotheses rather than its conclusion, and `mkSpecBackwardProof` applies the goal's excess state arguments only to the conclusion and its precondition. The premise therefore sat at the unapplied assertion type while the split VC beside it carried `s⃗`, so the spec rule failed to apply to it whenever the assertion type was stateful, and `FrameGoals.splitVC` silently meant `op ?F specPre` with no excess arguments and `op ?F W` with them. `FrameBackwardRule` and its cached slot positions come back, extended with the frame condition's position, so `commit` reads its three subgoals off by index instead of searching the applied rule's goals by shape. All `FrameGoals` fields are metavariables. `controlAt` replaces the hand-written `VCGenM`-to-`GrindM` reifier at the procedure call site. A procedure that wants the spec's parameters live applies the spec rule to the footprint entailment itself, at the excess arguments its own operator split produced: the separation-logic demo does this in `openFootprint`, and the precondition VC it gets back carries the spec's own metavariables, so cancelling against it pins them. Cancelling a pinned frame leaves that precondition VC to the user, which is how the abstract-predicate test now folds the representation without any parameter holes reaching `finish`.
…ents This PR adds a regression guard to the cost frame procedure. `vcgen` applies a spec at the goal's excess state arguments, so the footprint the frame rule leaves must be reachable there; the guard applies the spec rule to the footprint entailment and reports when it is not. Stating the footprint at the unapplied assertion type, which happens when a frame rule takes it as a hypothesis rather than in its conclusion, goes unnoticed by every test whose assertion type carries no state.
sgraf812
force-pushed
the
sg/vcgen-seplogic-next
branch
from
August 11, 2026 08:23
a4f04c3 to
8e423b4
Compare
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
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
2 participants
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.
This PR replaces the vcgen frame procedure protocol. A procedure now receives a
commitcallback that applies the frame rule and the spec rule eagerly and hands back the live subgoals (the frame?F, the split VCpre ⊑ (op ?F specPre) s⃗, theWP.Framescondition, and the spec's remaining goals); the procedure signals framing by calling it, in place of returning anOption FrameSplitthat the solver replayed. Because the split VC carries the spec's real parameter metavariables, cancelling atoms against it pins spec parameters permanently, which the previous speculative-application protocol could not do (itsspecPre?reopened the metavariables as unrelated copies after rollback).The frame rule is restated as
WP.Frames.op_le_wpwith the footprintPas a parameter, socommitneeds no proof surgery: applying the spec rule to the residual premise?P ⊑ Wand fixing?Pas the spec's precondition leaves the split VC in its final shape; when the spec rule does not fit the premise (its excess-argument count differs),?Pis fixed as the weakest footprintWand the split VC re-enterssolve, reproducing the deferred behavior of the meet and tick worlds. Procedures run inGrindM, return the subgoals they create, andFrameInferenceProc.ofFrame?recovers the plain frame-returning style for procedures that discharge nothing.FrameSplit,FrameBackwardRule,specPre?,mkResidualPre, andmkSplitVCSare deleted;peekSpecPre(aPattern.match?instantiation, data only) informs the commit decision.The separation-logic demo's procedure now cancels partially: paired atoms are cancelled out of the split VC (pinning the paired spec parameters), and unmatched footprint atoms survive into a residual VC
rest ⊑ ?F ∗ unmatchedwith the frame left schematic, surfaced as a hole the user fills. The demo's hand-ramifiedappendspecification and theemp-frame machinery serving it are removed: the plain specification now reaches every call site through cancellation. New tests exercise the partial-cancellation flow against an abstract-predicate mismatch.