Linter for native_decide

Stream: mathlib4

[Michael Rothgang]

In light of the discussion on https://github.com/nielsvoss/lean-pitfalls: should there be a mathlib linter against native_decide? Right now, CI does not enforce this.

[Michael Rothgang]

#25297 implements one

[Damiano Testa]

I did not look carefully at the setting and unsetting of native_decide, but should the linter rather warn about introducing ofReduceBool? Isn't the issue that native_decide opens the door to adding the unsafe ofReduceBool axiom, rather than the tactic itself being potentially malicious?

It would be great if, when native_decide finds a "good" proof, that it suggested a proof that does not risk of becoming dependent on ofReduceBool with a refactor, though.

[Michael Rothgang]

Sure, warning about ofReduceBool would also be good/ could help to make the error message more specific. That said, unless native_decide suggests a "good" proof automatically, having proofs that could silently start to depend on ofReduceBool does not sound good either.

[Michael Rothgang]

In other words: once native_decide becomes self-replacing, linting against it is fine because you can either replace by a good proof, or you proof depends on ofReduceBool already.

[Eric Wieser]

Is the real request here to just do an axiom check?

[Kyle Miller]

Is there any proposal to make native_decide not always use ofReduceBool like it currently does?

[Damiano Testa]

Oh, my comment may have been based on a false premise: does native_decide always imply a dependency on ofReduceBool?

[Damiano Testa]

I naively thought that it might introduce one, not that it was guaranteed to.

[Kyle Miller]

Yes, it always uses ofReduceBool.

[Damiano Testa]

Ah, ok, so the linter is good!

[Damiano Testa]

Although I think that also having an axiom check might be good.

[Kyle Miller]

I'd say this justifies having only the axiom check :-)

[Kyle Miller]

If the axiom is found, could the linter look through the infotrees to implicate a tactic or term that introduced it? That's expensive, but it's only done in the rare case the axiom is present.

[Damiano Testa]

Yes, that might be a nice feature!

[Kyle Miller]

I take this slightly back: having a native_decide linter for mathlib is a good idea, since it can quickly activate and explain why it's not allowed

[Kyle Miller]

Note that you'd need to check for decide +native and decide (config := { native := true }) etc. etc. (Not sure how to reliably do that!)

[Kyle Miller]

Maybe decide along with any "native" in the Syntax? That should only give false positives for decide -native, etc., but better safe than sorry.

[Eric Wieser]

I think it's much cheaper to do an axiom check globally

[Eric Wieser]

Otherwise we're recursing through the same constants every time we transitively check for axioms, instead of memoizing them across all of mathlib

[Eric Wieser]

(So I'm suggesting an environment linter)

[Kyle Miller]

For reference, how native_decide works:

1. It adds an auxiliary definition def auxdef : Bool := decide p
2. It adds an auxiliary lemma lemma aux : p := of_decide_eq_true (Lean.ofReduceBool auxdef true rfl).
3. If the kernel accepts the lemma, then aux is used as the proof of p.

Step 2 is what triggers evaluating auxdef using the "#eval interpreter."

There's not really any room for it come up with a proof that doesn't use ofReduceBool. If you accept ofReduceBool, you're happy with the proof, so there's no reason for it to then spend time having the kernel try reducing auxDef to true directly.

[Kyle Miller]

Eric Wieser said:

Otherwise we're recursing through the same constants every time we transitively check for axioms, instead of memoizing them across all of mathlib

It might only look at new constants, if that's somehow possible to detect.

Or there could be an environment extension for "this constant has been checked"

[Julian Berman]

Otherwise we're recursing through the same constants every time we transitively check for axioms, instead of memoizing them across all of mathlib

Is there a reason to prefer a linter if this is the case? Isn't whether (and how) to do an axiom checker somewhat related to Mathlib's CI running an external type checker (or checkers)? There was discussion of the latter in another thread I believe but Mathlib doesn't yet do so. E.g. running nanoda would allow both independently checking Mathlib's declarations with a second checker as well as ensuring no additional axioms are used?