max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: overeager uint constant folding (#11042)

Browse source 
This PR fixes a case of overeager constant folding on UInts where the
compiler would mistakenly
assume `0 - x = x`.
This commit is contained in:
Henrik Böving 2025-11-01 03:42:43 +01:00 • committed by GitHub
parent 282b583f1d
commit 51ef1dcc5e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 19 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Compiler/LCNF/Simp/ConstantFold.lean
View file

@ -356,10 +356,10 @@ def arithmeticFolders : List (Name × Folder) := [
(``UInt32.add, Folder.first #[Folder.mkBinary UInt32.add, Folder.leftRightNeutral (0 : UInt32)]),
(``UInt64.add, Folder.first #[Folder.mkBinary UInt64.add, Folder.leftRightNeutral (0 : UInt64)]),
(``Nat.sub, Folder.first #[Folder.mkBinary Nat.sub, Folder.leftRightNeutral 0]),
(``UInt8.sub, Folder.first #[Folder.mkBinary UInt8.sub, Folder.leftRightNeutral (0 : UInt8)]),
(``UInt16.sub, Folder.first #[Folder.mkBinary UInt16.sub, Folder.leftRightNeutral (0 : UInt16)]),
(``UInt32.sub, Folder.first #[Folder.mkBinary UInt32.sub, Folder.leftRightNeutral (0 : UInt32)]),
(``UInt64.sub, Folder.first #[Folder.mkBinary UInt64.sub, Folder.leftRightNeutral (0 : UInt64)]),
(``UInt8.sub, Folder.first #[Folder.mkBinary UInt8.sub, Folder.rightNeutral (0 : UInt8)]),
(``UInt16.sub, Folder.first #[Folder.mkBinary UInt16.sub, Folder.rightNeutral (0 : UInt16)]),
(``UInt32.sub, Folder.first #[Folder.mkBinary UInt32.sub, Folder.rightNeutral (0 : UInt32)]),
(``UInt64.sub, Folder.first #[Folder.mkBinary UInt64.sub, Folder.rightNeutral (0 : UInt64)]),
-- We don't convert Nat multiplication by a power of 2 into a left shift, because the fast path
-- for multiplication isn't any slower than a fast path for left shift that checks for overflow.
(``UInt8.mul, Folder.first #[Folder.mkBinary UInt8.mul, Folder.leftRightNeutral (1 : UInt8), Folder.leftRightAnnihilator (0 : UInt8) 0, Folder.mulShift ``UInt8.shiftLeft (UInt8.shiftLeft 1 ·) UInt8.log2]),

15
tests/lean/run/uint_bug_neutral.lean Normal file
View file

@ -0,0 +1,15 @@
/-!
This test guards against a uint constant folding bug
-/
def danger : UInt64 := UInt64.ofNat UInt64.size - 1
theorem danger_eq_large : danger = 18446744073709551615 := by decide +kernel
/--
error: Tactic `native_decide` evaluated that the proposition
danger = 1
is false
-/
#guard_msgs in
theorem danger_eq_one : danger = 1 := by native_decide
theorem bad : False := by simpa using danger_eq_large.symm.trans danger_eq_one