From efac4d7ad48716e345b2e52d48fc8b345333f4d7 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Mon, 29 Apr 2024 21:48:34 +0100
Subject: [PATCH] feat: upstream a handwritten proof for alive -
 alive_DivRemOfSelectLarge proofs one (#262)

* feat: upstream a handwritten proof for alive - alive_DivRemOfSelect

This proof is factored out of https://github.com/opencompl/ssa/pull/167
and is part of collection of proofs that we manually wrote to demonstrate
the status of leans automation in BitVectors and such.

* chore: golf

* chore: golf more --- intro; rcases -> rintro.

* chore: simp [simp_llvm] -> simp only [simp_llvm]

---------

Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>
---
 SSA/Projects/InstCombine/Alive.lean           |  1 +
 .../AliveHandwrittenLargeExamples.lean        | 53 +++++++++++++++++++
 2 files changed, 54 insertions(+)
 create mode 100644 SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean

diff --git a/SSA/Projects/InstCombine/Alive.lean b/SSA/Projects/InstCombine/Alive.lean
index 651b4d4c5..9d8dec04f 100644
--- a/SSA/Projects/InstCombine/Alive.lean
+++ b/SSA/Projects/InstCombine/Alive.lean
@@ -10,6 +10,7 @@ import SSA.Projects.InstCombine.AliveStatements
 -- This has those examples from alive that failed to be
 -- translated correctly due to bugs in the translator.
 import SSA.Projects.InstCombine.AliveHandwrittenExamples
+import SSA.Projects.InstCombine.AliveHandwrittenLargeExamples
 
 -- The semantics for the MLIR base dialect
 import SSA.Projects.InstCombine.Base
diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
new file mode 100644
index 000000000..871575c22
--- /dev/null
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -0,0 +1,53 @@
+import SSA.Projects.InstCombine.LLVM.EDSL
+import SSA.Projects.InstCombine.Tactic
+
+open BitVec
+open MLIR AST
+
+namespace AliveHandwritten
+
+namespace DivRemOfSelect
+
+/--
+Name: SimplifyDivRemOfSelect
+precondition: true
+%sel = select %c, %Y, 0
+%r = udiv %X, %sel
+  =>
+%r = udiv %X, %Y
+-/
+def alive_DivRemOfSelect_src (w : Nat) :=
+  [alive_icom (w)| {
+  ^bb0(%c: i1, %y : _, %x : _):
+    %c0 = "llvm.mlir.constant" () { value = 0 : _ } :() -> (_)
+    %v1 = "llvm.select" (%c,%y, %c0) : (i1, _, _) -> (_)
+    %v2 = "llvm.udiv"(%x, %v1) : (_, _) -> (_)
+    "llvm.return" (%v2) : (_) -> ()
+  }]
+
+def alive_DivRemOfSelect_tgt (w : Nat) :=
+  [alive_icom (w)| {
+  ^bb0(%c: i1, %y : _, %x : _):
+    %v1 = "llvm.udiv" (%x,%y) : (_, _) -> (_)
+    "llvm.return" (%v1) : (_) -> ()
+  }]
+
+theorem alive_DivRemOfSelect (w : Nat) :
+    alive_DivRemOfSelect_src w ⊑ alive_DivRemOfSelect_tgt w := by
+  unfold alive_DivRemOfSelect_src alive_DivRemOfSelect_tgt
+  simp_alive_ssa
+  simp_alive_undef
+  simp only [simp_llvm]
+  rintro y (rfl | ⟨vcond, hcond⟩) x
+  -- | select condition is itself `none`, nothing more to be done. propagate the `none`.
+  · cases x <;> cases y <;> simp
+  · simp at hcond
+    (obtain (rfl | rfl) : vcond = 1 ∨ vcond = 0 := by omega) <;> simp
+
+/--info: 'AliveHandwritten.DivRemOfSelect.alive_DivRemOfSelect' depends on
+axioms: [propext, Classical.choice, Quot.sound] -/
+#guard_msgs in #print axioms alive_DivRemOfSelect
+
+end DivRemOfSelect
+
+end AliveHandwritten