Contradiction?

Stream: lean4

[Markus Himmel]

I belive that I have found a proof of false in the current nightly of Lean 4. Could someone verify that this is indeed the case and I'm not doing something stupid?

theorem proofOfFalse : False := Nat.oneNeZero $ (Nat.modZero 1).symm.trans rfl
#print proofOfFalse
#print axioms proofOfFalse

$ lean --version
Lean (version 4.0.0-nightly-2021-01-31, commit 95ebd58ae95c, Release)
$ lean test.lean
theorem proofOfFalse : False :=
Nat.oneNeZero (Eq.trans (Eq.symm (Nat.modZero 1)) rfl)
'proofOfFalse' does not depend on any axioms

I'm on Ubuntu 20.04 and I'm using the prebuilt binaries from here.

[Mario Carneiro]

Here's the bug: https://github.com/leanprover/lean4/blob/master/src/include/lean/lean.h#L1361

(it should return n1 instead of 0 there)

[Mario Carneiro]

@Markus Himmel does it work on trust level 0? This bug involves executing C code via @[extern "lean_nat_mod"] that might not be executed at trust 0

[Markus Himmel]

Is this the right invocation?

$ lean --trust=0 test.lean
theorem proofOfFalse : False :=
Nat.oneNeZero (Eq.trans (Eq.symm (Nat.modZero 1)) rfl)
'proofOfFalse' does not depend on any axioms

[Mario Carneiro]

The bug is repeated in lean_nat_big_mod too

[Mario Carneiro]

I think it is lean -t 0

[Markus Himmel]

Passing -t 0 doesn't seem to make a difference

[Mario Carneiro]

it's also in lean_int_mod; it's not clear if lean_int_big_mod has the bug because it doesn't do a division by zero check, it just calls directly into GMP with a zero divisor, although I didn't manage to get it to crash and I'm not sure what GMP does with that

[Mario Carneiro]

from the docs it seems like it deliberately causes a division by zero exception, so maybe lean is catching it?

[Markus Himmel]

I have a crash involving big integers and modding by zero:

#eval (2147483648 % 0) + (-0)

crashes Lean 4 with a Floating point exception

[Mario Carneiro]

that doesn't look like it uses integers, is the elaborator doing something tricky with default instances?

[Markus Himmel]

Why shouldn't it use integers? I think Floating point exception is what you get when you do x % 0 in C/C++ code.

[Mario Carneiro]

Yeah, it's because the idiv instruction on x86 yields the SIGFPE fault which is "floating point exception"

[Mario Carneiro]

I don't understand why #check (rfl : Int.mod 123456789123456789 0 = 0) works though, even though #eval Int.mod 123456789123456789 0 causes the crash

[Mario Carneiro]

The same thing works with Int.div in place of Int.mod but in that case Int.div n 0 = 0 is actually correct

[Mario Carneiro]

Markus Himmel said:

Why shouldn't it use integers?

I meant that if you write that in lean 3 it won't use int unless you put a type ascription somewhere

[Mario Carneiro]

BTW kudos to the vscode-lean4 extension for being able to restart lean so smoothly after a crash; you can just change the text and the highlights come back

[Mario Carneiro]

theorem proofOfFalse : False := Nat.zeroNeOne (Nat.modZero 1)
#print axioms proofOfFalse

:golf:

[Marc Huisinga]

Mario Carneiro said:

Markus Himmel does it work on trust level 0? This bug involves executing C code via @[extern "lean_nat_mod"] that might not be executed at trust 0

I'm not sure if you can disable this particular feature, i.e. reduction of closed nat terms (see the bottom of https://leanprover.github.io/lean4/doc/nat.html).

Mario Carneiro said:

BTW kudos to the vscode-lean4 extension for being able to restart lean so smoothly after a crash; you can just change the text and the highlights come back

The watchdog in the server does this, not the extension. The vscode LSP client restarts aren't quite as smooth and tend to run into restart loops (until eventually giving up entirely after 4 retries).

[Mario Carneiro]

Is there a way to tell the difference between C code in the TCB from out? I was previously holding the contradictory beliefs that all extern functions were disabled at trust level 0, and operations on the new primitive nat literals are handled directly by the kernel

[Marc Huisinga]

It may also be that this does not apply to mod, given that it's in Data/Nat/Div and not Prelude. I'll wait for someone who understands the internals to chime in :)

[Mario Carneiro]

From https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/WHNF.lean#L550-L566, it looks like the only trusted replacements are the functions Nat.add, Nat.sub, Nat.mul, Nat.div, Nat.mod, Nat.ble, Nat.beq coming from reduceNat?, plus the more general purpose Lean.reduceBool, Lean.reduceNat coming from reduceNative? (and I think the latter show up in #print axioms)

[Mario Carneiro]

This also answers the question of why rfl : Int.mod 123456789123456789 0 = 0 worked, because it's not exercising the bug in lean_int_big_mod because it's evaluating the model instead of the efficient version, but that reduces to Nat.mod big_number 0 which reduces using the bad lean_nat_big_mod since Nat.mod is one of the trusted functions

[Leonardo de Moura]

I pushed a fix.
https://github.com/leanprover/lean4/commit/3fa1f355eb4b717a1b1f59e1bb8f1a9d32b45ca6
The bug was due to a mismatch between the Nat.mod definition in Lean and the implementation used in the runtime.
The Lean kernel type checker (implemented in C++) uses some Nat runtime functions to speedup reduction. Recall that I mentioned this new feature during the Lean 4 presentation at Lean Together. The kernel type checker that implements this feature is here:
https://github.com/leanprover/lean4/blob/master/src/kernel/type_checker.cpp#L585-L594
lean::nat_mod is just a wrapper for lean_nat_mod that is fixed by the commit above.

Remarks:

• The file Lean/Meta/WHNF.lean is not part of the kernel. It implements the whnf operation for the elaborator.

• The native implementation of the functions at https://github.com/leanprover/lean4/blob/master/src/kernel/type_checker.cpp#L585-L594
  are part of the trusted code base.

• I will add a flag for disabling this feature.

• The runtime implementation of Int.mod probably doesn't match the Lean definition too. I haven't checked yet, but it will not affect proofs because lean_int_mod is not used by the kernel type checker.