Checked example🔗

import Std.Tactic.BVDecide
/-! # Concrete facts

The concrete facts use native proof evaluation. -/
theorem equal : (2 : Nat) = 2 := by native_decide
theorem gcdValue : Nat.gcd 1071 462 = 21 := by decide +native
theorem commute (x y : BitVec 8) : x * y = y * x := by bv_decide

equal (theorem) [Prop] type=2 = 2 axioms=["equal._native.native_decide.ax_1_1"] -> compiler-trusting

equal._native.native_decide.ax_1_1 (axiom) [AXIOM, Prop] roles=["internal"] type=decide (2 = 2) = true axioms=["equal._native.native_decide.ax_1_1"] -> compiler-trusting

gcdValue (theorem) [Prop] type=Nat.gcd 1071 462 = 21 axioms=["gcdValue._native.decide.ax_1_1"] -> compiler-trusting

gcdValue._native.decide.ax_1_1 (axiom) [AXIOM, Prop] roles=["internal"] type=decide (Nat.gcd 1071 462 = 21) = true axioms=["gcdValue._native.decide.ax_1_1"] -> compiler-trusting

commute (theorem) [Prop] type=∀ (x y : BitVec 8), x * y = y * x axioms=["commute._native.bv_decide.ax_1_5", "Classical.choice", "propext", "Quot.sound"] -> compiler-trusting

commute._native.bv_decide.ax_1_5 (axiom) [AXIOM, Prop] roles=["internal"] type=Std.Tactic.BVDecide.Reflect.verifyBVExpr commute._expr_def_1_1 commute._cert_def_1_1 = true axioms=["commute._native.bv_decide.ax_1_5", "Classical.choice", "propext", "Quot.sound"] -> compiler-trusting

- import Std.Tactic.BVDecide
- /-! # Concrete facts
- 
- The concrete facts use native proof evaluation. -/
- theorem equal : (2 : Nat) = 2 := by native_decide
- theorem gcdValue : Nat.gcd 1071 462 = 21 := by decide +native
- theorem commute (x y : BitVec 8) : x * y = y * x := by bv_decide
+ import Init
+ /-! # Concrete facts
+ 
+ The same concrete facts have kernel proofs. -/
+ theorem equal : (2 : Nat) = 2 := rfl
+ theorem gcdValue : Nat.gcd 1071 462 = 21 := by decide
+ theorem commute (x y : BitVec 8) : x * y = y * x := BitVec.mul_comm x y

import Init
/-! # Concrete facts

The same concrete facts have kernel proofs. -/
theorem equal : (2 : Nat) = 2 := rfl
theorem gcdValue : Nat.gcd 1071 462 = 21 := by decide
theorem commute (x y : BitVec 8) : x * y = y * x := BitVec.mul_comm x y

The correction proves the same three facts by kernel-checked proofs: rfl, decide by kernel reduction, and the library lemma BitVec.mul_comm. The violation reports each generated axiom and its parent theorem.

Checked by a fresh single-file audit of <example>/Fixture.lean (axiomGate --file, claim kernel-only, execution checked): violating run rejected, corrected run completed.

How to fix it🔗

1. Replace by native_decide or by decide +native with by decide when kernel reduction of the decision procedure is feasible.

2. Replace by bv_decide with a proof from BitVec library lemmas, or with bv_normalize when normalization alone closes the goal.

3. Otherwise give a structural proof, or prove a smaller lemma that decide can handle and combine the pieces.

4. If the example exists only to teach the mechanism, keep it in documentation as a trusted-compiler teaching fence (RG4004), never on a claimed surface.

Why it matters🔗

Compiled evaluation is outside the kernel's checking. A compiler or runtime defect could make a false proposition "proved". Compiler-trusting is therefore not one of the three logical labels and never counts as conforming evidence.

What triggers it🔗

native_decide and decide +native evaluate a decision procedure with compiled code, and bv_decide, bv_decide? and bv_check check a SAT certificate with compiled code; each adds an axiom asserting the result through Lean.Meta.nativeEqTrue, named after the tactic name it passes (._native.native_decide.ax_…, ._native.decide.ax_…, ._native.bv_decide.ax_…), and private to the module when a module file elaborates the proof without exporting. The checker authenticates such an axiom from three observations: its name is one the scheme generates under the name of a declaration of its module; it asserts e = true with e in the tactic's exact shape, and an independent native replay of e returns true; and a fresh re-elaboration shows that the command introducing that declaration adds an axiom of the same origin and statement, and that no axiom declaration occurs in that command's syntax or macro expansions. The axiom and every declaration depending on it are then classified compiler-trusting and rejected with applicability compiler-trusting. The built-in axioms Lean.trustCompiler, Lean.ofReduceBool and Lean.ofReduceNat in a transitive axiom set are compiler-trusting by their exact identity.

Final environment metadata cannot authorize a generated native-proof axiom; fresh re-elaboration of the exact source establishes it. An unauthenticated axiom that only looks native is not compiler-trusting.

Required proof shape🔗

The replacement proof proves the same proposition. Kernel reduction (decide, rfl) is permitted, subject to the surface's foundation profile.

What a passing result establishes🔗

No positive declaration depends on a compiler-trusting axiom: an authenticated native-proof axiom or the built-in Lean.trustCompiler, Lean.ofReduceBool or Lean.ofReduceNat.

It does not establish:

• Performance of the kernel replacement proof; cost claims are separate (R-COST).

It leaves these review obligations open: R-QUALIFY, R-COST.

Configuration and exceptions🔗

Authenticated native proofs are reported separately in documentation teaching mode (lean-trusted-compiler fences) and remain excluded from conforming positives.

Limitations and unsupported cases🔗

The editor may defer authentication and report a pending result; the project command completes it.

An unauthenticated axiom that merely looks native is not compiler-trusting; it is rejected as an unknown axiom (RG1003) or project axiom (RG1001).

Authentication does not depend on the surrounding syntax: a native tactic anywhere in a declaration's elaboration is covered, in a tactic sequence or combinator, a nested by block, a grind => or sym => block, a where clause, a declaration with parameters (+revert), attributes or a namespaced, public or private name, under set_option … in, in ordinary and module files.

An axiom with a native name and a natively true statement stays a project axiom (RG1001) when the source declares it, as an axiom command written directly or produced by a macro, even one whose elaboration fails after adding it, or when a different command adds it than the one introducing the declaration its name belongs to. The declaration check reads syntax, quoted syntax included, and matches no names, so a command that both contains axiom syntax and uses a native tactic has no native axiom authenticated; its native axioms fail closed as RG1001 and RG1003. A custom tactic, elaborator or metaprogram that adds such an axiom without declaring it is classified compiler-trusting: the axiom asserts only what native evaluation confirmed.

The build is matched to the fresh re-elaboration by generated origin and asserted statement. When two commands add axioms of the same origin and statement, for example an authored spoof beside the genuine proof, neither is authenticated and both fail closed as RG1001 and RG1003.

Sources🔗

Normative clauses

standard §7.5 Proof Completeness and Foundation Strength

Checklist rows

FOUND-05, FOUND-03, THEOREM-10, THEOREM-01, THEOREM-06, DECL-03, COMP-01, BUILD-01

Detector, policy and proof sources

lean/RegulaPolicy/Decision.lean, lean/RegulaPolicy/NativeAxiom.lean, lean/Regula/Checker/Frontend.lean, lean/RegulaCore/Policy.lean

Proved linkage

The shared declaration decision RegulaPolicy.declarationFailure (its first failed requirement, declarationFailure_ordered) is mapped to a rule by the injective Regula.ruleForFailure. Project, file and documentation audits run it through Regula.Checker.Policy.checked_memberRule (ruleForMember_eq); the editor runs Regula.Linter.checked_editorDecision. For the same member and request, the editor passes exactly when the project decision selects no rule (Regula.Checker.Policy.editor_decision_none_iff), a rule it renders is the project decision's rule (editor_decision_rule), and a pending result withholds a project rule whose failure needs generated-role evidence (editor_decision_pending). The editor's request domain is the project's without teaching (editor_request_sound, editor_request_complete). The observed declaration fields and generated-role evidence are hypotheses of these theorems. The compiler-trusting and native role sets come from RegulaPolicy.authorize. RegulaPolicy.authorizedNativeAxioms_iff characterizes the authenticated native roles, and native_generated shows that each is a name Lean's nativeEqTrue scheme generates for native_decide, decide +native or bv_decide under a prefix related to an inventory declaration by GeneratedPrefix, and native_provenance that its statement was natively replayed and that a command of its module's fresh transcript adds an axiom of the same origin and statement while its recorded syntax declares no axiom. generatedPrefix_iff shows that, for a declaration name without macro scopes, these are exactly the names the generator gives that declaration in its own module in either privacy mode. The execution probe classifies by RegulaPolicy.compilerTrustingAxiomName, which compilerTrustingAxiomName_iff characterizes as exactly those generated names and Lean's three compiler axioms. Both characterizations assume the runtime string append RuntimeStringAppend.