fix: cbv getting stuck after a rewrite of cbv_opaque function (#13122)

This PR fixes `cbv` tactic getting stuck after rewriting functions
marked with `cbv_opaque` that have a `cbv_eval` lemma registered.

src/Init/Tactics.lean

@@ -2259,42 +2259,6 @@ with grind
 ```
 This is more convenient than the equivalent `· by rename_i _ acc _; exact I1 acc`.
 
-### Witnesses
-
-When a specification has a parameter whose type is tagged with `@[mvcgen_witness_type]`, `mvcgen`
-classifies the corresponding goal as a *witness* rather than a verification condition.
-Witnesses are concrete values that the user must provide (inspired by zero-knowledge proofs),
-as opposed to invariants (predicates maintained across loop iterations) or verification conditions
-(propositions to prove).
-
-Witness goals are labelled `witness1`, `witness2`, etc. and can be provided in a `witnesses` section
-that appears before the `invariants` section:
-```
-mvcgen [...] witnesses
-· W1
-· W2
-invariants
-· I1
-with grind
-```
-Like invariants, witnesses support case label syntax:
-```
-mvcgen [...] witnesses
-| witness1 => W1
-```
-
-See the `@[mvcgen_witness_type]` attribute for how to register custom witness types.
-
-### Invariant and witness type attributes
-
-The `@[mvcgen_invariant_type]` and `@[mvcgen_witness_type]` tag attributes control how `mvcgen`
-classifies subgoals:
-* A goal whose type is an application of a type tagged with `@[mvcgen_invariant_type]` is classified
-  as an invariant (`inv<n>`).
-* A goal whose type is an application of a type tagged with `@[mvcgen_witness_type]` is classified
-  as a witness (`witness<n>`).
-* All other goals are classified as verification conditions (`vc<n>`).
-
 ### Invariant suggestions
 
 `mvcgen` will suggest invariants for you if you use the `invariants?` keyword.

src/Lean/Compiler/IR/CompilerM.lean

@@ -10,6 +10,7 @@ public import Lean.Compiler.IR.Format
 public import Lean.Compiler.ExportAttr
 public import Lean.Compiler.LCNF.PublicDeclsExt
 import Lean.Compiler.InitAttr
+import all Lean.Compiler.ModPkgExt
 import Init.Data.Format.Macro
 import Lean.Compiler.LCNF.Basic
 
@@ -129,8 +130,14 @@ private def exportIREntries (env : Environment) : Array (Name × Array EnvExtens
   -- safety: cast to erased type
   let initDecls : Array EnvExtensionEntry := unsafe unsafeCast initDecls
 
+  -- needed during initialization via interpreter
+  let modPkg : Array (Option PkgId) := modPkgExt.exportEntriesFn env (modPkgExt.getState env) .private
+  -- safety: cast to erased type
+  let modPkg : Array EnvExtensionEntry := unsafe unsafeCast modPkg
+
   #[(declMapExt.name, irEntries),
-    (Lean.regularInitAttr.ext.name, initDecls)]
+    (Lean.regularInitAttr.ext.name, initDecls),
+    (modPkgExt.name, modPkg)]
 
 def findEnvDecl (env : Environment) (declName : Name) : Option Decl :=
   Compiler.LCNF.findExtEntry? env declMapExt declName findAtSorted? (·.2.find?)

src/Lean/Elab/Tactic/Do/Attr.lean

@@ -268,24 +268,3 @@ def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool :=
     mvcgenInvariantAttr.hasTag env name
   else
     false
-
-/--
-Marks a type as a witness type for the `mvcgen` tactic.
-Goals whose type is an application of a tagged type will be classified
-as witnesses rather than verification conditions.
-In the spirit of zero-knowledge proofs, witnesses are concrete values that the user
-must provide, as opposed to invariants (predicates maintained across iterations)
-or verification conditions (propositions to prove).
--/
-builtin_initialize mvcgenWitnessTypeAttr : TagAttribute ←
-  registerTagAttribute `mvcgen_witness_type
-    "marks a type as a witness type for the `mvcgen` tactic"
-
-/--
-Returns `true` if `ty` is an application of a type tagged with `@[mvcgen_witness_type]`.
--/
-def isMVCGenWitnessType (env : Environment) (ty : Expr) : Bool :=
-  if let .const name .. := ty.getAppFn then
-    mvcgenWitnessTypeAttr.hasTag env name
-  else
-    false

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -35,7 +35,6 @@ namespace VCGen
 
 structure Result where
   invariants : Array MVarId
-  witnesses : Array MVarId
   vcs : Array MVarId
 
 partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result := do
@@ -46,13 +45,10 @@ partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result
     for h : idx in *...state.invariants.size do
       let mv := state.invariants[idx]
       mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1)))
-    for h : idx in *...state.witnesses.size do
-      let mv := state.witnesses[idx]
-      mv.setTag (Name.mkSimple ("witness" ++ toString (idx + 1)))
     for h : idx in *...state.vcs.size do
       let mv := state.vcs[idx]
       mv.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ (← mv.getTag).eraseMacroScopes)
-    return { invariants := state.invariants, witnesses := state.witnesses, vcs := state.vcs }
+    return { invariants := state.invariants, vcs := state.vcs }
 where
   onFail (goal : MGoal) (name : Name) : VCGenM Expr := do
     -- trace[Elab.Tactic.Do.vcgen] "fail {goal.toExpr}"
@@ -356,70 +352,53 @@ where
 
 end VCGen
 
-/-- Shared implementation for elaborating goal sections (invariants, witnesses).
-    `tagPrefix` is `"inv"` or `"witness"`, used to parse labels like `inv1` or `witness2`.
-    `label` is `"invariant"` or `"witness"`, used in error messages.
-    When `requireAll` is true, an error is thrown if fewer alts are provided than goals. -/
-private def elabGoalSection (goals : Array MVarId) (alts : Array Syntax)
-    (tagPrefix : String) (label : String) (requireAll := true) : TacticM Unit := do
-  let goals ← goals.filterM (not <$> ·.isAssigned)
-  let mut dotOrCase := LBool.undef -- .true => dot
-  for h : n in 0...alts.size do
-    let alt := alts[n]
-    match alt with
-    | `(goalDotAlt| · $rhs) =>
-      if dotOrCase matches .false then
-        logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported."
-        break
-      dotOrCase := .true
-      let some mv := goals[n]? | do
-        logErrorAt alt m!"More {label}s have been defined ({alts.size}) than there were unassigned {label} goals `{tagPrefix}<n>` ({goals.size})."
-        continue
-      withRef rhs do
-      discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
-    | `(goalCaseAlt| | $tag $args* => $rhs) =>
-      if dotOrCase matches .true then
-        logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported."
-        break
-      dotOrCase := .false
-      let n? : Option Nat := do
-          let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal
-          let .str .anonymous s := tag.getId | none
-          s.dropPrefix? tagPrefix >>= String.Slice.toNat?
-      let some mv := do goals[(← n?) - 1]? | do
-        logErrorAt alt m!"No {label} with label {tag} {repr tag}."
-        continue
-      if ← mv.isAssigned then
-        logErrorAt alt m!"{label} {n?.get!} is already assigned."
-        continue
-      withRef rhs do
-      discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv
-    | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}"
-  if requireAll && alts.size < goals.size then
-    let missingTypes ← goals[alts.size:].toArray.mapM (·.getType)
-    throwError "Lacking definitions for the following {label}s.\n{toMessageList missingTypes}"
-
-def elabWitnesses (stx : Syntax) (witnesses : Array MVarId) : TacticM Unit := do
-  let some stx := stx.getOptional? | return ()
-  let stx : TSyntax ``witnessAlts := ⟨stx⟩
-  withRef stx do
-  match stx with
-  | `(witnessAlts| witnesses $alts*) =>
-    elabGoalSection witnesses alts "witness" "witness"
-  | _ => logErrorAt stx m!"Expected witnessAlts, got {stx}"
-
 def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) : TacticM Unit := do
   let some stx := stx.getOptional? | return ()
   let stx : TSyntax ``invariantAlts := ⟨stx⟩
   withRef stx do
   match stx with
   | `(invariantAlts| $invariantsKW $alts*) =>
+    let invariants ← invariants.filterM (not <$> ·.isAssigned)
+
+    let mut dotOrCase := LBool.undef -- .true => dot
+    for h : n in 0...alts.size do
+      let alt := alts[n]
+      match alt with
+      | `(goalDotAlt| · $rhs) =>
+        if dotOrCase matches .false then
+          logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
+          break
+        dotOrCase := .true
+        let some mv := invariants[n]? | do
+          logErrorAt alt m!"More invariants have been defined ({alts.size}) than there were unassigned invariants goals `inv<n>` ({invariants.size})."
+          continue
+        withRef rhs do
+        discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
+      | `(goalCaseAlt| | $tag $args* => $rhs) =>
+        if dotOrCase matches .true then
+          logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
+          break
+        dotOrCase := .false
+        let n? : Option Nat := do
+            let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal
+            let .str .anonymous s := tag.getId | none
+            s.dropPrefix? "inv" >>= String.Slice.toNat?
+        let some mv := do invariants[(← n?) - 1]? | do
+          logErrorAt alt m!"No invariant with label {tag} {repr tag}."
+          continue
+        if ← mv.isAssigned then
+          logErrorAt alt m!"Invariant {n?.get!} is already assigned."
+          continue
+        withRef rhs do
+        discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv
+      | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}"
+
     if let `(invariantsKW| invariants) := invariantsKW then
-      elabGoalSection invariants alts "inv" "invariant"
+      if alts.size < invariants.size then
+        let missingTypes ← invariants[alts.size:].toArray.mapM (·.getType)
+        throwErrorAt stx m!"Lacking definitions for the following invariants.\n{toMessageList missingTypes}"
     else
-      -- We have `invariants?`. First elaborate any user-provided alts, then suggest the rest.
-      elabGoalSection invariants alts "inv" "invariant" (requireAll := false)
-      let invariants ← invariants.filterM (not <$> ·.isAssigned)
+      -- Otherwise, we have `invariants?`. Suggest missing invariants.
       let mut suggestions := #[]
       for i in 0...invariants.size do
         let mv := invariants[i]!
@@ -478,8 +457,8 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
     | none => .unlimited
   let goal ← getMainGoal
   let goal ← if ctx.config.elimLets then elimLets goal else pure goal
-  let { invariants, witnesses, vcs } ← VCGen.genVCs goal ctx fuel
-  trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  let { invariants, vcs } ← VCGen.genVCs goal ctx fuel
+  trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
   let runOnVCs (tac : TSyntax `tactic) (extraMsg : MessageData) (vcs : Array MVarId) : TermElabM (Array MVarId) :=
     vcs.flatMapM fun vc =>
       tryCatchRuntimeEx
@@ -488,13 +467,10 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
         (fun ex => throwError "Error while running {tac} on {vc}Message: {indentD ex.toMessageData}\n{extraMsg}")
   let invariants ←
     if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." invariants else pure invariants
-  trace[Elab.Tactic.Do.vcgen] "before elabWitnesses {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  elabWitnesses stx[3] witnesses
-  let witnesses ← witnesses.filterM (not <$> ·.isAssigned)
-  trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  elabInvariants stx[4] invariants (suggestInvariant vcs)
+  trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  elabInvariants stx[3] invariants (suggestInvariant vcs)
   let invariants ← invariants.filterM (not <$> ·.isAssigned)
-  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
   let vcs ← do
     let vcs ← if ctx.config.trivial then runOnVCs (← `(tactic| try mvcgen_trivial)) "Try again with -trivial." vcs else pure vcs
     let vcs ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." vcs else pure vcs
@@ -502,17 +478,17 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
   -- Eliminating lets here causes some metavariables in `mkFreshPair_triple` to become nonassignable
   -- so we don't do it. Presumably some weird delayed assignment thing is going on.
   -- let vcs ← if ctx.config.elimLets then liftMetaM <| vcs.mapM elimLets else pure vcs
-  trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  let vcs ← elabVCs stx[5] vcs
-  trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
-  replaceMainGoal (invariants ++ witnesses ++ vcs).toList
+  trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  let vcs ← elabVCs stx[4] vcs
+  trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  replaceMainGoal (invariants ++ vcs).toList
   -- trace[Elab.Tactic.Do.vcgen] "replaced main goal, new: {← getGoals}"
 
 @[builtin_tactic Lean.Parser.Tactic.mvcgenHint]
 def elabMVCGenHint : Tactic := fun stx => withMainContext do
   let stx' : TSyntax ``mvcgen := TSyntax.mk <| stx
     |>.setKind ``Lean.Parser.Tactic.mvcgen
-    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push mkNullNode |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
+    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
   -- logInfo m!"{stx}\n{toString stx}\n{repr stx}"
   -- logInfo m!"{stx'}\n{toString stx'}\n{repr stx'}"
   Lean.Meta.Tactic.TryThis.addSuggestion stx stx'

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -73,10 +73,6 @@ structure State where
   -/
   invariants : Array MVarId := #[]
   /--
-  Holes of witness type that have been generated so far.
-  -/
-  witnesses : Array MVarId := #[]
-  /--
   The verification conditions that have been generated so far.
   -/
   vcs : Array MVarId := #[]
@@ -108,11 +104,8 @@ def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
   -- VC to the user as-is, without abstracting any variables in the local context.
   -- This only makes sense for synthetic opaque metavariables.
   goal.setKind .syntheticOpaque
-  let env ← getEnv
-  if isMVCGenInvariantType env ty then
+  if isMVCGenInvariantType (← getEnv) ty then
     modify fun s => { s with invariants := s.invariants.push goal }
-  else if isMVCGenWitnessType env ty then
-    modify fun s => { s with witnesses := s.witnesses.push goal }
   else
     modify fun s => { s with vcs := s.vcs.push goal }
 

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -206,7 +206,7 @@ def handleApp : Simproc := fun e => do
   match fn with
   | .const constName _ =>
     if (← isCbvOpaque constName) then
-      return (← tryCbvTheorems e).markAsDone
+      return markAsDoneIfFailed <| ← tryCbvTheorems e
     let info ← getConstInfo constName
     tryCbvTheorems <|> (guardSimproc (fun _ => info.hasValue) handleConstApp) <|> reduceRecMatcher <| e
   | .lam .. => betaReduce e
@@ -215,7 +215,7 @@ def handleApp : Simproc := fun e => do
 def handleOpaqueConst : Simproc := fun e => do
   let .const constName _ := e | return .rfl
   if (← isCbvOpaque constName) then
-    return (← tryCbvTheorems e).markAsDone
+    return markAsDoneIfFailed <| ← tryCbvTheorems e
   return .rfl
 
 def foldLit : Simproc := fun e => do

src/Lean/Meta/Tactic/Cbv/Util.lean

@@ -108,4 +108,8 @@ public partial def getListLitElems (e : Expr) (acc : Array Expr := #[]) : Option
   | List.cons _ a as => getListLitElems as <| acc.push a
   | _ => none
 
+public def markAsDoneIfFailed : Result → Result
+  | .rfl _ cd => .rfl true cd
+  | .step e h d cd => .step e h d cd
+
 end Lean.Meta.Tactic.Cbv

src/Std/Tactic/Do/Syntax.lean

@@ -364,30 +364,15 @@ macro "mvcgen_trivial" : tactic =>
   )
 
 /--
-A goal section alternative of the form `· term`, one per goal.
-Used by both `invariants` and `witnesses` sections.
+An invariant alternative of the form `· term`, one per invariant goal.
 -/
 syntax goalDotAlt := ppDedent(ppLine) cdotTk (colGe term)
 
 /--
-A goal section alternative of the form `| label<n> a b c => term`, one per goal.
-Used by both `invariants` and `witnesses` sections.
+An invariant alternative of the form `| inv<n> a b c => term`, one per invariant goal.
 -/
 syntax goalCaseAlt := ppDedent(ppLine) "| " caseArg " => " (colGe term)
 
-/--
-The contextual keyword ` witnesses `.
--/
-syntax witnessesKW := &"witnesses "
-
-/--
-After `mvcgen [...]`, there can be an optional `witnesses` followed by either
-* a bulleted list of witnesses `· term; · term`.
-* a labelled list of witnesses `| witness1 => term; witness2 a b c => term`, which is useful for
-  naming inaccessibles.
--/
-syntax witnessAlts := witnessesKW withPosition((colGe (goalDotAlt <|> goalCaseAlt))*)
-
 /--
 Either the contextual keyword ` invariants ` or its tracing form ` invariants? ` which suggests
 skeletons for missing invariants as a hint.
@@ -395,7 +380,7 @@ skeletons for missing invariants as a hint.
 syntax invariantsKW := &"invariants " <|> &"invariants? "
 
 /--
-After `mvcgen [...] witnesses ...`, there can be an optional `invariants` followed by either
+After `mvcgen [...]`, there can be an optional `invariants` followed by either
 * a bulleted list of invariants `· term; · term`.
 * a labelled list of invariants `| inv1 => term; inv2 a b c => term`, which is useful for naming
   inaccessibles.
@@ -419,7 +404,7 @@ syntax vcAlts := "with " (ppSpace colGt tactic)? withPosition((colGe vcAlt)*)
 @[tactic_alt Lean.Parser.Tactic.mvcgenMacro]
 syntax (name := mvcgen) "mvcgen" optConfig
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
-  (witnessAlts)? (invariantAlts)? (vcAlts)? : tactic
+  (invariantAlts)? (vcAlts)? : tactic
 
 /--
 A hint tactic that expands to `mvcgen invariants?`.