fix: fix vcgen frames feature for monads with multiple StateT transformers#14217
Draft
volodeyka wants to merge 13 commits into
Draft
fix: fix vcgen frames feature for monads with multiple StateT transformers#14217volodeyka wants to merge 13 commits into
vcgen frames feature for monads with multiple StateT transformers#14217volodeyka wants to merge 13 commits into
Conversation
Introduce `Residuated`, the join-distributivity class whose residual `Residuated.imp` and frame closure `Residuated.frameClosure` internalize the frame rule for any residuated operator, not just the lattice meet. `WP.Frames` and the frame gadgets are stated for an arbitrary residuated `conj`; the Heyting/meet case is the specialization.
Add the `@[frameproc]` attribute registering a frame inference metaprogram for `vcgen`, keyed by program type. A registered procedure supplies the inferred frame, its frame operator, and the lattice split that decomposes it; `vcgen` applies the operator's frame gadget and the split. Direct (non-pointwise) lattice splits are supported via an optional `applyLemma`.
Demonstrate a residuated frame operator that is not the lattice meet: `costConj` over `Nat → Prop`, the separating conjunction for the cost resource. `TickM.wp` bakes the frame rule in as a `frameClosure`, and a registered `@[frameproc]` lets plain `vcgen` infer and apply the cost frame end-to-end.
Add the lawful `WPMonad TickM` instance (pure/bind sound for `TickM.wp`), so `vcgen` can decompose `bind` and loops over `TickM` programs. The cost frame `d` threads through `pure` and `bind`.
`applyFrame` no longer frames the monad's structural combinators (`bind`/`pure`/`map`/`seq`), letting them decompose through their specs so frame inference applies to the leaf calls. Make `TickM`'s `WP` come solely from its `WPMonad` instance, and add a `tickList` loop verified end-to-end by plain `vcgen` with automatic cost framing.
A `@[frameproc]` now also carries the lattice split for its frame operator's residual wand (`Residuated.imp conj`). `splitLatticeOp?` dispatches a `Residuated.imp` goal on its inner operator, routing a custom frame's magic wand to that split while the meet `⇨` falls through to the built-in residual. The wand no longer surfaces in a VC, so `do tickList xs; tickList ys` verifies by plain `vcgen` with the costs framed automatically across both calls.
State `tickList`'s spec in the concrete stopwatch form `⦃· = 0⦄ tickList xs ⦃fun _ t => t = xs.length⦄` (notation `tickList xs ⏱ xs.length`) rather than a post-schematic spec, so `vcgen` frames it only where the start cost is non-zero. The schematic cost lemma becomes a non-`@[spec]` helper the stopwatch spec is derived from. The two-loop example now frames the second call by the cost the first accrued.
…it frames `matchFrameProc?` now sources the frame operator from the `@[frameproc]` registered for the program's type whether the frame comes from an explicit `frames` clause or from the registered procedure, instead of hardcoding the lattice meet for the `frames`-clause path. An explicit `frames` clause on a `TickM` program now frames with `costConj`, not meet. Also rewrite the `tickList` demo as an idiomatic `for` loop, and show the two-loop goal framed both explicitly and with frames omitted.
The `Residuated` class now takes a resource type `R` so the frame operator is `op : R → α → α` rather than `α → α → α`. A frame is a value of `R`, which need not be an element of the lattice: the cost monad in the demo frames by a plain `Nat` budget instead of an assertion. The lattice meet is the instance at `R = α`. `frameClosure` frames with the consistent order `op r (Q a)`, and `frameClosure_frames` assumes only an action law `op (comp r r') = op r ∘ op r'` for a resource composition `comp`, dropping the commutativity and associativity requirements. `WP.Frames`, the frame gadgets, and `WP.Frames.of_frameClosure` carry the resource frame `F : R` and thread `comp` with its action law. The frame-inference procedure receives the operator's resource type, so an explicit `frames` clause elaborates its term at `R`. `LatticeSplit` gains a `leadingArgs` field to account for the resource-type argument of `Residuated.imp`, and the residual dispatch reads the inner operator from its shifted position. The cost demo now frames by a `Nat`: `costConj r b = fun n => r ≤ n ∧ b (n - r)` with residual `fun m => b (m + r)`, a plain cost shift, so the two-loop example reads `frames | tickList xs => 0 | tickList ys => xs.length`.
Name the class for what it requires rather than an opaque property of its operators: `SupPreserving R α op` says each `op r ·` preserves arbitrary joins. Its right adjoint is `SupPreserving.upperAdjoint` (was `Residuated.imp`), with the unit/counit renamed to `le_upperAdjoint`/`upperAdjoint_le`. Reintroduce `himp` as the meet upper adjoint, `himp a b = SupPreserving.upperAdjoint (· ⊓ ·) a b`, with `⇨` as its notation, and give `vcgen` a dedicated `himp` lattice split so the meet residual decomposes through it.
Rename `SupPreserving R α op` to `PreservesSup (f : α → α)`, a predicate on a single join-preserving map following the Lean-core `Preserves*` convention (`PreservesLE`, `PreservesLeast?`). A frame operator is instantiated at its slice `op r`: the lattice meet at `meet a`, the cost combinator at `costConj r`. `upperAdjoint`/`le_upperAdjoint`/`upperAdjoint_le`/`map_mono` and `frameClosure` follow, with `frameClosure_frames` taking `[∀ r, PreservesSup (op r)]`. Make `himp` a `def` with its own API derived from the upper-adjoint properties (`le_himp`, `meet_himp_le`), `⇨` its notation. `vcgen` decomposes `⇨` through a dedicated `himp` split keyed on `le_himp`; the general residual split is gone, since custom operators register their own and the meet case is `himp`.
Drop the meet-specific `meet_wp_imp_le_wp_skipFrame`; `vcgen` now frames every operator, the lattice meet included, through the single gadget `op_wp_upperAdjoint_le_wp_skipFrame` (renamed from `wp_imp_le_wp_skipFrame`, built on `WP.Frames.op_wp_upperAdjoint_le_wp`). The meet residual `upperAdjoint (meet F) b` is folded to `F ⇨ b` (definitionally equal: `himp` is the meet upper adjoint) by `foldUpperAdjointMeet?`, exposing the meet operand so the `himp` split decomposes it. `applyFrame` no longer branches on the operator.
Extend `@[frameproc]` frame inference to a *nested-base* assertion lattice (e.g. `ComplexiT (StateM σ)`, lattice `Tick → σ → Prop`). There the frame operator is applied to more coordinates than the registered direct split lemma handles (`pre ⊑ cCostConj c R n s`, not `… n`), so `splitLatticeOp?` returns `none` and the raw goal — with an un-specced inner `wp` — is dumped on `finish`. Add two fallback steps in `solve`, run after the direct split and the wp phase (so flat lattices are untouched): for a registered frame `conj` or its residual wand, `mkReduceRule` builds a backward rule from a registered reduce-equation (`FrameProc.conjReduce` / `impReduce`) whose conclusion matches the goal head, and `applyChecked`s it. The single premise is the reduced subgoal — the built-in connective for the conj (the meet split then peels it over all coordinates), or the shifted body for the wand (exposing the inner `wp` for the spec step). `mkReduceRule` reuses `mkBackwardRuleForLattice`'s composition tail (`liftEqByArgs` + `Eq.mp` + `mkBackwardRuleFromExpr`), minus the `relLemma`. `tests/bench/vcgen/mwe_nested_frame.lean` documents the 2-level setup. Flat `TickM` is unchanged (the fallbacks never fire). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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
3 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 builds on top of
vcgen framesfeature and fixes some problems. More explanations yet to come