From 71921ab1ecde3b1a35fbe44949a038a05b03cef2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Thu, 2 Nov 2023 13:56:06 +0100
Subject: [PATCH 01/12] Factor out LLVM semantics

---
 SSA/Projects/InstCombine/Base.lean           |  1 +
 SSA/Projects/InstCombine/ForStd.lean         | 67 ------------------
 SSA/Projects/InstCombine/LLVM/Semantics.lean | 74 ++++++++++++++++++++
 3 files changed, 75 insertions(+), 67 deletions(-)
 create mode 100644 SSA/Projects/InstCombine/LLVM/Semantics.lean

diff --git a/SSA/Projects/InstCombine/Base.lean b/SSA/Projects/InstCombine/Base.lean
index 89c4d18bd..828ee677f 100644
--- a/SSA/Projects/InstCombine/Base.lean
+++ b/SSA/Projects/InstCombine/Base.lean
@@ -3,6 +3,7 @@ import SSA.Core.Framework
 import SSA.Core.Util
 import SSA.Core.Util.ConcreteOrMVar
 import SSA.Projects.InstCombine.ForStd
+import SSA.Projects.InstCombine.LLVM.Semantics
 
 /-!
   # InstCombine Dialect
diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index 2bbdfcb4a..b20866355 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -73,74 +73,7 @@ instance {α : Type u} [DecidableEq α] : DecidableRel (@Refinement α) := by
 end Refinement
 
 infix:50 (priority:=low) " ⊑ " => Refinement
-
-/--
-The value produced is the unsigned integer quotient of the two operands.
-Note that unsigned integer division and signed integer division are distinct operations; for signed integer division, use ‘sdiv’.
-Division by zero is undefined behavior.
--/
-def udiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
-  match y.toNat with
-    | 0 => none
-    | _ => some $ BitVec.ofNat w (x.toNat / y.toNat)
-
-/--
-The value produced is the signed integer quotient of the two operands rounded towards zero.
-Note that signed integer division and unsigned integer division are distinct operations; for unsigned integer division, use ‘udiv’.
-Division by zero is undefined behavior.
-Overflow also leads to undefined behavior; this is a rare case, but can occur, for example, by doing a 32-bit division of -2147483648 by -1.
--/
-def sdiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
-  if y.toInt = 0
-  then none
-  else
-    let div := (x.toInt / y.toInt)
-    if div < Int.ofNat (2^w)
-      then some $ BitVec.ofInt w div
-      else none
-
-/--
-This instruction returns the unsigned integer remainder of a division. This instruction always performs an unsigned division to get the remainder.
-Note that unsigned integer remainder and signed integer remainder are distinct operations; for signed integer remainder, use ‘srem’.
-Taking the remainder of a division by zero is undefined behavior.
--/
-def urem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
-  if y.toNat = 0
-  then none
-  else some $ BitVec.ofNat w (x.toNat % y.toNat)
-
-def _root_.Int.rem (x y : Int) : Int :=
-  if x ≥ 0 then (x % y) else ((x % y) - y.natAbs)
-
--- TODO: prove this to make sure it's the right implementation!
-theorem _root_.Int.rem_sign_dividend :
-  ∀ x y, Int.rem x y < 0 ↔ x < 0 :=  by sorry
-
-/--
-This instruction returns the remainder of a division (where the result is either zero or has the same sign as the dividend, op1),
-not the modulo operator (where the result is either zero or has the same sign as the divisor, op2) of a value.
-For more information about the difference, see The Math Forum.
-For a table of how this is implemented in various languages, please see Wikipedia: modulo operation.
-Note that signed integer remainder and unsigned integer remainder are distinct operations; for unsigned integer remainder, use ‘urem’.
-Taking the remainder of a division by zero is undefined behavior.
-For vectors, if any element of the divisor is zero, the operation has undefined behavior.
-Overflow also leads to undefined behavior; this is a rare case, but can occur, for example,
-by taking the remainder of a 32-bit division of -2147483648 by -1.
-(The remainder doesn’t actually overflow, but this rule lets srem be implemented using instructions that return both the result
-of the division and the remainder.)
--/
-def srem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
-  if y.toInt = 0
-  then none
-  else
-    let div := (x.toInt / y.toInt)
-    if div < Int.ofNat (2^w)
-      then some $ BitVec.ofInt w (x.toInt.rem y.toInt)
-      else none
-
 instance : Coe Bool (BitVec 1) := ⟨ofBool⟩
 
 instance decPropToBitvec1 (p : Prop) [Decidable p] : CoeDep Prop p (BitVec 1) where
   coe := ofBool $ decide p
-
-def sshr (a : BitVec n) (s : Nat) := BitVec.sshiftRight a s
diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
new file mode 100644
index 000000000..47e90d899
--- /dev/null
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -0,0 +1,74 @@
+import Std.Data.BitVec
+import SSA.Projects.InstCombine.ForStd
+
+
+open Std
+
+namespace Std.BitVec
+
+
+/--
+The value produced is the unsigned integer quotient of the two operands.
+Note that unsigned integer division and signed integer division are distinct operations; for signed integer division, use ‘sdiv’.
+Division by zero is undefined behavior.
+-/
+def udiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
+  match y.toNat with
+    | 0 => none
+    | _ => some $ BitVec.ofNat w (x.toNat / y.toNat)
+
+/--
+The value produced is the signed integer quotient of the two operands rounded towards zero.
+Note that signed integer division and unsigned integer division are distinct operations; for unsigned integer division, use ‘udiv’.
+Division by zero is undefined behavior.
+Overflow also leads to undefined behavior; this is a rare case, but can occur, for example, by doing a 32-bit division of -2147483648 by -1.
+-/
+def sdiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
+  if y.toInt = 0
+  then none
+  else
+    let div := (x.toInt / y.toInt)
+    if div < Int.ofNat (2^w)
+      then some $ BitVec.ofInt w div
+      else none
+
+/--
+This instruction returns the unsigned integer remainder of a division. This instruction always performs an unsigned division to get the remainder.
+Note that unsigned integer remainder and signed integer remainder are distinct operations; for signed integer remainder, use ‘srem’.
+Taking the remainder of a division by zero is undefined behavior.
+-/
+def urem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
+  if y.toNat = 0
+  then none
+  else some $ BitVec.ofNat w (x.toNat % y.toNat)
+
+def _root_.Int.rem (x y : Int) : Int :=
+  if x ≥ 0 then (x % y) else ((x % y) - y.natAbs)
+
+-- TODO: prove this to make sure it's the right implementation!
+theorem _root_.Int.rem_sign_dividend :
+  ∀ x y, Int.rem x y < 0 ↔ x < 0 :=  by sorry
+
+/--
+This instruction returns the remainder of a division (where the result is either zero or has the same sign as the dividend, op1),
+not the modulo operator (where the result is either zero or has the same sign as the divisor, op2) of a value.
+For more information about the difference, see The Math Forum.
+For a table of how this is implemented in various languages, please see Wikipedia: modulo operation.
+Note that signed integer remainder and unsigned integer remainder are distinct operations; for unsigned integer remainder, use ‘urem’.
+Taking the remainder of a division by zero is undefined behavior.
+For vectors, if any element of the divisor is zero, the operation has undefined behavior.
+Overflow also leads to undefined behavior; this is a rare case, but can occur, for example,
+by taking the remainder of a 32-bit division of -2147483648 by -1.
+(The remainder doesn’t actually overflow, but this rule lets srem be implemented using instructions that return both the result
+of the division and the remainder.)
+-/
+def srem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
+  if y.toInt = 0
+  then none
+  else
+    let div := (x.toInt / y.toInt)
+    if div < Int.ofNat (2^w)
+      then some $ BitVec.ofInt w (x.toInt.rem y.toInt)
+      else none
+
+def sshr (a : BitVec n) (s : Nat) := BitVec.sshiftRight a s

From 894b9bc8d1cea01dfeb8e411d4eb98303070ee9c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Thu, 2 Nov 2023 13:56:20 +0100
Subject: [PATCH 02/12] Update lake manifest

---
 lake-manifest.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index f017ded0a..661325826 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -20,7 +20,7 @@
   {"git":
    {"url": "https://github.com/tydeu/lean4-partax",
     "subDir?": null,
-    "rev": "573a45378782b9b32af8ecbe965052b46bfccd08",
+    "rev": "9dfc1672e14210ff61174d21f97c2f28cb904346",
     "opts": {},
     "name": "partax",
     "inputRev?": "master",

From 216f6ca1ceee225d8409800bc2f6a9bb4ecd18de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Thu, 2 Nov 2023 15:43:14 +0100
Subject: [PATCH 03/12] progress on LLVM semantics

---
 SSA/Projects/InstCombine/ForStd.lean         |  7 ++
 SSA/Projects/InstCombine/LLVM/Semantics.lean | 87 +++++++++++++++++++-
 2 files changed, 90 insertions(+), 4 deletions(-)

diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index b20866355..559799a68 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -75,5 +75,12 @@ end Refinement
 infix:50 (priority:=low) " ⊑ " => Refinement
 instance : Coe Bool (BitVec 1) := ⟨ofBool⟩
 
+def BitVec.coeWidth {m n : Nat} : BitVec m → BitVec n
+  | x => BitVec.ofNat n x.toNat
+
+-- not sure what the right `Coe`is for this case
+-- See: https://leanprover-community.github.io/mathlib4_docs/Init/Coe.html#Important-typeclasses
+--instance {m n: Nat} : CoeTail (BitVec m) (BitVec n) := ⟨BitVec.coeWidth⟩
+
 instance decPropToBitvec1 (p : Prop) [Decidable p] : CoeDep Prop p (BitVec 1) where
   coe := ofBool $ decide p
diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index 47e90d899..994c9181e 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -6,13 +6,64 @@ open Std
 
 namespace Std.BitVec
 
+/--
+The ‘and’ instruction returns the bitwise logical and of its two operands.
+-/
+def and? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
+ .some <| x ||| y
+
+
+/--
+The ‘or’ instruction returns the bitwise logical inclusive or of its two
+operands.
+-/
+def or? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
+ .some <| x &&& y
+
+/--
+The ‘xor’ instruction returns the bitwise logical exclusive or of its two
+operands.  The xor is used to implement the “one’s complement” operation, which
+is the “~” operator in C.
+-/
+def xor? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
+ .some <| x ^^^ y
+
+/--
+The value produced is the integer sum of the two operands.
+If the sum has unsigned overflow, the result returned is the mathematical result modulo 2n, where n is the bit width of the result.
+Because LLVM integers use a two’s complement representation, this instruction is appropriate for both signed and unsigned integers.
+-/
+def add? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
+ .some <| x + y
+
+/--
+The value produced is the integer difference of the two operands.
+If the difference has unsigned overflow, the result returned is the mathematical result modulo 2n, where n is the bit width of the result.
+Because LLVM integers use a two’s complement representation, this instruction is appropriate for both signed and unsigned integers.
+-/
+def sub? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
+ .some <| x - y
+
+/--
+The value produced is the integer product of the two operands.
+If the result of the multiplication has unsigned overflow, the result returned
+is the mathematical result modulo 2n, where n is the bit width of the result.
+Because LLVM integers use a two’s complement representation, and the result
+is the same width as the operands, this instruction returns the correct
+result for both signed and unsigned integers.
+
+If a full product (e.g. i32 * i32 -> i64) is needed, the operands should be
+sign-extended or zero-extended as appropriate to the width of the full product.
+-/
+def mul? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
+ .some <| x * y
 
 /--
 The value produced is the unsigned integer quotient of the two operands.
 Note that unsigned integer division and signed integer division are distinct operations; for signed integer division, use ‘sdiv’.
 Division by zero is undefined behavior.
 -/
-def udiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
+def udiv? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
   match y.toNat with
     | 0 => none
     | _ => some $ BitVec.ofNat w (x.toNat / y.toNat)
@@ -23,7 +74,7 @@ Note that signed integer division and unsigned integer division are distinct ope
 Division by zero is undefined behavior.
 Overflow also leads to undefined behavior; this is a rare case, but can occur, for example, by doing a 32-bit division of -2147483648 by -1.
 -/
-def sdiv? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
+def sdiv? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
   if y.toInt = 0
   then none
   else
@@ -37,7 +88,7 @@ This instruction returns the unsigned integer remainder of a division. This inst
 Note that unsigned integer remainder and signed integer remainder are distinct operations; for signed integer remainder, use ‘srem’.
 Taking the remainder of a division by zero is undefined behavior.
 -/
-def urem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
+def urem? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
   if y.toNat = 0
   then none
   else some $ BitVec.ofNat w (x.toNat % y.toNat)
@@ -62,7 +113,7 @@ by taking the remainder of a 32-bit division of -2147483648 by -1.
 (The remainder doesn’t actually overflow, but this rule lets srem be implemented using instructions that return both the result
 of the division and the remainder.)
 -/
-def srem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
+def srem? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
   if y.toInt = 0
   then none
   else
@@ -72,3 +123,31 @@ def srem? {w : Nat} (x y : BitVec w) : Option $ BitVec w :=
       else none
 
 def sshr (a : BitVec n) (s : Nat) := BitVec.sshiftRight a s
+
+/--
+Shift left instruction.
+The value produced is op1 * 2op2 mod 2n, where n is the width of the result.
+If op2 is (statically or dynamically) equal to or larger than the number of
+bits in op1, this instruction returns a poison value.
+-/
+def shl? {m n k} (op1 : BitVec n) (op2 : BitVec m) : Option (BitVec k) :=
+  let bits := op2.toNat -- should this be toInt?
+  if bits >= n then .none
+  else .some <| BitVec.coeWidth (op1 <<< op2)
+
+
+
+/-
+TODO:
+  | Op.const w val => Option.some (BitVec.ofInt w val)
+  | Op.lshr _ => pairMapM (. >>> .) arg.toPair
+  | Op.ashr _ => pairMapM (. >>>ₛ .) arg.toPair
+  | Op.select _ => tripleMapM BitVec.select arg.toTriple
+  | Op.icmp c _ => match c with
+
+
+These don't seem to exist in LLVM
+  | Op.not _ => Option.map (~~~.) arg.toSingle
+  | Op.copy _ => arg.toSingle
+  | Op.neg _ => Option.map (-.) arg.toSingle
+-/

From 4441d6c26a69567c115d2e33f60273b5468eb107 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Tue, 7 Nov 2023 14:29:46 +0100
Subject: [PATCH 04/12] Finish LLVM semantics, not tested, not integrated

---
 SSA/Projects/InstCombine/ForStd.lean         |   6 -
 SSA/Projects/InstCombine/LLVM/Semantics.lean | 150 +++++++++++++++++--
 2 files changed, 139 insertions(+), 17 deletions(-)

diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index 559799a68..b1abcf6bb 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -24,12 +24,6 @@ instance {n} : ShiftRight (BitVec n) := ⟨fun x y => x >>> y.toNat⟩
 
 infixl:75 ">>>ₛ" => fun x y => BitVec.sshiftRight x (BitVec.toNat y)
 
-/--
- If the condition is an i1 and it evaluates to 1, the instruction returns the first value argument; otherwise, it returns the second value argument.
--/
-def select {w : Nat} (c : BitVec 1) (x y : BitVec w) : BitVec w :=
-  cond (c.toNat != 0) x y
-
 -- A lot of this should probably go to a differet file here and not Mathlib
 inductive Refinement {α : Type u} : Option α → Option α → Prop
   | bothSome {x y : α } : x = y → Refinement (some x) (some y)
diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index 994c9181e..2d77dd234 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -135,19 +135,147 @@ def shl? {m n k} (op1 : BitVec n) (op2 : BitVec m) : Option (BitVec k) :=
   if bits >= n then .none
   else .some <| BitVec.coeWidth (op1 <<< op2)
 
+/--
+This instruction always performs a logical shift right operation.
+The most significant bits of the result will be filled with zero bits after
+the shift.
+
+If op2 is (statically or dynamically) equal to or larger than the number of bits in op1,
+this instruction returns a poison value.
+
+Corresponds to `Std.BitVec.ushiftRight` in the `some` case.
+-/
+def lhr? {m n k} (op1 : BitVec n) (op2 : BitVec m) : Option (BitVec k) :=
+  let bits := op2.toNat -- should this be toInt?
+  if bits >= n then .none
+  else .some <| BitVec.coeWidth (op1 >>> op2)
+
+
+/--
+This instruction always performs an arithmetic shift right operation,
+The most significant bits of the result will be filled with the sign bit of op1.
+
+If op2 is (statically or dynamically) equal to or larger than the number of bits in op1,
+this instruction returns a poison value.
+
+Corresponds to `Std.BitVec.sshiftRight` in the `some` case.
+-/
+def ashr? {m n k} (op1 : BitVec n) (op2 : BitVec m) : Option (BitVec k) :=
+  let bits := op2.toNat -- should this be toInt?
+  if bits >= n then .none
+  else .some <| BitVec.coeWidth (op1 >>>ₛ op2)
+
+/--
+ If the condition is an i1 and it evaluates to 1, the instruction returns the first value argument; otherwise, it returns the second value argument.
+-/
+def select {w : Nat} (c : BitVec 1) (x y : BitVec w) : BitVec w :=
+  cond (c.toNat != 0) x y
+
+/--
+ Wrapper around `select` (this cannot become `none` on its own)
+ If the condition is an i1 and it evaluates to 1, the instruction returns the first value argument; otherwise, it returns the second value argument.
+-/
+def select? {w : Nat} (c : BitVec 1) (x y : BitVec w) : Option (BitVec w) :=
+  Option.some <| select c x y
+
+inductive IntPredicate where
+  | eq
+  | ne
+  | ugt
+  | uge
+  | ult
+  | ule
+  | sgt
+  | sge
+  | slt
+  | sle
+deriving Inhabited, DecidableEq, Repr
+
+instance : ToString IntPredicate where
+  toString
+  | .eq => "eq"
+  | .ne => "ne"
+  | .ugt => "ugt"
+  | .uge => "uge"
+  | .ult => "ult"
+  | .ule => "ule"
+  | .sgt => "sgt"
+  | .sge => "sge"
+  | .slt => "slt"
+  | .sle => "sle"
+
+
+/--
+The ‘icmp’ instruction takes three operands.
+The first operand is the condition code indicating the kind of comparison to perform. It is not a value, just a keyword.
+The possible condition codes are:
+
+  - eq: equal
+  - ne: not equal
+  - ugt: unsigned greater than
+  - uge: unsigned greater or equal
+  - ult: unsigned less than
+  - ule: unsigned less or equal
+  - sgt: signed greater than
+  - sge: signed greater or equal
+  - slt: signed less than
+  - sle: signed less or equal
+
+The remaining two arguments must be integer. They must also be identical types.
+-/
+def icmp {w : Nat} (c : IntPredicate) (x y : BitVec w) : Bool :=
+  match c with
+    | .eq => (x == y)
+    | .ne => (x != y)
+    | .sgt => (x >ₛ y)
+    | .sge => (x ≥ₛ y)
+    | .slt => (x <ₛ y)
+    | .sle => (x ≤ₛ y)
+    | .ugt => (x >ᵤ y)
+    | .uge => (x ≥ᵤ y)
+    | .ult => (x <ᵤ y)
+    | .ule => (x ≤ᵤ y)
+
+
+/--
+Wrapper around `icmp` (this cannot become `none` on its own).
+
+The ‘icmp’ instruction takes three operands.
+The first operand is the condition code indicating the kind of comparison to perform. It is not a value, just a keyword.
+The possible condition codes are:
 
+  - eq: equal
+  - ne: not equal
+  - ugt: unsigned greater than
+  - uge: unsigned greater or equal
+  - ult: unsigned less than
+  - ule: unsigned less or equal
+  - sgt: signed greater than
+  - sge: signed greater or equal
+  - slt: signed less than
+  - sle: signed less or equal
+
+The remaining two arguments must be integer. They must also be identical types.
+-/
+def icmp? {w : Nat} {c : IntPredicate} (x y : BitVec w) : Option (BitVec 1) :=
+  Option.some ↑(icmp c x y)
+
+/--
+Unlike LLVM IR, MLIR does not have first-class constant values.
+Therefore, all constants must be created as SSA values before being used in other
+operations. llvm.mlir.constant creates such values for scalars and vectors.
+It has a mandatory value attribute, which must be an integer
+(currently the only supported type in these semantics).
 
-/-
-TODO:
-  | Op.const w val => Option.some (BitVec.ofInt w val)
-  | Op.lshr _ => pairMapM (. >>> .) arg.toPair
-  | Op.ashr _ => pairMapM (. >>>ₛ .) arg.toPair
-  | Op.select _ => tripleMapM BitVec.select arg.toTriple
-  | Op.icmp c _ => match c with
+The type of the attribute is one of the corresponding MLIR builtin types.
+The operation produces a new SSA value of the specified LLVM IR dialect type.
+The type of that value must correspond to the attribute type converted to LLVM IR.
 
+This interprets the value as a signed bitvector.
+If the bitwidth is not enough it will be reduced, returning
+the value `(2^w + (i mod 2^w)) mod 2^w`.
 
-These don't seem to exist in LLVM
-  | Op.not _ => Option.map (~~~.) arg.toSingle
-  | Op.copy _ => arg.toSingle
-  | Op.neg _ => Option.map (-.) arg.toSingle
+TODO: double-check that truncating works the same as MLIR (signedness, overflow, etc)
 -/
+def const? (i : Int): Option (BitVec w) :=
+  BitVec.ofInt w i

From dfc720f05b365abbd71f9d8abecc234212f5da35 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Tue, 7 Nov 2023 14:41:16 +0100
Subject: [PATCH 05/12] Fix InstCombine denote (make it typecheck again)

---
 SSA/Core/Util.lean                           |   8 +-
 SSA/Projects/InstCombine/Base.lean           | 108 +++++++------------
 SSA/Projects/InstCombine/ForStd.lean         |   2 +-
 SSA/Projects/InstCombine/LLVM/Semantics.lean |   8 +-
 4 files changed, 50 insertions(+), 76 deletions(-)

diff --git a/SSA/Core/Util.lean b/SSA/Core/Util.lean
index 501f84a3f..197d866e8 100644
--- a/SSA/Core/Util.lean
+++ b/SSA/Core/Util.lean
@@ -10,6 +10,12 @@ def pairBind [Monad m] (f : α → β → m γ) (pair : (m α × m β)) : m γ :
   let snd ← pair.snd
   f fst snd
 
+@[simp]
+def tripleBind [Monad m] (f : α → β → γ → m δ) (triple : (m α × m β × m γ)) : m δ := do
+  let (fstM,sndM,trdM) := triple
+  let (fst,snd,trd) := (← fstM,← sndM,← trdM)
+  f fst snd trd
+
 @[simp]
 def pairMapM [Monad m] (f : α → β → γ) (pair : (m α × m β)) : m γ := do
   let fst ← pair.fst
@@ -84,4 +90,4 @@ end LengthIndexedList
 elab "print_goal_as_error " : tactic => do
   let target ← Lean.Elab.Tactic.getMainTarget
   throwError target
-  pure ()
\ No newline at end of file
+  pure ()
diff --git a/SSA/Projects/InstCombine/Base.lean b/SSA/Projects/InstCombine/Base.lean
index 828ee677f..f6fc341da 100644
--- a/SSA/Projects/InstCombine/Base.lean
+++ b/SSA/Projects/InstCombine/Base.lean
@@ -25,33 +25,9 @@ namespace InstCombine
 
 open Std (BitVec)
 
-abbrev Width φ := ConcreteOrMVar Nat φ
+open LLVM
 
-inductive IntPredicate where
-  | eq
-  | ne
-  | ugt
-  | uge
-  | ult
-  | ule
-  | sgt
-  | sge
-  | slt
-  | sle
-deriving Inhabited, DecidableEq, Repr
-
-instance : ToString IntPredicate where
-  toString
-  | .eq => "eq"
-  | .ne => "ne"
-  | .ugt => "ugt"
-  | .uge => "uge"
-  | .ult => "ult"
-  | .ule => "ule"
-  | .sgt => "sgt"
-  | .sge => "sge"
-  | .slt => "slt"
-  | .sle => "sle"
+abbrev Width φ := ConcreteOrMVar Nat φ
 
 inductive MTy (φ : Nat)
   | bitvec (w : Width φ) : MTy φ
@@ -113,25 +89,25 @@ deriving Repr, DecidableEq, Inhabited
 
 instance : ToString (MOp φ) where
   toString
-  | .and w => "and"
-  | .or w => "or"
-  | .not w => "not"
-  | .xor w => "xor"
-  | .shl w => "shl"
-  | .lshr w => "lshr"
-  | .ashr w => "ashr"
-  | .urem w => "urem"
-  | .srem w => "srem"
-  | .select w => "select"
-  | .add w => "add"
-  | .mul w => "mul"
-  | .sub w => "sub"
-  | .neg w => "neg"
-  | .copy w => "copy"
-  | .sdiv w => "sdiv"
-  | .udiv w => "udiv"
-  | .icmp ty w => s!"icmp {ty}"
-  | .const w v => s!"const {v}"
+  | .and _ => "and"
+  | .or _ => "or"
+  | .not _ => "not"
+  | .xor _ => "xor"
+  | .shl _ => "shl"
+  | .lshr _ => "lshr"
+  | .ashr _ => "ashr"
+  | .urem _ => "urem"
+  | .srem _ => "srem"
+  | .select _ => "select"
+  | .add _ => "add"
+  | .mul _ => "mul"
+  | .sub _ => "sub"
+  | .neg _ => "neg"
+  | .copy _ => "copy"
+  | .sdiv _ => "sdiv"
+  | .udiv _ => "udiv"
+  | .icmp ty _ => s!"icmp {ty}"
+  | .const _ v => s!"const {v}"
 
 abbrev Op := MOp 0
 
@@ -190,35 +166,25 @@ instance : OpSignature (MOp φ) (MTy φ) where
 def Op.denote (o : Op) (arg : HVector Goedel.toType (OpSignature.sig o)) :
     (Goedel.toType <| OpSignature.outTy o) :=
   match o with
-  | Op.const w val => Option.some (BitVec.ofInt w val)
-  | Op.and _ => pairMapM (.&&&.) arg.toPair
-  | Op.or _ => pairMapM (.|||.) arg.toPair
-  | Op.xor _ => pairMapM (.^^^.) arg.toPair
-  | Op.shl _ => pairMapM (. <<< .) arg.toPair
-  | Op.lshr _ => pairMapM (. >>> .) arg.toPair
-  | Op.ashr _ => pairMapM (. >>>ₛ .) arg.toPair
-  | Op.sub _ => pairMapM (.-.) arg.toPair
-  | Op.add _ => pairMapM (.+.) arg.toPair
-  | Op.mul _ => pairMapM (.*.) arg.toPair
-  | Op.sdiv _ => pairBind BitVec.sdiv? arg.toPair
-  | Op.udiv _ => pairBind BitVec.udiv? arg.toPair
-  | Op.urem _ => pairBind BitVec.urem? arg.toPair
-  | Op.srem _ => pairBind BitVec.srem? arg.toPair
+  | Op.const _ val => const? val
+  | Op.and _ => pairBind and? arg.toPair
+  | Op.or _ => pairBind or? arg.toPair
+  | Op.xor _ => pairBind xor? arg.toPair
+  | Op.shl _ => pairBind shl? arg.toPair
+  | Op.lshr _ => pairBind lshr? arg.toPair
+  | Op.ashr _ => pairBind ashr? arg.toPair
+  | Op.sub _ => pairBind sub?  arg.toPair
+  | Op.add _ => pairBind add? arg.toPair
+  | Op.mul _ => pairBind mul? arg.toPair
+  | Op.sdiv _ => pairBind sdiv? arg.toPair
+  | Op.udiv _ => pairBind udiv? arg.toPair
+  | Op.urem _ => pairBind urem? arg.toPair
+  | Op.srem _ => pairBind srem? arg.toPair
   | Op.not _ => Option.map (~~~.) arg.toSingle
   | Op.copy _ => arg.toSingle
   | Op.neg _ => Option.map (-.) arg.toSingle
-  | Op.select _ => tripleMapM BitVec.select arg.toTriple
-  | Op.icmp c _ => match c with
-    | .eq => pairMapM (fun x y => ↑(x == y)) arg.toPair
-    | .ne => pairMapM (fun x y => ↑(x != y)) arg.toPair
-    | .sgt => pairMapM (. >ₛ .) arg.toPair
-    | .sge => pairMapM (. ≥ₛ .) arg.toPair
-    | .slt => pairMapM (. <ₛ .) arg.toPair
-    | .sle => pairMapM (. ≤ₛ .) arg.toPair
-    | .ugt => pairMapM (. >ᵤ .) arg.toPair
-    | .uge => pairMapM (. ≥ᵤ .) arg.toPair
-    | .ult => pairMapM (. <ᵤ .) arg.toPair
-    | .ule => pairMapM (. ≤ᵤ .) arg.toPair
+  | Op.select _ => tripleBind select? arg.toTriple
+  | Op.icmp c _ => pairBind (icmp? c) arg.toPair
 
 instance : OpDenote Op Ty := ⟨
   fun o args _ => Op.denote o args
diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index b1abcf6bb..7b3c9fb14 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -69,7 +69,7 @@ end Refinement
 infix:50 (priority:=low) " ⊑ " => Refinement
 instance : Coe Bool (BitVec 1) := ⟨ofBool⟩
 
-def BitVec.coeWidth {m n : Nat} : BitVec m → BitVec n
+def coeWidth {m n : Nat} : BitVec m → BitVec n
   | x => BitVec.ofNat n x.toNat
 
 -- not sure what the right `Coe`is for this case
diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index 2d77dd234..397831437 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -4,7 +4,7 @@ import SSA.Projects.InstCombine.ForStd
 
 open Std
 
-namespace Std.BitVec
+namespace LLVM
 
 /--
 The ‘and’ instruction returns the bitwise logical and of its two operands.
@@ -145,7 +145,7 @@ this instruction returns a poison value.
 
 Corresponds to `Std.BitVec.ushiftRight` in the `some` case.
 -/
-def lhr? {m n k} (op1 : BitVec n) (op2 : BitVec m) : Option (BitVec k) :=
+def lshr? {m n k} (op1 : BitVec n) (op2 : BitVec m) : Option (BitVec k) :=
   let bits := op2.toNat -- should this be toInt?
   if bits >= n then .none
   else .some <| BitVec.coeWidth (op1 >>> op2)
@@ -257,7 +257,7 @@ The possible condition codes are:
 
 The remaining two arguments must be integer. They must also be identical types.
 -/
-def icmp? {w : Nat} {c : IntPredicate} (x y : BitVec w) : Option (BitVec 1) :=
+def icmp? {w : Nat} (c : IntPredicate) (x y : BitVec w) : Option (BitVec 1) :=
   Option.some ↑(icmp c x y)
 
 /--
@@ -279,3 +279,5 @@ TODO: double-check that truncating works the same as MLIR (signedness, overflow,
 -/
 def const? (i : Int): Option (BitVec w) :=
   BitVec.ofInt w i
+
+end LLVM

From 3561b5c3297929738afd1be30df43616574218d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Tue, 7 Nov 2023 23:05:53 +0100
Subject: [PATCH 06/12] add missing import from moved code

---
 SSA/Projects/InstCombine/AliveStatements.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean
index e91b76549..362bc4186 100644
--- a/SSA/Projects/InstCombine/AliveStatements.lean
+++ b/SSA/Projects/InstCombine/AliveStatements.lean
@@ -2,9 +2,11 @@ import Std.Data.BitVec
 
 import SSA.Projects.InstCombine.TacticAuto
 import SSA.Projects.InstCombine.ForStd
+import SSA.Projects.InstCombine.LLVM.Semantics
 
 open Std
 open Std.BitVec
+open LLVM
 
 
 theorem bitvec_AddSub_1043 :

From bb022941531cde5de927e1a0bed157a15420bab1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Wed, 8 Nov 2023 08:23:57 +0100
Subject: [PATCH 07/12] Fixed copy-paste error in docstring, added some
 (incomplete) characterizations of sdiv?

---
 SSA/Projects/InstCombine/LLVM/Semantics.lean | 32 ++++++++++++++++++--
 1 file changed, 29 insertions(+), 3 deletions(-)

diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index 397831437..5d51ad9e8 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -66,7 +66,7 @@ Division by zero is undefined behavior.
 def udiv? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
   match y.toNat with
     | 0 => none
-    | _ => some $ BitVec.ofNat w (x.toNat / y.toNat)
+    | _ => some <| BitVec.ofInt w (x.toNat / y.toNat)
 
 /--
 The value produced is the signed integer quotient of the two operands rounded towards zero.
@@ -75,7 +75,7 @@ Division by zero is undefined behavior.
 Overflow also leads to undefined behavior; this is a rare case, but can occur, for example, by doing a 32-bit division of -2147483648 by -1.
 -/
 def sdiv? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
-  if y.toInt = 0
+  if y = 0
   then none
   else
     let div := (x.toInt / y.toInt)
@@ -83,6 +83,32 @@ def sdiv? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
       then some $ BitVec.ofInt w div
       else none
 
+def intMin (w : Nat) : BitVec w :=
+  BitVec.ofInt w <| 1 - ↑(2^(w-1))
+
+def intMax (w : Nat) : BitVec w :=
+  BitVec.ofInt w ↑(2^(w-1))
+
+theorem intMin_minus_one {w : Nat} : (intMin w - 1) = intMax w :=
+ --by simp [intMin, BitVec.toInt]
+ sorry
+
+
+-- Probably not a Mathlib worthy name,
+-- not sure how you'd mathlibify the precondition
+theorem sdiv?_eq_div_if {w : Nat} {x y : BitVec w} :
+  sdiv? x y =
+  if (y = 0) ∨ (x = -1 ∧ y = intMin w)
+    then none
+  else some <| BitVec.ofInt w (x.toInt / y.toInt)
+  := by
+  simp [sdiv?]
+  by_cases (y = 0)
+  · case pos h =>
+    simp [h]
+  · case neg h =>
+    sorry -- TODO: this is the interesting case
+
 /--
 This instruction returns the unsigned integer remainder of a division. This instruction always performs an unsigned division to get the remainder.
 Note that unsigned integer remainder and signed integer remainder are distinct operations; for signed integer remainder, use ‘srem’.
@@ -126,7 +152,7 @@ def sshr (a : BitVec n) (s : Nat) := BitVec.sshiftRight a s
 
 /--
 Shift left instruction.
-The value produced is op1 * 2op2 mod 2n, where n is the width of the result.
+The value produced is op1 * 2^op2 mod 2n, where n is the width of the result.
 If op2 is (statically or dynamically) equal to or larger than the number of
 bits in op1, this instruction returns a poison value.
 -/

From 5cace837453803e26f16de06552fafb6d7facc45 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Wed, 8 Nov 2023 12:38:08 +0100
Subject: [PATCH 08/12] Fix missing namespace changes in Transform

---
 SSA/Projects/InstCombine/LLVM/Transform.lean | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/SSA/Projects/InstCombine/LLVM/Transform.lean b/SSA/Projects/InstCombine/LLVM/Transform.lean
index ccf250131..9bad81a21 100644
--- a/SSA/Projects/InstCombine/LLVM/Transform.lean
+++ b/SSA/Projects/InstCombine/LLVM/Transform.lean
@@ -420,16 +420,16 @@ def mkExpr (Γ : Context φ) (opStx : Op φ) : ReaderM (Σ ty, Expr Γ ty) := do
       | "llvm.sub"    => pure (MOp.sub w₁)
       | "llvm.sdiv"   => pure (MOp.sdiv w₁)
       | "llvm.udiv"   => pure (MOp.udiv w₁)
-      | "llvm.icmp.eq" => pure (MOp.icmp InstCombine.IntPredicate.eq w₁)
-      | "llvm.icmp.ne" => pure (MOp.icmp InstCombine.IntPredicate.ne w₁)
-      | "llvm.icmp.ugt" => pure (MOp.icmp InstCombine.IntPredicate.ugt w₁)
-      | "llvm.icmp.uge" => pure (MOp.icmp InstCombine.IntPredicate.uge w₁)
-      | "llvm.icmp.ult" => pure (MOp.icmp InstCombine.IntPredicate.ult w₁)
-      | "llvm.icmp.ule" => pure (MOp.icmp InstCombine.IntPredicate.ule w₁)
-      | "llvm.icmp.sgt" => pure (MOp.icmp InstCombine.IntPredicate.sgt w₁)
-      | "llvm.icmp.sge" => pure (MOp.icmp InstCombine.IntPredicate.sge w₁)
-      | "llvm.icmp.slt" => pure (MOp.icmp InstCombine.IntPredicate.slt w₁)
-      | "llvm.icmp.sle" => pure (MOp.icmp InstCombine.IntPredicate.sle w₁)
+      | "llvm.icmp.eq" => pure (MOp.icmp LLVM.IntPredicate.eq w₁)
+      | "llvm.icmp.ne" => pure (MOp.icmp LLVM.IntPredicate.ne w₁)
+      | "llvm.icmp.ugt" => pure (MOp.icmp LLVM.IntPredicate.ugt w₁)
+      | "llvm.icmp.uge" => pure (MOp.icmp LLVM.IntPredicate.uge w₁)
+      | "llvm.icmp.ult" => pure (MOp.icmp LLVM.IntPredicate.ult w₁)
+      | "llvm.icmp.ule" => pure (MOp.icmp LLVM.IntPredicate.ule w₁)
+      | "llvm.icmp.sgt" => pure (MOp.icmp LLVM.IntPredicate.sgt w₁)
+      | "llvm.icmp.sge" => pure (MOp.icmp LLVM.IntPredicate.sge w₁)
+      | "llvm.icmp.slt" => pure (MOp.icmp LLVM.IntPredicate.slt w₁)
+      | "llvm.icmp.sle" => pure (MOp.icmp LLVM.IntPredicate.sle w₁)
       | opstr => throw <| .unsupportedOp s!"Unsuported binary operation or invalid arguments '{opstr}'"
     match op with
     | .icmp .. =>

From 7d9b44b8ce30350d45860a60f8a64b9201b5095e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Wed, 8 Nov 2023 12:55:16 +0100
Subject: [PATCH 09/12] Add new LLVM names to tactic, fix and and or being
 swapped

---
 SSA/Projects/InstCombine/LLVM/Semantics.lean | 5 ++---
 SSA/Projects/InstCombine/Tactic.lean         | 4 ++++
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index 5d51ad9e8..dd785318e 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -10,15 +10,14 @@ namespace LLVM
 The ‘and’ instruction returns the bitwise logical and of its two operands.
 -/
 def and? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
- .some <| x ||| y
-
+ .some <| x &&& y
 
 /--
 The ‘or’ instruction returns the bitwise logical inclusive or of its two
 operands.
 -/
 def or? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
- .some <| x &&& y
+ .some <| x ||| y
 
 /--
 The ‘xor’ instruction returns the bitwise logical exclusive or of its two
diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
index eada66502..53093456b 100644
--- a/SSA/Projects/InstCombine/Tactic.lean
+++ b/SSA/Projects/InstCombine/Tactic.lean
@@ -40,6 +40,10 @@ macro "simp_alive_peephole" : tactic =>
           bind, Option.bind, pure, DerivedContext.ofContext, DerivedContext.snoc,
           Ctxt.snoc, MOp.instantiateCom, InstCombine.MTy.instantiate,
           ConcreteOrMVar.instantiate, Vector.get, HVector.toSingle,
+          LLVM.and?, LLVM.or?, LLVM.xor?, LLVM.add?, LLVM.sub?,
+          LLVM.mul?, LLVM.udiv?, LLVM.sdiv?, LLVM.urem?, LLVM.srem?,
+          LLVM.sshr, LLVM.lshr?, LLVM.ashr?, LLVM.shl?, LLVM.select?,
+          LLVM.const?, LLVM.icmp?,
           HVector.toTuple, List.nthLe, bitvec_minus_one]
         try intros v0
         try intros v1

From 3706b294ced910e2dda74419f22149398f374452 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <a.goens@uva.nl>
Date: Wed, 8 Nov 2023 18:29:09 +0100
Subject: [PATCH 10/12] Update SSA/Projects/InstCombine/LLVM/Semantics.lean

Co-authored-by: Siddharth <siddu.druid@gmail.com>
---
 SSA/Projects/InstCombine/LLVM/Semantics.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index dd785318e..d357e8e48 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -140,7 +140,7 @@ of the division and the remainder.)
 -/
 def srem? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
   if y.toInt = 0
-  then none
+  then none -- Taking the remainder of a division by zero is undefined behavior.
   else
     let div := (x.toInt / y.toInt)
     if div < Int.ofNat (2^w)

From f93f5b18be620dcc46aa7bd8f22f16762494b735 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Thu, 9 Nov 2023 08:54:46 +0100
Subject: [PATCH 11/12] Add inbounds predicate

---
 SSA/Projects/InstCombine/LLVM/Semantics.lean | 25 ++++++++++++--------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index d357e8e48..dcf4dc1be 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -67,6 +67,16 @@ def udiv? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
     | 0 => none
     | _ => some <| BitVec.ofInt w (x.toNat / y.toNat)
 
+def intMin (w : Nat) : BitVec w :=
+  BitVec.ofInt w <| 1 - ↑(2^(w-1))
+
+def intMax (w : Nat) : BitVec w :=
+  BitVec.ofInt w ↑(2^(w-1))
+
+def ofIntInbounds (w : Nat) (v : Int) : Prop := v >= (intMin w).toInt && v < (intMax w).toInt
+
+instance : Decidable (ofIntInbounds w v) := inferInstanceAs (Decidable (v >= (intMin w).toInt && v < (intMax w).toInt))
+
 /--
 The value produced is the signed integer quotient of the two operands rounded towards zero.
 Note that signed integer division and unsigned integer division are distinct operations; for unsigned integer division, use ‘udiv’.
@@ -78,15 +88,10 @@ def sdiv? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
   then none
   else
     let div := (x.toInt / y.toInt)
-    if div < Int.ofNat (2^w)
-      then some $ BitVec.ofInt w div
+    if ofIntInbounds w div
+      then some <| BitVec.ofInt w div
       else none
 
-def intMin (w : Nat) : BitVec w :=
-  BitVec.ofInt w <| 1 - ↑(2^(w-1))
-
-def intMax (w : Nat) : BitVec w :=
-  BitVec.ofInt w ↑(2^(w-1))
 
 theorem intMin_minus_one {w : Nat} : (intMin w - 1) = intMax w :=
  --by simp [intMin, BitVec.toInt]
@@ -116,7 +121,7 @@ Taking the remainder of a division by zero is undefined behavior.
 def urem? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
   if y.toNat = 0
   then none
-  else some $ BitVec.ofNat w (x.toNat % y.toNat)
+  else some <| BitVec.ofNat w (x.toNat % y.toNat)
 
 def _root_.Int.rem (x y : Int) : Int :=
   if x ≥ 0 then (x % y) else ((x % y) - y.natAbs)
@@ -143,8 +148,8 @@ def srem? {w : Nat} (x y : BitVec w) : Option <| BitVec w :=
   then none -- Taking the remainder of a division by zero is undefined behavior.
   else
     let div := (x.toInt / y.toInt)
-    if div < Int.ofNat (2^w)
-      then some $ BitVec.ofInt w (x.toInt.rem y.toInt)
+    if ofIntInbounds w div
+      then some <| BitVec.ofInt w (x.toInt.rem y.toInt)
       else none
 
 def sshr (a : BitVec n) (s : Nat) := BitVec.sshiftRight a s

From 7ba3a63f259e3ec434e1c69dd55c909c33b80513 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <a.goens@uva.nl>
Date: Thu, 9 Nov 2023 11:08:39 +0100
Subject: [PATCH 12/12] Update SSA/Projects/InstCombine/LLVM/Semantics.lean

Co-authored-by: Siddharth <siddu.druid@gmail.com>
---
 SSA/Projects/InstCombine/LLVM/Semantics.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index dcf4dc1be..8b51a9121 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -71,7 +71,7 @@ def intMin (w : Nat) : BitVec w :=
   BitVec.ofInt w <| 1 - ↑(2^(w-1))
 
 def intMax (w : Nat) : BitVec w :=
-  BitVec.ofInt w ↑(2^(w-1))
+  BitVec.ofInt w ↑(2^(w-1) - 1)
 
 def ofIntInbounds (w : Nat) (v : Int) : Prop := v >= (intMin w).toInt && v < (intMax w).toInt