From df340c3d632a3214049772c34c421e4957344b85 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Fri, 28 Aug 2026 14:02:14 +0000 Subject: [PATCH 1/4] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index b8f3deceb..8a1e1338d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-08-27 +leanprover/lean4-pr-releases:pr-release-14953-7c37619 From 32522e66ac855d590f43cd5c78c3497caeb54434 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 28 Aug 2026 14:46:21 +0000 Subject: [PATCH 2/4] mathlib4: drop removed `reduceNative?` unfolding step `Lean.Meta.reduceNative?` was removed along with in-kernel native reduction; upstream dropped the corresponding branch from `whnfImp`, which `unfolds` mirrors. --- mathlib4/Mathlib/Tactic/ClickSuggestions/Unfold.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/mathlib4/Mathlib/Tactic/ClickSuggestions/Unfold.lean b/mathlib4/Mathlib/Tactic/ClickSuggestions/Unfold.lean index e972fdb6b..fc2494fa1 100644 --- a/mathlib4/Mathlib/Tactic/ClickSuggestions/Unfold.lean +++ b/mathlib4/Mathlib/Tactic/ClickSuggestions/Unfold.lean @@ -92,8 +92,6 @@ where return ← go e (acc.push e) if let some e ← reduceNat? e then return acc.push e - if let some e ← reduceNative? e then - return acc.push e if let some e ← unfoldProjDefaultInst? e then -- when unfolding a default instance, don't add it to the array of unfolds. let e ← whnfCore e From 6a32a59e72e005831c6616e320bdecbf4d25190c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 28 Aug 2026 14:49:05 +0000 Subject: [PATCH 3/4] reference-manual: adapt to removal of in-kernel native reduction `Lean.trustCompiler`, `Lean.reduceBool`/`reduceNat` and `Lean.ofReduceBool`/`ofReduceNat` no longer exist, so `{name}` and `signature` references to them no longer resolve. Drop the "Standard Axioms" entries and the reflection example that used them, and describe the per-invocation axioms that `native_decide` and `bv_decide` have generated since Lean 4.29.0 instead. The historical `validating-trustCompiler` section keeps its text as plain code spans. --- reference-manual/Manual/Axioms.lean | 36 ++----------------- .../Manual/BasicTypes/BitVec.lean | 2 +- reference-manual/Manual/BasicTypes/Float.lean | 2 +- reference-manual/Manual/ValidatingProofs.lean | 8 ++--- 4 files changed, 8 insertions(+), 40 deletions(-) diff --git a/reference-manual/Manual/Axioms.lean b/reference-manual/Manual/Axioms.lean index 2772f4744..ca652f161 100644 --- a/reference-manual/Manual/Axioms.lean +++ b/reference-manual/Manual/Axioms.lean @@ -181,7 +181,7 @@ Because they occur only in a proof, the compiler has no problem generating code: tag := "standard-axioms" %%% -There are seven standard axioms in Lean. The first three axioms are important parts of how mathematics is done in Lean: +There are four standard axioms in Lean. The first three axioms are important parts of how mathematics is done in Lean: * ```signature Classical.choice.{u} {α : Sort u} : Nonempty α → α ``` @@ -202,40 +202,8 @@ Uses of this axiom are not intended to occur in finished proofs, as it can be us sorryAx {α : Sort u} (synthetic := true) : α ``` -Three final axioms do not truly exist for their _mathematical_ content; from a mathematical perspective they prove trivial statements: - - * ```signature - Lean.trustCompiler : True - ``` - - * ```signature - Lean.ofReduceBool (a b : Bool) : Lean.reduceBool a = b → a = b - ``` - * ```signature - Lean.ofReduceNat (a b : Nat) : Lean.reduceNat a = b → a = b - ``` - -These axioms instead track proofs that depend on the correctness of the entire compiler, and not just on the much smaller {tech}`kernel`. - -:::example "Creating and Tracking Proofs That Trust the Compiler" -The functions {name}`Lean.reduceBool` and {name}`Lean.reduceNat` can be invoked to have the compiler perform a calculation; this can greatly improve performance of implementations of proof by reflection. - -```lean -def largeNumber : Nat := Lean.reduceNat (230_000 + 4_500 + 1_000_067) -``` - -The resulting term depends on the axiom {name}`Lean.trustCompiler` in order to track the fact that this calculation depends on the correctness of the compiler. - -```lean (name := printAxExC1) -#print axioms largeNumber -``` -```leanOutput printAxExC1 -'largeNumber' depends on axioms: [Lean.trustCompiler] -``` -::: - :::example "Axioms and the `native_decide` Tactic" -Instead of appealing to {name}`Lean.trustCompiler`, the {tactic}`native_decide` tactic creates a bespoke axiom for each invocation. +The {tactic}`native_decide` tactic creates a bespoke axiom for each invocation. This allows each axiom to be audited for the precise statement that it proves. ```lean (name := printAxExC2) diff --git a/reference-manual/Manual/BasicTypes/BitVec.lean b/reference-manual/Manual/BasicTypes/BitVec.lean index 78e8e8f07..9fe6d6fe6 100644 --- a/reference-manual/Manual/BasicTypes/BitVec.lean +++ b/reference-manual/Manual/BasicTypes/BitVec.lean @@ -167,7 +167,7 @@ tag := "BitVec-automation" In addition to the full suite of automation and tools provided by Lean for every type, the {tactic}`bv_decide` tactic can solve many bitvector-related problems. This tactic invokes an external automated theorem prover (`cadical`) and reconstructs the proof that it provides in Lean's own logic. -The resulting proofs rely only on the axiom {name}`Lean.ofReduceBool`; the external prover is not part of the trusted code base. +The resulting proofs rely only on a dedicated axiom that {tactic}`bv_decide` generates for each invocation; the external prover is not part of the trusted code base. :::example "Popcount" diff --git a/reference-manual/Manual/BasicTypes/Float.lean b/reference-manual/Manual/BasicTypes/Float.lean index b0b615256..210c62ba8 100644 --- a/reference-manual/Manual/BasicTypes/Float.lean +++ b/reference-manual/Manual/BasicTypes/Float.lean @@ -359,7 +359,7 @@ Floating-point numbers fall into one of three categories: ### Inequalities The decision procedures for inequalities are opaque constants in the logic. -They can only be used via the {name}`Lean.ofReduceBool` axiom, e.g. via the {tactic}`native_decide` tactic. +They can only be used via native evaluation, e.g. via the {tactic}`native_decide` tactic. {docstring Float.le} diff --git a/reference-manual/Manual/ValidatingProofs.lean b/reference-manual/Manual/ValidatingProofs.lean index 57ea002ce..a19e8f540 100644 --- a/reference-manual/Manual/ValidatingProofs.lean +++ b/reference-manual/Manual/ValidatingProofs.lean @@ -110,7 +110,7 @@ This command prints the set of axioms used by the theorem and the theorems it de The three axioms above are standard axioms of Lean's logic, and benign. * If {name}`sorryAx` is reported, then this theorem or one of its dependencies uses {lean}`sorry` or is otherwise incomplete. -* If {name}`Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion. +* If an axiom generated by native evaluation is reported, then compiled code is trusted as part of the proof; see below for a discussion. * Any other axiom means that a custom axiom was declared and used, and the theorem is only valid relative to the soundness of these axioms. ## Trust @@ -227,11 +227,11 @@ This is used by the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +nati Specific uses wrapped in {tech}[honest] tactics (e.g. {tactic}`bv_decide`) are generally trustworthy. The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted. -General use ({tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` or direct use of {name}`Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation. +General use ({tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` or direct use of `Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation. In particular, for every {attr}`implemented_by`/{attr}`extern` attribute in libraries it becomes part of the trusted code base that the replacement is semantically equivalent. -All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`. +All these uses show up as an axiom `Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`. External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler. When that level of checking is needed, proofs have to avoid using native evaluation. -Since Lean 4.29.0, the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` and {tactic}`bv_decide` tactics no longer use {name}`Lean.trustCompiler`, but instead introduce one dedicated axiom for each computation that is asserted by native computation. The {name}`Lean.trustCompiler` machinery is deprecated and will eventually be removed. +Since Lean 4.29.0, the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` and {tactic}`bv_decide` tactics no longer use `Lean.trustCompiler`, but instead introduce one dedicated axiom for each computation that is asserted by native computation. The `Lean.trustCompiler` machinery has since been removed. From fb57dfe5283e05e0a8a7a40dccd50eb48f41de19 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Sat, 29 Aug 2026 10:34:55 +0000 Subject: [PATCH 4/4] downstream: undo overrides --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 8a1e1338d..b8f3deceb 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14953-7c37619 +leanprover/lean4:nightly-2026-08-27