diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index e302ee1d4e73..16416cf6b767 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -192,6 +192,7 @@ where -- avoid follow-up errors by (trying to) add broken decl as axiom addAsAxiom throw ex + recordAxioms decl addAsAxiom := do -- try to add as axiom with given type for def/theorem match decl with diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 81f3d84a62a9..f500d9b013c0 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -7,6 +7,7 @@ module prelude public import Lean.Elab.Deriving.Basic public import Lean.Elab.PreDefinition.Main +import Lean.TrustedAxiomAttr import all Lean.Elab.ErrorUtils public section namespace Lean.Elab @@ -1441,6 +1442,14 @@ this warning can be disabled with `set_option warn.classDefReducibility false`." addPreDefinitions docCtx preDefs for view in views, funFVar in funFVars do addLocalVarInfo view.declId funFVar + if linter.untrustedAxioms.get (← getOptions) then + -- lint on the kernel-check chain so that `collectAxioms` does not block elaboration + let act ← Core.wrapAsyncAsSnapshot (cancelTk? := none) + (desc := s!"linting axioms of {headers.map (·.declName)}") fun _ => + for header in headers do + withRef header.declId <| warnIfUsesUntrustedAxioms header.declName + let task ← BaseIO.mapTask act (← getEnv).checked + Core.logSnapshotTask { stx? := none, reportingRange := .skip, cancelTk? := none, task } processDeriving (headers : Array DefViewElabHeader) := do for header in headers, view in views do diff --git a/src/Lean/TrustedAxiomAttr.lean b/src/Lean/TrustedAxiomAttr.lean new file mode 100644 index 000000000000..fbc44559408b --- /dev/null +++ b/src/Lean/TrustedAxiomAttr.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2026 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 +import Lean.Util.CollectAxioms +import Lean.Util.Sorry +import Lean.Linter.Init +import Lean.AddDecl + +namespace Lean + +/-- +Marks an axiom as "trusted" so that the `linter.untrustedAxioms` linter does not warn about +declarations depending on axioms tagged with this attribute. +-/ +@[builtin_doc] +public builtin_initialize trustedAxiomAttr : TagAttribute ← + registerTagAttribute `trusted_axiom "mark an axiom as trusted so that `linter.untrustedAxioms` does not warn about declarations depending on it" fun declName => do + unless getOriginalConstKind? (← getEnv) declName matches some .axiom do + throwError "Cannot add attribute `@[trusted_axiom]` to non-axiom `{.ofConstName declName}`" + +public register_builtin_option linter.untrustedAxioms : Bool := { + defValue := false + descr := "Warn when a declaration added to the environment depends on an axiom that is not \ + tagged with `@[trusted_axiom]`. This should be considered a preliminary elaboration-side \ + check that does not replace the use of external checker tools such as `comparator` with \ + their own axiom checks. Unlike other linters, this linter is not enabled by `linter.all` \ + but only by setting this option explicitly, as it is useful only with a curated set of \ + `@[trusted_axiom]` declarations." +} + +open Linter in +public def warnIfUsesUntrustedAxioms (declName : Name) : CoreM Unit := do + unless linter.untrustedAxioms.get (← getOptions) do return + if (← MonadLog.hasErrors) then return + let env ← getEnv + let some info := env.find? declName | return + if info.isUnsafe then return + let axioms ← collectAxioms declName + -- Check the axioms first: a syntactic `sorry` always shows up as `sorryAx` in them, so we can + -- avoid the `hasSorry` term traversal for sorry-free declarations. + if axioms.contains ``sorryAx && warn.sorry.get (← getOptions) && + (info.type.hasSorry || (info.value? (allowOpaque := true)).any (·.hasSorry)) then + return + let offending := axioms.filter (!trustedAxiomAttr.hasTag env ·) + unless offending.isEmpty do + let axMsgs := offending.toList.map fun ax => m!"`{MessageData.ofConstName ax}`" + logLint linter.untrustedAxioms (← getRef) + m!"declaration depends on axioms that are not tagged \ + `@[trusted_axiom]`: {MessageData.joinSep axMsgs ", "}" + +end Lean diff --git a/src/Lean/Util/CollectAxioms.lean b/src/Lean/Util/CollectAxioms.lean index dc9897059a44..df92b84ef296 100644 --- a/src/Lean/Util/CollectAxioms.lean +++ b/src/Lean/Util/CollectAxioms.lean @@ -13,7 +13,11 @@ namespace Lean namespace CollectAxioms structure State where - /-- Cache mapping constants to their (sorted) axiom dependencies. -/ + /-- + Cache mapping constants walked by this run to their (sorted) axiom dependencies. Constants + answered by `extFind?` are deliberately not copied into this layer, so it contains exactly the + constants whose dependencies were not already recorded elsewhere. + -/ seen : NameMap (Array Name) := {} /-- Axioms accumulated for the current constant being processed. -/ axioms : NameSet := {} @@ -28,7 +32,8 @@ private def insertArray (s : NameSet) (axs : Array Name) : NameSet := /-- Collect axioms reachable from constant `c`, using `extFind?` to look up pre-computed axioms -for imported declarations. Results are cached in `State.seen`. +for imported and already-recorded declarations. Results for walked constants are cached in +`State.seen`, the second layer of the cache on top of `extFind?`. When processing a constant not found in `extFind?` or the cache, the function temporarily clears the axiom accumulator, recurses into the constant's dependencies, caches the result @@ -38,9 +43,9 @@ private partial def collect (extFind? : Environment → Name → Option (Array Name)) (c : Name) : M Unit := do let env ← read - -- Check extension for pre-computed axioms (imported declarations) + -- Check extension for pre-computed axioms (imported and already-recorded declarations) if let some axs := extFind? env c then - modify fun s => { s with axioms := insertArray s.axioms axs, seen := s.seen.insert c axs } + modify fun s => { s with axioms := insertArray s.axioms axs } return -- Check local cache let s ← get @@ -77,6 +82,8 @@ private partial def collect private def collectAndGet (extFind? : Environment → Name → Option (Array Name)) (c : Name) : M (Array Name) := do + if let some axs := extFind? (← read) c then + return axs collect extFind? c let some axs := (← get).seen.find? c | panic! s!"collectAndGet: '{c}' not in seen after collect" return axs @@ -95,10 +102,12 @@ binary search without requiring the extension object. -/ private structure ExportedAxiomsState where importedModuleEntries : Array (Array (Name × Array Name)) := #[] + /-- Axiom dependencies of current-module declarations, filled eagerly by `recordAxioms`. -/ + localEntries : NameMap (Array Name) := {} instance : Inhabited ExportedAxiomsState := ⟨{}⟩ -/-- Look up pre-computed axioms for an imported declaration. -/ +/-- Look up pre-computed axioms for an imported or already-recorded local declaration. -/ private def ExportedAxiomsState.find? (s : ExportedAxiomsState) (env : Environment) (c : Name) : Option (Array Name) := match env.getModuleIdxFor? c with @@ -108,14 +117,17 @@ private def ExportedAxiomsState.find? (s : ExportedAxiomsState) (env : Environme | some entry => some entry.2 | none => none else none - | none => none + | none => s.localEntries.find? c /-- Environment extension that records axiom dependencies for all declarations in a module. -Entries are computed once by `beforeExportFn` when the olean is serialized, not during -elaboration. During elaboration, `collectAxioms` walks bodies directly. Downstream modules -look up pre-computed entries for imported declarations, so axiom collection never crosses -module boundaries. +Entries for the current module are filled eagerly by `recordAxioms` as declarations pass the +kernel; the `sync` mode makes these writes accumulate along the `checked` environment chain so +that recording a declaration reuses the entries of all prior declarations. When the olean is +serialized, `exportEntriesFnEx` exports the entries of all exported declarations, computing any +entry missing due to e.g. realizations or error recovery. Downstream modules look up +pre-computed entries for imported declarations, so axiom collection never crosses module +boundaries. -/ private builtin_initialize exportedAxiomsExt : PersistentEnvExtension (Name × Array Name) (Name × Array Name) ExportedAxiomsState ← @@ -142,14 +154,38 @@ private builtin_initialize exportedAxiomsExt : -- Sort by name for binary search at import time. let entries := entries.qsort fun a b => Name.quickLt a.1 b.1 .uniform entries - asyncMode := .mainOnly + asyncMode := .sync } +/-- +Computes and records the axiom dependencies of the given just-added declaration into +`exportedAxiomsExt`. Entries recorded for earlier declarations are reused, so each constant is +walked only once per module. Skipped in realization contexts, which would require extension +replay; declarations without an entry are walked on demand by `collectAxioms` instead. +-/ +public def recordAxioms [Monad m] [MonadEnv m] (decl : Declaration) : m Unit := do + let env ← getEnv + if env.isRealizing then return + let privateEnv := env.setExporting false + let s := exportedAxiomsExt.getState env + let (_, st) := decl.getTopLevelNames.mapM (CollectAxioms.collectAndGet s.find?) + |>.run privateEnv |>.run {} + -- `seen` contains exactly the walked constants; skip walked imported constants missing from + -- the export table, which `find?` could never answer from `localEntries`. + let newEntries := st.seen.foldl (init := #[]) fun acc c axs => + if (env.getModuleIdxFor? c).isNone then + acc.push (c, axs) + else + acc + unless newEntries.isEmpty do + modifyEnv fun env => exportedAxiomsExt.modifyState env fun s => + { s with localEntries := newEntries.foldl (init := s.localEntries) fun m (c, axs) => m.insert c axs } + /-- Collect all axioms transitively used by a constant. -/ public def collectAxioms [Monad m] [MonadEnv m] (constName : Name) : m (Array Name) := do let env ← getEnv let privateEnv := env.setExporting false - let s := exportedAxiomsExt.getState (asyncMode := .mainOnly) env + let s := exportedAxiomsExt.getState env return CollectAxioms.runM privateEnv do CollectAxioms.collectAndGet s.find? constName diff --git a/tests/elab/linterUntrustedAxioms.lean b/tests/elab/linterUntrustedAxioms.lean new file mode 100644 index 000000000000..a8a6632edc40 --- /dev/null +++ b/tests/elab/linterUntrustedAxioms.lean @@ -0,0 +1,153 @@ +/-! +Tests the `@[trusted_axiom]` attribute and the `linter.untrustedAxioms` linter, which warns when a +declaration transitively depends on an axiom not tagged `@[trusted_axiom]`. +-/ + +axiom untrustedAx : 1 = 2 + +@[trusted_axiom] axiom trustedAx : 1 = 1 + +-- The linter is off by default. +#guard_msgs in +theorem offByDefault : 1 = 2 := untrustedAx + +-- `linter.all` does not enable this linter; it must be enabled explicitly. +set_option linter.all true in +#guard_msgs in +theorem allDoesNotEnable : 1 = 2 := untrustedAx + +set_option linter.untrustedAxioms true + +/-! Axiom declarations themselves are not linted, only their uses. -/ + +#guard_msgs in +axiom anotherUntrustedAx : 2 = 3 + +#guard_msgs in +@[trusted_axiom] axiom anotherTrustedAx : 2 = 2 + +/-! Direct use of an untrusted axiom warns; use of a trusted axiom does not. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesUntrusted : 1 = 2 := untrustedAx + +#guard_msgs in +theorem usesTrusted : 1 = 1 := trustedAx + +/-! Transitive dependencies are reported. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesTransitively : 2 = 1 := usesUntrusted.symm + +/-! All offending axioms are listed in a single warning. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `anotherUntrustedAx`, `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesBoth : 1 = 3 := untrustedAx.trans anotherUntrustedAx + +/-! Private declarations are linted as well. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +private theorem privateUses : 1 = 2 := untrustedAx + +/-! +Internal auxiliary declarations (e.g. `match` functions) are not linted separately; their axioms +are reported once via the surrounding declaration. +-/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesViaMatch : (n : Nat) → 1 = 2 + | 0 => untrustedAx + | _+1 => untrustedAx + +/-! +`sorryAx` is not reported for a declaration containing the `sorry` itself, which already produces +the `warn.sorry` warning. +-/ + +/-- +warning: declaration uses `sorry` +-/ +#guard_msgs in +theorem usesSorry : 1 = 2 := sorry + +/-! Transitive `sorry`s are not covered by `warn.sorry`, so `sorryAx` is reported for them. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `sorryAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesSorryTransitively : 2 = 1 := usesSorry.symm + +/-! The synchronous elaboration path warns as well. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +set_option Elab.async false in +theorem usesUntrustedSync : 1 = 2 := untrustedAx + +/-! `example`s are linted. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +example : 1 = 2 := untrustedAx + +/-! Explicitly disabling the linter. -/ + +set_option linter.untrustedAxioms false in +#guard_msgs in +theorem explicitOff : 1 = 2 := untrustedAx + +/-! The attribute can only be applied to axioms in the current module. -/ + +def notAnAxiom : Nat := 1 + +/-- error: Cannot add attribute `@[trusted_axiom]` to non-axiom `notAnAxiom` -/ +#guard_msgs in +attribute [trusted_axiom] notAnAxiom + +/-- +error: Cannot add attribute `[trusted_axiom]` to declaration `propext` because it is in an imported module +-/ +#guard_msgs in +attribute [trusted_axiom] propext + +/-- +error: Invalid attribute scope: Attribute `[trusted_axiom]` must be global, not `local` +-/ +#guard_msgs in +attribute [local trusted_axiom] anotherUntrustedAx