fix: interaction between cbv_opaque and inline (#12981)

This PR fixes the interaction between `cbv_opaque` and
`inline`/`always_inline` annotations, to make sure that inlined
definitions marked as `cbv_opaque` are not unfolded during the
preprocessing stage of `cbv` tactic.

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

@@ -100,6 +100,51 @@ is marked done regardless of whether a rule fires. Otherwise it tries in order:
 namespace Lean.Meta.Tactic.Cbv
 open Lean.Meta.Sym.Simp
 
+/-- Like `Sym.unfoldReducibleStep` but skips `@[cbv_opaque]` declarations. -/
+private def unfoldReducibleStep (e : Expr) : MetaM TransformStep := do
+  let .const declName _ := e.getAppFn | return .continue
+  unless (← isReducible declName) do return .continue
+  if (← getEnv).isProjectionFn declName then return .continue
+  if (← isCbvOpaque declName) then return .continue
+  let some v ← unfoldDefinition? e | return .continue
+  return .visit v
+
+/-- Like `Sym.unfoldReducible` but skips `@[cbv_opaque]` declarations. -/
+private def unfoldReducible (e : Expr) : MetaM Expr := do
+  Meta.transform e (pre := unfoldReducibleStep)
+
+/-- Like `Sym.preprocessExpr` but skips `@[cbv_opaque]` declarations during unfolding. -/
+private def preprocessExpr (e : Expr) : Sym.SymM Expr := do
+  Sym.shareCommon (← unfoldReducible (← instantiateMVars e))
+
+/-- Like `Sym.preprocessMVar` but skips `@[cbv_opaque]` declarations during unfolding. -/
+private def preprocessMVar (mvarId : MVarId) : Sym.SymM MVarId := do
+  let mvarDecl ← mvarId.getDecl
+  let lctx ← preprocessLCtx mvarDecl.lctx
+  let type ← preprocessExpr mvarDecl.type
+  let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances type .syntheticOpaque mvarDecl.userName
+  mvarId.assign mvarNew
+  return mvarNew.mvarId!
+where
+  preprocessLCtx (lctx : LocalContext) : Sym.SymM LocalContext := do
+    let auxDeclToFullName := lctx.auxDeclToFullName
+    let mut fvarIdToDecl := {}
+    let mut decls := {}
+    let mut index := 0
+    for decl in lctx do
+      let decl ← match decl with
+        | .cdecl _ fvarId userName type bi kind =>
+          let type ← preprocessExpr type
+          pure <| LocalDecl.cdecl index fvarId userName type bi kind
+        | .ldecl _ fvarId userName type value nondep kind =>
+          let type ← preprocessExpr type
+          let value ← preprocessExpr value
+          pure <| LocalDecl.ldecl index fvarId userName type value nondep kind
+      index := index + 1
+      decls := decls.push (some decl)
+      fvarIdToDecl := fvarIdToDecl.insert decl.fvarId decl
+    return { fvarIdToDecl, decls, auxDeclToFullName }
+
 public register_builtin_option cbv.warning : Bool := {
   defValue := true
   descr    := "disable `cbv` usage warning"
@@ -320,7 +365,7 @@ public def cbvEntry (e : Expr) : MetaM Result := do
   let simprocs ← getCbvSimprocs
   let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) }
   let methods := mkCbvMethods simprocs
-  let e ← Sym.unfoldReducible e
+  let e ← unfoldReducible e
   Sym.SymM.run do
     let e ← Sym.shareCommon e
     SimpM.run' (simp e) (methods := methods) (config := config)
@@ -342,7 +387,7 @@ After all reductions, attempts `refl` to close equation goals of the form `v = v
 public def cbvGoal (mvarId : MVarId) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) : MetaM (Option MVarId) := do
   let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) }
   Sym.SymM.run do
-    let mvarId ← Sym.preprocessMVar mvarId
+    let mvarId ← preprocessMVar mvarId
     mvarId.withContext do
       let mut mvarIdNew := mvarId
       let mut toAssert : Array Hypothesis := #[]
@@ -403,7 +448,7 @@ public def cbvDecideGoal (m : MVarId) : MetaM Unit := do
       | .error err => return m!"decide_cbv: {err.toMessageData}") do
   let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) }
   Sym.SymM.run do
-    let m ← Sym.preprocessMVar m
+    let m ← preprocessMVar m
     let mType ← m.getType
     let some (_, lhs, _) := mType.eq? |
       throwError "`decide_cbv`: expected goal of the form `decide _ = true`, got: {indentExpr mType}"

tests/elab/cbv_opaque_inline.lean

@@ -0,0 +1,126 @@
+set_option cbv.warning false
+
+/-! Test that `@[cbv_opaque]` is respected for `@[inline]` and `@[always_inline]` definitions.
+These are reducible, so the preprocessing stage must skip them when they are also `@[cbv_opaque]`. -/
+
+/-! ## `@[inline]` + `@[cbv_opaque]` -/
+
+@[inline, cbv_opaque] def inlineSecret : Nat := 42
+
+/--
+error: unsolved goals
+⊢ inlineSecret = 42
+-/
+#guard_msgs in
+example : inlineSecret = 42 := by conv => lhs; cbv
+
+@[inline, cbv_opaque] def inlineAdd (a b : Nat) : Nat := a + b
+
+/--
+error: unsolved goals
+⊢ inlineAdd 1 2 = 3
+-/
+#guard_msgs in
+example : inlineAdd 1 2 = 3 := by conv => lhs; cbv
+
+/-! ## `@[always_inline]` + `@[cbv_opaque]` -/
+
+@[always_inline, cbv_opaque] def alwaysInlineSecret : Nat := 99
+
+/--
+error: unsolved goals
+⊢ alwaysInlineSecret = 99
+-/
+#guard_msgs in
+example : alwaysInlineSecret = 99 := by conv => lhs; cbv
+
+@[always_inline, cbv_opaque] def alwaysInlineMul (a b : Nat) : Nat := a * b
+
+/--
+error: unsolved goals
+⊢ alwaysInlineMul 3 4 = 12
+-/
+#guard_msgs in
+example : alwaysInlineMul 3 4 = 12 := by conv => lhs; cbv
+
+/-! ## `@[cbv_eval]` overrides `@[cbv_opaque]` even for inline definitions -/
+
+@[inline, cbv_opaque] def inlineOpaqueAdd (a b : Nat) : Nat := a + b
+@[cbv_eval] theorem inlineOpaqueAdd_eq (a b : Nat) : inlineOpaqueAdd a b = a + b := rfl
+
+example : inlineOpaqueAdd 1 2 = 3 := by conv => lhs; cbv
+
+@[always_inline, cbv_opaque] def alwaysInlineOpaqueMul (a b : Nat) : Nat := a * b
+@[cbv_eval] theorem alwaysInlineOpaqueMul_eq (a b : Nat) : alwaysInlineOpaqueMul a b = a * b := rfl
+
+example : alwaysInlineOpaqueMul 3 4 = 12 := by conv => lhs; cbv
+
+/-! ## Inline definitions without `@[cbv_opaque]` still unfold normally -/
+
+@[inline] def inlineNormal (n : Nat) : Nat := n + 1
+
+example : inlineNormal 5 = 6 := by cbv
+
+@[always_inline] def alwaysInlineNormal (n : Nat) : Nat := n * 2
+
+example : alwaysInlineNormal 5 = 10 := by cbv
+
+/-! ## `@[cbv_opaque]` + `@[inline]` with `cbvGoal` (uses `preprocessMVar`) -/
+
+/-- The kernel's `isDefEq` in `cbvGoal` still closes inline opaque goals. -/
+example : inlineSecret = 42 := by cbv
+example : alwaysInlineSecret = 99 := by cbv
+
+/-! ## `@[cbv_opaque]` + `@[inline]` used as argument to a non-opaque function -/
+
+def mySucc (n : Nat) : Nat := n + 1
+
+/--
+error: unsolved goals
+⊢ inlineSecret.succ = 43
+-/
+#guard_msgs in
+example : mySucc inlineSecret = 43 := by conv => lhs; cbv
+
+/-! ## Pattern matching on `@[cbv_opaque]` + `@[inline]` discriminant gets stuck -/
+
+def isEven : Nat → Bool
+  | 0 => true
+  | 1 => false
+  | n + 2 => isEven n
+
+/--
+error: unsolved goals
+⊢ (match inlineSecret with
+    | 0 => true
+    | 1 => false
+    | a.succ.succ => isEven a) =
+    true
+-/
+#guard_msgs in
+example : isEven inlineSecret = true := by conv => lhs; cbv
+
+/-! ## Projections on `@[cbv_opaque]` + `@[inline]` structures are not reduced -/
+
+@[inline, cbv_opaque] def inlinePair : Nat × Nat := (10, 20)
+
+/--
+error: unsolved goals
+⊢ inlinePair.1 = 10
+-/
+#guard_msgs in
+example : inlinePair.1 = 10 := by conv => lhs; cbv
+
+/-! ## `decide_cbv` with `@[cbv_opaque]` + `@[inline]` -/
+
+@[inline, cbv_opaque] def inlineBoolVal : Bool := true
+@[cbv_eval] theorem inlineBoolVal_eq : inlineBoolVal = true := rfl
+
+example : inlineBoolVal = true := by decide_cbv
+
+/-! Without `@[cbv_eval]`, `decide_cbv` gets stuck on inline opaque -/
+
+@[inline, cbv_opaque] def inlineBoolStuck : Bool := true
+
+#guard_msgs (drop error) in
+example : inlineBoolStuck = true := by decide_cbv