[#14953] feat: remove deprecated in-kernel native reduction - #27
Open
downstream-lean4[bot] wants to merge 3 commits into
Open
[#14953] feat: remove deprecated in-kernel native reduction#27downstream-lean4[bot] wants to merge 3 commits into
downstream-lean4[bot] wants to merge 3 commits into
Conversation
downstream-lean4
Bot
added
the
adaptation
Contributor
Author
Build report for reference-manual: adapt to removal of in-kernel native reductionStayed green
|
`Lean.Meta.reduceNative?` was removed along with in-kernel native reduction; upstream dropped the corresponding branch from `whnfImp`, which `unfolds` mirrors.
`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.
Kha
reviewed
Aug 28, 2026
|
|
||
| * 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. |
Member
There was a problem hiding this comment.
We should probably describe here what such axioms look like?
There was a problem hiding this comment.
At the very least, we should have a bit about precisely how the axiom connects to the compiled code.
Kha
reviewed
Aug 28, 2026
| 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. |
Member
There was a problem hiding this comment.
Note, since it's not part of the diff: this is the "up to 4.28" section
| 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. |
There was a problem hiding this comment.
the external prover is not part of the trusted code base.
Is this still true? Before, the compiler was trusted and we ran a checker using compiled code. But if we "merely" emit an axiom, then we are trusting the checker, right? If not, then I think this sentence needs a bit of expansion to say in what way we are not trusting the external checker for the truth of the axiom.
Member
There was a problem hiding this comment.
Cadical remains outside the TCB as the elaborator, formerly the kernel, runs the certificate checker. We should probably say here that this is what the axiom stands for /cc @hargoniX
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is the adaptation PR for leanprover/lean4#14953.