From 2f502c04622724401eeb9e9f043fa6d4eb327575 Mon Sep 17 00:00:00 2001 From: Mathieu Fehr Date: Tue, 15 Sep 2026 13:25:45 +0100 Subject: [PATCH] chore(lean) : update lean to version 4.34.0 --- ExArray/lean/ExArray/Basic.lean | 7 ++- Veir/Data/Float/Basic.lean | 10 ++-- Veir/ForLean.lean | 72 +++++++++++------------ Veir/IR/Attribute.lean | 2 +- Veir/IR/GetSet.lean | 8 +-- Veir/PatternRewriter/Puddle/Validity.lean | 2 +- Veir/Rewriter/GetSet/BlockOperands.lean | 4 +- lean-ctrees/lean-toolchain | 2 +- lean-toolchain | 2 +- 9 files changed, 55 insertions(+), 54 deletions(-) diff --git a/ExArray/lean/ExArray/Basic.lean b/ExArray/lean/ExArray/Basic.lean index 7ad1dd3c9c..9326678859 100644 --- a/ExArray/lean/ExArray/Basic.lean +++ b/ExArray/lean/ExArray/Basic.lean @@ -443,7 +443,12 @@ theorem readRec_succ (w : Nat) (buf : ExArray) (n : UInt64) numBytes h : theorem readRec_uset_disjoint {w : Nat} (buf : ExArray) (n: UInt64) numBytes m (x: UInt8) (hDisjoint: m.toNat ∉ support n.toNat numBytes) h₁ h₂ : (buf.uset m x h₁).readRec n numBytes h₂ = buf.readRec (w := w) n numBytes (by grind) := by - induction numBytes generalizing n buf x <;> grind [readRec_succ] + induction numBytes generalizing n + case zero => + grind + case succ numBytes ih => + simp only [readRec_succ] + grind @[simp, grind =] theorem readRec_blitRec_self (w : Nat) (buf : ExArray) (n : UInt64) numBytes (x : BitVec w) h h' : diff --git a/Veir/Data/Float/Basic.lean b/Veir/Data/Float/Basic.lean index 47760ecf5b..bf0409cfff 100644 --- a/Veir/Data/Float/Basic.lean +++ b/Veir/Data/Float/Basic.lean @@ -45,7 +45,7 @@ that represents IEEE-style floating point formats. @[expose] def FloatFormat.toLeanFormat (format : FloatFormat) (hm : 0 < format.mantissa := by grind) - (he : 0 < format.exponent := by grind) : _root_.Float.Model.Format where + (he : 2 ≤ format.exponent := by grind) : _root_.Float.Model.Format where exponentBits := format.exponent mantissaBitsWithoutImplicit := format.mantissa hm := hm @@ -54,7 +54,7 @@ def FloatFormat.toLeanFormat (format : FloatFormat) @[simp] theorem FloatFormat.numBits_toLeanFormat_eq_bitwidth (format : FloatFormat) - (hm : 0 < format.mantissa) (he : 0 < format.exponent) : + (hm : 0 < format.mantissa) (he : 2 ≤ format.exponent) : (format.toLeanFormat hm he).numBits = format.bitwidth := by simp [toLeanFormat, _root_.Float.Model.Format.numBits, bitwidth] @@ -122,7 +122,7 @@ of `UnpackedFloat.pack`. -/ def ofUnpackedFloat (format : FloatFormat) (uf : UnpackedFloat) (hm : 0 < format.mantissa := by grind) - (he : 0 < format.exponent := by grind) : FloatValue format := + (he : 2 ≤ format.exponent := by grind) : FloatValue format := .ofBits <| match uf with | .notANumber => (UnpackedFloat.packedNaN format.toLeanFormat).cast (by simp) @@ -165,11 +165,11 @@ def ofUnpackedFloat (format : FloatFormat) (uf : UnpackedFloat) The value of `(-1)^negative * significand * 10^exponent` in `format`. Converts a base-10 float to the exact IEEE-754 bit pattern of `format`, -using round-to-nearest, ties-to-even. +using round-to-nearest, ties-to-even. -/ def ofScientific (format : FloatFormat) (negative : Bool) (significand : Nat) (exponent : Int) : FloatValue format := - if hty : format.mantissa = 0 ∨ format.exponent = 0 then + if hty : format.mantissa = 0 ∨ format.exponent < 2 then .ofBits 0#_ else let uf := UnpackedFloat.ofScientific format.toLeanFormat significand exponent diff --git a/Veir/ForLean.lean b/Veir/ForLean.lean index fa8b56be4a..6c9ad9b799 100644 --- a/Veir/ForLean.lean +++ b/Veir/ForLean.lean @@ -495,8 +495,8 @@ theorem sdiv_one_shl_of_smod_eq_zero {w₁ w₂ : Nat} (x : BitVec w₁) (k : Bi (hk : k.toNat + 1 < w₁) (h : x.smod ((1#w₁) <<< k) = 0#w₁) : x.sdiv ((1#w₁) <<< k) = x.sshiftRight' k := by have hy : ((1#w₁) <<< k).toInt = ((2 ^ k.toNat : Nat) : Int) := by - rw [BitVec.shiftLeft_eq', ← BitVec.twoPow_eq, BitVec.toInt_twoPow, if_neg (by omega), - if_neg (by omega)] + rw [BitVec.shiftLeft_eq', ← BitVec.twoPow_eq, BitVec.toInt_twoPow, ite_eq_right (by omega), + ite_eq_right (by omega)] exact (Int.natCast_pow 2 k.toNat).symm apply BitVec.eq_of_toInt_eq have hsmod : x.toInt.fmod ((1#w₁) <<< k).toInt = 0 := by @@ -529,7 +529,7 @@ theorem toInt_neg_one_shl {w₁ w₂ : Nat} (k : BitVec w₂) (hk : k.toNat < w rw [BitVec.toNat_neg, hy, Nat.mod_eq_of_lt (Nat.sub_lt (Nat.two_pow_pos w₁) (Nat.two_pow_pos k.toNat)), hsubval] have hcond : ¬ (2 * (-((1#w₁) <<< k)).toNat < 2 ^ w₁) := by rw [hneg]; omega - rw [BitVec.toInt_eq_toNat_cond, if_neg hcond, hneg] + rw [BitVec.toInt_eq_toNat_cond, ite_eq_right hcond, hneg] omega /-- Negative-divisor analogue of `sdiv_one_shl_of_smod_eq_zero`: an exact `sdiv` by `-2^k` agrees @@ -560,9 +560,9 @@ theorem Int.tdiv_eq_ediv_add_of_pos {a p : Int} (hp : 0 < p) : have hpne : p ≠ 0 := by omega rw [Int.tdiv_eq_ediv, Int.sign_eq_one_of_pos hp] by_cases ha : a < 0 - · rw [if_pos ha] + · rw [ite_eq_left ha] by_cases hdvd : p ∣ a - · rw [if_pos (Or.inr hdvd)] + · rw [ite_eq_left (Or.inr hdvd)] obtain ⟨q, hq⟩ := hdvd subst hq have hrw : p * q + (p - 1) = (p - 1) + q * p := by @@ -573,7 +573,7 @@ theorem Int.tdiv_eq_ediv_add_of_pos {a p : Int} (hp : 0 < p) : rw [Int.ediv_eq_zero_of_lt h1 h2, Int.mul_ediv_cancel_left q hpne] omega · have hnotor : ¬ (0 ≤ a ∨ p ∣ a) := fun h => h.elim (fun h0 => absurd h0 (by omega)) hdvd - rw [if_neg hnotor] + rw [ite_eq_right hnotor] have hr : a % p + a / p * p = a := Int.emod_add_ediv_mul a p have hr0 : 0 ≤ a % p := Int.emod_nonneg a hpne have hrlt : a % p < p := Int.emod_lt_of_pos a hp @@ -589,7 +589,7 @@ theorem Int.tdiv_eq_ediv_add_of_pos {a p : Int} (hp : 0 < p) : rw [Int.ediv_eq_zero_of_lt h1 h2] simp · have haux : 0 ≤ a ∨ p ∣ a := Or.inl (by omega) - rw [if_neg ha, if_pos haux, Int.add_zero, Int.add_zero] + rw [ite_eq_right ha, ite_eq_left haux, Int.add_zero, Int.add_zero] /-- A shifted-in-from-the-left all-ones mask (`(2^w - 1) >>> (w - k)`, i.e. the top `w - k` bits of `allOnes w` cleared) is exactly the `k`-bit all-ones mask `2^k - 1`. Used to compute the @@ -621,14 +621,14 @@ theorem toNat_sign_mask_shift {w₁ : Nat} (x : BitVec w₁) (k : Nat) (hk : k < omega rw [BitVec.toNat_ushiftRight] by_cases hmsb : x.msb = true - · rw [if_pos hmsb, BitVec.toNat_sshiftRight_of_msb_true hmsb] + · rw [ite_eq_left hmsb, BitVec.toNat_sshiftRight_of_msb_true hmsb] have hxge : 2 ^ (w₁ - 1) ≤ x.toNat := BitVec.le_toNat_of_msb_true hmsb have hxlt : x.toNat < 2 ^ w₁ := x.isLt have hzero : (2 ^ w₁ - 1 - x.toNat) >>> (w₁ - 1) = 0 := by rw [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt (by omega)] rw [hzero, Nat.sub_zero] exact Nat.shiftRight_two_pow_sub_one hk - · rw [if_neg hmsb] + · rw [ite_eq_right hmsb] have hmsb' : x.msb = false := by simpa using hmsb rw [BitVec.toNat_sshiftRight_of_msb_false hmsb'] have hxlt : x.toNat < 2 ^ (w₁ - 1) := BitVec.toNat_lt_of_msb_false hmsb' @@ -648,8 +648,8 @@ theorem sdiv_one_shl_eq_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec w₁) ( x.sdiv ((1#w₁) <<< k) = (x + (x.sshiftRight (w₁ - 1) >>> (w₁ - k.toNat))).sshiftRight' k := by have hy : ((1#w₁) <<< k).toInt = ((2 ^ k.toNat : Nat) : Int) := by - rw [BitVec.shiftLeft_eq', ← BitVec.twoPow_eq, BitVec.toInt_twoPow, if_neg (by omega), - if_neg (by omega)] + rw [BitVec.shiftLeft_eq', ← BitVec.twoPow_eq, BitVec.toInt_twoPow, ite_eq_right (by omega), + ite_eq_right (by omega)] exact (Int.natCast_pow 2 k.toNat).symm generalize hcorr_def : x.sshiftRight (w₁ - 1) >>> (w₁ - k.toNat) = corr have hcorrNat : corr.toNat = if x.msb then 2 ^ k.toNat - 1 else 0 := by @@ -660,8 +660,8 @@ theorem sdiv_one_shl_eq_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec w₁) ( rw [BitVec.msb_eq_toInt] at hcorrNat simp only [decide_eq_true_eq] at hcorrNat by_cases hx : x.toInt < 0 - · rw [if_pos hx] at hcorrNat - rw [if_pos hx] + · rw [ite_eq_left hx] at hcorrNat + rw [ite_eq_left hx] have hlt : 2 * corr.toNat < 2 ^ w₁ := by rw [hcorrNat] have : 2 ^ (w₁ - 1) * 2 = 2 ^ w₁ := by @@ -669,8 +669,8 @@ theorem sdiv_one_shl_eq_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec w₁) ( omega rw [BitVec.toInt_eq_toNat_of_lt hlt, hcorrNat] exact Int.natCast_sub Nat.one_le_two_pow - · rw [if_neg hx] at hcorrNat - rw [if_neg hx] + · rw [ite_eq_right hx] at hcorrNat + rw [ite_eq_right hx] have hlt : 2 * corr.toNat < 2 ^ w₁ := by rw [hcorrNat] have := Nat.two_pow_pos w₁ @@ -691,12 +691,12 @@ theorem sdiv_one_shl_eq_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec w₁) ( have hdouble : (2:Int) ^ (w₁ - 1) * 2 = ((2 ^ w₁ : Nat) : Int) := by exact_mod_cast hdoubleNat rw [hcorrInt] by_cases hx : x.toInt < 0 - · rw [if_pos hx] + · rw [ite_eq_left hx] have hb1 : (0:Int) ≤ ((2 ^ k.toNat : Nat) : Int) - 1 := by have : (1:Int) ≤ ((2 ^ k.toNat : Nat) : Int) := by exact_mod_cast Nat.one_le_two_pow omega apply Int.bmod_eq_of_le <;> omega - · rw [if_neg hx] + · rw [ite_eq_right hx] simp only [Int.add_zero] apply Int.bmod_eq_of_le <;> omega have hppos : (0:Int) < ((2 ^ k.toNat : Nat) : Int) := by @@ -724,8 +724,8 @@ theorem sdiv_neg_one_shl_eq_neg_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec rw [BitVec.msb_eq_toInt] at hcorrNat simp only [decide_eq_true_eq] at hcorrNat by_cases hx : x.toInt < 0 - · rw [if_pos hx] at hcorrNat - rw [if_pos hx] + · rw [ite_eq_left hx] at hcorrNat + rw [ite_eq_left hx] have hlt : 2 * corr.toNat < 2 ^ w₁ := by rw [hcorrNat] have : 2 ^ (w₁ - 1) * 2 = 2 ^ w₁ := by @@ -733,8 +733,8 @@ theorem sdiv_neg_one_shl_eq_neg_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec omega rw [BitVec.toInt_eq_toNat_of_lt hlt, hcorrNat] exact Int.natCast_sub Nat.one_le_two_pow - · rw [if_neg hx] at hcorrNat - rw [if_neg hx] + · rw [ite_eq_right hx] at hcorrNat + rw [ite_eq_right hx] have hlt : 2 * corr.toNat < 2 ^ w₁ := by rw [hcorrNat] have := Nat.two_pow_pos w₁ @@ -756,12 +756,12 @@ theorem sdiv_neg_one_shl_eq_neg_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec have hdouble : (2:Int) ^ (w₁ - 1) * 2 = ((2 ^ w₁ : Nat) : Int) := by exact_mod_cast hdoubleNat rw [hcorrInt] by_cases hx : x.toInt < 0 - · rw [if_pos hx] + · rw [ite_eq_left hx] have hb1 : (0:Int) ≤ ((2 ^ k.toNat : Nat) : Int) - 1 := by have : (1:Int) ≤ ((2 ^ k.toNat : Nat) : Int) := by exact_mod_cast Nat.one_le_two_pow omega apply Int.bmod_eq_of_le <;> omega - · rw [if_neg hx] + · rw [ite_eq_right hx] simp only [Int.add_zero] apply Int.bmod_eq_of_le <;> omega have hppos : (0:Int) < ((2 ^ k.toNat : Nat) : Int) := by @@ -827,7 +827,7 @@ theorem sdiv_one_shl_eq_sshiftRight_of_msb_false (x : BitVec 64) (k : BitVec 6) by_cases hk : k.toNat + 1 < 64 · have hcorr0 : x.sshiftRight 63 >>> (64 - k.toNat) = 0#64 := by apply BitVec.eq_of_toNat_eq - rw [toNat_sign_mask_shift x k.toNat (by omega), if_neg (by simp [hx])] + rw [toNat_sign_mask_shift x k.toNat (by omega), ite_eq_right (by simp [hx])] rfl rw [sdiv_one_shl_eq_biased_sshiftRight x k hk] show (x + (x.sshiftRight (63 : Nat) >>> (64 - k.toNat))).sshiftRight k.toNat = @@ -841,7 +841,7 @@ theorem sdiv_one_shl_eq_sshiftRight_of_msb_false (x : BitVec 64) (k : BitVec 6) rw [hy, BitVec.sdiv_intMin] have hxne : x ≠ BitVec.intMin 64 := by intro h; rw [h] at hx; simp [BitVec.msb_intMin] at hx - rw [if_neg hxne] + rw [ite_eq_right hxne] apply BitVec.eq_of_toNat_eq show (0 : BitVec 64).toNat = (x.sshiftRight (-1 : BitVec 6).toNat).toNat rw [BitVec.toNat_sshiftRight_of_msb_false hx] @@ -873,13 +873,13 @@ theorem sdiv_one_shl_eq_ite_sshiftRight (x : BitVec 64) (k : BitVec 6) : else x.sshiftRight' k := by by_cases hx : x.msb - · rw [if_pos hx] + · rw [ite_eq_left hx] by_cases hk0 : k = 0 - · rw [if_pos hk0, hk0] + · rw [ite_eq_left hk0, hk0] simp [BitVec.sshiftRight_eq', BitVec.sdiv_one] - · rw [if_neg hk0] + · rw [ite_eq_right hk0] by_cases hk63 : k ≠ (-1 : BitVec 6) - · rw [if_pos hk63] + · rw [ite_eq_left hk63] have hk0' : 0 < k.toNat := by bv_omega have hk' : k.toNat + 1 < 64 := by bv_omega have h1 : (1 : BitVec 6).toNat = 1 := BitVec.toNat_one (by decide) @@ -891,11 +891,11 @@ theorem sdiv_one_shl_eq_ite_sshiftRight (x : BitVec 64) (k : BitVec 6) : (x + (x.sshiftRight (-1 : BitVec 6).toNat >>> (-k : BitVec 6).toNat)).sshiftRight k.toNat rw [heq1, heq2] exact sdiv_one_shl_eq_biased_sshiftRight x k hk' - · rw [if_neg hk63] + · rw [ite_eq_right hk63] have hk63' : k = (-1 : BitVec 6) := Decidable.not_not.mp hk63 have hy : (1#64) <<< k = BitVec.intMin 64 := by rw [hk63']; decide rw [hy, BitVec.sdiv_intMin] - · rw [if_neg hx] + · rw [ite_eq_right hx] exact sdiv_one_shl_eq_sshiftRight_of_msb_false x k (by simpa using hx) /-- Negative-divisor analogue of `sdiv_one_shl_eq_sshiftRight_of_msb_false`: when `x` is @@ -908,7 +908,7 @@ theorem sdiv_neg_one_shl_eq_neg_sshiftRight_of_msb_false (x : BitVec 64) (k : Bi have hk : k.toNat < 64 := k.isLt have hcorr0 : x.sshiftRight 63 >>> (64 - k.toNat) = 0#64 := by apply BitVec.eq_of_toNat_eq - rw [toNat_sign_mask_shift x k.toNat (by omega), if_neg (by simp [hx])] + rw [toNat_sign_mask_shift x k.toNat (by omega), ite_eq_right (by simp [hx])] rfl rw [sdiv_neg_one_shl_eq_neg_biased_sshiftRight x k hk, hcorr0, BitVec.add_zero] @@ -930,13 +930,13 @@ theorem sdiv_neg_one_shl_eq_ite_sshiftRight (x : BitVec 64) (k : BitVec 6) : else -(x.sshiftRight' k) := by by_cases hx : x.msb - · rw [if_pos hx] + · rw [ite_eq_left hx] by_cases hk0 : k = 0 - · rw [if_pos hk0, hk0] + · rw [ite_eq_left hk0, hk0] have hy : (-((1#64) <<< (0 : BitVec 6))) = (-1 : BitVec 64) := by simp rw [hy, BitVec.sdiv_neg (by decide)] simp [BitVec.sdiv_one, BitVec.sshiftRight_eq'] - · rw [if_neg hk0] + · rw [ite_eq_right hk0] have hk0' : 0 < k.toNat := by bv_omega have hk' : k.toNat < 64 := k.isLt have h1 : (1 : BitVec 6).toNat = 1 := BitVec.toNat_one (by decide) @@ -948,7 +948,7 @@ theorem sdiv_neg_one_shl_eq_ite_sshiftRight (x : BitVec 64) (k : BitVec 6) : -((x + (x.sshiftRight (-1 : BitVec 6).toNat >>> (-k : BitVec 6).toNat)).sshiftRight k.toNat) rw [heq1, heq2] exact sdiv_neg_one_shl_eq_neg_biased_sshiftRight x k hk' - · rw [if_neg hx] + · rw [ite_eq_right hx] exact sdiv_neg_one_shl_eq_neg_sshiftRight_of_msb_false x k (by simpa using hx) @[veir_bv_normalize] diff --git a/Veir/IR/Attribute.lean b/Veir/IR/Attribute.lean index 641bf54d38..6574729d8d 100644 --- a/Veir/IR/Attribute.lean +++ b/Veir/IR/Attribute.lean @@ -73,7 +73,7 @@ that represents IEEE-style floating point formats. -/ abbrev toFormat (type : FloatType) (hm : 0 < type.mantissa := by grind) - (he : 0 < type.exponent := by grind) : Float.Model.Format := + (he : 2 ≤ type.exponent := by grind) : Float.Model.Format := type.format.toLeanFormat hm he def f16 : FloatType := { format := .f16 } diff --git a/Veir/IR/GetSet.lean b/Veir/IR/GetSet.lean index ec8c3e9a2f..ce65f7b04a 100644 --- a/Veir/IR/GetSet.lean +++ b/Veir/IR/GetSet.lean @@ -5462,13 +5462,7 @@ theorem BlockPtr.get!_OpOperandPtrPtr_set {block : BlockPtr} : else block.get! ctx | _ => block.get! ctx := by - cases ptr' - · grind - · split - · grind - · simp only [OpOperandPtrPtr.set_valueFirstUse, get!_ValuePtr_setFirstUse, - Array.set!_eq_setIfInBounds] - split <;> grind + rcases ptr' with operand | ⟨result | arg⟩ <;> grind @[simp, grind =] theorem BlockPtr.firstUse!_OpOperandPtrPtr_set {block : BlockPtr} : diff --git a/Veir/PatternRewriter/Puddle/Validity.lean b/Veir/PatternRewriter/Puddle/Validity.lean index 6e2dfa2876..c2d7e768b6 100644 --- a/Veir/PatternRewriter/Puddle/Validity.lean +++ b/Veir/PatternRewriter/Puddle/Validity.lean @@ -362,7 +362,7 @@ macro "provePuddleValid" : tactic => constructor · provePuddleSupported · cbv - · cbv + · native_decide )) end Veir.Puddle diff --git a/Veir/Rewriter/GetSet/BlockOperands.lean b/Veir/Rewriter/GetSet/BlockOperands.lean index 02b7ae5e78..13dbf83fde 100644 --- a/Veir/Rewriter/GetSet/BlockOperands.lean +++ b/Veir/Rewriter/GetSet/BlockOperands.lean @@ -436,7 +436,9 @@ theorem OperationPtr.getSuccessors!_initBlockOperands {operation : OperationPtr} else operation.getSuccessors! ctx := by simp only [OperationPtr.getSuccessors!_def] - grind + /- We need to remove some grind patterns from the default grind set, as they make the search + space explode. See https://github.com/leanprover/lean4/issues/15183 -/ + grind [-Array.range'_append, -Array.range'_append_1] @[simp, grind =, simp_getset] theorem BlockPtr.getNumArguments!_initBlockOperands {block : BlockPtr} : diff --git a/lean-ctrees/lean-toolchain b/lean-ctrees/lean-toolchain index 025e59548e..3d1dc1d0f5 100644 --- a/lean-ctrees/lean-toolchain +++ b/lean-ctrees/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 +leanprover/lean4:v4.35.0-rc1 diff --git a/lean-toolchain b/lean-toolchain index 025e59548e..3d1dc1d0f5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 +leanprover/lean4:v4.35.0-rc1