feat: @[allow_native_decide] kernel check

src/Init/Prelude.lean

@@ -1019,7 +1019,7 @@ support.
    | true, false  => isFalse (fun h => Bool.noConfusion h)
    | true, true   => isTrue rfl
 
-@[inline] instance : DecidableEq Bool :=
+@[inline, allow_native_decide] instance : DecidableEq Bool :=
    Bool.decEq
 
 /--
@@ -1236,7 +1236,9 @@ class OfNat (α : Type u) (_ : Nat) where
   `α`. -/
   ofNat : α
 
-@[default_instance 100] /- low prio -/
+attribute [allow_native_decide] OfNat.ofNat
+
+@[default_instance 100, allow_native_decide] /- low prio -/
 instance instOfNatNat (n : Nat) : OfNat Nat n where
   ofNat := n
 
@@ -2354,7 +2356,7 @@ protected def BitVec.ofNatLT {w : Nat} (i : Nat) (p : LT.lt i (hPow 2 w)) : BitV
 /--
 The bitvector with value `i mod 2^n`.
 -/
-@[expose, match_pattern]
+@[expose, match_pattern, allow_native_decide]
 protected def BitVec.ofNat (n : Nat) (i : Nat) : BitVec n where
   toFin := Fin.Internal.ofNat (HPow.hPow 2 n) (Nat.pow_pos (Nat.zero_lt_succ _)) i
 

src/Lean.lean

@@ -48,3 +48,4 @@ public import Lean.ErrorExplanations
 public import Lean.DefEqAttrib
 public import Lean.Shell
 public import Lean.ExtraModUses
+public import Lean.AllowNativeDecide

src/Lean/AllowNativeDecide.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+module
+
+prelude
+
+public import Lean.Attributes
+
+namespace Lean
+
+builtin_initialize allowNativeDecideAttr : TagAttribute ←
+  registerTagAttribute `allow_native_decide
+    "mark definition as allowed to be used in `native_decide` computations"
+
+@[export lean_has_disallowed_native_decide]
+partial def hasDisallowedNativeDecide (kenv : Kernel.Environment) (n : Name) : Option Name :=
+  let env := Environment.ofKernelEnv kenv
+  go env n
+where go (env : Environment) (n : Name) : Option Name := Id.run do
+  let some c := kenv.find? n | return some n
+  match c with
+  | .defnInfo d =>
+    if allowNativeDecideAttr.hasTag env d.name then
+      none
+    else if !n.isInternalDetail then
+      some n
+    else
+      return d.value.foldConsts (init := none) (go env · <|> ·)
+  | .ctorInfo _ => none
+  | .inductInfo _ => none
+  | c => some c.name

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -465,11 +465,6 @@ def SemanticTokenType.names : Array String :=
 def SemanticTokenType.toNat (tokenType : SemanticTokenType) : Nat :=
   tokenType.ctorIdx
 
--- sanity check
-example {v : SemanticTokenType} : open SemanticTokenType in
-    names[v.toNat]?.map (toString <| toJson ·) = some (toString <| toJson v) := by
-  cases v <;> native_decide
-
 /--
 The semantic token modifiers included by default in the LSP specification.
 Not used by the Lean core, but implementing them here allows them to be
@@ -496,11 +491,6 @@ def SemanticTokenModifier.names : Array String :=
 def SemanticTokenModifier.toNat (modifier : SemanticTokenModifier) : Nat :=
   modifier.ctorIdx
 
--- sanity check
-example {v : SemanticTokenModifier} : open SemanticTokenModifier in
-    names[v.toNat]?.map (toString <| toJson ·) = some (toString <| toJson v) := by
-  cases v <;> native_decide
-
 structure SemanticTokensLegend where
   tokenTypes     : Array String
   tokenModifiers : Array String

src/Std/Tactic/BVDecide/Reflect.lean

@@ -183,7 +183,7 @@ theorem verifyCert_correct : ∀ cnf cert, verifyCert cnf cert = true → cnf.Un
 /--
 Verify that `cert` is an UNSAT proof for the SAT problem obtained by bitblasting `bv`.
 -/
-def verifyBVExpr (bv : BVLogicalExpr) (cert : String) : Bool :=
+@[allow_native_decide] def verifyBVExpr (bv : BVLogicalExpr) (cert : String) : Bool :=
   verifyCert (AIG.toCNF bv.bitblast.relabelNat) cert
 
 theorem unsat_of_verifyBVExpr_eq_true (bv : BVLogicalExpr) (c : String)

src/kernel/type_checker.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "runtime/interrupt.h"
 #include "runtime/sstream.h"
 #include "runtime/flet.h"
+#include "runtime/option_ref.h"
 #include "util/lbool.h"
 #include "kernel/type_checker.h"
 #include "kernel/expr_maps.h"
@@ -534,11 +535,16 @@ object * run_boxed_kernel(environment const & env, options const & opts, name co
 expr mk_bool_true();
 expr mk_bool_false();
 
+extern "C" object * lean_has_disallowed_native_decide(object * env, object * n);
+
 optional<expr> reduce_native(environment const & env, expr const & e) {
     if (!is_app(e)) return none_expr();
     expr const & arg = app_arg(e);
     if (!is_constant(arg)) return none_expr();
     if (app_fn(e) == *g_lean_reduce_bool) {
+        if (option_ref<name> has_disallowed = option_ref<name>(lean_has_disallowed_native_decide(env.to_obj_arg(), const_name(arg).to_obj_arg()))) {
+            throw kernel_exception(env, sstream() << "cannot native-reduce expression involving definition `" << has_disallowed.get_val() << "` not marked `@[allow_native_decide]`");
+        }
         object * r = ir::run_boxed_kernel(env, options(), const_name(arg), 0, nullptr);
         if (!lean_is_scalar(r)) {
             lean_dec_ref(r);
@@ -547,6 +553,9 @@ optional<expr> reduce_native(environment const & env, expr const & e) {
         return lean_unbox(r) == 0 ? some_expr(mk_bool_false()) : some_expr(mk_bool_true());
     }
     if (app_fn(e) == *g_lean_reduce_nat) {
+        if (option_ref<name> has_disallowed = option_ref<name>(lean_has_disallowed_native_decide(env.to_obj_arg(), const_name(arg).to_obj_arg()))) {
+            throw kernel_exception(env, sstream() << "cannot native-reduce expression involving definition `" << has_disallowed.get_val() << "` not marked `@[allow_native_decide]`");
+        }
         object * r = ir::run_boxed_kernel(env, options(), const_name(arg), 0, nullptr);
         if (lean_is_scalar(r) || lean_is_mpz(r)) {
             return some_expr(mk_lit(literal(nat(r))));

src/lake/Lake/Build/Trace.lean

@@ -130,10 +130,6 @@ public def ofHex (s : String) : Hash :=
     else if 97 ≤ c then n*16 + (c - 87).toUInt64 -- c - 'a' + 10 = (c - 87)
     else n*16 + (c - 55).toUInt64 -- c - 'A' + 10 = (c - 55)
 
--- sanity check
-example : ofHex "0123456789" = ⟨0x0123456789⟩ ∧
-  ofHex "abcdeF" = ⟨0xabcdef⟩ ∧ ofHex "ABCDEF" = ⟨0xABCDEF⟩ := by native_decide
-
 /-- Parse a hash from a 16-digit string of hexadecimal digits. -/
 public def ofHex? (s : String) : Option Hash :=
   if s.utf8ByteSize = 16 && isHex s then ofHex s else none