About native_decide

Stream: general

[Alfredo Moreira-Rosa]

I just discovered native_decide (before was doing the same using an elab evalExpr).
I've almost created a kernel verified automated proof for a decidable equivalence, but meanwhile i'm using native_decide and it's nice to have this option while working on the formal proof.

And so, i have two questions.

• i see that native_decide is not allowed in mathlib. So i guess it's considered harmful even if not trying to exploit the already identified hacks people have found ?
• i'm curious if there could be a subset of lean (that prevents using the already discovered hacks) that could be activated through a flag to have a more trusted native_decide ?

[(deleted)]

Yeah native_decide can be used to hack Lean, so all uses of native_decide are banned.

[Weiyi Wang]

I think it is hard to define the boundary of "subset without known hacks" (or rather, the boundary is already decided: things without native_decide vs with native_decide).

[(deleted)]

Currently, there is no version of native_decide that is less hackable, so we have to make do with decide. Even though there are things that can't be solved with decide.

[(deleted)]

Yi is right.

[(deleted)]

But don't despair! simp might be magical enough to do what you need

[Henrik Böving]

Weiyi Wang said:

I think it is hard to define the boundary of "subset without known hacks" (or rather, the boundary is already decided: things without native_decide vs with native_decide).

That's a bit too pessimistic. If you e.g. have a system for proof by reflection where you control all the code that actually gets executed within the native_decide call and only the input is under control of the attacker things can very much turn out to be fine.

[Alfredo Moreira-Rosa]

yes, i'm halfway through my automated proof, exactly using simp and custom simpsets , so in the mean time i just make lean show a warning message when it's used :
image.png

[Weiyi Wang]

Henrik Böving said:

Weiyi Wang said:

I think it is hard to define the boundary of "subset without known hacks" (or rather, the boundary is already decided: things without native_decide vs with native_decide).

That's a bit too pessimistic. If you e.g. have a system for proof by reflection where you control all the code that actually gets executed within the native_decide call and only the input is under control of the attacker things can very much turn out to be fine.

I agree with you when I use native_decidein my personal project. If I were to put the position of a mathlib maintainer, I would be more pessimistic: the idea that "mathlib could be wrong because of native_decide" is contagious, even if it isn't true

[Weiyi Wang]

(I realized I posted this in the context of mathlib because OP mentioned it. But I agree with you if we are talking about projects in general)

[Alfredo Moreira-Rosa]

Just finished my automated proof! no more native_decide, it served me well :)
image.png

[Alfredo Moreira-Rosa]

But it's about 10 times slower :sweat_smile:

[Violeta Hernández]

(off-topic, but i believe "kinetic" is the word you're looking for)

[Alfredo Moreira-Rosa]

Yes, I'm french, we have our own words :grinning_face_with_smiling_eyes:

[Siddhartha Gadgil]

For completeness, there is decide +kernel which is more powerful than decide but trusted.

[Alfredo Moreira-Rosa]

So an alternative question, is decide +kernel considered an ok proof ?

[Alfredo Moreira-Rosa]

an example for a dimensional analysis check :

theorem not_e_equal_mc_dim_check (E : WithDim Dimension.Energy) (m : WithDim Dimension.Mass) :
   ¬ 𝒟 E =  𝒟 (m * c) := by
    simp_dim
    decide +kernel

[Alfredo Moreira-Rosa]

does this generate terms that an external checker can check ?

[Eric Wieser]

It should do, the kernel is the bit that external checkers implement

[Kyle Miller]

Both decide and decide +kernel for a goal t is the same as doing of_decide_eq_true (id (Eq.refl true) : decide t = true); the only difference is that +kernel sends the term to the kernel for checking immediately.

If you use show_term, you'll see something like not_e_equal_mc_dim_check._proof_1_1. The way decide +kernel works is that it wraps up this of_decide_eq_true proof as an auxiliary theorem and sends it to the kernel for checking. Without +kernel, it will additionally use the elaborator typechecker.

The decide +kernel tactic is nearly always faster than decide if it succeeds. If it fails, decide is potentially faster (it respects definition transparency, so might unfold less). Since decide is frequently attempted in automation, for example the trivial tactic, so failing fast is important.