diff --git a/src/Lean/Elab/BindersUtil.lean b/src/Lean/Elab/BindersUtil.lean
index e9439e4cc347..a4475e8308bd 100644
--- a/src/Lean/Elab/BindersUtil.lean
+++ b/src/Lean/Elab/BindersUtil.lean
@@ -13,17 +13,6 @@ import Init.Syntax
 
 public section
 
-/--
-Determines the local declaration kind of a binder using its name.
-
-Names that begin with `__` are implementation details (`.implDetail`).
--/
-def Lean.LocalDeclKind.ofBinderName (binderName : Name) : LocalDeclKind :=
-  if binderName.isImplementationDetail then
-    .implDetail
-  else
-    .default
-
 namespace Lean.Elab.Term
 /--
   Recall that
diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean
index 76be1ea1ceb1..3599b8e319a5 100644
--- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean
@@ -134,11 +134,51 @@ public structure VCGen.Context where
   once the program in `wp⟦e⟧` matches `pat`, before applying a spec. -/
   untilPat? : Option Sym.Pattern := none
 
+/-- Per-alt binder layout of a join point's split: the segment sizes of the alt telescope the body
+split introduces at each jump site (`fields ++ overlaps ++ discrEqs ++ extraEqs`, per
+`MatcherApp.TransformAltFVars.all`), and the number of alt binders of the synthetic spec (the
+matcher alt's own parameters: fields, then discriminant equations, or a single thunk parameter).
+Positions the spec binders within the jump-site telescope without unification. -/
+public structure JPAltLayout where
+  bodyFields : Nat
+  bodyOverlaps : Nat
+  bodyDiscrEqs : Nat
+  bodyExtraEqs : Nat
+  specBinders : Nat
+  deriving Inhabited
+
+/-- Length of the alt telescope the body split introduces at a jump site. -/
+public def JPAltLayout.bodyTeleLen (l : JPAltLayout) : Nat :=
+  l.bodyFields + l.bodyOverlaps + l.bodyDiscrEqs + l.bodyExtraEqs
+
+/-- Definition-site info for a `__do_jp` join point, indexed by the JP's let-fvar. Recorded when the
+JP is registered and consulted at each jump site to build the jump's payload for the alt-specific
+precondition mvar `hypsMVars[altIdx]`. -/
+public structure JPDefInfo where
+  /-- The join point's body proof, `∀ joinParams, Triple ⌜match discrs => ?Hᵢ⌝ (fv joinParams) Q`,
+  bound as a local hypothesis. Each jump is closed by `rel_trans` against `jpProof joinArgs`. -/
+  jpProof : Expr
+  /-- The precondition abstracted over the join params, `fun joinParams => ⌜match discrs => ?Hᵢ⌝`.
+  Applied at each jump to form the mid-point of the `rel_trans`, avoiding a walk over the post `Q`. -/
+  pjpBodyAbs : Expr
+  /-- Per-alt synthetic-opaque precondition mvars. Each has type
+  `(joinParams ++ altParams) → Prop`, assigned by `finalizeJPs`. -/
+  hypsMVars : Array MVarId
+  /-- Size of the local context at the JP definition site. Locals introduced beyond this index
+  are alt-local and get existentially closed when building the jump-site `φ`. -/
+  outerLCtxSize : Nat
+  /-- Per-alt binder layouts, aligned with `hypsMVars`. -/
+  altLayouts : Array JPAltLayout
+  /-- The largest `bodyTeleLen` over `altLayouts`: the length of the assumption-search window each
+  jump uses to discharge its branch hypotheses. -/
+  maxBodyTeleLen : Nat
+  deriving Inhabited
+
 public structure VCGen.Scope where
   /-- Spec database in scope: globals plus locals from in-scope hypotheses. -/
   specs : SpecTheorems
-  /-- `__do_jp` fvars currently in scope. -/
-  jps : FVarIdMap JumpSiteInfo := {}
+  /-- `__do_jp` fvars currently in scope, mapped to their def-site info. -/
+  jps : FVarIdMap JPDefInfo := {}
   /-- The most recently lifted pure precondition. `tryLiftedHyp` closes handoff VCs against
   it without walking the local context. -/
   lastLiftedPre? : Option FVarId := none
@@ -146,6 +186,25 @@ public structure VCGen.Scope where
   nextDeclIdx : Nat := 0
   deriving Inhabited
 
+/-- The applicable alternative of a JP jump: its index, the payload proposition (an existential
+closure of the join-argument equalities, abstracted over the alt-precondition mvar's binders), the
+witnesses for the payload's existentials, and the reduction `redProof : matchExpr = redExpr` of the
+precondition match to the alternative. -/
+public structure ResolvedJump where
+  altIdx : Nat
+  payload : Expr
+  witnesses : Array Expr
+  redExpr : Expr
+  redProof : Expr
+
+/-- A deferred join-point jump: its resolved alternative, the alt-precondition mvar it targets, and
+its open precondition subgoal `pre ⊑ ⌜match discrs => ?Hᵢ⌝ ss`. Resolved by `finalizeJPs`, which
+recovers everything else from the subgoal's type. -/
+public structure DeferredJump where
+  jump : ResolvedJump
+  hypsMVar : MVarId
+  goal : MVarId
+
 public structure VCGen.State where
   /--
   A cache mapping registered SpecThms to their backward rule to apply.
@@ -207,15 +266,19 @@ public structure VCGen.State where
   this to know which user-provided alts have already been consumed (so it doesn't
   warn about them). -/
   inlineHandledInvariants : Std.HashSet Nat := {}
+  /-- All join-point alt-precondition mvars, in registration order. Assigned by `finalizeJPs`. -/
+  jpHypsMVars : Array MVarId := #[]
+  /-- Deferred join-point jumps, in jump order. Discharged by `finalizeJPs`. -/
+  jpJumps : Array DeferredJump := #[]
 
 public abbrev VCGenM := ReaderT VCGen.Context (StateRefT VCGen.State Grind.GrindM)
 
 namespace VCGen
 
-public def Scope.registerJP (s : Scope) (fv : FVarId) (info : JumpSiteInfo) : Scope :=
+public def Scope.registerJP (s : Scope) (fv : FVarId) (info : JPDefInfo) : Scope :=
   { s with jps := s.jps.insert fv info }
 
-public def Scope.knownJP? (s : Scope) (fv : FVarId) : Option JumpSiteInfo :=
+public def Scope.knownJP? (s : Scope) (fv : FVarId) : Option JPDefInfo :=
   s.jps.get? fv
 
 public def Scope.insertSpec (s : Scope) (thm : SpecTheorem) : Scope :=
@@ -229,7 +292,10 @@ public def Scope.collectLocalSpecs (scope : Scope) (goal : MVarId) : VCGenM Scop
     let lctx ← getLCtx
     if scope.nextDeclIdx == lctx.decls.size then return scope
     let scope ← lctx.foldlM (init := scope) (start := scope.nextDeclIdx) fun scope decl => do
-      if decl.isAuxDecl then return scope
+      -- Skip implementation-detail hypotheses (e.g. the `+jp` body proof `__do_jp_spec`, the
+      -- `__do_jp` continuation): they are never user specs, and building a spec pattern from one
+      -- runs `preprocessType` over its post, scaling with the continuation.
+      if decl.isImplementationDetail then return scope
       try
         if let some thm ← mkSpecTheoremFromLocal decl.fvarId (eval_prio low) then
           return scope.insertSpec thm
diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean
index f40d2df51a1f..63d5c5d066fd 100644
--- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean
@@ -62,10 +62,11 @@ each in `State.invariants` (1-based stable index) and try to inline-elaborate
 its matching user alt. Returns the remaining non-invariant subgoals for `work`
 to enqueue. Eager handling here ensures dependent VCs see `?inv` assigned by
 the time they reach `emitVC`. -/
-private def handleInvariantSubgoals (subgoals : List MVarId) : VCGenM (Array MVarId) := do
+private def handleInvariantSubgoals (subgoals : List (Scope × MVarId)) :
+    VCGenM (Array (Scope × MVarId)) := do
   let env ← getEnv
-  let mut others : Array MVarId := #[]
-  for sg in subgoals do
+  let mut others : Array (Scope × MVarId) := #[]
+  for (scope, sg) in subgoals do
     if isSpecInvariantType env (← sg.getType) then
       let n := (← get).invariants.size + 1
       modify fun s => { s with invariants := s.invariants.push sg }
@@ -74,7 +75,7 @@ private def handleInvariantSubgoals (subgoals : List MVarId) : VCGenM (Array MVa
       else
         sg.setKind .syntheticOpaque
     else
-      others := others.push sg
+      others := others.push (scope, sg)
   return others
 
 /--
@@ -111,18 +112,19 @@ public def work (scope : Scope) (goal : Grind.Goal) : VCGenM Unit := do
     match ← solve s.scope goal.mvarId with
     | .stop _reason =>
       emitVC goal
-    | .goals scope subgoals =>
+    | .goals scopedSubgoals =>
       -- Handle invariant subgoals eagerly here, so that VC subgoals popped
       -- from the worklist later see the invariant MVar already assigned.
       -- Non-invariant subgoals go to the worklist as usual and will eventually go through `emitVC`.
-      let subgoals ← handleInvariantSubgoals subgoals
+      let kept ← handleInvariantSubgoals scopedSubgoals
       let goal ←
-        if subgoals.size > 1 then
+        if kept.size > 1 then
           processHypotheses goal
         else
           pure goal
-      worklist := worklist ++ subgoals.reverse.map (fun mv =>
+      worklist := worklist ++ kept.reverse.map (fun (scope, mv) =>
         { goal := { goal with mvarId := mv }, scope })
+  finalizeJPs
 
 public structure Result where
   /-- All invariant goals emitted during VC generation, in emit order. The MVarId at
diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean
index 21332e35c5b0..c716a5533cbb 100644
--- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean
@@ -44,11 +44,15 @@ public inductive SolveResult.StopReason where
 
 /-- The result of one `solve` step of VC generation. -/
 public inductive SolveResult where
-  /-- Successfully decomposed the goal. These are the subgoals, sharing `scope`. -/
-  | goals (scope : VCGen.Scope) (subgoals : List MVarId)
+  /-- Successfully decomposed the goal. Each subgoal carries its own scope. -/
+  | goals (subgoals : List (VCGen.Scope × MVarId))
   /-- No further progress possible; emit the current goal as a VC. -/
   | stop (reason : SolveResult.StopReason)
 
+/-- Decomposition result whose subgoals all share `scope`. -/
+public def SolveResult.goalsInScope (scope : VCGen.Scope) (subgoals : List MVarId) : SolveResult :=
+  .goals (subgoals.map (scope, ·))
+
 private def isDuplicable (e : Expr) : Bool := match e with
   | .bvar .. | .mvar .. | .fvar .. | .const .. | .lit .. | .sort .. => true
   | .mdata _ e | .proj _ _ e => isDuplicable e
@@ -73,19 +77,10 @@ private def forallIntro? (goal : MVarId) (target : Expr) : VCGenM (Option (List
     throwError "Failed to intro forall target {goal}"
   return some [goal']
 
-private def throwIfUnsupportedJP (name : Name) (val : Expr) : VCGenM Unit := do
-  if (← read).useJP && Lean.Elab.Tactic.Do.isJP name && val.isLambda then
-    throwError "vcgen: shared-continuation handling for `__do_jp` is not yet \
-      implemented. Detection point reached at {name}; the upstream \
-      `Lean.Elab.Tactic.Do.onJoinPoint` (`src/Lean/Elab/Tactic/Do/VCGen.lean:215`) \
-      needs to be ported to the worklist style. Drop `(jp := true)` to fall back \
-      to the default zeta-unfold behaviour."
-
 /-- Strategy 2: zeta-substitute a duplicable top-level `let` in the target, otherwise
 introduce it into the local context. -/
 private def targetLetIntro? (goal : MVarId) (target : Expr) : VCGenM (Option MVarId) := do
   let .letE name _ val body _ := target | return none
-  throwIfUnsupportedJP name val
   if isDuplicable val then
     trace[Elab.Tactic.Do.vcgen] "let-zeta-dup: {name}"
     return some (← goal.replaceTargetDefEqFast (← Sym.instantiateRevBetaS body #[val]))
@@ -113,7 +108,11 @@ Runs before the precondition lift so a spec handoff `pre ⊑ specPre` closes by
 than an assumption search. The pattern matcher keeps synthetic-opaque invariant holes rigid, so
 `⊤ ⊑ ?inv args` is left untouched. -/
 private def rfl? (goal : MVarId) : VCGenM (Option (List MVarId)) := do
-  let .goals gs ← (← read).backwardRules.refl.apply goal | return none
+  -- Reflexivity is best-effort: the unifier throws on an un-decomposed program-head `let` (e.g. a
+  -- chained `__do_jp`) rather than reporting "not equal". A throw leaves `goal` unassigned, so
+  -- treat it as "not reflexive here" and let `wp` decomposition handle the `let`.
+  let .goals gs ← try (← read).backwardRules.refl.apply goal catch _ => return none
+    | return none
   trace[Elab.Tactic.Do.vcgen] "Solved by rfl {goal}"
   return some gs
 
@@ -221,11 +220,24 @@ private def wpConsumeMData? (goal : MVarId) (info : WPApp) : VCGenM (Option MVar
   let .mdata .. := info.prog | return none
   return some (← replaceProgDefEq goal info info.prog.consumeMData)
 
+/-- `+jp`: wrap the continuation of a `__do_jp` let in `jpGadget`, tagging the join point so the
+usual let-introduction runs (`wpLet?`) and `tryJPGadget?` then registers it. -/
+private def tryMarkJP? (goal : MVarId) (info : WPApp) : VCGenM (Option MVarId) := do
+  unless (← read).useJP do return none
+  let .letE name ty val body nondep := info.prog.getAppFn | return none
+  unless Lean.Elab.Tactic.Do.isJP name do return none
+  unless val.isLambda do return none
+  if body.getAppFn.isConstOf ``Std.Internal.Do.jpGadget then return none
+  let uα ← Sym.getLevel info.Prog
+  let uβ ← Sym.getLevel ty
+  let wrapped := Expr.letE name ty val
+    (mkAppN (mkConst ``Std.Internal.Do.jpGadget [uα, uβ]) #[info.Prog, ty, .bvar 0, body]) nondep
+  return some (← replaceProgDefEq goal info (← mkAppRevS wrapped info.prog.getAppRevArgs))
+
 /-- Strategy 11a: hoist or zeta-substitute a `let` from the program head. -/
 private def wpLet? (goal : MVarId) (info : WPApp) : VCGenM (Option MVarId) := do
   let .letE name type val body nondep := info.prog.getAppFn | return none
   let appArgs := info.prog.getAppRevArgs
-  throwIfUnsupportedJP name val
   if isDuplicable val then
     trace[Elab.Tactic.Do.vcgen] "let-zeta-dup: {name}"
     let body' ← Sym.instantiateRevBetaS body #[val]
@@ -245,6 +257,112 @@ private def wpLet? (goal : MVarId) (info : WPApp) : VCGenM (Option MVarId) := do
       | throwError "Failed to intro hoisted let"
     return some goal
 
+/-- The per-alt body-side binder segment sizes of `JPAltLayout` (`bodyFields`/`bodyOverlaps`/
+`bodyDiscrEqs`/`bodyExtraEqs`), computed the same way the actual jump-site split introduces them
+(`mkBackwardRuleForSplit`, splitter form with added equalities). `specBinders` is left `0` and filled
+by the caller from the spec-side split. -/
+private def computeBodyAltLayouts (sinfo : Lean.Elab.Tactic.Do.SplitInfo) (progTy : Expr) :
+    MetaM (Array JPAltLayout) := do
+  match sinfo with
+  | .ite _ | .dite _ =>
+    -- The body split forces the splitter (`dite`) form, whose alt telescope is exactly the single
+    -- condition proof; the spec-side split leaves 0 alt binders, reconciled by the `min`-based pairing.
+    let one : JPAltLayout :=
+      { bodyFields := 1, bodyOverlaps := 0, bodyDiscrEqs := 0, bodyExtraEqs := 0, specBinders := 0 }
+    return #[one, one]
+  | .matcher _ =>
+    let ref ← IO.mkRef (#[] : Array JPAltLayout)
+    discard <| sinfo.withAbstract progTy fun abstractInfo _ =>
+      abstractInfo.splitWith (mkSort .zero) (useSplitter := true)
+          fun _name _expAltType _idx altFVars => do
+        ref.modify (·.push
+          { bodyFields := altFVars.fields.size, bodyOverlaps := altFVars.overlaps.size
+            bodyDiscrEqs := altFVars.discrEqs.size, bodyExtraEqs := altFVars.extraEqs.size
+            specBinders := 0 })
+        pure (mkConst ``True)
+    ref.get
+
+/-- `+jp`: at `wp⟦jpGadget fv rest⟧` with `rest` an `if`/`match`, register the join point `fv` and
+split into two subgoals, the JP body (proved once, bound as the `__do_jp_spec` hypothesis and closed
+against by every jump) and the (gadget-stripped) `rest`.
+
+The body's precondition splits the same way as `rest`: in branch `i` it is a fresh metavariable
+`?Hᵢ`, which the jumps reaching that branch fill in with the facts that hold there, and `finalizeJPs`
+assigns the disjunction of. -/
+private def tryJPGadget? (scope : Scope) (goal : MVarId) (info : WPApp) :
+    VCGenM (Option SolveResult) := do
+  let_expr Std.Internal.Do.jpGadget _α _β fv rest := info.prog | return none
+  let some fvId := fv.fvarId? | return none
+  goal.withContext do
+  -- Strip the gadget for the rest subgoal.
+  let restGoal ← replaceProgDefEq goal info rest
+  let some sinfo ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? rest
+    | return some (.goalsInScope scope [restGoal])
+  let some resTy := sinfo.resTy
+    | return some (.goalsInScope scope [restGoal])
+  let Q := info.post
+  let joinTy ← Sym.inferType fv
+  let numJoinParams ← liftMetaM <| Lean.Elab.Tactic.Do.getNumJoinParams joinTy resTy
+
+  -- Create the `?Hᵢ` mvars in the outer local context so they stay shared across jump sites.
+  let outerLCtx ← liftMetaM getLCtx
+  let outerLocalInsts ← liftMetaM getLocalInstances
+  let instCL ← liftMetaM <| Meta.synthInstance (← Meta.mkAppM ``Lean.Order.CompleteLattice #[info.Pred])
+  let (bodyTy, pjpBodyAbs, hypsMVars, specSizes) ← liftMetaM <|
+    Meta.forallBoundedTelescope joinTy numJoinParams fun joinParams _ => do
+      let hypsMVarsRef ← IO.mkRef (#[] : Array MVarId)
+      let specSizesRef ← IO.mkRef (#[] : Array Nat)
+      -- Split the precondition at `Prop` (each `?Hᵢ` produces a `Prop`) and embed the match via `⌜·⌝`.
+      -- Each jump discharges its instance by construction (`ofProp_eq_top` of the witnessed alt); the
+      -- body proof case-splits the bare `Prop` match that `⌜φ⌝ s` reduces to.
+      let propMatch ← sinfo.splitWith (mkSort .zero) (useSplitter := false)
+          fun _name _expAltType _idx altFVars => do
+        let allBinders := joinParams ++ altFVars.all
+        let mvarTy ← Meta.mkForallFVars allBinders (mkSort .zero)
+        let hypsMVar ← Meta.mkFreshExprMVarAt outerLCtx outerLocalInsts mvarTy .syntheticOpaque
+        hypsMVarsRef.modify (·.push hypsMVar.mvarId!)
+        specSizesRef.modify (·.push altFVars.all.size)
+        pure (mkAppN hypsMVar allBinders)
+      let pjpBody ← Meta.mkAppOptM ``Lean.Order.CompleteLattice.ofProp #[info.Pred, instCL, propMatch]
+      let tripleTy ← Meta.mkAppOptM ``Std.Internal.Do.Triple
+        #[info.Pred, info.EPred, info.Prog, info.Value, info.instAL, info.instEAL,
+          mkAppN fv joinParams, info.instWP, pjpBody, Q, info.epost]
+      pure (← Meta.mkForallFVars joinParams tripleTy, ← Meta.mkLambdaFVars joinParams pjpBody,
+        ← hypsMVarsRef.get, ← specSizesRef.get)
+
+  let bodyLayouts ← liftMetaM <| computeBodyAltLayouts sinfo info.Prog
+  unless bodyLayouts.size == specSizes.size do
+    throwError "vcgen +jp: alt count mismatch between spec and body splits of{indentExpr rest}"
+  let altLayouts := bodyLayouts.zipWith (fun layout sB => { layout with specBinders := sB }) specSizes
+
+  -- `finalizeJPs` assigns each `?Hᵢ` the disjunction of its recorded jump payloads (`False` when
+  -- no jump reaches the alt, e.g. behind an early `return` or a `throw`).
+  modify fun s => { s with jpHypsMVars := s.jpHypsMVars ++ hypsMVars }
+
+  -- The telescope built this with `MetaM` primitives; internalize it once here, so the jumps'
+  -- `betaS` applications of it stay on sharing-preserving `SymM` primitives. `bodyTy` is left as
+  -- built: it embeds the post `Q` and the `?Hᵢ` mvars, so hash-consing it would re-walk the
+  -- continuation at every registration.
+  let pjpBodyAbs ← shareCommonInc pjpBodyAbs
+
+  let bodyMV ← liftMetaM <| Meta.mkFreshExprSyntheticOpaqueMVar bodyTy (← goal.getTag)
+  -- Bind the body proof as a local hypothesis so each jump references it by fvar (`jpProof joinArgs`),
+  -- keeping the shared continuation proof in one `let` binding that survives proof-term instantiation.
+  -- `Sym.introN` derives the declaration kind from the `__`-prefixed name, so the hypothesis is an
+  -- implementation detail and stays out of local-spec collection and assumption search.
+  let restGoal ← liftMetaM <| restGoal.define `__do_jp_spec bodyTy bodyMV
+  let .goal newDecls restGoal ← Sym.introN restGoal 1
+    | throwError "vcgen +jp: failed to introduce the join point body proof"
+  let jpProofFVar := newDecls[0]!
+
+  let outerLCtxSize := (← restGoal.getDecl).lctx.numIndices
+  let maxBodyTeleLen := altLayouts.foldl (fun acc l => max acc l.bodyTeleLen) 0
+  let jpDefInfo : JPDefInfo :=
+    { jpProof := .fvar jpProofFVar, pjpBodyAbs, hypsMVars, outerLCtxSize, altLayouts, maxBodyTeleLen }
+  -- `bodyMV` keeps the original scope so its own head is not treated as a JP.
+  let restScope := scope.registerJP fvId jpDefInfo
+  return some (.goals [(restScope, restGoal), (scope, bodyMV.mvarId!)])
+
 /-- Strategy 11b: split an `ite`/`dite`/match program, or iota-reduce a matcher with a concrete
 discriminant. -/
 private def wpMatch? (goal : MVarId) (info : WPApp) :
@@ -264,11 +382,12 @@ private def wpMatch? (goal : MVarId) (info : WPApp) :
     | .closed => continue
   return some simpGoals.toList
 
-/-- Strategy 11c: zeta-unfold a local let-bound fvar used as the program head. -/
-private def wpFVarZeta? (goal : MVarId) (info : WPApp) :
+/-- Strategy 11c: zeta-unfold a let-bound fvar used as the program head, unless it is a registered JP. -/
+private def wpFVarZeta? (scope : VCGen.Scope) (goal : MVarId) (info : WPApp) :
     VCGenM (Option MVarId) := do
   let f := info.prog.getAppFn
   let some fvarId := f.fvarId? | return none
+  if (scope.knownJP? fvarId).isSome then return none
   let some val ← fvarId.getValue? | return none
   trace[Elab.Tactic.Do.vcgen] "fvar-zeta: {(← fvarId.getUserName)}"
   let prog ← shareCommonInc (val.betaRev info.prog.getAppRevArgs)
@@ -296,6 +415,219 @@ private def stopOrErrorOnMissingSpec (prog monad : Expr) (thms : Array SpecTheor
     throwError "No spec matching the monad {monad} found for program {prog}. \
       Candidates were {thms.map (·.proof)}."
 
+/-- At a JP jump site `__do_jp args`, build this jump's `ResolvedJump`. `finalizeJPs` assigns `?Hᵢ` the
+disjunction of its jumps' payloads and discharges each jump by construction.
+
+The applicable alt and its reduction are found by rewriting the precondition match, discharging the
+branch condition / matcher congruence hypotheses by an assumption search bounded to the locals
+introduced since the join point was registered (context index `≥ outerLCtxSize`). Because the
+`__do_jp` let is always outer to the split whose branches jump to it, that slice holds exactly the
+enclosing split's hypotheses, so the search is bounded by the local nesting rather than the whole
+context. -/
+private def mkJPJumpPayload? (jpInfo : JPDefInfo) (e matchExpr : Expr) :
+    VCGenM (Option ResolvedJump) := do
+  let joinArgs := e.getAppArgs
+  let lctx ← liftMetaM getLCtx
+  -- Locals introduced since the join point was registered. The enclosing split's alt telescope
+  -- (`fields ++ overlaps ++ discrEqs ++ extraEqs`, of length `bodyTeleLen`) sits at the front and
+  -- pairs positionally with the recorded `JPAltLayout`; the locals past it are `∃`-closed below.
+  let slice := lctx.foldl (init := #[]) (start := jpInfo.outerLCtxSize) Array.push
+  -- The branch hypotheses a jump needs are that telescope, whose length is at most `maxBodyTeleLen`.
+  -- So confining the assumption search to `[outerLCtxSize, outerLCtxSize + maxBodyTeleLen)` covers
+  -- every alt's full discriminant evidence in a fixed window, independent of how deep the jump sits.
+  let upperBound := jpInfo.outerLCtxSize + jpInfo.maxBodyTeleLen
+  let mut found : Option (Nat × Expr × Expr) := none
+  for idx in [:jpInfo.altLayouts.size] do
+    let red ← liftMetaM <| Lean.Elab.Tactic.Do.rwIfOrMatcher idx matchExpr
+      (assumptionLowerBound := jpInfo.outerLCtxSize) (assumptionUpperBound := upperBound)
+    let some redProof := red.proof? | continue
+    found := some (idx, red.expr, redProof)
+    break
+  let some (altIdx, redExpr, redProof) := found | return none
+  let hypsMVar := jpInfo.hypsMVars[altIdx]!
+  trace[Elab.Tactic.Do.vcgen] "JP jump: alt {altIdx} args={joinArgs}"
+  let layout := jpInfo.altLayouts[altIdx]!
+  -- The mvar type is the syntactic `∀`-chain built at registration, so no reducing telescope.
+  Meta.forallTelescope (← liftMetaM hypsMVar.getType) fun allBinders _ => do
+      let numJP := joinArgs.size
+      unless numJP ≤ allBinders.size do return none
+      let jpBinders := allBinders.extract 0 numJP
+      let altBinders := allBinders.extract numJP allBinders.size
+      -- The leading jump-site locals are the body split's alt telescope,
+      -- `fields ++ overlaps ++ discrEqs ++ extraEqs` with the sizes recorded in `layout`. The mvar's
+      -- alt binders are the fields and discrEqs of the spec-side split, so they pair positionally;
+      -- the remaining telescope binders are the split's own bookkeeping, which the consuming side
+      -- re-derives when it splits the match/ite hypothesis, and are dropped. Locals beyond the
+      -- telescope (inner split conditions, monadic binders) are kept and closed over below.
+      -- The spec binders are the matcher alt's own parameters, fields first and then discriminant
+      -- equations; a thunked nullary alt has a single `Unit` parameter on the spec side only, which
+      -- stays unpaired and unused.
+      let pairedFields := min layout.specBinders layout.bodyFields
+      let pairedEqs := min (layout.specBinders - pairedFields) layout.bodyDiscrEqs
+      unless altBinders.size == layout.specBinders &&
+          layout.bodyTeleLen ≤ slice.size &&
+          layout.specBinders - pairedFields - pairedEqs ≤ 1 do
+        throwError "vcgen +jp: jump-site telescope does not match the recorded alt layout for \
+          {indentExpr e}"
+      let eqStart := layout.bodyFields + layout.bodyOverlaps
+      let matchedLocals := (slice.extract 0 pairedFields ++ slice.extract eqStart (eqStart + pairedEqs))
+        |>.map LocalDecl.toExpr
+      let matchedBinders := altBinders.extract 0 (pairedFields + pairedEqs)
+      let eqs ← jpBinders.mapIdxM fun i jp => do
+        let τ ← Sym.inferType jp
+        return mkApp3 (mkConst ``Eq [← Sym.getLevel τ]) τ jp joinArgs[i]!
+      -- Locals past the telescope are `∃`/`let`-closed. Implementation-detail decls (compiler
+      -- internal) must never become `∃` binders or witnesses, so drop them here.
+      let restDecls := slice.filter (fun decl => !decl.isImplementationDetail)
+        (start := layout.bodyTeleLen)
+      let restLocals := restDecls.map LocalDecl.toExpr
+      -- `∃ rest, joinParams = joinArgs`, existentially/let-closing the kept locals; the paired ones
+      -- are then rewritten to the mvar's own alt binders.
+      let (_, φPropClosed) ← restDecls.foldrM (init := (restLocals, (mkAndN eqs.toList).abstract restLocals))
+          fun decl (locals, φ) => do
+        let locals := locals.pop
+        let type := (← instantiateMVarsS decl.type).abstract locals
+        match decl.value? with
+        | some v =>
+          let val := (← instantiateMVarsS v).abstract locals
+          return (locals, Lean.mkLet decl.userName type val φ (nondep := decl.isNondep))
+        | none =>
+          let typeLevel ← Sym.getLevel decl.type
+          return (locals, mkApp2 (mkConst ``Exists [typeLevel]) type (Expr.lam decl.userName type φ .default))
+      let φPropClosed := φPropClosed.replaceFVars matchedLocals matchedBinders
+      -- The `∃` binders are exactly the non-let rest locals, in order; hand them back as witnesses.
+      return some {
+        altIdx, redExpr, redProof
+        payload := ← liftMetaM <| Meta.mkLambdaFVars allBinders φPropClosed
+        witnesses := (restDecls.filter (·.value?.isNone)).map LocalDecl.toExpr }
+
+/-- Build the proof of `∃ locals, ⋀ joinParams = joinArgs`, supplying each `∃` binder from
+`witnesses` (the actual locals) and closing the residual equalities by `rfl`. Every node of the
+payload is built by `mkJPJumpPayload?`, so its shape is matched syntactically: `let`-closed locals
+zeta-reduce as they are passed and the universe levels are read off the payload's own constants. -/
+private partial def mkJPWitness (ty : Expr) (witnesses : List Expr) : MetaM Expr := do
+  if let .letE _ _ v b _ := ty then
+    return ← mkJPWitness (b.instantiate1 v) witnesses
+  match_expr ty with
+  | Exists α p =>
+    let w :: ws := witnesses | throwError "JP witness underflow"
+    return mkApp4 (mkConst ``Exists.intro ty.getAppFn.constLevels!) α p w
+      (← mkJPWitness (p.beta #[w]) ws)
+  | And a b =>
+    return mkApp4 (mkConst ``And.intro) a b (← mkJPWitness a witnesses) (← mkJPWitness b witnesses)
+  | True => return mkConst ``True.intro
+  | Eq α lhs _ => return mkApp2 (mkConst ``Eq.refl ty.getAppFn.constLevels!) α lhs
+  | _ => throwError "JP witness: unexpected residual{indentExpr ty}"
+
+/-- Prove disjunct `idx` of the `count`-fold right-nested disjunction `φ`, witnessing the selected
+disjunct via `mkJPWitness`. -/
+private partial def proveJPDisjunct (φ : Expr) (idx count : Nat) (witnesses : List Expr) :
+    MetaM Expr := do
+  if count == 1 then
+    mkJPWitness φ witnesses
+  else
+    let_expr Or a b := φ | throwError "JP finalization: expected disjunction{indentExpr φ}"
+    match idx with
+    | 0 => return mkApp3 (mkConst ``Or.inl) a b (← proveJPDisjunct a 0 1 witnesses)
+    | idx + 1 => return mkApp3 (mkConst ``Or.inr) a b (← proveJPDisjunct b idx (count - 1) witnesses)
+
+/-- Discharge a recorded JP jump: prove its own disjunct (number `idx` of `count`) of the assigned
+`?Hᵢ`, then close the jump goal `pre ⊑ (⌜match discrs => ?Hᵢ⌝ : Pred) ss` with it, built by
+construction from the goal's own type. The disjunct proof `φPrf : redExpr` is transported across the
+match reduction (`Eq.mpr redProof`) to `hMatch : matchExpr`, then `le_ofProp` at the postcondition
+lattice with the constant precondition `fun _ => pre` yields `(fun _ => pre) ⊑ ⌜matchExpr⌝`; applying
+the state args reduces the sides to `pre` and the goal's `rhs` by `β`-reduction, which the kernel
+discharges. -/
+private def dischargeJPJump (r : DeferredJump) (idx count : Nat) : VCGenM Unit :=
+  r.goal.withContext do
+    let goalTy ← r.goal.getType
+    let_expr Lean.Order.PartialOrder.rel _α _inst pre rhs := goalTy
+      | throwError "vcgen +jp: unexpected jump goal{indentExpr goalTy}"
+    -- `rhs` is `ofProp Pred instCL matchExpr s₁ … sₙ`; `ofProp` and `le_ofProp` share the auto-bound
+    -- `l : Type u`, so its const level instantiates both.
+    let ofPropFn := rhs.getAppFn
+    let rhsArgs := rhs.getAppArgs
+    unless ofPropFn.isConstOf ``Lean.Order.CompleteLattice.ofProp && rhsArgs.size ≥ 3 do
+      throwError "vcgen +jp: jump precondition is not a `⌜·⌝` embedding{indentExpr rhs}"
+    let Pred := rhsArgs[0]!
+    let instCL := rhsArgs[1]!
+    let matchExpr := rhsArgs[2]!
+    let ss := rhsArgs.extract 3 rhsArgs.size
+    let φPrf ← liftMetaM <|
+      proveJPDisjunct (← instantiateMVarsS r.jump.redExpr) idx count r.jump.witnesses.toList
+    -- `matchExpr : Prop`, so its reduction equality lives at `Prop`; `Eq.mpr` transports `φPrf` back.
+    let hMatch := mkApp4 (mkConst ``Eq.mpr [.zero]) matchExpr r.jump.redExpr r.jump.redProof φPrf
+    -- `fun _ => pre` at the postcondition lattice; the binder domains are `Pred`'s own.
+    let mut stateTys : Array Expr := #[]
+    let mut PredIt := Pred
+    for _ in [:ss.size] do
+      stateTys := stateTys.push PredIt.bindingDomain!
+      PredIt := PredIt.bindingBody!
+    let constFn := stateTys.foldr (fun ty body => Expr.lam `s ty body .default) pre
+    let base := mkAppN (mkConst ``Lean.Order.le_ofProp ofPropFn.constLevels!)
+      #[Pred, instCL, constFn, matchExpr, hMatch]
+    r.goal.assign (← mkAppNS base ss)
+
+/-- Assign every `+jp` alt-precondition mvar `?Hᵢ` the disjunction of the payloads its recorded
+jumps provided (`False` when no jump reaches the alt, e.g. behind an early `return` or a `throw`),
+then discharge each recorded jump goal with its own disjunct. -/
+public def finalizeJPs : VCGenM Unit := do
+  let s ← get
+  if s.jpHypsMVars.isEmpty then return
+  let grouped : Std.HashMap MVarId (Array DeferredJump) :=
+    s.jpJumps.foldl (init := {}) fun m r =>
+      m.alter r.hypsMVar (fun rs? => some ((rs?.getD #[]).push r))
+  for mv in s.jpHypsMVars do
+    let records := grouped.getD mv #[]
+    unless ← mv.isAssigned do
+      liftMetaM <| Meta.forallTelescope (← mv.getType) fun bs _ => do
+        let props := records.map (·.jump.payload.beta bs)
+        let φ := match props.back? with
+          | none => mkConst ``False
+          | some last => props.pop.foldr (init := last) mkOr
+        mv.assign (← Meta.mkLambdaFVars bs φ)
+    for h : i in [:records.size] do
+      dischargeJPJump records[i] i records.size
+
+/-- Close a JP jump `fv joinArgs` directly against the join point's body proof, bypassing the spec
+and backward-rule machinery. Join points are tail-called, so the use-site post equals the body's post
+up to definitional equality; the proof is `rel_trans hPre (jpProof joinArgs ss)` with `hPre` the
+recorded precondition VC `pre ⊑ ⌜match discrs => ?Hᵢ⌝ ss`, and the post equality is left to the kernel.
+Building the proof term touches neither the post nor a discrimination-tree pattern, so it stays O(1)
+in the size of the continuation. -/
+private def tryJPJump? (scope : Scope) (goal : MVarId) (info : WPApp) : VCGenM (Option SolveResult) := do
+  let some fvId := info.prog.getAppFn.fvarId? | return none
+  let some jpInfo := scope.knownJP? fvId | return none
+  let joinArgs := info.prog.getAppArgs
+  -- `pjpBodyAbs` is a lambda over the join params; beta-reduce so the head is `⌜·⌝` (`ofProp`).
+  -- The precondition carries no post `Q`, so this stays cheap. `betaS` keeps the result shared,
+  -- since it flows into the deferred subgoal's type below.
+  let ofPropMatch ← betaS jpInfo.pjpBodyAbs joinArgs
+  let_expr Lean.Order.CompleteLattice.ofProp _ _ matchExpr := ofPropMatch
+    | throwError "vcgen +jp: join point precondition is not a `⌜·⌝` embedding{indentExpr ofPropMatch}"
+  let some jump ← mkJPJumpPayload? jpInfo info.prog matchExpr
+    | throwError "vcgen +jp: could not resolve the alternative of jump{indentExpr info.prog}"
+  goal.withContext do
+    let goalTy ← goal.getType
+    let_expr Lean.Order.PartialOrder.rel α inst pre zGoal := goalTy | return none
+    let lvls := goalTy.getAppFn.constLevels!
+    let ss := info.excessArgs
+    -- `jpProof joinArgs : Triple …` is a one-field structure; project its `⊑ wp` field (`Triple.le_wp`)
+    -- before applying the excess state args, which the function-lattice `⊑` accepts pointwise.
+    let jpRel := Expr.proj ``Std.Internal.Do.Triple 0 (← mkAppNS jpInfo.jpProof joinArgs)
+    let jpAppliedSS ← mkAppNS jpRel ss
+    let yBase ← mkAppNS ofPropMatch ss
+    let hPreTy ← mkAppNS (mkConst ``Lean.Order.PartialOrder.rel lvls) #[α, inst, pre, yBase]
+    let hPre ← liftMetaM <| Meta.mkFreshExprSyntheticOpaqueMVar hPreTy (← goal.getTag)
+    let proof ← mkAppNS (mkConst ``Lean.Order.PartialOrder.rel_trans lvls)
+      #[α, inst, pre, yBase, zGoal, hPre, jpAppliedSS]
+    goal.assign proof
+    -- Record the jump's precondition subgoal for `finalizeJPs`.
+    let record : DeferredJump :=
+      { jump, hypsMVar := jpInfo.hypsMVars[jump.altIdx]!, goal := hPre.mvarId! }
+    modify fun s => { s with jpJumps := s.jpJumps.push record }
+    return some (.goalsInScope scope [])
+
 /-- Select the highest-priority `@[spec]` theorem matching `prog`, or a stop result when none matches.
 Hands `findSpecs` the sole reference to the spec database so its in-place pattern internalization does
 not copy the discrimination tree, then threads the updated database back into the returned scope. -/
@@ -322,8 +654,7 @@ private def applySpec (scope : VCGen.Scope) (goal : MVarId) (info : WPApp) (thm
     VCGenM SolveResult := do
   trace[Elab.Tactic.Do.vcgen] "Applying spec {thm.proof} for {info.prog}. Excess args: {info.excessArgs}"
   let some rule ←
-    try
-      mkBackwardRuleFromSpecCached thm info |>.run
+    try (mkBackwardRuleFromSpecCached thm info).run
     catch ex =>
       throwError "Failed to construct rule {thm.proof} for {indentExpr info.prog}\n\
         error: {ex.toMessageData}\n\
@@ -344,7 +675,7 @@ private def applySpec (scope : VCGen.Scope) (goal : MVarId) (info : WPApp) (thm
         Pred:{indentExpr info.Pred}\n\
         excessArgs: {info.excessArgs}\n\
         rule type:{indentExpr ruleType}"
-  return .goals scope goals
+  return .goalsInScope scope goals
 
 /-- True iff the program matches the `until` pattern, in which case VC generation stops at this
 goal. -/
@@ -380,13 +711,15 @@ private def elabFrame (resourceTy : Expr) (entry : FrameEntry) (res : Sym.MatchU
   for h : i in [0:entry.varNames.size] do
     if let some nm := entry.varNames[i] then
       if h2 : i < res.args.size then
-        decls := decls.push (nm, ← Meta.inferType res.args[i]!, res.args[i]!)
+        decls := decls.push (nm, ← Sym.inferType res.args[i]!, res.args[i]!)
   Meta.withDefault <| withLetDeclsDND decls fun fvs => do
     let frameExpr ← Lean.Elab.Term.TermElabM.run' do
       let e ← Lean.Elab.Term.elabTermEnsuringType entry.frameStx (some resourceTy)
       Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
       mkLetFVars fvs e
-    instantiateMVarsS frameExpr
+    -- The elaborated frame enters the goals, so hash-cons it; `instantiateMVarsS` alone returns an
+    -- mvar-free elaboration unshared.
+    shareCommon (← liftMetaM <| instantiateMVars frameExpr)
 
 /-- Find an unretired `frames` alternative matching the program (earliest source order wins),
 elaborate its frame at the resource type `resourceTy`, and retire it so it applies at most once. -/
@@ -465,23 +798,25 @@ private def applyFrameOrSpec (scope : VCGen.Scope) (goal : MVarId) (pre : Expr)
   let fp := info.M.getAppFn.constName?.bind (procs[·]?) |>.getD meetFrameProc
   let resourceTy ← fp.resourceTy info
   if let some F ← matchFrame? resourceTy info then
-    return .goals scope (← applyFrameRule goal info fp F)
+    return .goalsInScope scope (← applyFrameRule goal info fp F)
   let some proc := fp.proc | return ← applySpec scope goal info thm
   -- Apply the spec speculatively, then let the frame procedure inspect its precondition VC. No frame
   -- keeps the application; a frame rolls it back and frames instead.
   let saved ← Meta.saveState
-  let .goals _ subgoals ← applySpec scope goal info thm
+  let .goals scopedSubgoals ← applySpec scope goal info thm
     | throwError "vcgen: speculative spec application for{indentExpr info.prog} did not produce goals"
+  let subgoals := scopedSubgoals.map Prod.snd
   let frame? ← match ← specPreOf? subgoals with
     | some specPre => proc resourceTy pre info specPre
     | none => pure none
-  let some F := frame? | return .goals scope subgoals
+  let some F := frame? | return .goals scopedSubgoals
   -- Capture the frame before rolling back: `saved.restore` un-assigns the speculative metavariables,
-  -- so instantiate `F` against them now (and reshare).
-  let F ← instantiateMVarsS F
+  -- so instantiate `F` against them now. `shareCommonInc` hash-conses the frame even when it carried
+  -- no metavariables (which `instantiateMVarsS` returns unshared).
+  let F ← shareCommonInc (← instantiateMVarsS F)
   trace[Elab.Tactic.Do.vcgen] "`@[frameproc]` matched {info.prog}; frame:{indentExpr F}"
   saved.restore
-  return .goals scope (← applyFrameRule goal info fp F)
+  return .goalsInScope scope (← applyFrameRule goal info fp F)
 
 /--
 The main VC generation step. Operates on a plain `MVarId` with no knowledge of grind.
@@ -515,12 +850,12 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
   trace[Elab.Tactic.Do.vcgen] "🎯 Target: {target}"
 
   -- Phase 1: simplify `target` until it is of the form `pre ⊑ rhs`.
-  if let some g ← consumeMData? goal target then return .goals scope [g]
-  if let some gs ← forallIntro? goal target then return .goals scope gs
-  if let some g ← targetLetIntro? goal target then return .goals scope [g]
-  if let some g ← tripleUnfold? goal target then return .goals scope [g]
-  if let some g ← bareWPToLe? goal target then return .goals scope [g]
-  if let some gs ← liftedHypBare? scope goal target then return .goals scope gs
+  if let some g ← consumeMData? goal target then return .goalsInScope scope [g]
+  if let some gs ← forallIntro? goal target then return .goalsInScope scope gs
+  if let some g ← targetLetIntro? goal target then return .goalsInScope scope [g]
+  if let some g ← tripleUnfold? goal target then return .goalsInScope scope [g]
+  if let some g ← bareWPToLe? goal target then return .goalsInScope scope [g]
+  if let some gs ← liftedHypBare? scope goal target then return .goalsInScope scope gs
 
   let_expr PartialOrder.rel α inst pre rhs := target
     | return .stop (.noEntailment target)
@@ -533,8 +868,8 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
 
   -- Phase 2: close reflexive goals, then drive `pre` toward `⊤`, lifting any pure content so a
   -- later spec application sees a `⊤` precondition.
-  if let some gs ← rfl? goal then return .goals scope gs
-  if let some (scope, gs) ← normalizePre? scope goal α pre target then return .goals scope gs
+  if let some gs ← rfl? goal then return .goalsInScope scope gs
+  if let some (scope, gs) ← normalizePre? scope goal α pre target then return .goalsInScope scope gs
 
   -- Collect new local specs before any strategy that may emit multiple subgoals
   -- (`wpMatch?`, `splitLatticeOp?`) or apply a registered spec (`applySpec`).
@@ -542,10 +877,10 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
 
   -- Phase 3: shape the `rhs` (reduce an EPost projection, decompose a lattice connective or a
   -- forall, then discharge a residual entailment against the lifted hypothesis).
-  if let some g ← reduceEPostHead? goal target α inst pre rhs then return .goals scope [g]
-  if let some gs ← splitLatticeOp? goal rhs then return .goals scope gs
-  if let some gs ← splitForallLe? goal rhs then return .goals scope gs
-  if let some gs ← liftedHyp? scope goal α pre rhs then return .goals scope gs
+  if let some g ← reduceEPostHead? goal target α inst pre rhs then return .goalsInScope scope [g]
+  if let some gs ← splitLatticeOp? goal rhs then return .goalsInScope scope gs
+  if let some gs ← splitForallLe? goal rhs then return .goalsInScope scope gs
+  if let some gs ← liftedHyp? scope goal α pre rhs then return .goalsInScope scope gs
 
   -- Phase 4: wp decomposition. The program-shape steps below all consume one unit of fuel
   -- (the `stepLimit` config option) when they make progress.
@@ -555,19 +890,27 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
     if ← matchesUntilPattern info.prog then
       return .stop (.untilPatternMatched info.M)
     if let some g ← wpConsumeMData? goal info then
-      return .goals scope [g]
+      return .goalsInScope scope [g]
+    if let some r ← tryJPGadget? scope goal info then
+      VCGen.burnOne
+      return r
+    if let some g ← tryMarkJP? goal info then
+      return .goalsInScope scope [g]
     if let some g ← wpLet? goal info then
       VCGen.burnOne
-      return .goals scope [g]
+      return .goalsInScope scope [g]
     if let some gs ← wpMatch? goal info then
       VCGen.burnOne
-      return .goals scope gs
-    if let some g ← wpFVarZeta? goal info then
+      return .goalsInScope scope gs
+    if let some g ← wpFVarZeta? scope goal info then
       VCGen.burnOne
-      return .goals scope [g]
+      return .goalsInScope scope [g]
     if let some g ← wpHeadReduce? goal info then
       VCGen.burnOne
-      return .goals scope [g]
+      return .goalsInScope scope [g]
+    if let some r ← tryJPJump? scope goal info then
+      VCGen.burnOne
+      return r
     let f := info.prog.getAppFn
     if f.isConst || f.isFVar then
       VCGen.burnOne
diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.lean
index 353e7f14976e..f31ef9c19c19 100644
--- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/WPApp.lean
@@ -45,12 +45,18 @@ public def Value (info : WPApp) : Expr := info.args[1]!
 public def Pred (info : WPApp) : Expr := info.args[2]!
 /-- Exception postcondition type argument of `wp`. -/
 public def EPred (info : WPApp) : Expr := info.args[3]!
+/-- Assertion-lattice instance argument of `wp`. -/
+public def instAL (info : WPApp) : Expr := info.args[4]!
+/-- Exception-assertion-lattice instance argument of `wp`. -/
+public def instEAL (info : WPApp) : Expr := info.args[5]!
 /-- `WP` instance argument of `wp`. -/
 public def instWP (info : WPApp) : Expr := info.args[6]!
 /-- Program expression classified by VCGen. -/
 public def prog (info : WPApp) : Expr := info.args[7]!
 /-- Postcondition argument of `wp`. -/
 public def post (info : WPApp) : Expr := info.args[8]!
+/-- Exception postcondition argument of `wp`. -/
+public def epost (info : WPApp) : Expr := info.args[9]!
 
 end VCGen.WPApp
 
diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
index 9f6d4959639a..41ff2a723cce 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -343,6 +343,9 @@ where
     let .forallE _ φ' .. := jumpGoal | throwError "jumpGoal {jumpGoal} is not a forall"
     trace[Elab.Tactic.Do.vcgen] "φ applied: {φ}, prf applied: {prf}, type: {← inferType prf}"
     let rwPrf ← rwIfOrMatcher info.altIdx φ'
+    if rwPrf.proof?.isNone then
+      throwError "Bug in `mvcgen`: `rwIfOrMatcher` failed to rewrite alternative {info.altIdx} of\
+        {indentExpr φ'}"
     trace[Elab.Tactic.Do.vcgen] "joinPrf: {← inferType info.joinPrf}"
     let jumpPrf := mkAppN info.joinPrf (joinArgs.push (← rwPrf.mkEqMPR prf))
     let prf₁ := mkApp2 (mkConst ``SPred.true_intro [uWP]) σs goal.hyps
diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Split.lean b/src/Lean/Elab/Tactic/Do/VCGen/Split.lean
index 1a2a02abaf20..ae1b9cfd36c6 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen/Split.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen/Split.lean
@@ -188,12 +188,20 @@ def getSplitInfo? (e : Expr) : MetaM (Option SplitInfo) := do
   else
     return none
 
-def rwIfOrMatcher (idx : Nat) (e : Expr) : MetaM Simp.Result := do
+/-- Rewrite the `ite`/`dite`/matcher `e` to its `idx`-th alternative, returning a `Simp.Result` whose
+`proof?` is `none` when the alternative does not apply here (the `ite`/`dite` branch condition or the
+matcher congruence hypotheses cannot be discharged), never throwing on that account. With a
+`[assumptionLowerBound, assumptionUpperBound)` window those hypotheses are discharged by an assumption
+search confined to that window of the local context rather than the whole of it (an
+`assumptionUpperBound` of `0` means the end of the context). -/
+def rwIfOrMatcher (idx : Nat) (e : Expr) (assumptionLowerBound : Nat := 0)
+    (assumptionUpperBound : Nat := 0) : MetaM Simp.Result := do
   if e.isAppOf ``ite || e.isAppOf ``dite then
     let c := e.getArg! 1
     let c := if idx = 0 then c else mkNot c
-    let .some fv ← findLocalDeclWithType? c
-      | throwError "Failed to find proof for if condition {c}"
+    let some fv ← findLocalDeclWithType? c (lowerBound := assumptionLowerBound)
+        (upperBound := assumptionUpperBound)
+      | return { expr := e }
     rwIfWith (mkFVar fv) e
   else
-    rwMatcher idx e
+    rwMatcher idx e assumptionLowerBound assumptionUpperBound
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index d7d25d1abb83..9ecba339c0f0 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -47,6 +47,17 @@ inductive LocalDeclKind
   | auxDecl
   deriving Inhabited, Repr, DecidableEq, Hashable
 
+/--
+Determines the local declaration kind of a binder using its name.
+
+Names that begin with `__` are implementation details (`.implDetail`).
+-/
+def LocalDeclKind.ofBinderName (binderName : Name) : LocalDeclKind :=
+  if binderName.isImplementationDetail then
+    .implDetail
+  else
+    .default
+
 /-- A declaration for a `LocalContext`. This is used to register which free variables are in scope.
 
 See `LocalDecl.index`, `LocalDecl.fvarId`, `LocalDecl.userName`, `LocalDecl.type` for accessors for
diff --git a/src/Lean/Meta/Match/Rewrite.lean b/src/Lean/Meta/Match/Rewrite.lean
index abf51e233f5a..7dcbc43a2554 100644
--- a/src/Lean/Meta/Match/Rewrite.lean
+++ b/src/Lean/Meta/Match/Rewrite.lean
@@ -72,7 +72,12 @@ equation theorem cannot be discharged by assumption or reflixivity.
 See `Lean.Meta.Tactic.FunInd.buildInductionBody` and `Lean.Elab.Tactic.Do.VCGen.Split` for examples
 of how to coerce `MatherApp.transform` into doing the substitution on the motive for you.
 -/
-def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
+def rwMatcher (altIdx : Nat) (e : Expr) (assumptionLowerBound : Nat := 0)
+    (assumptionUpperBound : Nat := 0) : MetaM Simp.Result := do
+  -- Close `g` by an assumption at context index in `[assumptionLowerBound, assumptionUpperBound)`, so
+  -- the search for the congruence-equation hypotheses is confined to a window of the local context.
+  let assumptionProc (g : MVarId) : MetaM Bool :=
+    g.assumptionCore assumptionLowerBound assumptionUpperBound
   if e.isAppOf ``PSum.casesOn || e.isAppOf ``PSigma.casesOn then
     let mut e := e
     while true do
@@ -95,6 +100,17 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
       trace[Meta.Match.debug] "When trying to reduce arm {altIdx}, only {eqns.size} equations for {.ofConstName matcherDeclName}"
       return { expr := e }
     let eqnThm := eqns[altIdx]!
+    -- Close an `Eq`/`HEq` hypothesis `h` by reflexivity without throwing when it is not reflexive.
+    let tryRefl (h : MVarId) (hType : Expr) : MetaM Bool := do
+      if let some (_, a, b) := hType.eq? then
+        unless ← isDefEq a b do return false
+        h.assign (← mkEqRefl a)
+        return true
+      if let some (α, a, β, b) := hType.heq? then
+        unless ← (isDefEq α β <&&> isDefEq a b) do return false
+        h.assign (← mkHEqRefl a)
+        return true
+      return false
     try
       withTraceNode `Meta.Match.debug (fun _ => pure m!"rewriting with {.ofConstName eqnThm} in{indentExpr e}") do
       let eqProof := mkAppN (mkConst eqnThm e.getAppFn.constLevels!) e.getAppArgs
@@ -106,8 +122,10 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
         if let some (_, lhs, _, rhs) := eqType.heq? then pure (true, lhs, rhs) else
         if let some (_, lhs, rhs) := eqType.eq? then pure (false, lhs, rhs) else
         throwError m!"Type of `{.ofConstName eqnThm}` is not an equality"
-      if !(← isDefEq e lhs) then
-        throwError m!"Left-hand side `{lhs}` of `{.ofConstName eqnThm}` does not apply to `{e}`"
+      -- The alternative not applying here (`isDefEq`/discharge failure below) is a normal outcome
+      -- reported via `proof? := none`, not an error: callers probing alternatives must not pay for
+      -- exception handling on each miss.
+      if !(← isDefEq e lhs) then return { expr := e }
       /-
       Here we instantiate the hypotheses of the congruence equation theorem
       There are two sets of hypotheses to instantiate:
@@ -121,17 +139,18 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
       for h in hyps do
         unless (← h.isAssigned) do
           let hType ← h.getType
-          if Simp.isEqnThmHypothesis hType then
-            -- Using unrestricted h.substVars here does not work well; it could
-            -- even introduce a dependency on the `oldIH` we want to eliminate
-            h.assumption <|> throwError "Failed to discharge `{h}`"
-          else if hType.isEq then
-            h.assumption <|> h.refl <|> throwError m!"Failed to resolve `{h}`"
-          else if hType.isHEq then
-            h.assumption <|> h.hrefl <|> throwError m!"Failed to resolve `{h}`"
-      let unassignedHyps ← hyps.filterM fun h => return !(← h.isAssigned)
-      unless unassignedHyps.isEmpty do
-        throwError m!"Not all hypotheses of `{.ofConstName eqnThm}` could be discharged: {unassignedHyps}"
+          let discharged ←
+            if Simp.isEqnThmHypothesis hType then
+              -- Using unrestricted h.substVars here does not work well; it could
+              -- even introduce a dependency on the `oldIH` we want to eliminate
+              assumptionProc h
+            else if hType.isEq || hType.isHEq then
+              assumptionProc h <||> tryRefl h hType
+            else
+              pure true
+          unless discharged do return { expr := e }
+      if ← hyps.anyM fun h => return !(← h.isAssigned) then
+        return { expr := e }
       let rhs ← instantiateMVars rhs
       let proof ← instantiateMVars proof
       let proof ← if isHeq then
diff --git a/src/Lean/Meta/Sym/Intro.lean b/src/Lean/Meta/Sym/Intro.lean
index 3bb7f1a40c01..2178f16cc42d 100644
--- a/src/Lean/Meta/Sym/Intro.lean
+++ b/src/Lean/Meta/Sym/Intro.lean
@@ -78,7 +78,7 @@ def introCore (mvarId : MVarId) (max : Nat) (names : Array Name) (hygienic : Boo
     | .forallE n type body bi =>
       let type       ← instantiateRevS type fvars
       let fvarId     ← mkFreshFVarId
-      let lctx       := lctx.mkLocalDecl fvarId (← mkName lctx n i) type bi
+      let lctx       := lctx.mkLocalDecl fvarId (← mkName lctx n i) type bi (.ofBinderName n)
       let fvar       ← mkFVarS fvarId
       let fvars      := fvars.push fvar
       let localInsts := updateLocalInsts localInsts fvar type
@@ -91,8 +91,10 @@ def introCore (mvarId : MVarId) (max : Nat) (names : Array Name) (hygienic : Boo
       We have both dependent and non-dependent `let` expressions result in dependent `ldecl`s.
       This is fine here since we never revert them in the Sym framework.
       **Note**: If `type` is a proposition we could use a `cdecl`.
+      An implementation-detail binder (name prefixed with `__`, e.g. a `__do_jp` join point) is marked
+      so downstream consumers such as `grind` skip it and it stays hidden from the user.
       -/
-      let lctx       := lctx.mkLetDecl fvarId (← mkName lctx n i) type value
+      let lctx       := lctx.mkLetDecl fvarId (← mkName lctx n i) type value (kind := .ofBinderName n)
       let fvar       ← mkFVarS fvarId
       let fvars      := fvars.push fvar
       let localInsts := updateLocalInsts localInsts fvar type
diff --git a/src/Lean/Meta/Tactic/Assumption.lean b/src/Lean/Meta/Tactic/Assumption.lean
index 5d4d8f5ca066..fc72c779e09f 100644
--- a/src/Lean/Meta/Tactic/Assumption.lean
+++ b/src/Lean/Meta/Tactic/Assumption.lean
@@ -12,21 +12,40 @@ public section
 
 namespace Lean.Meta
 
-/-- Return a local declaration whose type is definitionally equal to `type`. -/
-def findLocalDeclWithType? (type : Expr) : MetaM (Option FVarId) := do
-  (← getLCtx).findDeclRevM? fun localDecl => do
+/-- Return a local declaration whose type is definitionally equal to `type`, searching most-recent
+first. With `lowerBound > 0` and/or `upperBound > 0`, only declarations at context index in
+`[lowerBound, upperBound)` are considered (an `upperBound` of `0` means the end of the context), so
+the scan is confined to a window of the local context rather than the whole of it. -/
+def findLocalDeclWithType? (type : Expr) (lowerBound : Nat := 0) (upperBound : Nat := 0) :
+    MetaM (Option FVarId) := do
+  let check (localDecl : LocalDecl) : MetaM (Option FVarId) := do
     if localDecl.isImplementationDetail then
       return none
     else if (← isDefEq type localDecl.type) then
       return some localDecl.fvarId
     else
       return none
+  let lctx ← getLCtx
+  if lowerBound == 0 && upperBound == 0 then
+    lctx.findDeclRevM? check
+  else
+    let hi := if upperBound == 0 then lctx.numIndices else min upperBound lctx.numIndices
+    let rec go : Nat → MetaM (Option FVarId)
+      | 0 => return none
+      | i + 1 => do
+        if i < lowerBound then return none
+        if let some localDecl := lctx.getAt? i then
+          if let some fvarId ← check localDecl then return some fvarId
+        go i
+    go hi
 
-/-- Return `true` if managed to close goal `mvarId` using an assumption. -/
-def _root_.Lean.MVarId.assumptionCore (mvarId : MVarId) : MetaM Bool :=
+/-- Return `true` if managed to close goal `mvarId` using an assumption at a context index in
+`[lowerBound, upperBound)` (see `findLocalDeclWithType?`). -/
+def _root_.Lean.MVarId.assumptionCore (mvarId : MVarId) (lowerBound : Nat := 0)
+    (upperBound : Nat := 0) : MetaM Bool :=
   mvarId.withContext do
     mvarId.checkNotAssigned `assumption
-    match (← findLocalDeclWithType? (← mvarId.getType)) with
+    match (← findLocalDeclWithType? (← mvarId.getType) lowerBound upperBound) with
     | none => return false
     | some fvarId => mvarId.assign (mkFVar fvarId); return true
 
diff --git a/src/Std/Internal/Do/Triple/Gadget.lean b/src/Std/Internal/Do/Triple/Gadget.lean
index 92ed594a0d31..99406f116626 100644
--- a/src/Std/Internal/Do/Triple/Gadget.lean
+++ b/src/Std/Internal/Do/Triple/Gadget.lean
@@ -37,6 +37,11 @@ theorem Spec.assertGadget (name : Name) (as : Pred) [∀ a : Pred, PreservesSup
     (Triple.pure (m := m) (pre := as ⊓ (as ⇨ post ⟨⟩)) (post := post) (epost := epost)
       (a := ⟨⟩) (h := meet_himp_le))
 
+set_option linter.unusedVariables false in
+/-- The identity on `x`, tagging it with the join-point function `fv` so `vcgen +jp` can recognize
+the continuation `x` of a shared join point. -/
+def jpGadget.{ua, ub} {α : Sort ua} {β : Sort ub} (fv : β) (x : α) : α := x
+
 end Std.Internal.Do
 
 end -- public section
diff --git a/tests/bench/vcgen/cases/Cases.lean b/tests/bench/vcgen/cases/Cases.lean
index ec1eb08ac18b..3dd39ec1446c 100644
--- a/tests/bench/vcgen/cases/Cases.lean
+++ b/tests/bench/vcgen/cases/Cases.lean
@@ -3,7 +3,9 @@ import Cases.AddSubCancelDeep
 import Cases.AddSubCancelSimp
 import Cases.DiteSplit
 import Cases.GetThrowSet
+import Cases.IfsJP
 import Cases.LetBinding
+import Cases.MatchesJP
 import Cases.MatchIota
 import Cases.MatchSplit
 import Cases.PurePrecond
diff --git a/tests/bench/vcgen/cases/Cases/IfsJP.lean b/tests/bench/vcgen/cases/Cases/IfsJP.lean
new file mode 100644
index 000000000000..13890817e99a
--- /dev/null
+++ b/tests/bench/vcgen/cases/Cases/IfsJP.lean
@@ -0,0 +1,31 @@
+import Lean
+import Std.Tactic.Do
+
+/-!
+Several `if`s with a shared continuation. Each `if` makes the do-elaborator emit a `__do_jp` for
+its trailing code, so `vcgen +jp` proves each continuation once instead of zeta-unfolding it into
+both branches. Without `+jp` the VC count grows exponentially in the number of `if`s.
+-/
+
+open Lean Meta Order Std.Internal.Do
+
+namespace IfsJP
+
+set_option mvcgen.warning false
+
+def step (v : Nat) : StateM Nat Unit := do
+  let s ← get
+  let mut x := s
+  if x > 0 then x := x + v else x := x + (v + 1)
+  if x > 1 then x := x + v else x := x + (v + 1)
+  if x > 2 then x := x + v else x := x + (v + 1)
+  set x
+
+def loop (n : Nat) : StateM Nat Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+def Goal (n : Nat) : Prop := ⦃fun _ => True⦄ loop n ⦃fun _ s => 0 < s⦄
+
+end IfsJP
diff --git a/tests/bench/vcgen/cases/Cases/MatchesJP.lean b/tests/bench/vcgen/cases/Cases/MatchesJP.lean
new file mode 100644
index 000000000000..ff8263690747
--- /dev/null
+++ b/tests/bench/vcgen/cases/Cases/MatchesJP.lean
@@ -0,0 +1,41 @@
+import Lean
+import Std.Tactic.Do
+
+/-!
+Several `match`es with a shared continuation, the matcher analogue of `IfsJP`. Each `match` makes the
+do-elaborator emit a `__do_jp` for its trailing code, so `vcgen +jp` proves each continuation once
+instead of zeta-unfolding it into every alternative. Exercises `+jp` on matcher-shaped join points
+(genuine `rwMatcher` discharge), where `IfsJP` exercises only `ite`.
+-/
+
+open Lean Meta Order Std.Internal.Do
+
+namespace MatchesJP
+
+set_option mvcgen.warning false
+
+def step (v : Nat) : StateM Nat Unit := do
+  let s ← get
+  let mut x := s
+  match x with
+  | 0 => x := x + v
+  | 1 => x := x + (v + 1)
+  | _ => x := x + (v + 2)
+  match x with
+  | 0 => x := x + v
+  | 1 => x := x + (v + 1)
+  | _ => x := x + (v + 2)
+  match x with
+  | 0 => x := x + v
+  | 1 => x := x + (v + 1)
+  | _ => x := x + (v + 2)
+  set x
+
+def loop (n : Nat) : StateM Nat Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+def Goal (n : Nat) : Prop := ⦃fun _ => True⦄ loop n ⦃fun _ s => 0 < s⦄
+
+end MatchesJP
diff --git a/tests/bench/vcgen/lakefile.lean b/tests/bench/vcgen/lakefile.lean
index 299d86794cf3..21f4ae2f5fec 100644
--- a/tests/bench/vcgen/lakefile.lean
+++ b/tests/bench/vcgen/lakefile.lean
@@ -17,7 +17,7 @@ lean_lib Cases where
 lean_lib VCGenBench where
   roots := #[`vcgen_add_sub_cancel, `vcgen_add_sub_cancel_deep, `vcgen_add_sub_cancel_simp,
              `vcgen_get_throw_set, `vcgen_get_throw_set_grind, `vcgen_pure_precond,
-             `vcgen_reader_state, `vcgen_match_split]
+             `vcgen_reader_state, `vcgen_match_split, `vcgen_jp]
   moreLeanArgs := #["--tstack=102400"] -- 100 MB in KB
 
 @[default_target]
diff --git a/tests/bench/vcgen/test_vcgen.lean b/tests/bench/vcgen/test_vcgen.lean
index bfcd675d40a8..3eeaf3d720f5 100644
--- a/tests/bench/vcgen/test_vcgen.lean
+++ b/tests/bench/vcgen/test_vcgen.lean
@@ -23,6 +23,8 @@ Each case exercises a different aspect of the VC generation:
 - `DiteSplit`: Dependent if-then-else (`if h : cond then ...`)
 - `MatchIota`: Pattern matching with concrete discriminants (iota-reduced, no split)
 - `MatchSplit`: Pattern matching with symbolic discriminant (state), exercising match split
+- `IfsJP`: several `if`s with a shared continuation, exercising `vcgen +jp`
+- `MatchesJP`: several `match`es with a shared continuation, exercising `vcgen +jp` on matchers
 -/
 
 open Lean Order Parser Meta Elab Tactic Sym Std Internal.Do
@@ -57,6 +59,12 @@ set_option maxHeartbeats 10000000
     `(tactic| vcgen) `(tactic| sorry) [10]
   runBenchUsingTactic ``MatchSplit.Goal [``MatchSplit.loop, ``MatchSplit.step]
     `(tactic| vcgen) `(tactic| grind) [10]
+  -- `+jp` shares the trailing continuation across the splitter alts; without it the VC count
+  -- grows exponentially in the number of `if`s in `step`.
+  runBenchUsingTactic ``IfsJP.Goal [``IfsJP.loop, ``IfsJP.step]
+    `(tactic| vcgen +jp) `(tactic| grind) [3]
+  runBenchUsingTactic ``MatchesJP.Goal [``MatchesJP.loop, ``MatchesJP.step]
+    `(tactic| vcgen +jp) `(tactic| sorry) [3]
 
 -- Verify `simplifying_assumptions [Nat.add_assoc]` works end-to-end with `simp only` unfolding.
 /--
diff --git a/tests/bench/vcgen/vcgen_jp.lean b/tests/bench/vcgen/vcgen_jp.lean
new file mode 100644
index 000000000000..883c5df4670d
--- /dev/null
+++ b/tests/bench/vcgen/vcgen_jp.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+import Cases.IfsJP
+import Cases.MatchesJP
+import Driver
+
+/-! Benchmark driver for `vcgen +jp`: loops whose bodies chain `if`s (`IfsJP`) or `match`es
+(`MatchesJP`) with shared continuations. `+jp` proves each trailing continuation once; without it
+every alternative zeta-unfolds the `__do_jp` body and the VC count grows exponentially. -/
+
+set_option mvcgen.warning false
+
+open Lean Order Parser Meta Elab Tactic Sym Std Internal.Do
+
+set_option maxRecDepth 10000
+set_option maxHeartbeats 10000000
+
+#eval runBenchUsingTactic ``IfsJP.Goal [``IfsJP.loop, ``IfsJP.step] `(tactic| vcgen +jp) `(tactic| sorry)
+  [30]
+
+#eval runBenchUsingTactic ``MatchesJP.Goal [``MatchesJP.loop, ``MatchesJP.step] `(tactic| vcgen +jp) `(tactic| sorry)
+  [30]
diff --git a/tests/elab/vcgenJPs.lean b/tests/elab/vcgenJPs.lean
new file mode 100644
index 000000000000..fed5c58ad097
--- /dev/null
+++ b/tests/elab/vcgenJPs.lean
@@ -0,0 +1,235 @@
+import Lean
+import Std.Internal
+import Std.Tactic.Do
+
+/-! Tests for `vcgen +jp`: shared-continuation (`__do_jp`) handling. A shared tail after an
+`if`/`match` makes do-elaboration emit a `__do_jp`; `+jp` proves the tail once and discharges each
+jump through a synthetic spec instead of inlining it. Ported from `mvcgenJPs.lean`. -/
+
+open Lean Order Meta Elab Tactic Sym Std Internal.Do
+
+set_option grind.warning false
+set_option mvcgen.warning false
+
+def ifs_pure (n : Nat) : Id Nat := do
+  let mut x := 0
+  if n > 0 then x := x + 1 else x := x + 2
+  if n > 1 then x := x + 3 else x := x + 4
+  if n > 2 then x := x + 1 else x := x + 2
+  if n > 3 then x := x + 1 else x := x + 2
+  if n > 4 then x := x + 1 else x := x + 2
+  if n > 5 then x := x + 1 else x := x + 2
+  return x
+
+theorem ifs_pure_triple : ⦃ True ⦄ ifs_pure n ⦃ fun r => r > 0 ⦄ := by
+  unfold ifs_pure
+  vcgen +jp
+  all_goals grind
+
+def difs_pure (n : Nat) : Id Nat := do
+  let mut x := 0
+  if h : n > 0 then x := x + 1 else x := x + 2
+  if h : n > 1 then x := x + 3 else x := x + 4
+  if h : n > 2 then x := x + 1 else x := x + 2
+  if h : n > 3 then x := x + 1 else x := x + 2
+  if h : n > 4 then x := x + 1 else x := x + 2
+  if h : n > 5 then x := x + 1 else x := x + 2
+  return x
+
+theorem difs_pure_triple : ⦃ True ⦄ difs_pure n ⦃ fun r => r > 0 ⦄ := by
+  unfold difs_pure
+  vcgen +jp
+  all_goals grind
+
+def matches_pure (f : Nat → Option Nat) : Id Nat := do
+  let mut x := 0
+  match f 0 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 1 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 2 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 3 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 4 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 5 with | some y => x := x + y + 1 | none => x := x + 2
+  return x
+
+theorem matches_pure_triple : ⦃ True ⦄ matches_pure f ⦃ fun r => r > 0 ⦄ := by
+  unfold matches_pure
+  vcgen +jp
+  all_goals grind
+
+def dmatches_pure (f : Nat → Option Nat) : Id Nat := do
+  let mut x := 0
+  match h : f 0 with | some y => x := x + (cast (congrArg (fun _ => Nat) h) y) + 1 | none => x := x + 2
+  match h : f 1 with | some y => x := x + (cast (congrArg (fun _ => Nat) h) y) + 1 | none => x := x + 2
+  match h : f 2 with | some y => x := x + (cast (congrArg (fun _ => Nat) h) y) + 1 | none => x := x + 2
+  match h : f 3 with | some y => x := x + (cast (congrArg (fun _ => Nat) h) y) + 1 | none => x := x + 2
+  match h : f 4 with | some y => x := x + (cast (congrArg (fun _ => Nat) h) y) + 1 | none => x := x + 2
+  match h : f 5 with | some y => x := x + (cast (congrArg (fun _ => Nat) h) y) + 1 | none => x := x + 2
+  return x
+
+theorem dmatches_pure_triple : ⦃ True ⦄ dmatches_pure f ⦃ fun r => r > 0 ⦄ := by
+  unfold dmatches_pure
+  vcgen +jp
+  all_goals grind
+
+def mixed_matches_pure (f : Nat → Option Nat) : Id Nat := do
+  let mut x := 0
+  match h : f 0, f 10 with | some y, some z => x := x + (cast (congrArg (fun _ => Nat) h) y) + z + 1 | _, some _ => x := x + 2 | _, _ => x := x + 1
+  match h : f 1, f 11 with | some y, some z => x := x + (cast (congrArg (fun _ => Nat) h) y) + z + 1 | _, some _ => x := x + 2 | _, _ => x := x + 1
+  match h : f 2, f 12 with | some y, some z => x := x + (cast (congrArg (fun _ => Nat) h) y) + z + 1 | _, some _ => x := x + 2 | _, _ => x := x + 1
+  match h : f 3, f 13 with | some y, some z => x := x + (cast (congrArg (fun _ => Nat) h) y) + z + 1 | _, some _ => x := x + 2 | _, _ => x := x + 1
+  match h : f 4, f 14 with | some y, some z => x := x + (cast (congrArg (fun _ => Nat) h) y) + z + 1 | _, some _ => x := x + 2 | _, _ => x := x + 1
+  match h : f 5, f 15 with | some y, some z => x := x + (cast (congrArg (fun _ => Nat) h) y) + z + 1 | _, some _ => x := x + 2 | _, _ => x := x + 1
+  return x
+
+theorem mixed_matches_pure_triple : ⦃ True ⦄ mixed_matches_pure f ⦃ fun r => r > 0 ⦄ := by
+  unfold mixed_matches_pure
+  vcgen +jp
+  all_goals grind
+
+def if_state (f : Nat → Bool) : StateM Nat Nat := do
+  let mut x := 0
+  if f 0 then x := x + 1 else x := x + 2
+  if f 1 then x := x + 1 else x := x + 2
+  if f 2 then x := x + 1 else x := x + 2
+  if f 3 then x := x + 1 else x := x + 2
+  if f 4 then x := x + 1 else x := x + 2
+  if f 5 then x := x + 1 else x := x + 2
+  return x
+
+theorem if_state_triple : ⦃ fun _ => True ⦄ if_state f ⦃ fun r => ⌜r > 0⌝ ⦄ := by
+  unfold if_state
+  vcgen +jp
+  all_goals grind
+
+def matches_state (f : Nat → Option Nat) : StateM Nat Nat := do
+  let mut x := 0
+  match f 0 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 1 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 2 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 3 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 4 with | some y => x := x + y + 1 | none => x := x + 2
+  match f 5 with | some y => x := x + y + 1 | none => x := x + 2
+  return x
+
+theorem matches_state_triple : ⦃ fun _ => True ⦄ matches_state f ⦃ fun r => ⌜r > 0⌝ ⦄ := by
+  unfold matches_state
+  vcgen +jp
+  all_goals grind
+
+def set42 : StateM Nat Unit := set 42
+
+@[spec]
+theorem set42_triple : ⦃ fun _ => True ⦄ set42 ⦃ fun _ s => ⌜s > 13⌝ ⦄ := by
+  vcgen [set42]
+  grind
+
+def mixed_matches_state (f : Nat → Option Nat) : StateM Nat Nat := do
+  set 42
+  let mut x := 0
+  match h : f 0, f 10 with
+  | some y, some z =>
+    set y
+    set42
+    x := x + (cast (congrArg (fun _ => Nat) h) y) + z + 1
+  | _, some _ =>
+    x := x + 2
+  | _, _ =>
+    x := x + (← get)
+  match h : f 1, f 11 with
+  | some y, some z =>
+    set y
+    x := x + (cast (congrArg (fun _ => Nat) h) y) + z + 1
+  | _, some _ =>
+    set42
+    x := x + 2
+  | _, _ =>
+    x := x + (← get)
+  return x
+
+theorem mixed_matches_state_triple : ⦃ fun _ => True ⦄ mixed_matches_state f ⦃ fun r => ⌜r > 0⌝ ⦄ := by
+  unfold mixed_matches_state
+  vcgen +jp
+  all_goals grind
+
+def early_return (f : Nat → Option Nat) : Id Nat := do
+  let mut x := 1
+  match f 0 with | some _ => return x | none => x := x + 1
+  match f 1 with | some y => x := x + y + 1 | none => return x
+  match f 2 with | some y => x := x + y + 1 | none => x := x + 1
+  return x
+
+theorem early_return_triple : ⦃ True ⦄ early_return f ⦃ fun r => r > 0 ⦄ := by
+  unfold early_return
+  vcgen +jp
+  all_goals grind
+
+-- Two mutable variables: the join carries several join-argument equalities.
+def multi_mut (f : Nat → Option Nat) : Id Nat := do
+  let mut x := 0
+  let mut y := 1
+  match f 0 with | some z => x := x + z; y := y + x | none => y := y + 2
+  match f 1 with | some z => x := x + z + y | none => x := x + y
+  return x + y
+
+theorem multi_mut_triple : ⦃ True ⦄ multi_mut f ⦃ fun r => r > 0 ⦄ := by
+  unfold multi_mut
+  vcgen +jp
+  all_goals grind
+
+-- The shared tail performs an effect, so the join-point body applies specs under the
+-- match-valued precondition hypothesis.
+def monadic_tail (f : Nat → Option Nat) : StateM Nat Nat := do
+  let mut x := 1
+  match f 0 with | some y => x := x + y | none => x := x + 2
+  set x
+  match f 1 with | some y => x := x + y | none => x := x + 2
+  set x
+  return x
+
+theorem monadic_tail_triple : ⦃ fun _ => True ⦄ monadic_tail f ⦃ fun r => ⌜r > 0⌝ ⦄ := by
+  unfold monadic_tail
+  vcgen +jp
+  all_goals grind
+
+-- Literal and successor patterns produce a `Nat.casesOn`-shaped matcher.
+def literal_patterns (n m : Nat) : Id Nat := do
+  let mut x := 1
+  match n with | 0 => x := x + 1 | k+1 => x := x + k + 2
+  match m with | 0 => x := x + 1 | k+1 => x := x + k + 2
+  return x
+
+theorem literal_patterns_triple : ⦃ True ⦄ literal_patterns n m ⦃ fun r => r > 0 ⦄ := by
+  unfold literal_patterns
+  vcgen +jp
+  all_goals grind
+
+-- A split nested inside an alt: both branches of the inner `if` jump to the same alt of the
+-- outer join point, so its precondition is the disjunction of the two jump payloads.
+def nested_split (f : Nat → Option Nat) : Id Nat := do
+  let mut x := 0
+  match f 0 with
+  | some y => if y > 0 then x := x + y else x := x + 1
+  | none => x := x + 2
+  match f 1 with
+  | some y => if y > 0 then x := x + y else x := x + 1
+  | none => x := x + 2
+  return x
+
+theorem nested_split_triple : ⦃ True ⦄ nested_split f ⦃ fun r => r > 0 ⦄ := by
+  unfold nested_split
+  vcgen +jp
+  all_goals grind
+
+-- The `none` alt throws: its jump is dead code behind `throw`, so the alt's precondition is
+-- finalized to `False`.
+def throwing (f : Nat → Option Nat) : ExceptT String (StateM Nat) Nat := do
+  let mut x := 1
+  match f 0 with | some y => x := x + y | none => throw "none"
+  match f 1 with | some y => x := x + y | none => x := x + 2
+  return x
+
+theorem throwing_triple :
+    ⦃ fun _ => True ⦄ throwing f ⦃ fun r => ⌜r > 0⌝; epost⟨fun _ _ => True⟩ ⦄ := by
+  unfold throwing
+  vcgen +jp
+  all_goals grind