Using `native_decide` to prove False?

Stream: general

[Jason Rute]

The three ways I know to use native_decide to prove False are to:

• Find a compiler bug
• Sneak in axioms (using @csimp, using cast)
• Use implemented_by

Are there others, especially ones which currently work but don't involve making new axioms or new implemented_bys?

[Bhavik Mehta]

There's also https://github.com/leanprover/lean4/issues/7463, which is somewhat a mix of your two and three

[Robin Arnez]

Well @[extern], but that fits in the same realm as @[implemented_by]. Otherwise I'd argue that the definition of a compiler bug is that it allows you to prove False using native_decide under otherwise sound conditions.

[Robin Arnez]

Oh and well ways to prove False without native_decide (e.g. skipKernelTC) are naturally also ways to let native_decide prove False

[Robin Arnez]

Example:

set_option debug.skipKernelTC true in
theorem hiThere [Add Nat] : 1 + 1 = 2 := by
  simp

theorem myFalse : False := by
  have := @hiThere ⟨fun _ _ => 0⟩
  simp only [instHAdd] at this
  contradiction

example : False := by
  let dvd : (2 : Int) ∣ -1 := myFalse.elim
  have h1 : Int.divExact (-1) 2 dvd = -1 := rfl
  have h2 : Int.divExact (-1) 2 dvd = 0 := by native_decide
  rw [h1] at h2
  contradiction

[Robin Arnez]

although I guess that doesn't really count because you already have False without it

[Bhavik Mehta]

There's also examples like this one: https://live.lean-lang.org/#project=mathlib-stable&codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOJgCmAdnAAoToCexEIwS6etxAxnWAK4xJbqFwAJoQBmcAOZwAFKQBccAHIoAlHHlL4sgLzSAGnAB6cOXEC4hAG1dAXWUA6YigAihcVEKEcaQtEIg4IKgB9ND95SQAGQzgAJjhAAyI4SO04LCohQlZgYTgAagBrQihiQiYvHz8AZ1QIAHdAkUYKgXkAMUbmnQDg1D8pVLgoGrhzcSsAbjgK0DBlIA, which are fixed by lean4#8060 where native_decide isn't used. (This example is deliberately non-minimal and uses mathlib, more elementary ones are available!)

import Mathlib

open Polynomial

noncomputable def g (n : Nat) : Nat := (X ^ n : ℝ[X]).natDegree
theorem my_thm : g 0 ^ 2 ≠ 0 := by decide +kernel
theorem show_false : False := my_thm (by rw [g]; simp)

[Robin Arnez]

Yeah, right, soundness problems count there too (hope that we don't have any more of those...)

[Robin Arnez]

Oh wait I forgot one: IO (although @[export] is the core reason still):

def getHeartbeats (x : List Nat) : Nat :=
  match IO.addHeartbeats x[0]! () with
  | .ok _ state =>
    match IO.getNumHeartbeats state with
    | .ok val _ => val

def compareHeartbeats (x : Nat) : Bool :=
  getHeartbeats [x] != getHeartbeats [x + 1 - 1]

example : False := by
  have : compareHeartbeats 100 := by native_decide
  simp [compareHeartbeats, getHeartbeats] at this

[Robin Arnez]

That's just because IO.RealWorld := Unit... (I am pretty sure there are more states of the real world than one)

[Yury G. Kudryashov]

Why can you use IO operations to get back to a pure function?

[Yury G. Kudryashov]

Also, shouldn't IO.RealWorld be opaque?

[Robin Arnez]

That might be a compiler thing I'm not sure. At least the intention of making it opaque is stated:

/- Like <https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld>.
   Makes sure we never reorder `IO` operations.

   TODO: mark opaque -/
def IO.RealWorld : Type := Unit

[Jason Rute]

This one I find the most interesting so far because it can be inlined into a single tactic proof using only the usual tactics:

example : False := by
  let getHeartbeats (x : List Nat): Nat :=
    match IO.addHeartbeats x[0]! () with
    | .ok _ state =>
      match IO.getNumHeartbeats state with
      | .ok val _ => val
  let compareHeartbeats (x : Nat) : Bool :=
    getHeartbeats [x] != getHeartbeats [x + 1 - 1]
  have : compareHeartbeats 100 := by native_decide
  simp [compareHeartbeats, getHeartbeats] at this

[Jason Rute]

By the way, should we file an issue about this last one? It might be intentional, but it sure feels like a compiler bug.

[Jason Rute]

(By "compiler bug", I guess I mean mismatches between pure code and their external implementations in core Lean.)

[Niels Voss]

Would making IO.RealWorld opaque fix this issue?

[Eric Wieser]

I think yes, unless we can make the above work without the ()

[Eric Wieser]

(I checked, you can't because native_decide won't operate on free variables)

[Eric Wieser]

A golfed version of the above:

example : False := by
  let getHeartbeats (x : Nat) : Nat :=
    let .ok _ state := IO.mkRef x ()  -- ensure `x` is not eliminated
    let .ok val state := IO.getNumHeartbeats state
    val
  have : getHeartbeats 0 ≠ getHeartbeats (0 + 1 - 1) := by native_decide
  simp [getHeartbeats] at this

[Mario Carneiro]

this seems a bit better than the random number version of this exploit I wrote a while back since that one only fails with 1/4 probability

[Mario Carneiro]

but it was added to the lean4checker test suite so you could add this one too

[Jason Rute]

I can’t find the random number exploit on the lean4checker GitHub repo. Do you have a link?

[Jason Rute]

Ok, I found the topic: #lean4 > soundness bug: native_decide leakage

[Jason Rute]

The example uses Lean.reduceBool (which again is a good reminder for those writing ad-hoc checks against this sort or thing that banning particular tactics, with say a regex, is not the right way to go :slight_smile: ).

[Jason Rute]

And here is the corresponding test in Lean4Checker: https://github.com/leanprover/lean4checker/blob/master/Lean4CheckerTests/ReduceBool.lean

[Jason Rute]

I just checked on the latest nightly and I think the above exploit using getHeartbeats is patched.

[Robin Arnez]

It's not, the compiler just got better at inlining. My version above still works

[Jason Rute]

Ok, here is Mario's golfed version, but with a dummy parameter y to prevent inlining:

example : False := by
  let getHeartbeats (x y : Nat): Nat :=  -- parameter `y` prevents inlining
    let .ok _ state := IO.mkRef x ()  -- ensure `x` is not eliminated
    let .ok val state := IO.getNumHeartbeats state
    val
  have : getHeartbeats 0 0 ≠ getHeartbeats (0 + 1 - 1) 1 := by native_decide
  simp [getHeartbeats] at this

[Jason Rute]

Here is even a simpler example. You don't need to use the input at all (although maybe this could get inlined away in the future).

example : False := by
  let getHeartbeats (x : Nat): Nat :=
    let .ok _ state := IO.mkRef 0 ()
    let .ok val state := IO.getNumHeartbeats state
    val
  have : getHeartbeats 0 ≠ getHeartbeats 1 := by native_decide
  simp [getHeartbeats] at this

[Cameron Zwarich]

@Robin Arnez @Jason Rute thanks for making test cases for lean4#9631! There are some incomplete aspects of the PR, but hopefully we can get it landed in the next week or so.

[Cameron Zwarich]

I'd like to come up with a plan to fix all of the known bugs with native_decide, prioritizing issues that are likely to come up with people using RL against Mathlib than ones that would likely only come from more directly adversarial usage.

[Jason Rute]

The most likely real world cases are bad implemented_bys, but they are already fixed immediately when found.

[Jason Rute]

Does this PR also fix the stochastic exploit in #lean4 > soundness bug: native_decide leakage?

[Cameron Zwarich]

Yes, it fixes the initial example Mario posted, in that the axiom list now always includes sorryAx.

[Parth Shastri]

Note that ST is also problematic: #lean4 > Ensuring naive purity @ 💬