chore: bump lean version

RISCV/ForLean.lean

@@ -11,25 +11,14 @@ theorem BitVec.sshiftRight_eq_setWidth_extractLsb_signExtend {w : Nat} (n : Nat)
   by_cases hni : (n + i) < w
   <;> (simp [hni]; omega)
 
-theorem BitVec.extractLsb'_eq_setWidth {x : BitVec w} : x.extractLsb' 0 n = x.setWidth n := by
-  ext i hi
-  simp
-
 theorem BitVec.extractLsb'_ofInt_eq_ofInt {x : Int} {w w' : Nat} (h : w ≤ w') :
     (BitVec.extractLsb' 0 w (BitVec.ofInt w' x)) = (BitVec.ofInt w x) := by
-  simp only [extractLsb'_eq_setWidth, ← BitVec.signExtend_eq_setWidth_of_le _ (by omega)]
+  rw [← BitVec.setWidth_eq_extractLsb' (by omega), ← BitVec.signExtend_eq_setWidth_of_le _ (by omega)]
   apply BitVec.eq_of_toInt_eq
   simp only [BitVec.toInt_signExtend, BitVec.toInt_ofInt, h, Nat.min_eq_left]
   rw [Int.bmod_bmod_of_dvd]
   apply Nat.pow_dvd_pow 2 h
 
-theorem BitVec.extractLsb_setWidth_of_lt (x : BitVec w) (hi lo v : Nat) (hilo : lo < hi) (hhi : hi < v):
-    BitVec.extractLsb hi lo (BitVec.setWidth v x) = BitVec.extractLsb hi lo x := by
-  simp only [BitVec.extractLsb]
-  ext k
-  simp only [BitVec.getElem_extractLsb', BitVec.getLsbD_setWidth, Bool.and_eq_right_iff_imp,
-    decide_eq_true_eq]
-  omega
 
 theorem Int.lt_tmod_of_neg (a : Int) {b : Int} (H : b < 0) : b < Int.tmod a b :=
   match a, b, Int.eq_negSucc_of_lt_zero H with
@@ -120,25 +109,6 @@ theorem reverse_reverse (x : BitVec w) :
   ext i hi
   simp [← BitVec.getLsbD_eq_getElem]
 
-theorem exctractLsb'_extractLsb'_eq_extractLsb'_of_le {m n w : Nat} {x : BitVec w} (h : m ≤ n) :
-    BitVec.extractLsb' 0 m (BitVec.extractLsb' 0 n x) = BitVec.extractLsb' 0 m x := by
-  ext i hi
-  simp [getElem_extractLsb', Nat.zero_add, show i < n by omega]
-
-@[simp]
-theorem extractLsb'_cons (x : BitVec w) :
-    (x.cons y).extractLsb' 0 w = x := by
-  simp [BitVec.toNat_eq, Nat.or_mod_two_pow, Nat.shiftLeft_eq]
-
-theorem extractLsb'_concat (x : BitVec (w+1)) (y : Bool):
-    BitVec.extractLsb' 0 (t+1) (x.concat y) = (BitVec.extractLsb' 0 t x).concat y := by
-  ext i hi
-  simp only [← getLsbD_eq_getElem, getLsbD_extractLsb', hi, decide_true, Nat.zero_add,
-    getLsbD_concat, Bool.true_and]
-  split
-  · simp
-  · simp [show i - 1 < t by omega]
-
 theorem toNat_ofNat_of_le {w n : Nat} (h : n ≤ w) :
     (BitVec.ofNat w n).toNat = n := by
   have := Nat.lt_pow_self (a := 2) (n := w)
@@ -161,3 +131,11 @@ theorem signExtend_signExtend_of_le {x : BitVec w} (h : w ≤ v) :
   · have : w = 0 := by omega
     subst this
     simp [msb_signExtend, of_length_zero]
+
+theorem BitVec.extractLsb_setWidth_of_lt' {x : BitVec w} {hi lo v : Nat} (h : lo < v) (h' : hi < v):
+    BitVec.extractLsb hi lo (BitVec.setWidth v x) = BitVec.extractLsb hi lo x := by
+  simp only [BitVec.extractLsb]
+  ext k
+  simp only [BitVec.getElem_extractLsb', BitVec.getLsbD_setWidth, Bool.and_eq_right_iff_imp,
+    decide_eq_true_eq]
+  omega

RISCV/SailPure.lean

@@ -1,5 +1,4 @@
-import LeanRV64D.Sail.Sail
-import LeanRV64D.Sail.BitVec
+import LeanRV64D.Defs
 import LeanRV64D
 
 open LeanRV64D.Functions
@@ -23,8 +22,8 @@ def itype (imm : BitVec 12) (rs1_val : BitVec 64) (op : iop) : BitVec 64 :=
   let immext : xlenbits := (sign_extend (m := 64) imm)
   match op with
   | iop.ADDI => rs1_val + immext
-  | iop.SLTI => zero_extend (m := 64) (bool_to_bits (zopz0zI_s rs1_val immext))
-  | iop.SLTIU => zero_extend (m := 64) (bool_to_bits (zopz0zI_u rs1_val immext))
+  | iop.SLTI => zero_extend (m := 64) (bool_to_bit (zopz0zI_s rs1_val immext))
+  | iop.SLTIU => zero_extend (m := 64) (bool_to_bit (zopz0zI_u rs1_val immext))
   | iop.ANDI =>  rs1_val &&& immext
   | iop.ORI => rs1_val ||| immext
   | iop.XORI => rs1_val ^^^ immext
@@ -46,8 +45,8 @@ def rtype (op : rop) (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :=
   | rop.SLL =>
     (Sail.shift_bits_left rs1_val
         (Sail.BitVec.extractLsb rs2_val (LeanRV64D.Functions.log2_xlen -i 1) 0))
-  | rop.SLT => (zero_extend (m := 64) (bool_to_bits (zopz0zI_s rs1_val rs2_val)))
-  | rop.SLTU => (zero_extend (m := 64) (bool_to_bits (zopz0zI_u rs1_val rs2_val)))
+  | rop.SLT => (zero_extend (m := 64) (bool_to_bit (zopz0zI_s rs1_val rs2_val)))
+  | rop.SLTU => (zero_extend (m := 64) (bool_to_bit (zopz0zI_u rs1_val rs2_val)))
   | rop.XOR => rs1_val ^^^ rs2_val
   | rop.SRL =>
     (Sail.shift_bits_right rs1_val
@@ -202,7 +201,7 @@ def zbs_rtype (rs2_val : BitVec 64) (rs1_val : BitVec 64) (op : brop_zbs) : BitV
   let result : xlenbits :=
     match op with
     | .BCLR => (rs1_val &&& (Complement.complement mask))
-    | .BEXT => (zero_extend (m := 64) (bool_to_bits (bne (rs1_val &&& mask) (zeros (n := 64)))))
+    | .BEXT => (zero_extend (m := 64) (bool_to_bit (bne (rs1_val &&& mask) (zeros (n := 64)))))
     | .BINV => (rs1_val ^^^ mask)
     | .BSET => (rs1_val ||| mask)
   result
@@ -212,7 +211,7 @@ def zbs_iop (shamt : BitVec 6) (rs1_val : BitVec 64) (op : biop_zbs) : BitVec 64
   let result : xlenbits :=
     match op with
     | .BCLRI => (rs1_val &&& (Complement.complement mask))
-    | .BEXTI => (zero_extend (m := 64) (bool_to_bits (bne (rs1_val &&& mask) (zeros (n := 64)))))
+    | .BEXTI => (zero_extend (m := 64) (bool_to_bit (bne (rs1_val &&& mask) (zeros (n := 64)))))
     | .BINVI => (rs1_val ^^^ mask)
     | .BSETI => (rs1_val ||| mask)
   result

RISCV/SailPureToInstructions.lean

@@ -1,7 +1,7 @@
 import RISCV.SailPure
 import RISCV.Instructions
 import RISCV.ForLean
-import LeanRV64D.Arithmetic
+import LeanRV64D.Defs
 
 /-!
   Proofs of the equivalence between monad-free Sail specifications and bitvec-only semantics for
@@ -27,15 +27,20 @@ theorem itype_addi_eq (imm : BitVec 12) (rs1_val : BitVec 64) :
 
 theorem itype_slti_eq (imm : BitVec 12) (rs1_val : BitVec 64) :
     SailRV64.itype imm rs1_val iop.SLTI = slti imm rs1_val := by
-  simp [SailRV64.itype, LeanRV64D.Functions.sign_extend, Sail.BitVec.signExtend, zero_extend, LeanRV64D.Functions.bool_to_bits, Sail.BitVec.zeroExtend, LeanRV64D.Functions.bool_bits_forwards, LeanRV64D.Functions.zopz0zI_s, slti]
+  simp only [SailRV64.itype, zero_extend, Sail.BitVec.zeroExtend, LeanRV64D.Functions.bool_to_bit,
+    LeanRV64D.Functions.bool_bit_forwards, LeanRV64D.Functions.zopz0zI_s,
+    LeanRV64D.Functions.sign_extend, Sail.BitVec.signExtend, BitVec.truncate_eq_setWidth, slti]
   split <;>
   case _ arg h =>
   apply BitVec.eq_of_toInt_eq
   simp [BitVec.slt, h]
 
 theorem itype_sltiu_eq (imm : BitVec 12) (rs1_val : BitVec 64) :
     SailRV64.itype imm rs1_val iop.SLTIU = sltiu imm rs1_val := by
-  simp [SailRV64.itype, LeanRV64D.Functions.sign_extend, Sail.BitVec.signExtend, zero_extend, LeanRV64D.Functions.bool_to_bits, Sail.BitVec.zeroExtend, LeanRV64D.Functions.bool_bits_forwards, LeanRV64D.Functions.zopz0zI_u, sltiu, Sail.BitVec.toNatInt]
+  simp only [SailRV64.itype, zero_extend, Sail.BitVec.zeroExtend, LeanRV64D.Functions.bool_to_bit,
+    LeanRV64D.Functions.bool_bit_forwards, LeanRV64D.Functions.zopz0zI_u, Sail.BitVec.toNatInt,
+    Int.ofNat_eq_natCast, LeanRV64D.Functions.sign_extend, Sail.BitVec.signExtend, Int.ofNat_lt,
+    BitVec.truncate_eq_setWidth, sltiu]
   split <;>
   case _ arg h =>
   apply BitVec.eq_of_toInt_eq
@@ -58,8 +63,8 @@ theorem addiw_eq (imm : BitVec 12) (rs1_val : BitVec 64) :
   simp only [SailRV64.addiw, LeanRV64D.Functions.sign_extend, Sail.BitVec.signExtend, Nat.sub_zero,
     Nat.reduceAdd, Sail.BitVec.extractLsb, addiw]
   rw [BitVec.extractLsb, BitVec.setWidth_eq_extractLsb' (by omega)]
-  unfold instHPowInt_leanRV64D
-  bv_decide
+  simp only [Nat.sub_zero, Nat.reduceAdd, BitVec.add_comm]
+  congr
 
 theorem shiftiop_slli_eq (shamt : BitVec 6) (rs1_val : BitVec 64) :
     SailRV64.shiftiop shamt sop.SLLI rs1_val = slli shamt rs1_val := by
@@ -93,8 +98,8 @@ theorem rtype_slt_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
 theorem rtype_sltu_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
     SailRV64.rtype rop.SLTU rs2_val rs1_val = sltu rs2_val rs1_val := by
   simp [SailRV64.rtype, sltu]
-  simp [zero_extend, Sail.BitVec.zeroExtend, LeanRV64D.Functions.bool_to_bits,
-    Sail.BitVec.toNatInt, LeanRV64D.Functions.bool_bits_forwards, LeanRV64D.Functions.zopz0zI_u]
+  simp [zero_extend, Sail.BitVec.zeroExtend, LeanRV64D.Functions.bool_to_bit,
+    Sail.BitVec.toNatInt, LeanRV64D.Functions.bool_bit_forwards, LeanRV64D.Functions.zopz0zI_u]
   by_cases h : rs1_val.toNat < rs2_val.toNat <;>
   simp [h, BitVec.ult]
 
@@ -177,8 +182,7 @@ theorem rem_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
   rw [BitVec.extractLsb'_ofInt_eq_ofInt (h := by simp)]
   by_cases h : rs1_val = 0#64
   · simp [h]
-  · have h' := h
-    simp only [← BitVec.toInt_inj, BitVec.toInt_zero] at h
+  · simp only [← BitVec.toInt_inj, BitVec.toInt_zero] at h
     simp only [h, reduceIte, ← BitVec.toInt_inj, BitVec.toInt_srem, BitVec.ofInt_toInt_tmod_toInt]
 
 theorem remu_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
@@ -237,7 +241,7 @@ theorem mul_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
     simp only [Nat.reduceLeDiff, BitVec.toInt_signExtend_of_le]
   simp [SailRV64.mul, LeanRV64D.Functions.mult_to_bits_half, Sail.BitVec.extractLsb,
     LeanRV64D.Functions.to_bits_truncate, Sail.get_slice_int, mul, BitVec.extractLsb,
-    h2, h1, BitVec.ofInt_mul, BitVec.extractLsb'_eq_setWidth, BitVec.setWidth_mul,
+    h2, h1, BitVec.ofInt_mul, ← BitVec.setWidth_eq_extractLsb', BitVec.setWidth_mul,
     BitVec.setWidth_setWidth_of_le, BitVec.setWidth_signExtend_eq_self, BitVec.mul_comm]
 
 theorem mulh_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
@@ -250,8 +254,8 @@ theorem mulh_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
   simp only [SailRV64.mul, LeanRV64D.Functions.mult_to_bits_half, Int.cast_ofNat_Int,
     Int.reduceMul, Int.reduceSub, Int.reduceToNat, Nat.reduceSub, Nat.reduceAdd,
     Sail.BitVec.extractLsb, BitVec.extractLsb, LeanRV64D.Functions.to_bits_truncate,
-    Sail.get_slice_int, h2, h1, BitVec.ofInt_mul, BitVec.ofInt_toInt, BitVec.extractLsb'_eq_setWidth, mulh]
-  rw [BitVec.extractLsb'_setWidth_of_le (by omega), BitVec.setWidth_eq_extractLsb' (by omega)]
+    Sail.get_slice_int, h2, h1, BitVec.ofInt_mul, BitVec.ofInt_toInt, mulh]
+  rw [BitVec.extractLsb'_extractLsb'_of_le (by omega), BitVec.setWidth_eq_extractLsb' (by omega)]
   simp
 
 theorem mulhu_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
@@ -281,10 +285,8 @@ theorem mulhsu_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
   simp only [BitVec.truncate_eq_setWidth, BitVec.toInt_setWidth, Nat.reducePow, BitVec.ofInt_mul,
     BitVec.ofInt_toInt]
   rw [Int.bmod_eq_of_le (n := (rs1_val.toNat : Int)) (by omega) (by omega), BitVec.ofInt_natCast,
-    BitVec.extractLsb'_eq_setWidth, BitVec.extractLsb_setWidth_of_lt]
+    ← BitVec.setWidth_eq_extractLsb' (by omega), BitVec.extractLsb_setWidth_of_lt' (by omega) (by omega)]
   simp only [Int.toNat_natCast, BitVec.ofNat_toNat]
-  · omega
-  · omega
 
 theorem mulw_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
     SailRV64.mulw rs1_val rs2_val = mulw rs1_val rs2_val := by
@@ -482,10 +484,6 @@ theorem zbb_rtype_rol_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
       simp
     simp [hzero']
   · have : (64#6 - BitVec.extractLsb 5 0 rs1_val).toNat = ((64 : Int) - (Int.ofNat (rs1_val.toNat % 64)).toNat).toNat := by
-      have : (64 - ((Int.ofNat (rs1_val.toNat % 64)).toNat : Int)).toNat = 64 - (Int.ofNat (rs1_val.toNat % 64)).toNat := by
-        rw [Int.ofNat_toNat]
-        omega
-      simp only [this]
       simp
       omega
     rw [this]
@@ -514,23 +512,23 @@ theorem zbb_rtypew_rolw_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
     BitVec.extractLsb_toNat, Nat.shiftRight_zero, Nat.reducePow, Sail.shiftr, Sail.BitVec.length,
     rolw, BitVec.shiftLeft_eq', BitVec.ushiftRight_eq', LeanRV64D.Functions.sign_extend, Sail.BitVec.signExtend]
   by_cases hzero : rs1_val.toNat % 32 = 0
-  · simp only [hzero, Int.cast_ofNat_Int, BitVec.shiftLeft_zero, BitVec.signExtend_or, BitVec.reduceOfNat, BitVec.zero_sub,
-      BitVec.toNat_neg, Nat.reducePow, BitVec.extractLsb_toNat, Nat.shiftRight_zero, Nat.sub_zero,
-      Nat.reduceAdd, Nat.mod_self, BitVec.ushiftRight_zero, BitVec.or_self]
+  · simp only [hzero, Int.ofNat_eq_natCast, Int.cast_ofNat_Int, Int.toNat_zero,
+    BitVec.shiftLeft_zero, Int.sub_zero, Int.reduceToNat, BitVec.signExtend_or, BitVec.reduceOfNat,
+    BitVec.zero_sub, BitVec.toNat_neg, Nat.reducePow, BitVec.extractLsb_toNat, Nat.shiftRight_zero,
+    Nat.sub_zero, Nat.reduceAdd, Nat.mod_self, BitVec.ushiftRight_zero, BitVec.or_self]
     have : BitVec.setWidth 32 rs2_val >>> 32 = 0#32 := by
       ext i hi
       simp
-    simp [this, BitVec.extractLsb, BitVec.extractLsb'_eq_setWidth]
+    rw [this, BitVec.setWidth_eq_extractLsb' (by omega), BitVec.extractLsb'_eq_extractLsb (h := by omega)]
+    simp
   · have : (32#5 - BitVec.extractLsb 5 0 rs1_val).toNat = ((32 : Int) - (Int.ofNat (rs1_val.toNat % 32)).toNat).toNat := by
-      have : (32 - ((Int.ofNat (rs1_val.toNat % 32)).toNat : Int)).toNat = 32 - (Int.ofNat (rs1_val.toNat % 32)).toNat := by
-        omega
       simp
       omega
     congr
     simp only [BitVec.reduceOfNat, Nat.sub_zero, Nat.reduceAdd, BitVec.extractLsb,
-      BitVec.extractLsb'_eq_setWidth, Nat.reduceLeDiff, BitVec.setWidth_setWidth_of_le,
+      ← BitVec.setWidth_eq_extractLsb', Nat.reduceLeDiff, BitVec.setWidth_setWidth_of_le,
       BitVec.zero_sub, BitVec.toNat_neg, Nat.reducePow, BitVec.toNat_setWidth, Int.ofNat_toNat] at this
-    simp [BitVec.extractLsb, BitVec.extractLsb'_eq_setWidth, this]
+    simp [BitVec.extractLsb, ← BitVec.setWidth_eq_extractLsb', this]
 
 theorem zbb_rtypew_rorw_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
     SailRV64.zbb_rtypew rs1_val rs2_val bropw_zbb.RORW  = rorw rs1_val rs2_val := by
@@ -539,17 +537,15 @@ theorem zbb_rtypew_rorw_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
     BitVec.extractLsb_toNat, Nat.shiftRight_zero, Nat.reducePow, Sail.shiftr, Sail.BitVec.length,
     rorw, BitVec.shiftLeft_eq', BitVec.ushiftRight_eq', LeanRV64D.Functions.sign_extend, Sail.BitVec.signExtend]
   by_cases hzero : rs1_val.toNat % 32 = 0
-  · simp [hzero, BitVec.extractLsb, BitVec.extractLsb'_eq_setWidth]
+  · simp [hzero, BitVec.extractLsb, ← BitVec.setWidth_eq_extractLsb']
   · have : (32#5 - BitVec.extractLsb 5 0 rs1_val).toNat = ((32 : Int) - (Int.ofNat (rs1_val.toNat % 32)).toNat).toNat := by
-      have : (32 - ((Int.ofNat (rs1_val.toNat % 32)).toNat : Int)).toNat = 32 - (Int.ofNat (rs1_val.toNat % 32)).toNat := by
-        omega
       simp
       omega
     congr
     simp only [BitVec.reduceOfNat, Nat.sub_zero, Nat.reduceAdd, BitVec.extractLsb,
-      BitVec.extractLsb'_eq_setWidth, Nat.reduceLeDiff, BitVec.setWidth_setWidth_of_le,
+      ← BitVec.setWidth_eq_extractLsb', Nat.reduceLeDiff, BitVec.setWidth_setWidth_of_le,
       BitVec.zero_sub, BitVec.toNat_neg, Nat.reducePow, BitVec.toNat_setWidth, Int.ofNat_toNat] at this
-    simp [BitVec.extractLsb, BitVec.extractLsb'_eq_setWidth, this]
+    simp [BitVec.extractLsb, ← BitVec.setWidth_eq_extractLsb', this]
 
 theorem zbb_extop_sextb_eq (rs1_val : BitVec 64) :
     SailRV64.zbb_extop rs1_val extop_zbb.SEXTB  = sextb rs1_val := by
@@ -566,22 +562,22 @@ theorem zbb_extop_zexth_eq (rs1_val : BitVec 64) :
 theorem zbb_clz_eq (rs1_val : BitVec 64) :
     SailRV64.zbb_clz rs1_val = clz rs1_val := by
   simp [SailRV64.zbb_clz, clz, LeanRV64D.Functions.to_bits, Sail.get_slice_int,
-    Sail.BitVec.countLeadingZeros, BitVec.extractLsb'_eq_setWidth]
+    Sail.BitVec.countLeadingZeros, ← BitVec.setWidth_eq_extractLsb']
 
 theorem zbb_clzw_eq (rs1_val : BitVec 64) :
     SailRV64.zbb_clzw rs1_val = clzw rs1_val := by
   simp [SailRV64.zbb_clzw, clzw, LeanRV64D.Functions.to_bits, Sail.get_slice_int,
-    Sail.BitVec.countLeadingZeros, BitVec.extractLsb'_eq_setWidth, Sail.BitVec.extractLsb]
+    Sail.BitVec.countLeadingZeros, ← BitVec.setWidth_eq_extractLsb', Sail.BitVec.extractLsb]
 
 theorem zbb_ctz_eq (rs1_val : BitVec 64) :
     SailRV64.zbb_ctz rs1_val = ctz rs1_val := by
   simp [SailRV64.zbb_ctz, ctz, LeanRV64D.Functions.to_bits, Sail.get_slice_int, BitVec.ctz,
-    Sail.BitVec.countTrailingZeros, Sail.BitVec.countLeadingZeros, BitVec.extractLsb'_eq_setWidth]
+    Sail.BitVec.countTrailingZeros, Sail.BitVec.countLeadingZeros, ← BitVec.setWidth_eq_extractLsb']
 
 theorem zbb_ctzw_eq (rs1_val : BitVec 64) :
     SailRV64.zbb_ctzw rs1_val = ctzw rs1_val := by
   simp [SailRV64.zbb_ctzw, ctzw, LeanRV64D.Functions.to_bits, Sail.get_slice_int, BitVec.ctz,
-    Sail.BitVec.countTrailingZeros, Sail.BitVec.countLeadingZeros, BitVec.extractLsb'_eq_setWidth,
+    Sail.BitVec.countTrailingZeros, Sail.BitVec.countLeadingZeros, ← BitVec.setWidth_eq_extractLsb',
     Sail.BitVec.extractLsb]
 
 theorem zbb_roriw_eq (shamt : BitVec 5) (rs1_val : BitVec 64) :
@@ -608,12 +604,9 @@ theorem zbb_rori_eq (shamt : BitVec 5) (rs1_val : BitVec 64) :
     BitVec.toNat_sub, BitVec.toNat_ofNat, Nat.reduceMod]
   by_cases hzero : shamt.toNat = 0
   · simp [hzero]
-  · have : ((64 : Int) - (((shamt.toNat : Int) % 64) : Int).toNat).toNat = ((64 - shamt.toNat % 64) % 64) := by
-      rw [Int.emod_eq_of_lt (by omega) (by omega), Int.toNat_natCast, Int.toNat_sub',
-        Nat.mod_eq_of_lt (a := shamt.toNat) (by omega), Nat.mod_eq_of_lt (by omega)]
-      simp
-    rw [this]
-    congr
+  · congr
+    simp only [Int.ofNat_toNat, Nat.add_zero]
+    omega
 
 /-! ## Zbc: Carry-less multiplication -/
 
@@ -626,7 +619,7 @@ theorem zbs_bclr_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
 theorem zbs_bext_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
     SailRV64.zbs_rtype rs1_val rs2_val brop_zbs.BEXT = bext rs1_val rs2_val := by
   simp only [SailRV64.zbs_rtype, zero_extend, Sail.BitVec.zeroExtend,
-    LeanRV64D.Functions.bool_to_bits, LeanRV64D.Functions.bool_bits_forwards, Sail.shift_bits_left,
+    LeanRV64D.Functions.bool_to_bit, LeanRV64D.Functions.bool_bit_forwards, Sail.shift_bits_left,
     Nat.sub_zero, Nat.reduceAdd, BitVec.ofNat_eq_ofNat, BitVec.truncate_eq_setWidth,
     BitVec.reduceSetWidth, Sail.BitVec.extractLsb, BitVec.shiftLeft_eq', BitVec.extractLsb_toNat,
     Nat.shiftRight_zero, Nat.reducePow, LeanRV64D.Functions.zeros, BitVec.zero_eq, bext, bne_iff_ne,
@@ -653,7 +646,7 @@ theorem zbs_iop_bclri_eq (shamt : BitVec 6) (rs1_val : BitVec 64) :
 theorem zbs_iop_bexti_eq (shamt : BitVec 6) (rs1_val : BitVec 64) :
     SailRV64.zbs_iop shamt rs1_val biop_zbs.BEXTI = bexti shamt rs1_val := by
   simp only [SailRV64.zbs_iop, zero_extend, Sail.BitVec.zeroExtend,
-    LeanRV64D.Functions.bool_to_bits, LeanRV64D.Functions.bool_bits_forwards, Sail.shift_bits_left,
+    LeanRV64D.Functions.bool_to_bit, LeanRV64D.Functions.bool_bit_forwards, Sail.shift_bits_left,
     BitVec.ofNat_eq_ofNat, BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.shiftLeft_eq',
     LeanRV64D.Functions.zeros, BitVec.zero_eq, bexti, bne_iff_ne, ne_eq, ite_not]
   split

lake-manifest.json

@@ -5,11 +5,21 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "933afb61dc5bb8d4a628e08d7cebdd50116f4789",
+   "rev": "1c5153dd9f1410d1316fd23a2f0680d47e15fc80",
    "name": "Lean_RV64D",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/rems-project/lean-sail",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "aed25177482c50db6a7d8da8144388cc69da10f2",
+   "name": "Sail",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v2",
+   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "RISCV",
  "lakeDir": ".lake"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-11-18
+leanprover/lean4:nightly-2026-01-22