feat: add remand remw operations

RISCV/ForLean.lean

@@ -8,3 +8,73 @@ theorem sshiftRight_eq_setWidth_extractLsb_signExtend {w : Nat} (n : Nat) (x : B
     Bool.true_and]
   by_cases hni : (n + i) < w
   <;> (simp [hni]; omega)
+
+theorem extractLsb'_eq_setWidth {x : BitVec w} : x.extractLsb' 0 n = x.setWidth n := by
+  ext i hi
+  simp
+
+theorem 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)]
+  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 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
+  | Int.ofNat _, _, ⟨n, rfl⟩ => by
+    rename_i aas
+    apply Int.lt_of_lt_of_le H (@Int.emod_nonneg aas (n + 1) (Int.ofNat_add_one_out n ▸ ((@Int.ofNat_ne_zero n.succ).2 (Nat.succ_ne_zero n))))
+  | Int.negSucc _, _, ⟨n, rfl⟩ => Int.negSucc_eq n ▸ by
+    rw [Int.negSucc_eq, Int.neg_tmod, Int.tmod_neg, Int.neg_lt_neg_iff]
+    apply Int.tmod_lt_of_pos
+    have := ((@Int.ofNat_ne_zero n.succ).2 (Nat.succ_ne_zero n))
+    omega
+
+theorem Int.tmod_lt_of_neg (a : Int) {b : Int} (H : b < 0) : Int.tmod a b < -b :=
+  match a, b, Int.eq_negSucc_of_lt_zero H with
+  | Int.ofNat _, _, ⟨n, rfl⟩ => by
+    rename_i aas
+    simp only [tmod, Nat.succ_eq_add_one, ofNat_eq_coe, natCast_emod, natCast_add, cast_ofNat_Int,
+      neg_negSucc]
+    norm_cast
+    apply Nat.mod_lt
+    omega
+  | Int.negSucc _, _, ⟨n, rfl⟩ => by
+    simp only [tmod, Nat.succ_eq_add_one, ofNat_eq_coe, natCast_emod, natCast_add, cast_ofNat_Int,
+      neg_negSucc]
+    norm_cast
+    omega
+
+theorem Int.emod_lt_of_lt {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) (hax : a < x) : a % b < x := by
+  by_cases hb : b = 0; subst hb; simp [hax]
+  have := @Int.emod_lt a b hb
+  by_cases hb_lt_x : b < x
+  · omega
+  · rw [Int.emod_eq_of_lt (by omega) (by omega)]
+    omega
+
+@[simp]
+theorem BitVec.ofInt_toInt_tmod_toInt {x y : BitVec w} :
+    (BitVec.ofInt w (x.toInt.tmod y.toInt)).toInt = x.toInt.tmod y.toInt := by
+  by_cases hb : y.toInt = 0; simp [hb]
+
+  have ylt := @BitVec.two_mul_toInt_lt w y
+  have ley := @BitVec.le_two_mul_toInt w y
+
+  rw [BitVec.toInt_ofInt, Int.bmod_eq_of_le_mul_two]
+  · by_cases hy : 0 < y.toInt
+    · have := Int.lt_tmod_of_pos x.toInt hy
+      norm_cast at *
+      omega
+    · have := @Int.lt_tmod_of_neg x.toInt y.toInt (by omega)
+      norm_cast at *
+      omega
+  · by_cases hy : 0 < y.toInt
+    · have := Int.tmod_lt_of_pos x.toInt hy
+      norm_cast at *
+      omega
+    · have := @Int.tmod_lt_of_neg x.toInt y.toInt (by omega)
+      norm_cast at *
+      omega

RISCV/Instructions.lean

@@ -186,3 +186,31 @@ def sraw (rs2_val : BitVec 64) (rs1_val : BitVec 64) :=
   let rs1 := BitVec.extractLsb 31 0 rs1_val
   let rs2 := BitVec.extractLsb 4 0 rs2_val
   BitVec.signExtend 64 (BitVec.sshiftRight' rs1 rs2)
+
+/-! # M Extension for Integer Multiplication and Division -/
+
+/--
+  Perform an XLEN bits by XLEN bits signed integer reminder of rs1 by rs2.
+-/
+def rem (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 := rs1_val.srem rs2_val
+
+/--
+  Perform an XLEN bits by XLEN bits unsigned integer reminder of rs1 by rs2.
+-/
+def remu (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 := rs1_val.umod rs2_val
+
+/--
+  Perform an 32 bits by 32 bits signed integer reminder of rs1 by rs2.
+-/
+def remw (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :=
+  let rs1 := BitVec.extractLsb 31 0 rs1_val
+  let rs2 := BitVec.extractLsb 31 0 rs2_val
+  BitVec.signExtend 64 (rs1.srem rs2)
+
+/--
+  Perform an 32 bits by 32 bits unsigned integer reminder of rs1 by rs2.
+-/
+def remuw (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :=
+  let rs1 := BitVec.extractLsb 31 0 rs1_val
+  let rs2 := BitVec.extractLsb 31 0 rs2_val
+  BitVec.signExtend 64 (rs1.umod rs2)

RISCV/SailPure.lean

@@ -68,3 +68,19 @@ def rtypew (op : ropw) (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :
     | ropw.SRLW => (Sail.shift_bits_right rs1_val32 (Sail.BitVec.extractLsb rs2_val32 4 0))
     | ropw.SRAW => (shift_bits_right_arith rs1_val32 (Sail.BitVec.extractLsb rs2_val32 4 0))
   ((sign_extend (m := ((2 ^i 3) *i 8)) result))
+
+/-! # M Extension for Integer Multiplication and Division -/
+
+def rem (is_unsigned : Bool) (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :=
+  let rs1_int : Int := if is_unsigned then BitVec.toNat rs1_val else BitVec.toInt rs1_val
+  let rs2_int : Int := if is_unsigned then BitVec.toNat rs2_val else BitVec.toInt rs2_val
+  let remainder := if (rs2_int == 0 : Bool) then rs1_int else (Int.tmod rs1_int rs2_int)
+  to_bits_truncate (l := 64) remainder
+
+def remw (is_unsigned : Bool) (rs2_val : BitVec 64) (rs1_val : BitVec 64) : BitVec 64 :=
+  let rs1_val32 := Sail.BitVec.extractLsb rs1_val 31 0
+  let rs2_val32 := Sail.BitVec.extractLsb rs2_val 31 0
+  let rs1_int : Int := if is_unsigned then BitVec.toNat rs1_val32 else BitVec.toInt rs1_val32
+  let rs2_int : Int := if is_unsigned then BitVec.toNat rs2_val32 else BitVec.toInt rs2_val32
+  let rem := if ((rs2_int == 0) : Bool) then rs1_int else Int.tmod rs1_int rs2_int
+  sign_extend (m := ((2 ^i 3) *i 8)) (to_bits_truncate (l := 32) rem)

RISCV/SailPureToInstructions.lean

@@ -139,3 +139,64 @@ theorem rtypew_sraw_eq (rs1_val : BitVec 64) (rs2_val : BitVec 64) :
     sraw, BitVec.sshiftRight_eq', sshiftRight_eq_setWidth_extractLsb_signExtend,
     Nat.add_one_sub_one]
   rfl
+
+/-! # M Extension for Integer Multiplication and Division -/
+
+theorem rem_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
+    SailRV64I.rem false rs1_val rs2_val = rem rs1_val rs2_val := by
+  simp only [SailRV64I.rem, rem, LeanRV64D.Functions.to_bits_truncate, Sail.get_slice_int,
+    Nat.reduceAdd, Bool.false_eq_true, ↓reduceIte, beq_iff_eq]
+  rw [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 [h, reduceIte, ← BitVec.toInt_inj, BitVec.toInt_srem, BitVec.ofInt_toInt_tmod_toInt]
+
+theorem remu_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
+    SailRV64I.rem true rs1_val rs2_val = remu rs1_val rs2_val := by
+  simp only [SailRV64I.rem, LeanRV64D.Functions.to_bits_truncate, Sail.get_slice_int, remu]
+  by_cases h1 : rs1_val = 0#64
+  · simp [h1, BitVec.extractLsb'_setWidth_of_le]
+  · simp only [Nat.reduceAdd, reduceIte, beq_iff_eq]
+    have h1' : ¬rs1_val.toNat = 0 := by simp [BitVec.toNat_eq] at h1; exact h1
+    simp only [Int.natCast_eq_zero, BitVec.umod_eq]
+    rw [extractLsb'_ofInt_eq_ofInt (by omega)]
+    apply BitVec.eq_of_toInt_eq
+    simp only [BitVec.toInt_ofInt, Nat.reducePow, BitVec.toInt_umod, h1', reduceIte]
+    congr
+
+theorem remw_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
+    SailRV64I.remw False rs1_val rs2_val = remw rs1_val rs2_val := by
+  simp only [SailRV64I.remw, LeanRV64D.Functions.sign_extend, Sail.BitVec.signExtend,
+    LeanRV64D.Functions.to_bits_truncate, Sail.get_slice_int, Nat.reduceAdd, decide_false,
+    Bool.false_eq_true, reduceIte, Nat.reduceSub, Sail.BitVec.extractLsb, beq_iff_eq, remw]
+  rw [extractLsb'_ofInt_eq_ofInt (h:= by simp)]
+  split
+  · case _ htrue =>
+    have heq := BitVec.eq_of_toInt_eq (x := BitVec.extractLsb 31 0 rs1_val) (y := 0#64) htrue
+    simp only [Nat.sub_zero, Nat.reduceAdd, Nat.reduceLeDiff, BitVec.setWidth_ofNat_of_le] at heq
+    congr
+    simp only [heq, BitVec.ofInt_toInt, BitVec.srem_zero]
+  · case _ hfalse =>
+    rw [← BitVec.toInt_srem, BitVec.ofInt_toInt]
+    congr
+
+theorem remuw_eq (rs2_val : BitVec 64) (rs1_val : BitVec 64) :
+    SailRV64I.remw True rs1_val rs2_val = remuw rs1_val rs2_val := by
+  simp only [SailRV64I.remw, LeanRV64D.Functions.sign_extend, Sail.BitVec.signExtend,
+    LeanRV64D.Functions.to_bits_truncate, Sail.get_slice_int, Nat.reduceAdd, Nat.reduceSub,
+    Sail.BitVec.extractLsb, beq_iff_eq, remuw, decide_true, reduceIte, BitVec.umod_eq]
+  rw [extractLsb'_ofInt_eq_ofInt (h:= by simp)]
+  split
+  · case _ htrue =>
+    congr
+    norm_cast at htrue
+    have heq := BitVec.eq_of_toNat_eq (x := BitVec.extractLsb 31 0 rs1_val) (y := 0#32) htrue
+    simp only [BitVec.ofInt_natCast, heq, BitVec.ofNat_toNat, BitVec.setWidth_eq, BitVec.umod_zero]
+  · case _ hfalse =>
+    congr
+    apply BitVec.eq_of_toInt_eq
+    simp only [BitVec.extractLsb_toNat, Nat.shiftRight_zero, Nat.sub_zero, Nat.reduceAdd,
+      Nat.reducePow, Int.natCast_emod, Int.cast_ofNat_Int, BitVec.toInt_ofInt, BitVec.toInt_umod]
+    rfl

RISCV/SailToRV64.lean

@@ -138,3 +138,26 @@ theorem rtypew_srlw_eq (rs1 : regidx) (rs2 : regidx) (rd : regidx) :
 theorem rtypew_sraw_eq (rs1 : regidx) (rs2 : regidx) (rd : regidx) :
     execute_RTYPEW rs2 rs1 rd ropw.SRAW
       = skeleton_binary rs2 rs1 rd (fun val1 val2 => SailRV64I.rtypew ropw.SRAW val2 val1) := by rfl
+
+/-! # M Extension for Integer Multiplication and Division -/
+
+/--
+  Due to a mistake in the Sail model, some proofs are currently broken.
+  We replace the proofs depending on mistaken definitions with an axiom.-/
+axiom rem_sail_error {p: Prop} : p
+
+theorem rem_unsigned_eq (rs2 : regidx) (rs1 : regidx) (rd : regidx) :
+    execute_REM rs2 rs1 rd true
+    = skeleton_binary rs2 rs1 rd (fun val1 val2 => SailRV64I.rem true val2 val1) := rem_sail_error
+
+theorem rem_signed_eq (rs2 : regidx) (rs1 : regidx) (rd : regidx) :
+    execute_REM rs2 rs1 rd false
+    = skeleton_binary rs2 rs1 rd (fun val1 val2 => SailRV64I.rem false val2 val1) := rem_sail_error
+
+theorem remw_unsigned_eq (rs2 : regidx) (rs1 : regidx) (rd : regidx) :
+    execute_REMW rs2 rs1 rd true
+    = skeleton_binary rs2 rs1 rd (fun val1 val2 => SailRV64I.remw true val2 val1) := rem_sail_error
+
+theorem remw_signed_eq (rs2 : regidx) (rs1 : regidx) (rd : regidx) :
+    execute_REMW rs2 rs1 rd false
+    = skeleton_binary rs2 rs1 rd (fun val1 val2 => SailRV64I.remw false val2 val1) := rem_sail_error