Remove toNat from LLVM semantics (#699)

This closes: #694

SSA/Projects/InstCombine/LLVM/Lemmas.lean

@@ -4,19 +4,23 @@ import Mathlib.Tactic
 /-- Note that this assumes that the input and output bitwidths are the same,
 which is by far the common case. -/
 @[simp]
-theorem LLVM.lshr?_eq_some {a b : BitVec w} (hb : b.toNat < w) :
+theorem LLVM.lshr?_eq_some {a b : BitVec w} (hb : b < w) :
     LLVM.lshr? a b = .some (BitVec.ushiftRight a b.toNat) := by
   simp only [LLVM.lshr?]
   split_ifs
-  case pos contra => linarith
+  case pos contra =>
+    have hb' : ¬ b ≥ w := by
+      simp at hb
+      simp only [BitVec.natCast_eq_ofNat, ge_iff_le, BitVec.not_le, hb]
+    contradiction
   case neg _ =>
     simp only [HShiftRight.hShiftRight]
     rfl
 
 /-- Note that this assumes that the input and output bitwidths are the same,
 which is by far the common case. -/
 @[simp]
-theorem LLVM.lshr?_eq_none {a b : BitVec w} (hb : b.toNat ≥ w) : LLVM.lshr? a b = .none := by
+theorem LLVM.lshr?_eq_none {a b : BitVec w} (hb : b ≥ w) : LLVM.lshr? a b = .none := by
   simp only [LLVM.lshr?]
   split_ifs; simp
 

SSA/Projects/InstCombine/LLVM/Semantics.lean

@@ -178,9 +178,9 @@ Division by zero is undefined behavior.
 -/
 @[simp_llvm]
 def udiv? {w : Nat} (x y : BitVec w) : IntW w :=
-  match y.toNat with
-    | 0 => none
-    | _ => pure <| BitVec.ofInt w (x.toNat / y.toNat)
+  if y = 0
+  then none
+  else pure <| BitVec.ofInt w (x.toNat / y.toNat)
 
 structure ExactFlag where
   exact : Bool := false
@@ -253,7 +253,7 @@ Taking the remainder of a division by zero is undefined behavior.
 -/
 @[simp_llvm]
 def urem? {w : Nat} (x y : BitVec w) : IntW w :=
-  if y.toNat = 0
+  if y = 0
   then none
   else pure <| BitVec.ofNat w (x.toNat % y.toNat)
 
@@ -333,8 +333,8 @@ bits in op1, this instruction returns a poison value.
 -/
 @[simp_llvm]
 def shl? {n} (op1 : BitVec n) (op2 : BitVec n) : IntW n :=
-  let bits := op2.toNat
-  if bits >= n then .none
+  if op2 >= n
+  then .none
   else pure (op1 <<< op2)
 
 
@@ -362,8 +362,8 @@ Corresponds to `Std.BitVec.ushiftRight` in the `pure` case.
 -/
 @[simp_llvm]
 def lshr? {n} (op1 : BitVec n) (op2 : BitVec n) : IntW n :=
-  let bits := op2.toNat
-  if bits >= n then .none
+  if op2 >= n
+  then .none
   else pure (op1 >>> op2)
 
 @[simp_llvm_option]
@@ -386,8 +386,8 @@ Corresponds to `Std.BitVec.sshiftRight` in the `pure` case.
 -/
 @[simp_llvm]
 def ashr? {n} (op1 : BitVec n) (op2 : BitVec n) : IntW n :=
-  let bits := op2.toNat -- should this be toInt?
-  if bits >= n then .none
+  if op2 >= n
+  then .none
   else pure (op1 >>>ₛ op2)
 
 @[simp_llvm_option]

SSA/Projects/InstCombine/PaperExamples.lean

@@ -32,11 +32,15 @@ theorem shift_mul:
   simp_alive_ops
   intros A B
   rcases A with rfl | A  <;>
-  rcases B with rfl | B  <;> (try (simp only [bind, Option.bind, Refinement.refl]; done)) <;>
-  by_cases h : w ≤ BitVec.toNat B <;>
-    simp only [Bool.false_eq_true, ge_iff_le, toNat_allOnes, false_and, _root_.or_self, ↓reduceIte,
-      shiftLeft_eq', EffectKind.return_impure_toMonad_eq, Option.pure_def, mul_eq,
-      Option.bind_eq_bind, Option.none_bind, Option.bind_none, Option.some_bind, Refinement.refl, h]
+  rcases B with rfl | B  <;> (try (simp only [Bool.false_eq_true, shiftLeft_eq', false_and, ↓reduceIte, ushiftRight_eq', natCast_eq_ofNat,
+  ge_iff_le, EffectKind.return_impure_toMonad_eq, Option.pure_def, truncate_eq_setWidth, ofNat_eq_ofNat, toNat_ofNat,
+  mul_eq, Option.bind_eq_bind, Option.some_bind, Option.none_bind, Option.bind_none, Refinement.refl]; done)) ;
+  by_cases h : (BitVec.ofNat w w) ≤ B <;>
+    simp only [Bool.false_eq_true, shiftLeft_eq', false_and, ↓reduceIte, ushiftRight_eq',
+      natCast_eq_ofNat, ge_iff_le, EffectKind.return_impure_toMonad_eq, Option.pure_def,
+      truncate_eq_setWidth, ofNat_eq_ofNat, toNat_ofNat, mul_eq, Option.bind_eq_bind,
+      Option.some_bind, Refinement.refl, h]
+  simp
   simp
 
 /--