oleans and lean files

Stream: new members

[Huỳnh Trần Khanh]

does lean check whether the oleans actually match the lean files? or lean just trusts whatever is in the oleans?

[Kevin Buzzard]

I'm not an expert, but it must check, because otherwise you wouldn't get a load of orange bars when you have different mathlib leans and oleans.

[Jason Rute]

My understanding, which might be wrong is that lean uses the file (out of .lean and .olean) with the newest time stamp. Hence if you modify and save a file (even if you don’t make any changes), it will invalidate the .olean.

[Jason Rute]

Also, if an olean is invalidated, so will be all the olean s which depend on it.

[Kevin Buzzard]

Maybe this used to be true but isn't true any more? Nowadays I can edit a file in mathlib to test something, save it, and then delete all the changes and restart Lean and it's fine.

[Huỳnh Trần Khanh]

ok so let me phrase my question in a different way: if i were to download oleans from Hacker X, can Hacker X trick me into thinking that the dec_trivial tactic (or any other tactic) closes a certain goal when it actually doesn't?

[Huỳnh Trần Khanh]

I'm asking this question purely out of curiosity, I won't be hacking mathlib olean servers to screw people over

[Huỳnh Trần Khanh]

can the oleans contain entirely different proofs of the same statements?

[Jason Rute]

I believe no, a hacker couldn’t do that. When lean loads oleans, the oleans contain complete (term) proofs that are quickly rechecked every time. Again (as above), I could be mistaken.

[Jason Rute]

See here for the first question: https://github.com/leanprover-community/lean/issues/112. I think they now use file hashes instead of time stamps. (But again, even if the lean and olean disagree but a hacker makes them look like they agree so the olean is used, it will not lead to proof of false I think. Although, I’m sure it could be used to trick the user by subtly changing a definition say.)

[Eric Wieser]

We've had a situation in the past where a hash collision results in a happy lean but a sad leanchecker

[Eric Wieser]

So yes, I think a hacker can serve you up oleans that let you prove false, but when you export the proof for checking with leanchecker, leanchecker will say "no this is nonsense"

[Huỳnh Trần Khanh]

Wow. How did you have a collision in the first place? Aren't collisions like... impossible to happen?

[Eric Wieser]

32 bits is a small hash

[Alex J. Best]

https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.236572.20crashes.20leanchecker/near/229293401

[Eric Wieser]

I think the odds of this having happened over the lifetime of mathlib are somewhere between 1% and 10%

[Eric Wieser]

Based on https://preshing.com/images/small-probabilities.png

[Ruben Van de Velde]

I guess the odds are 100%, since we'd have several reports of it happening

[Jason Rute]

Even without hash collisions is there anything preventing a hacker from just constructing a dubious olean file with a hash matching the lean file?

[Jason Rute]

(I’m not saying we need to worry about such hacks, but just trying to understand the OPs question.)