feat: support join points in vcgen via synthetic backward rules#14398
Draft
sgraf812 wants to merge 14 commits into
Draft
feat: support join points in vcgen via synthetic backward rules#14398sgraf812 wants to merge 14 commits into
sgraf812 wants to merge 14 commits into
Conversation
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
This PR adds `+jp` shared-continuation handling to `vcgen`: when the branches of an `if`/`match` share a trailing continuation (a `__do_jp` join point), the continuation is verified once instead of being duplicated into every branch, avoiding the exponential growth in verification conditions on nested splits. At a `let __do_jp := fun args => body; rest` whose `rest` is a splitter, `tryJoinPointDef` registers a synthetic `Triple` spec for `__do_jp` keyed on `@fv joinParams` and splits into the join-point body and the rest; each jump `__do_jp args` then discharges through the normal `applySpec` pipeline, with `tryAssignJPHyps` filling the alt-specific precondition and `tryRwSplitterRHS` reducing the resulting `Pjp args`. The join-point fvar is re-marked nondep after introduction so its spec keys on the fvar rather than the zeta-reduced body. Tests: `tests/elab/vcgenJPs.lean` exercises `vcgen +jp` on multi-`if` pure and stateful programs; `tests/elab/symZetaJPMwe.lean` isolates the `Sym.introN`/`preprocessType` zeta; `tests/bench/vcgen` adds an `IfsJP` bench case.
This PR reworks how `vcgen +jp` recognizes a join point: instead of hoisting and re-parsing the goal inside a single step, `tryMarkJP?` wraps the continuation of a `__do_jp` let in the identity gadget `jpGadget fv rest`, the usual `wpLet?` introduces the let, and `tryJPGadget?` then detects the gadget and registers the synthetic spec directly from the `WPApp` (no re-derivation of `Pred`/`post`/the splitter). This removes the bespoke `hoistProgLetIntro` helper and keeps the join-point setup on the ordinary `wp` decomposition path.
This PR adds the `IfsJP` shared-continuation case to `test_vcgen.lean`, run at n=10 with `vcgen +jp`, so the join-point path is covered by the vcgen test suite alongside the standalone `vcgen_ifs_jp` benchmark.
This PR makes `vcgen +jp` work on sequenced/looping programs where one join point's continuation contains another (e.g. `do let a <- st x; let b <- st a`). The reflexivity step's unifier can throw on an un-decomposed program-head `let`; `rfl?` now treats that as "not reflexive here" (rolling back state) and lets `wp` decomposition handle the join point instead.
This PR extends `vcgen +jp` to `match`-based join points (not just `if`/`match`-on-`ite`): the synthetic precondition `Pjp` is now built with the matcher form (`useSplitter := false`) rather than the `.splitter`, so `tryRwSplitterRHS` can reduce it at each jump. Also drops the `saveState`/`restore` from the `rfl?` chained-JP fallback: a unifier throw leaves the goal unassigned, so `catch`-and-return-none suffices without the snapshot cost.
Build the join-point precondition at `Prop` and close it over the excess state args the way the regular split path does (`fun s⃗ => match discrs => ?Hᵢ`), so applying the state β-reduces it to a bare `Prop` match that `grind` case-splits; this brings stateful match join points to parity with `mvcgen +jp`. Assign `False` to the precondition of a `rest` alt that never jumps to the join point, so an early `return` in one branch no longer leaves an unassigned metavariable. Drop the now-unreachable `tryRwSplitterRHS` strategy. Expand `tests/elab/vcgenJPs.lean` to the full `mvcgenJPs` port. The dependent-discriminant cases (`match h : …`) are commented out: they fail `vcgen`'s matcher transform on their own, independently of `+jp`.
Rebased onto `master` (which now splits `match h : e` discriminant-equation matchers), so the single-discriminant `dmatches_pure` case discharges under `vcgen +jp`. The two `mixed_matches_*` cases stay commented: a multi-discriminant dependent match makes the jump-site precondition a proof-carrying existential that `grind` cannot witness, which needs the join point to construct the witness directly.
Prove each join-point jump's precondition VC directly instead of leaving it for `grind`: `tryAssignJPHyps` hands back the applicable alt and the jump's own locals, and `tryCloseJPPrecond` reduces the synthetic `⌜match discrs => ?Hᵢ⌝` precondition to that alt and witnesses the resulting existential. This brings multi-discriminant dependent-match join points to parity with `mvcgen +jp`, where `grind` could not witness the proof-carrying existentials, and cuts the emitted VC count sharply. Key the precondition on `⌜·⌝` so the witness closes generically via `ofProp_eq_top`, adding `CompleteLattice.le_ofProp`. Drop the `setNondep` re-marking now that `Sym.preprocessType` no longer zeta-reduces the join-point fvar, and remove the corresponding MWE. Complete `tests/elab/vcgenJPs.lean` to all ten `mvcgenJPs` cases.
Pair the join-point spec's alt binders with the corresponding jump-site locals instead of existentially closing over the whole alt context: the body split's alt telescope is the matcher's alt telescope interleaved with overlap hypotheses and added discriminant equalities, so the pattern variables and user equations are matched up as an order-preserving subsequence and substituted, leaving only the splitter-specific binders under the existential. The join-point body then sees the shared precondition expressed directly in its own pattern variables, which `grind` discharges without unfolding nested existentials; the six-way multi-discriminant dependent-match case in `tests/elab/vcgenJPs.lean` is restored to full size and the whole file elaborates in under two seconds.
Keep an unpaired jump-site local in the join-point precondition only when the join-argument equalities transitively reference it through kept let values. Split bookkeeping such as overlap hypotheses and added discriminant equalities is re-derived on the consuming side when the match hypothesis is split, so dropping it leaves the precondition free of existentials in the common case, matching what `mvcgen +jp` emits.
Add join-point cases along axes the suite did not exercise: several mutable variables (multiple join-argument equalities), an effectful shared tail (spec application inside the join-point body), and literal/successor patterns (a `Nat.casesOn`-shaped matcher). A split nested inside an alt and a throwing alt fail under `vcgen +jp` and `mvcgen +jp` alike and are recorded as commented cases.
Defer assignment of the join-point alt-precondition mvars to a finalization pass after VC generation: each jump records its payload and witnesses, and `finalizeJPs` assigns every `?Hᵢ` the disjunction of its recorded payloads before discharging each jump goal with its own disjunct. An alt no jump reaches gets `False`, so a jump that is dead code behind a `throw` no longer leaves an unassigned metavariable, and several jumps into one alt, as arise from an `if` nested inside a match alt, no longer race for a single assignment. Payload closure now drops exactly the outer split's own bookkeeping (overlap hypotheses, added discriminant equalities, an outer `ite`'s condition proof), which the consuming side re-derives when splitting the match hypothesis; facts from within the alt, such as an inner `if` condition, are kept under the existential. Tests: `nested_split` and `throwing` in `tests/elab/vcgenJPs.lean` exercise the two shapes; both also fail under legacy `mvcgen +jp`.
Replace the defeq-based pairing of the join-point spec's alt binders with jump-site locals by a structural layout recorded at registration: `JPAltLayout` stores the segment sizes of the body split's alt telescope (`fields ++ overlaps ++ discrEqs ++ extraEqs`, per `MatcherApp.TransformAltFVars`) alongside the spec's own binder count, so pairing and bookkeeping classification become positional slicing. A thunked nullary alt's `Unit` parameter exists on the spec side only and stays unpaired. Layout mismatches and jumps yielding no precondition subgoal now raise errors instead of degrading silently. Also restore `wpFVarZeta?` to dependent-let values only, reuse `Lean.Order.le_ofProp` in place of a duplicate lemma, group recorded jumps and build the finalization simp context once, and drop a redundant second telescope of the precondition mvar's type.
Close a jump subgoal `∀ xs, lhs ⊑ rhs` with definitionally equal sides directly in `applySpec`. The synthetic spec's postcondition is the registration goal's, so the jump's post-monotonicity premise carries the same postcondition on both sides, differing at most by eta; on the worklist the target simp unfolded the entailment and re-verified the continuation that postcondition carries, once per jump, which made the VC count grow exponentially in the number of sequenced splits. The `IfsJP` benchmark drops from 49 VCs and 2.4s of grind at n = 3 to a single VC discharged in under 30ms.
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 adds
+jpshared-continuation handling tovcgen: when the branches of anif/matchshare a trailing continuation (a__do_jpjoin point), the continuation is verified once instead of being duplicated into every branch, avoiding the exponential growth in verification conditions on nested splits. Pure and statefulif/matchjoin points, dependent-discriminant matches, and earlyreturnare supported.At a
let __do_jp := fun args => body; restwhoserestis a splitter, the continuation is tagged with ajpGadgetmarker so the usual let-introduction runs; a syntheticTriplespec for__do_jpkeyed on@fv joinParamsis then registered, and each jump__do_jp argsdischarges through the normalapplySpecpipeline rather than inliningbody.The synthetic precondition splits at
Propand embeds via⌜·⌝: in branchiit is⌜∃ locals, joinParams = joinArgs⌝with the alt-local facts. Each jump discharges its own precondition VC by construction, reducing the match to the applicable alt and witnessing the existential with the jump's locals, sogrindnever has to witness the proof-carrying existentials that dependentmatch h : …produces. Arestalt that never jumps to the join point gets preconditionFalse, so an earlyreturnin one branch leaves no unassigned metavariable.Tests:
tests/elab/vcgenJPs.leanexercisesvcgen +jpacross pure and statefulif/match, dependent and multi-discriminant matches, and early return;tests/bench/vcgenadds anIfsJPcase.