Stream: lean4

Markus Himmel (Jan 31 2021 at 05:54):

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 (Jan 31 2021 at 06:01): (it should return n1 instead of 0 there) Mario Carneiro (Jan 31 2021 at 06:03): @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 (Jan 31 2021 at 06:04): 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 (Jan 31 2021 at 06:06):

The bug is repeated in lean_nat_big_mod too

Mario Carneiro (Jan 31 2021 at 06:08):

I think it is lean -t 0

Markus Himmel (Jan 31 2021 at 06:08):

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

Mario Carneiro (Jan 31 2021 at 06:25):

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 (Jan 31 2021 at 06:28):

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

Markus Himmel (Jan 31 2021 at 06:28):

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 (Jan 31 2021 at 06:30):

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

Markus Himmel (Jan 31 2021 at 06:31):

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 (Jan 31 2021 at 06:32):

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

Mario Carneiro (Jan 31 2021 at 06:33):

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 (Jan 31 2021 at 06:34):

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 (Jan 31 2021 at 06:37):

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 (Jan 31 2021 at 06:39):

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 (Jan 31 2021 at 06:43):

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


:golf:

Marc Huisinga (Jan 31 2021 at 10:30):

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 (Jan 31 2021 at 10:33):

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 (Jan 31 2021 at 10:37):

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 (Jan 31 2021 at 10:44):

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 (Jan 31 2021 at 10:47):

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 (Jan 31 2021 at 16:36):

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.

Last updated: May 07 2021 at 12:15 UTC