native.float equality is inconsistent

Stream: general

[Mario Carneiro]

I just noticed that float equality is exposed as an implementation of decidable_eq. This is not correct:

def test_eq {α} [decidable_eq α] (x : α) := to_bool (x = x)

theorem test_eq_tt {α} [decidable_eq α] (x : α) : test_eq x = tt :=
(to_bool_iff _).2 rfl

#eval test_eq native.float.qNaN -- ff

[Mario Carneiro]

We could just implement has_equiv or some other notation instead of = (which means something specific in lean and does not permit funny things like IEEE float equality)

[Mario Carneiro]

Since there is no to_bits function on native.float, it would also be possible to implement a decidable_eq instance that makes any two NaNs equal, i.e. x = y <-> x.eq y \/ (is_nan x /\ is_nan y)

[Marc Huisinga]

https://github.com/leanprover/lean4/commit/705530b62bc23b47c0ba9baa8e199ab376b8fd7b :grinning:

[Jacques Carette]

Note that you also run into trouble with +-infinity -- if they both invert to unsigned 0, things get weird again. But +-0 are supposed to be equal (in IEEE's highly non-mathematical notion of equal).

[Mario Carneiro]

ah, that's true, my proposed alternative would have to check for signed zero

[Mario Carneiro]

probably the easiest implementation of a conforming = is just x.to_bits = y.to_bits

[Marc Huisinga]

yup, +0 = -0 but 1/+0 = +inf != -inf = 1/-0

[Mario Carneiro]

def test_congr {α} [decidable_eq α] (x y : α) (f : α → α) := to_bool (x = y → f x = f y)

theorem test_congr_tt {α} [decidable_eq α] (x y : α) (f) : test_congr x y f = tt :=
(to_bool_iff _).2 (λ x, by rw x)

#eval test_congr (0:native.float) (-0) (λ x, 1 / x) -- ff

[Eric Wieser]

I'm guessing not even a quot can represent the irreflexivity of nan equality?

[Mario Carneiro]

no, that would help with the congr example just given but not irreflexivity

[Mario Carneiro]

But I think any quotient that identifies 0 and -0 and is closed under congr would have to identify +inf and -inf; is it possible to prove this also identifies all finite numbers?

[Mario Carneiro]

oh lol there is -nan too

[Marc Huisinga]

Mario Carneiro said:

is it possible to prove this also identifies all finite numbers?

-inf <= x <= +inf?

[Mario Carneiro]

uh oh: tanh inf = 1, tanh -inf = -1

[Mario Carneiro]

Are you assuming le_antisymm there @Marc Huisinga ?

[Mario Carneiro]

I'm just assuming that the equality is closed under congruence

[Marc Huisinga]

i haven't actually looked up how stuff is specified in lean 3, just guessing

[Mario Carneiro]

There is no specification, they are mostly uninterpreted functions

[Mario Carneiro]

which is mostly fine, except that this still assumes they are "functions", i.e. respect equality

[Mario Carneiro]

and so implementing decidable_eq is a strong statement since two things that are equal can't be distinguished by later function application

[Mario Carneiro]

I'm not even sure it's totally safe to assume they are functions in this sense in lean 4 since the compilation works by generating C code and gcc can do funny things like increasing the precision on intermediate computations

[Mario Carneiro]

so determinism goes out the window

[Leonardo de Moura]

@Marc Huisinga There is no float type in Lean 3. It seems someone added them to the Lean 3 community branch.

[Bryan Gin-ge Chen]

float was added to community Lean 3 by @Edward Ayers in lean#2.

[Jason Rute]

When you say "inconsistent", do you mean you can prove false or just that it is weird behavior in the meta world? I tried to turn your example into a proof of tt = ff, but even though #eval test_eq native.float.qNaN comes out asff, I can't find a way to prove test_eq native.float.qNaN = ff. Does the fact that float is meta protect the consistency of Lean (3 community version)?

[Jason Rute]

This won't even check:

example : decidable_eq native.float := native.float.dec_eq

So even though native.float.dec_eq looks like an inconsistent axiom, is not usable in proofs it seems. (Maybe this is all obvious, but I got confused with the "inconsistent" terminology.)

[Jason Rute]

Again this is probably obvious to everyone else, but I convinced myself by "inconsistent" here we just mean that if we prove something about = we should try to make make our meta definitions behave as if they are functions which respect Lean's equality rule, which float currently does not.

[Jason Rute]

Other than that there is nothing logically inconsistent since meta definitions don't have to obey Lean theorems about functions and equality. Here is an example I coded up reproducing the problems with float but just using a meta type I coded in Lean:

meta def paradox : unit -> false
| u := paradox u

meta def cheat (p : Prop) : p := false.elim (paradox ())

meta inductive bad_int
| nan : bad_int
| pos : ℕ → bad_int  -- has +0
| neg : ℕ → bad_int  -- has -0

namespace bad_int

meta def bad_eq : bad_int → bad_int → bool
| (pos 0) (neg 0) := tt
| nan nan := ff
| (pos i) (pos j) := i = j
| (neg i) (neg j) := i = j
| _ _ := ff

meta def bad_sign : bad_int → bad_int
| (pos n) := pos 1
| (neg n) := neg 1
| nan := nan

meta def dec_eq_rel (i j : bad_int) : decidable (i = j) :=
if bad_eq i j then
  decidable.is_true (cheat (i = j))
else
 decidable.is_false (cheat (i ≠ j))

meta def dec_eq : decidable_eq bad_int := dec_eq_rel
attribute [instance] dec_eq

def test_eq {α} [decidable_eq α] (x : α) := to_bool (x = x)

theorem test_eq_tt {α} [decidable_eq α] (x : α) : test_eq x = tt :=
(to_bool_iff _).2 rfl

#eval test_eq nan -- ff


def test_congr {α} [decidable_eq α] (x y : α) (f : α → α) := to_bool (x = y → f x = f y)

theorem test_congr_tt {α} [decidable_eq α] (x y : α) (f) : test_congr x y f = tt :=
(to_bool_iff _).2 (λ x, by rw x)

#eval test_congr (pos 0) (neg 0) bad_sign -- ff

end bad_int

[Mario Carneiro]

Yes, you can argue in this way. However, keep in mind that bad meta definitions also compromise the correctness of lean's compiler, which matters even for meta code because this is what gives them meaning. That is, to the extent that meta code is like code you would find in C or Haskell, this kind of thing can cause miscompilation because lean makes some assumptions about pure code being pure

[Mario Carneiro]

We're doing a similar thing right now to cover up another inconsistency in level I found a long time ago:

open level
meta example : max zero zero ≠ zero := λ h, level.no_confusion h
#eval to_bool (max zero zero = zero) -- tt

[Kevin Buzzard]

If it's not a proof of false, it's not an inconsistency, surely

[Chris Hughes]

It's still a problem if it means your unsafe code is even less safe than you expected.

[Mario Carneiro]

I will note that a proof of false was in fact used in Jason's example

[Mario Carneiro]

meta code allows you to bypass restrictions, it's not "safe". But that doesn't mean we shouldn't make every effort to not be wrong

[Kevin Lacker]

i think the right thing to do for floating point equality is to check x.to_bits = y.to_bits and if you need the abomination that is ieee equality to call it ieee_eq or something

[Kevin Lacker]

in general you rarely want to be checking ieee equality for floating point numbers anyway, only if you're doing something like verifying that a serialization->deserialization worked where you'd want bitwise equality

[Patrick Massot]

This will be even more important in Lean 4 where we'll have more power to create custom commands. For instance it should be pretty easy to create a major_theorem command which acts like theorem excepts it replaces whatever statement you type with 0 = 0 before asking for a proof. Of course the Lean kernel will see a statement and proof of 0 = 0 but a human reading the Lean file will see any statement you want.

[Mario Carneiro]

Kevin Lacker said:

i think the right thing to do for floating point equality is to check x.to_bits = y.to_bits and if you need the abomination that is ieee equality to call it ieee_eq or something

I agree with this. Using = or == is a bad habit inherited from other programming languages that don't have such a strong stance on formal correctness. Rust uses PartialEq instead of Eq essentially only because floats exist, but I would much rather compromise on notational convenience of float ops because it's important to recognize the float weirdness happening in each operation.

[Mario Carneiro]

Patrick Massot said:

This will be even more important in Lean 4 where we'll have more power to create custom commands. For instance it should be pretty easy to create a major_theorem command which acts like theorem excepts it replaces whatever statement you type with 0 = 0 before asking for a proof. Of course the Lean kernel will see a statement and proof of 0 = 0 but a human reading the Lean file will see any statement you want.

I think it's possible to override theorem to do that, actually

[Johan Commelin]

wait, and you are telling us now...

[Patrick Massot]

It may be possible in Lean 3 already, but I wanted to point out it will probably be easy in Lean 4.

[Johan Commelin]

all these months we've been sweating to prove our theorems... and we were just one override and a rfl away from proving them

[Mario Carneiro]

Yes, this is a major concern of mine regarding the tremendous syntax flexibility of lean 4. You basically can't trust anything you see

[Kevin Lacker]

[Johan Commelin]

"trusted syntax is an editor feature" -- anonymous

[Leonardo de Moura]

I think it is important to clarify a few points and avoid misinformation being spread.

1- Most users assume "inconsistent" means "being able to prove false". This is not the case here.

2- The bug is in the native implementation (in C++) of float equality. The bug is in the Lean 3 community branch only.

3- The bug only affects people using the Lean 3 community branch as a programming language.
One may claim it also affects users writing tactics. As far as I know, nobody uses float for writing tactics.
However, even if someone wrote a tactic using them, it would be just another buggy tactic. Incorrect proofs produced by buggy tactics are caught by the kernel.

4- A less alarmist way to describe the bug is: "The native implementation of float equality is incorrect. It doesn't correctly implement the type it claims to implement. This bug affects people using the Lean 3 community branch, float, and Lean as a programming language".

5- No "proof of false" has ever been reported to a Lean developer. If a "proof of false" is one day found, we would tag it as a high priority and would fix it.

6- In Lean, users can inspect, and export objects constructed using the system. This allows users to scrutinize any result proved using Lean. In Lean 4, users have access to not only the Kernel terms but all built-in data structures representing parsers, elaborators, instances, classes, etc.

7- One doesn't need "tremendous syntax flexibility" to tricky naive users to believe they proved something they didn't. Example:

notation `false` := true

theorem unsound : false :=
  trivial

One can easily obfuscate the example above and make the exploit less obvious. However, the previous point remains, we provide tools for users to scrutinize and export their results.

8- Users can write their own independent type checkers and visualizers for Lean developments. A few independent type checkers have already been implemented. I know that 2 of them are efficient enough for checking real/big Lean developments.

To be honest, some of the comments on this thread read like FUD https://en.wikipedia.org/wiki/Fear,_uncertainty,_and_doubt

[Mario Carneiro]

I'm not laying any blame at lean 4 here. My original post was about lean 3 community edition. Some of the follow on comments apply to lean 4, but this particular issue has already been fixed

[Mario Carneiro]

Re: 7, I agree that it's easy to write things that don't mean what they say in lean 3 (and even easier in lean 4). This doesn't make me any less concerned. Ideally we would have something like the export format with trusted syntax, but where you can actually read it. This does not currently exist.

[Mario Carneiro]

Re: 1, I don't have a good term for this. Is "miscompilation" better? "Inconsistent with reality"? The code doesn't do what it says. Regarding "can't prove false", of course in meta code you very much can, but that's obviously not what people are talking about. native.float is a meta feature, it lacks whatever sense of correctness you can meaningfully apply to meta things.

[Mario Carneiro]

Mario Carneiro said:

Yes, this is a major concern of mine regarding the tremendous syntax flexibility of lean 4. You basically can't trust anything you see

I admit this is hyperbolic. Of course in practice this isn't likely to be a major issue. But from a formal perspective, I really don't know if I can tighten this claim up very much; you more or less have to read the entirety of the lean code and parser infrastructure before you can make any sure claims about the lack of tricky parser mechanisms in use. Maybe we need a "Lean Zero" for verified syntax? :)

[Patrick Massot]

Leo, I don't know how much of your message is directed towards my two messages in this thread, but I'd like to clarify that I'm not worried at all, and I'm super excited to get access to Lean 4 flexibility in the future. My message was a comment on Mario's "meta code allows you to bypass restrictions, it's not "safe". But that doesn't mean we shouldn't make every effort to not be wrong". As you point out yourself, there are ways to write deceiving Lean code, but this wasn't meant as a critique, only reinforcing the claim that we should make every effort to write good meta code.

[Mario Carneiro]

Jason Rute said:

When you say "inconsistent", do you mean you can prove false or just that it is weird behavior in the meta world? I tried to turn your example into a proof of tt = ff, but even though #eval test_eq native.float.qNaN comes out asff, I can't find a way to prove test_eq native.float.qNaN = ff. Does the fact that float is meta protect the consistency of Lean (3 community version)?

Leo already said this, but just to be clear: This is just weird behavior in meta world. The kernel doesn't see any declarations marked meta, so logical soundness of the lean kernel is not compromised.

[Leonardo de Moura]

@Mario Carneiro This is not the first message I see from you that has a very "alarmist tone".
The main point is the bug does not affect the soundness of results proved using Lean.
The key issue here for me is: Should we trust results proved using Lean?

Regarding "can't prove false", of course in meta code you very much can, but that's obviously not what people are talking about.

I disagree. It was not obvious to Jason Rute. He wrote

When you say "inconsistent", do you mean you can prove false or just that it is weird behavior in the meta world?

He is clearly concerned about the soundness of the system.

Re: 1, I don't have a good term for this. Is "miscompilation" better?

You could have simply said: "this bug does not affect the soundness of results proved using Lean"
You could have just answered "no, you cannot prove false" to Jason. He was clearly asking whether the bug affects the soundness of the system or not.

Ideally we would have something like the export format with trusted syntax, but where you can actually read it. This does not currently exist.

We don't need an export format in Lean 4 anymore. Users can traverse all data structures and export whatever they want using the format they want.
As far as I know, Gabriel's external type checker can pretty-print the results it checked.

Maybe we need a "Lean Zero" for verified syntax? :smile:

If you are concerned so much about this problem, you should do it.
I am not. There are many more important problems that need to be addressed.
I acknowledge that Lean has many problems, but soundness is not one of them. As I said, no "proof of false" has ever been reported to me.
I am clearly referring to "non-meta" here.