feat: one axiom per native computation (#12217)

This PR implements RFC #12216: native computation (`native_decide`,
`bv_decide`) is represented in the logic as one axiom per computation,
asserting the equality that was obtained from the native computation.
`#print axiom` will no longer show `Lean.trustCompiler`, but rather the
auto-generated names of these axioms (with, for example,
`._native.bv_decide.` in the name). See the RFC for more information.


This PR introduces a common MetaM helper (`nativeEqTrue`) used by
`native_decide` and `bv_decide` alike that runs the computation and then
asserts the result using an axiom.

It also deprecated the `ofReduceBool` axioms etc.

Not included in this PR is infrastructure for enumerating these axioms,
prettier `#print axioms` (should we want his) and tactic concurrency.

Fixes #12216.

src/Init/Core.lean

@@ -2360,8 +2360,10 @@ namespace Lean
 /--
 Depends on the correctness of the Lean compiler, interpreter, and all `[implemented_by ...]` and `[extern ...]` annotations.
 -/
+@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 axiom trustCompiler : True
 
+set_option linter.deprecated false in
 /--
 When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
 The kernel will not use the interpreter if `c` is not a constant.
@@ -2381,11 +2383,13 @@ Recall that the compiler trusts the correctness of all `[implemented_by ...]` an
 If an extern function is executed, then the trusted code base will also include the implementation of the associated
 foreign function.
 -/
+@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 opaque reduceBool (b : Bool) : Bool :=
   -- This ensures that `#print axioms` will track use of `reduceBool`.
   have := trustCompiler
   b
 
+set_option linter.deprecated false in
 /--
 Similar to `Lean.reduceBool` for closed `Nat` terms.
 
@@ -2393,12 +2397,14 @@ Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α)
 The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
 We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection).
 -/
+@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 opaque reduceNat (n : Nat) : Nat :=
   -- This ensures that `#print axioms` will track use of `reduceNat`.
   have := trustCompiler
   n
 
 
+set_option linter.deprecated false in
 /--
 The axiom `ofReduceBool` is used to perform proofs by reflection. See `reduceBool`.
 
@@ -2412,8 +2418,10 @@ external type checkers that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
+@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b
 
+set_option linter.deprecated false in
 /--
 The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool`.
 
@@ -2423,6 +2431,7 @@ external type checkers that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
+@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b
 
 

src/Init/Tactics.lean

@@ -1321,7 +1321,7 @@ structure DecideConfig where
   however kernel reduction ignores transparency settings. -/
   kernel : Bool := false
   /-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
-  admitting the result via the axiom `Lean.ofReduceBool`.  This can be significantly more efficient,
+  admitting the result via an axiom. This can be significantly more efficient,
   but it is at the cost of increasing the trusted code base, namely the Lean compiler
   and all definitions with an `@[implemented_by]` attribute.
   The instance is only evaluated once. The `native_decide` tactic is a synonym for `decide +native`. -/
@@ -1351,7 +1351,7 @@ Options:
   It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything,
   and (2) it reduces the `Decidable` instance only once instead of twice.
 - `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance,
-  admitting the result via the `Lean.ofReduceBool` axiom.
+  admitting the result via an axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
   This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
   of the trusted code base.
   Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute.
@@ -1412,7 +1412,7 @@ of `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this
 uses `#eval` to evaluate the decidability instance.
 
 This should be used with care because it adds the entire lean compiler to the trusted
-part, and the axiom `Lean.ofReduceBool` will show up in `#print axioms` for theorems using
+part, and a new axiom will show up in `#print axioms` for theorems using
 this method or anything that transitively depends on them. Nevertheless, because it is
 compiled, this can be significantly more efficient than using `decide`, and for very
 large computations this is one way to run external programs and trust the result.
@@ -1827,8 +1827,7 @@ In order to avoid calling a SAT solver every time, the proof can be cached with
 If solving your problem relies inherently on using associativity or commutativity, consider enabling
 the `bv.ac_nf` option.
 
-
-Note: `bv_decide` uses `ofReduceBool` and thus trusts the correctness of the code generator.
+Note: `bv_decide` trusts the correctness of the code generator and adds a axioms asserting its result.
 
 Note: include `import Std.Tactic.BVDecide`
 -/

src/Lean/Elab/Print.lean

@@ -239,7 +239,7 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
   if axioms.isEmpty then
     logInfo m!"'{constName}' does not depend on any axioms"
   else
-    logInfo m!"'{constName}' depends on axioms: {axioms.qsort Name.lt |>.toList}"
+    logInfo m!"'{constName}' depends on axioms: {axioms.qsort Name.lt |>.map MessageData.ofConstName |>.toList}"
 
 @[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
   | `(#print%$tk axioms $id) => withRef tk do

src/Lean/Elab/Tactic.lean

@@ -54,3 +54,4 @@ public import Lean.Elab.Tactic.SimpArith
 public import Lean.Elab.Tactic.Show
 public import Lean.Elab.Tactic.Lets
 public import Lean.Elab.Tactic.Do
+public import Lean.Elab.Tactic.Decide

src/Lean/Elab/Tactic/BVDecide.lean

@@ -57,8 +57,8 @@ There are also some options to influence the behavior of `bv_decide` and friends
 8. Chain all the proofs so far to demonstrate that the original goal holds.
 
 ## Axioms
-`bv_decide` makes use of proof by reflection and `ofReduceBool`, thus adding the Lean compiler to
-the trusted code base.
+`bv_decide` makes use of proof by reflection and adds the result of the compiled check as an axoim,
+thus adding the Lean compiler to the trusted code base.
 
 
 ## Adding a new primitive

src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean

@@ -36,7 +36,7 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta
   TacticContext.new lratPath cfg
 
 /--
-Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`.
+Prepare an `Expr` that proves `bvExpr.unsat` using native evalution.
 -/
 def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do
   let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.SatAtBVLogical
 public import Lean.Elab.Tactic.BVDecide.Frontend.Normalize
 public import Lean.Elab.Tactic.BVDecide.Frontend.LRAT
+import Lean.Meta.Native
 
 public section
 
@@ -283,27 +284,15 @@ def LratCert.toReflectionProof (cert : LratCert) (cfg : TacticContext)
 
   let reflectedExpr := mkConst cfg.exprDef
   let certExpr := mkConst cfg.certDef
+  let reflectionTerm := mkApp2 (mkConst ``verifyBVExpr) reflectedExpr certExpr
 
-  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling reflection proof term") do
-    let auxValue := mkApp2 (mkConst ``verifyBVExpr) reflectedExpr certExpr
-    mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool)
-
-  let auxType ← mkEq (mkConst cfg.reflectionDef) (toExpr true)
-  let auxProof :=
-    mkApp3
-      (mkConst ``Lean.ofReduceBool)
-      (mkConst cfg.reflectionDef)
-      (toExpr true)
-      (← mkEqRefl (toExpr true))
-  try
-    let auxLemma ←
-      -- disable async TC so we can catch its exceptions
-      withOptions (Elab.async.set · false) do
-        withTraceNode `Meta.Tactic.sat (fun _ => return "Verifying LRAT certificate") do
-          mkAuxLemma [] auxType auxProof
-    return mkApp3 (mkConst ``unsat_of_verifyBVExpr_eq_true) reflectedExpr certExpr (mkConst auxLemma)
-  catch e =>
-    throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"
+  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling and evaluating reflection proof term") do
+    match (← nativeEqTrue `bv_decide reflectionTerm (axiomDeclRange? := (← getRef))) with
+    | .notTrue =>
+      throwError m!"Tactic `bv_decide` failed: The LRAT certificate could not be verified; \
+        evaluating the following term returned `false`:{indentExpr reflectionTerm}"
+    | .success auxProof =>
+      return mkApp3 (mkConst ``unsat_of_verifyBVExpr_eq_true) reflectedExpr certExpr auxProof
 where
   /--
   Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.

src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean

@@ -63,7 +63,7 @@ where
     else
       return option
 
-/-- An LRAT proof read from a file. This will get parsed using ofReduceBool. -/
+/-- An LRAT proof read from a file. This will get parsed using native evaluation. -/
 abbrev LratCert := String
 
 instance : ToExpr LRAT.IntAction where

src/Lean/Elab/Tactic/Decide.lean

@@ -0,0 +1,187 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Lean.Elab.Tactic.Basic
+import Lean.Meta.Native
+import Lean.Elab.Tactic.ElabTerm
+
+public section
+
+namespace Lean.Elab.Tactic
+open Meta
+
+/--
+Make sure `expectedType` does not contain free and metavariables.
+It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
+-/
+private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
+  let mut expectedType ← instantiateMVars expectedType
+  if expectedType.hasFVar then
+    expectedType ← zetaReduce expectedType
+  if expectedType.hasMVar then
+    throwError "Expected type must not contain metavariables{indentExpr expectedType}"
+  if expectedType.hasFVar then
+    throwError m!"Expected type must not contain free variables{indentExpr expectedType}"
+      ++ .hint' m!"Use the `+revert` option to automatically clean up and revert free variables"
+  return expectedType
+
+/--
+Given the decidable instance `inst`, reduces it and returns a decidable instance expression
+in whnf that can be regarded as the reason for the failure of `inst` to fully reduce.
+-/
+private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := withIncRecDepth do
+  let inst ← whnf inst
+  -- If it's the Decidable recursor, then blame the major premise.
+  if inst.isAppOfArity ``Decidable.rec 5 then
+    return ← blameDecideReductionFailure inst.appArg!
+  -- If it is a matcher, look for a discriminant that's a Decidable instance to blame.
+  if let .const c _ := inst.getAppFn then
+    if let some info ← getMatcherInfo? c then
+      if inst.getAppNumArgs == info.arity then
+        let args := inst.getAppArgs
+        for i in *...info.numDiscrs do
+          let inst' := args[info.numParams + 1 + i]!
+          if (← Meta.isClass? (← inferType inst')) == ``Decidable then
+            let inst'' ← whnf inst'
+            if !(inst''.isAppOf ``isTrue || inst''.isAppOf ``isFalse) then
+              return ← blameDecideReductionFailure inst''
+  return inst
+
+def elabNativeDecideCore (tacticName : Name) (expectedType : Expr) : TacticM Expr := do
+  let d ← mkDecide expectedType
+  match (← nativeEqTrue tacticName d (axiomDeclRange? := (← getRef))) with
+  | .notTrue =>
+    throwError m!"\
+      Tactic `{tacticName}` evaluated that the proposition\
+      {indentExpr expectedType}\n\
+      is false"
+  | .success prf =>
+    -- get instance from `d`
+    let s := d.appArg!
+    return mkApp3 (mkConst ``of_decide_eq_true) expectedType s prf
+
+def evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) : TacticM Unit := do
+  if cfg.revert then
+    -- In revert mode: clean up the local context and then revert everything that is left.
+    liftMetaTactic1 fun g => do
+      let g ← g.cleanup
+      let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
+      return g
+  closeMainGoalUsing tacticName fun expectedType _ => do
+    if cfg.kernel && cfg.native then
+      throwError "Tactic `{tacticName}` failed: Cannot simultaneously set both `+kernel` and `+native`"
+    let expectedType ← preprocessPropToDecide expectedType
+    if cfg.native then
+      elabNativeDecideCore tacticName expectedType
+    else if cfg.kernel then
+      doKernel expectedType
+    else
+      doElab expectedType
+where
+  doElab (expectedType : Expr) : TacticM Expr := do
+    let pf ← mkDecideProof expectedType
+    -- Get instance from `pf`
+    let s := pf.appFn!.appArg!
+    let r ← withAtLeastTransparency .default <| whnf s
+    if r.isAppOf ``isTrue then
+      -- Success!
+      -- While we have a proof from reduction, we do not embed it in the proof term,
+      -- and instead we let the kernel recompute it during type checking from the following more
+      -- efficient term. The kernel handles the unification `e =?= true` specially.
+      return pf
+    else
+      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
+      throwError MessageData.ofLazyM (es := #[expectedType]) do
+        diagnose expectedType s r
+
+  doKernel (expectedType : Expr) : TacticM Expr := do
+    let pf ← mkDecideProof expectedType
+    -- Get instance from `pf`
+    let s := pf.appFn!.appArg!
+    -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
+    -- The `mkAuxLemma` function caches the result in two ways:
+    -- 1. First, the function makes use of a `type`-indexed cache per module.
+    -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
+    let levelsInType := (collectLevelParams {} expectedType).params
+    -- Level variables occurring in `expectedType`, in ambient order
+    let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
+    try
+      let lemmaName ← withOptions (Elab.async.set · false) do
+        mkAuxLemma lemmaLevels expectedType pf
+      return mkConst lemmaName (lemmaLevels.map .param)
+    catch ex =>
+      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
+      throwError MessageData.ofLazyM (es := #[expectedType]) do
+        let r ← withAtLeastTransparency .default <| whnf s
+        if r.isAppOf ``isTrue then
+          return m!"\
+            Tactic `{tacticName}` failed. The elaborator is able to reduce the \
+            `{.ofConstName ``Decidable}` instance, but the kernel fails with:\n\
+            {indentD ex.toMessageData}"
+        diagnose expectedType s r
+
+  diagnose (expectedType s : Expr) (r : Expr) : MetaM MessageData := do
+    if r.isAppOf ``isFalse then
+      return m!"\
+        Tactic `{tacticName}` proved that the proposition\
+        {indentExpr expectedType}\n\
+        is false"
+    -- Re-reduce the instance and collect diagnostics, to get all unfolded Decidable instances
+    let (reason, unfoldedInsts) ← withoutModifyingState <| withOptions (fun opt => diagnostics.set opt true) do
+      modifyDiag (fun _ => {})
+      let reason ← withAtLeastTransparency .default <| blameDecideReductionFailure s
+      let unfolded := (← get).diag.unfoldCounter.foldl (init := #[]) fun cs n _ => cs.push n
+      let unfoldedInsts ← unfolded |>.qsort Name.lt |>.filterMapM fun n => do
+        let e ← mkConstWithLevelParams n
+        if (← Meta.isClass? (← inferType e)) == ``Decidable then
+          return m!"`{.ofConst e}`"
+        else
+          return none
+      return (reason, unfoldedInsts)
+    let stuckMsg :=
+      if unfoldedInsts.isEmpty then
+        m!"Reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
+      else
+        let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
+        m!"After unfolding the {instances} {.andList unfoldedInsts.toList}, \
+        reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
+    let hint :=
+      if reason.isAppOf ``Eq.rec then
+        .hint' m!"Reduction got stuck on `▸` ({.ofConstName ``Eq.rec}), \
+          which suggests that one of the `{.ofConstName ``Decidable}` instances is defined using tactics such as `rw` or `simp`. \
+          To avoid tactics, make use of functions such as \
+          `{.ofConstName ``inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
+          to alter a proposition."
+      else if reason.isAppOf ``Classical.choice then
+        .hint' m!"Reduction got stuck on `{.ofConstName ``Classical.choice}`, \
+          which indicates that a `{.ofConstName ``Decidable}` instance \
+          is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
+          The `{tacticName}` tactic works by evaluating a decision procedure via reduction, \
+          and it cannot make progress with such instances. \
+          This can occur due to the `open scoped Classical` command, which enables the instance \
+          `{.ofConstName ``Classical.propDecidable}`."
+      else
+        MessageData.nil
+    return m!"\
+      Tactic `{tacticName}` failed for proposition\
+      {indentExpr expectedType}\n\
+      because its `{.ofConstName ``Decidable}` instance\
+      {indentExpr s}\n\
+      did not reduce to `{.ofConstName ``isTrue}` or `{.ofConstName ``isFalse}`.\n\n\
+      {stuckMsg}{hint}"
+
+declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
+
+@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  evalDecideCore `decide cfg
+
+@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
+  let cfg ← elabDecideConfig stx[1]
+  let cfg := { cfg with native := true }
+  evalDecideCore `native_decide cfg

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -361,215 +361,4 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
       replaceMainGoal [← (← getMainGoal).rename fvarId h.getId]
   | _ => throwUnsupportedSyntax
 
-
-/--
-Make sure `expectedType` does not contain free and metavariables.
-It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
--/
-private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
-  let mut expectedType ← instantiateMVars expectedType
-  if expectedType.hasFVar then
-    expectedType ← zetaReduce expectedType
-  if expectedType.hasMVar then
-    throwError "Expected type must not contain metavariables{indentExpr expectedType}"
-  if expectedType.hasFVar then
-    throwError m!"Expected type must not contain free variables{indentExpr expectedType}"
-      ++ .hint' m!"Use the `+revert` option to automatically clean up and revert free variables"
-  return expectedType
-
-/--
-Given the decidable instance `inst`, reduces it and returns a decidable instance expression
-in whnf that can be regarded as the reason for the failure of `inst` to fully reduce.
--/
-private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := withIncRecDepth do
-  let inst ← whnf inst
-  -- If it's the Decidable recursor, then blame the major premise.
-  if inst.isAppOfArity ``Decidable.rec 5 then
-    return ← blameDecideReductionFailure inst.appArg!
-  -- If it is a matcher, look for a discriminant that's a Decidable instance to blame.
-  if let .const c _ := inst.getAppFn then
-    if let some info ← getMatcherInfo? c then
-      if inst.getAppNumArgs == info.arity then
-        let args := inst.getAppArgs
-        for i in *...info.numDiscrs do
-          let inst' := args[info.numParams + 1 + i]!
-          if (← Meta.isClass? (← inferType inst')) == ``Decidable then
-            let inst'' ← whnf inst'
-            if !(inst''.isAppOf ``isTrue || inst''.isAppOf ``isFalse) then
-              return ← blameDecideReductionFailure inst''
-  return inst
-
-private unsafe def elabNativeDecideCoreUnsafe (tacticName : Name) (expectedType : Expr) : TacticM Expr := do
-  let d ← mkDecide expectedType
-  let levels := (collectLevelParams {} expectedType).params.toList
-  let auxDeclName ← Term.mkAuxName `_nativeDecide
-  let decl := Declaration.defnDecl {
-    name := auxDeclName
-    levelParams := levels
-    type := mkConst ``Bool
-    value := d
-    hints := .abbrev
-    safety := .safe
-  }
-  try
-    -- disable async codegen so we can catch its exceptions; we don't want to report `evalConst`
-    -- failures below when the actual reason was a codegen failure
-    withOptions (Elab.async.set · false) do
-      addAndCompile decl
-  catch ex =>
-    throwError m!"Tactic `{tacticName}` failed. Error: {ex.toMessageData}"
-
-  -- get instance from `d`
-  let s := d.appArg!
-  let rflPrf ← mkEqRefl (toExpr true)
-  let levelParams := levels.map .param
-  let pf := mkApp3 (mkConst ``of_decide_eq_true) expectedType s <|
-    mkApp3 (mkConst ``Lean.ofReduceBool) (mkConst auxDeclName levelParams) (toExpr true) rflPrf
-  try
-    -- disable async TC so we can catch its exceptions
-    withOptions (Elab.async.set · false) do
-      let lemmaName ← mkAuxLemma levels expectedType pf
-      return .const lemmaName levelParams
-  catch ex =>
-    -- Diagnose error
-    throwError MessageData.ofLazyM (es := #[expectedType]) do
-      let r ←
-        try
-          evalConst Bool auxDeclName
-        catch ex =>
-          return m!"\
-            Tactic `{tacticName}` failed: Could not evaluate decidable instance. \
-            Error: {ex.toMessageData}"
-      if !r then
-        return m!"\
-          Tactic `{tacticName}` evaluated that the proposition\
-          {indentExpr expectedType}\n\
-          is false"
-      else
-        return m!"Tactic `{tacticName}` failed. Error: {ex.toMessageData}"
-
-@[implemented_by elabNativeDecideCoreUnsafe]
-private opaque elabNativeDecideCore (tacticName : Name) (expectedType : Expr) : TacticM Expr
-
-def evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) : TacticM Unit := do
-  if cfg.revert then
-    -- In revert mode: clean up the local context and then revert everything that is left.
-    liftMetaTactic1 fun g => do
-      let g ← g.cleanup
-      let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := true) (← g.getDecl).lctx.getFVarIds
-      return g
-  closeMainGoalUsing tacticName fun expectedType _ => do
-    if cfg.kernel && cfg.native then
-      throwError "Tactic `{tacticName}` failed: Cannot simultaneously set both `+kernel` and `+native`"
-    let expectedType ← preprocessPropToDecide expectedType
-    if cfg.native then
-      elabNativeDecideCore tacticName expectedType
-    else if cfg.kernel then
-      doKernel expectedType
-    else
-      doElab expectedType
-where
-  doElab (expectedType : Expr) : TacticM Expr := do
-    let pf ← mkDecideProof expectedType
-    -- Get instance from `pf`
-    let s := pf.appFn!.appArg!
-    let r ← withAtLeastTransparency .default <| whnf s
-    if r.isAppOf ``isTrue then
-      -- Success!
-      -- While we have a proof from reduction, we do not embed it in the proof term,
-      -- and instead we let the kernel recompute it during type checking from the following more
-      -- efficient term. The kernel handles the unification `e =?= true` specially.
-      return pf
-    else
-      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
-      throwError MessageData.ofLazyM (es := #[expectedType]) do
-        diagnose expectedType s r
-
-  doKernel (expectedType : Expr) : TacticM Expr := do
-    let pf ← mkDecideProof expectedType
-    -- Get instance from `pf`
-    let s := pf.appFn!.appArg!
-    -- Reduce the decidable instance to (hopefully!) `isTrue` by passing `pf` to the kernel.
-    -- The `mkAuxLemma` function caches the result in two ways:
-    -- 1. First, the function makes use of a `type`-indexed cache per module.
-    -- 2. Second, once the proof is added to the environment, the kernel doesn't need to check the proof again.
-    let levelsInType := (collectLevelParams {} expectedType).params
-    -- Level variables occurring in `expectedType`, in ambient order
-    let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
-    try
-      let lemmaName ← withOptions (Elab.async.set · false) do
-        mkAuxLemma lemmaLevels expectedType pf
-      return mkConst lemmaName (lemmaLevels.map .param)
-    catch ex =>
-      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
-      throwError MessageData.ofLazyM (es := #[expectedType]) do
-        let r ← withAtLeastTransparency .default <| whnf s
-        if r.isAppOf ``isTrue then
-          return m!"\
-            Tactic `{tacticName}` failed. The elaborator is able to reduce the \
-            `{.ofConstName ``Decidable}` instance, but the kernel fails with:\n\
-            {indentD ex.toMessageData}"
-        diagnose expectedType s r
-
-  diagnose (expectedType s : Expr) (r : Expr) : MetaM MessageData := do
-    if r.isAppOf ``isFalse then
-      return m!"\
-        Tactic `{tacticName}` proved that the proposition\
-        {indentExpr expectedType}\n\
-        is false"
-    -- Re-reduce the instance and collect diagnostics, to get all unfolded Decidable instances
-    let (reason, unfoldedInsts) ← withoutModifyingState <| withOptions (fun opt => diagnostics.set opt true) do
-      modifyDiag (fun _ => {})
-      let reason ← withAtLeastTransparency .default <| blameDecideReductionFailure s
-      let unfolded := (← get).diag.unfoldCounter.foldl (init := #[]) fun cs n _ => cs.push n
-      let unfoldedInsts ← unfolded |>.qsort Name.lt |>.filterMapM fun n => do
-        let e ← mkConstWithLevelParams n
-        if (← Meta.isClass? (← inferType e)) == ``Decidable then
-          return m!"`{.ofConst e}`"
-        else
-          return none
-      return (reason, unfoldedInsts)
-    let stuckMsg :=
-      if unfoldedInsts.isEmpty then
-        m!"Reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
-      else
-        let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
-        m!"After unfolding the {instances} {.andList unfoldedInsts.toList}, \
-        reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
-    let hint :=
-      if reason.isAppOf ``Eq.rec then
-        .hint' m!"Reduction got stuck on `▸` ({.ofConstName ``Eq.rec}), \
-          which suggests that one of the `{.ofConstName ``Decidable}` instances is defined using tactics such as `rw` or `simp`. \
-          To avoid tactics, make use of functions such as \
-          `{.ofConstName ``inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
-          to alter a proposition."
-      else if reason.isAppOf ``Classical.choice then
-        .hint' m!"Reduction got stuck on `{.ofConstName ``Classical.choice}`, \
-          which indicates that a `{.ofConstName ``Decidable}` instance \
-          is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
-          The `{tacticName}` tactic works by evaluating a decision procedure via reduction, \
-          and it cannot make progress with such instances. \
-          This can occur due to the `open scoped Classical` command, which enables the instance \
-          `{.ofConstName ``Classical.propDecidable}`."
-      else
-        MessageData.nil
-    return m!"\
-      Tactic `{tacticName}` failed for proposition\
-      {indentExpr expectedType}\n\
-      because its `{.ofConstName ``Decidable}` instance\
-      {indentExpr s}\n\
-      did not reduce to `{.ofConstName ``isTrue}` or `{.ofConstName ``isFalse}`.\n\n\
-      {stuckMsg}{hint}"
-
-declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig
-
-@[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx => do
-  let cfg ← elabDecideConfig stx[1]
-  evalDecideCore `decide cfg
-
-@[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun stx => do
-  let cfg ← elabDecideConfig stx[1]
-  let cfg := { cfg with native := true }
-  evalDecideCore `native_decide cfg
-
 end Lean.Elab.Tactic

src/Lean/Environment.lean

@@ -2491,6 +2491,7 @@ where
       let decl ← match info with
         | .thmInfo thm   => pure <| .thmDecl thm
         | .defnInfo defn => pure <| .defnDecl defn
+        | .axiomInfo ax  => pure <| .axiomDecl ax
         | _              =>
           return panic! s!"{c.constInfo.name} must be definition/theorem"
       -- realized kernel additions cannot be interrupted - which would be bad anyway as they can be

src/Lean/Meta/Native.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+module
+prelude
+public import Lean.Meta.Basic
+import Lean.Util.CollectLevelParams
+import Lean.AddDecl
+import Lean.Meta.AppBuilder
+import Lean.Elab.DeclarationRange
+
+open Lean Meta
+
+namespace Lean.Meta
+
+/-!
+This module contains infrastructure for proofs by native evaluation (`native decide`, `bv_decide`).
+Such proofs involve a native computation using the Lean kernel, and then asserting the result
+of that computation as an axiom towards the logic.
+-/
+
+public inductive NativeEqTrueResult where
+  /-- The given expression `e` evalutes to true. `prf` is a proof of `e = true`. -/
+  | success (prf : Expr)
+  /-- The given expression `e` evalutes to false. -/
+  | notTrue
+
+/--
+A call to `nativeEqTrue tacName e`, where `e` is a closed value of type `Bool`, will compile and run
+that value, check that it evaluates to `true`, and if so, will add an axiom asserting `e = true` and
+return that axiom.
+
+It is the basis for `native_decide` and `bv_decide` tactics.
+-/
+public def nativeEqTrue (tacticName : Name) (e : Expr) (axiomDeclRange? : Option Syntax := none) : MetaM NativeEqTrueResult  := do
+  let e ← instantiateMVars e
+  if e.hasFVar then
+    throwError m!"Tactic `{tacticName}` failed: Cannot native decide proposition with free variables:{indentExpr e}"
+  if e.hasMVar then
+    throwError m!"Tactic `{tacticName}` failed: Cannot native decide proposition with metavariables:{indentExpr e}"
+  let levels := (collectLevelParams {} e).params.toList
+  let isTrue ← withoutModifyingEnv do
+    let auxDeclName ← mkAuxDeclName <| `_native ++ tacticName ++ `decl
+    let decl := Declaration.defnDecl {
+      name := auxDeclName
+      levelParams := levels
+      type := mkConst ``Bool
+      value := e
+      hints := .abbrev
+      safety := .safe
+    }
+    try
+      -- disable async codegen so we can catch its exceptions; we don't want to report `evalConst`
+      -- failures below when the actual reason was a codegen failure
+      withOptions (Elab.async.set · false) do
+        addAndCompile decl
+    catch ex =>
+      throwError m!"Tactic `{tacticName}` failed. Error: {ex.toMessageData}"
+
+    -- Now evaluate the constant, and check that it is true.
+    try
+      unsafe evalConst Bool auxDeclName
+    catch ex =>
+      throwError m!"\
+        Tactic `{tacticName}` failed: Could not evaluate decidable instance. \
+        Error: {ex.toMessageData}"
+
+  unless isTrue do return .notTrue
+
+  let auxAxiomName ← mkAuxDeclName <| `_native ++ tacticName ++ `ax
+  let axDecl := Declaration.axiomDecl {
+    name := auxAxiomName
+    levelParams := levels
+    type := mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) e (mkConst ``Bool.true)
+    isUnsafe := false
+  }
+  addDecl axDecl
+  if let some ref := axiomDeclRange? then
+    Elab.addDeclarationRangesFromSyntax auxAxiomName ref
+
+  let levelParams := levels.map mkLevelParam
+  return .success <| mkConst auxAxiomName levelParams

tests/lean/decideNativePanic.lean

@@ -0,0 +1,12 @@
+/-!
+Panic during evaluation
+-/
+
+inductive ItsTrue2 : Prop
+  | mk
+
+instance : Decidable ItsTrue2 :=
+  have : Inhabited (Decidable ItsTrue2) := ⟨isTrue .mk⟩
+  panic! "oh no"
+
+example : ItsTrue2 := by native_decide

tests/lean/decideNativePanic.lean.expected.out

@@ -0,0 +1 @@
+PANIC at instDecidableItsTrue2 lean.decideNativePanic:10:2: oh no

tests/lean/run/bv_axiom_check.lean

@@ -5,7 +5,7 @@ open BitVec
 theorem bv_axiomCheck (x y z : BitVec 1) : x < y → y < z → x < z := by bv_decide
 
 /--
-info: 'bv_axiomCheck' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]
+info: 'bv_axiomCheck' depends on axioms: [propext, Classical.choice, Quot.sound, bv_axiomCheck._native.bv_decide.ax_1_5]
 -/
 #guard_msgs in
 #print axioms bv_axiomCheck

tests/lean/run/collectAxioms.lean

@@ -23,14 +23,10 @@ info: 'A2' depends on axioms: [A0, A1, A2]
 theorem one_add_one : 1 + 1 = 2 := by
   native_decide
 
-/--
-info: #[`Lean.ofReduceBool, `Lean.trustCompiler]
--/
+/-- info: #[`one_add_one._native.native_decide.ax_1_1] -/
 #guard_msgs in
 #eval Lean.collectAxioms ``one_add_one
 
-/--
-info: 'one_add_one' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler]
--/
+/-- info: 'one_add_one' depends on axioms: [one_add_one._native.native_decide.ax_1_1] -/
 #guard_msgs in
 #print axioms one_add_one

tests/lean/run/decideNative.lean

@@ -6,8 +6,11 @@ import Lean
 /-!
 Simplest example.
 -/
-theorem ex1 : True := by native_decide
-/-- info: 'ex1' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler] -/
+theorem ex1 : True := by
+  skip
+  native_decide
+  skip
+/-- info: 'ex1' depends on axioms: [ex1._native.native_decide.ax_1_1] -/
 #guard_msgs in #print axioms ex1
 
 
@@ -112,21 +115,3 @@ instance : Decidable ItsTrue := sorry
 error: Tactic `native_decide` failed: Could not evaluate decidable instance. Error: cannot evaluate code because 'instDecidableItsTrue' uses 'sorry' and/or contains errors
 -/
 #guard_msgs in example : ItsTrue := by native_decide
-
-
-/-!
-Panic during evaluation
--/
-
-inductive ItsTrue2 : Prop
-  | mk
-
-instance : Decidable ItsTrue2 :=
-  have : Inhabited (Decidable ItsTrue2) := ⟨isTrue .mk⟩
-  panic! "oh no"
-
--- Note: this test fails within VS Code
-/--
-info: output: PANIC at instDecidableItsTrue2 lean.run.decideNative:126:2: oh no
--/
-#guard_msgs in example : ItsTrue2 := by collect_stdout native_decide

tests/lean/run/nativeReflBackdoor.lean

@@ -1,4 +1,4 @@
---
+set_option linter.unusedVariables false
 
 /-
 This example demonstratea that when we are using `native_decide`,
@@ -35,6 +35,6 @@ We managed to prove `False` using the unsound annotation `implemented_by` above.
 theorem unsound : False :=
 Bool.noConfusion trueEqFalse
 
-/-- info: 'unsound' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler] -/
+/-- info: 'unsound' depends on axioms: [fConst._native.native_decide.ax_1_3] -/
 #guard_msgs in
 #print axioms unsound

tests/lean/run/replayConst.lean

@@ -1,7 +1,7 @@
 import Lean.Elab.Tactic.Basic
 import Std.Tactic.BVDecide
 
-/-! `replayConst` should be able to replay constants using `native_decide`. -/
+/-! `replayConst` should be able to replay constants using additional axioms. -/
 
 open Lean Lean.Meta Lean.Elab.Tactic in
 elab "replay" ts:tacticSeq : tactic => do

tests/pkg/leanchecker/LeanCheckerTests/NativeDecide.lean

@@ -1,4 +0,0 @@
-/-! `native_decide` is intentionally not supported at this point. -/
-
-theorem nat_dec : True := by native_decide
-#print axioms nat_dec

tests/pkg/leanchecker/LeanCheckerTests/NativeDecide.lean.expected.out

@@ -1,2 +0,0 @@
-leanchecker found a problem in LeanCheckerTests.NativeDecide
-uncaught exception: (kernel) (interpreter) unknown declaration 'nat_dec._nativeDecide_1_1'