# Zulip Chat Archive

## Stream: lean4

### Topic: Contradiction?

#### 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):

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 (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