Yet another UInt64 miscompilation

Stream: lean4

[Geoffrey Irving]

This seems bad (on leanprover/lean4:v4.25.0-rc2):

import Batteries.Data.UInt

def danger : UInt64 := UInt64.ofNat UInt64.size - 1
theorem danger_eq_large : danger = 18446744073709551615 := by decide +kernel
theorem danger_eq_one : danger = 1 := by native_decide
theorem bad : False := by simpa using danger_eq_large.symm.trans danger_eq_one

[Henrik Böving]

Fixed #11042

[Yury G. Kudryashov]

Do you mean lean#11042?

[Yaël Dillies]

Numbers were clearly never meant to be decided :grinning_face_with_smiling_eyes:

[Geoffrey Irving]

@Henrik Böving Thank you for the fix!

Do you know when it’s likely to land in a release?

[Henrik Böving]

Will be in an rc 15 ish days from now

[Yury G. Kudryashov]

In the meantime, you can use the nightly build, if you need it.

[Gavin Zhao]

I'm curious, how did you even find this bug...?

[Gavin Zhao]

It occurred to me in a dream tha 18446744073709551615 might be equal to 1 due to some constant folding optimizations.

[Geoffrey Irving]

For both this one and the previous UInt64 miscompilation, it was caught by my unit tests in https://github.com/girving/interval.

[Henrik Böving]

Gavin Zhao said:

I'm curious, how did you even find this bug...?

Finding this bug is pretty easy, the above test is far from an MWE, if you had written def f (x : UInt64) := 0 - x you would've already found it.

[Henrik Böving]

Maybe we should start fuzzing the code generator at some point...

[Geoffrey Irving]

Code generator fuzzing would be very good!

[Geoffrey Irving]

Henrik Böving said:

Gavin Zhao said:

I'm curious, how did you even find this bug...?

Finding this bug is pretty easy, the above test is far from an MWE, if you had written def f (x : UInt64) := 0 - x you would've already found it.

This seems to be conflating “finding” and “confirming” the bug. :)

[Geoffrey Irving]

I can confirm that leanprover/lean4:v4.26.0-rc1 fixes this problem! :tada: