feat: support fixed integers and conditions in meta-simp-set (#346)

- add `ConcreteOrMVar.instantiate_ofNat_eq` to simplify instantiation
and canonicalize to ofNat.

Unfortunately, this seems to lead to a 'motive not type correct' error.
To resolve it we use simp! that just unfolds. This should be debugged
further: #349.

- generalize `toSnoc_toMap` to work on sequences of snoc

---------

Co-authored-by: Siddharth <[email protected]>

SSA/Core/ErasedContext.lean

@@ -143,7 +143,7 @@ def castCtxt {Γ : Ctxt Op} (h_eq : Γ = Δ) : Γ.Var ty → Δ.Var ty
 theorem toMap_last {Γ : Ctxt Ty} {t : Ty} : (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl
 
 @[simp]
-theorem toSnoc_toMap {Γ : Ctxt Ty} {t : Ty} {var : Ctxt.Var Γ t} {f : Ty → Ty₂} :
+theorem toSnoc_toMap {Γ : Ctxt Ty} {t : Ty} {var : Ctxt.Var Γ t'} {f : Ty → Ty₂} :
     var.toSnoc.toMap (Γ := Γ.snoc t) (f := f) = var.toMap.toSnoc := rfl
 
 /-- This is an induction principle that case splits on whether or not a variable

SSA/Core/Util/ConcreteOrMVar.lean

@@ -48,9 +48,14 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α
   | .concrete w => w
   | .mvar i => as.get i
 
+/-- We choose ConcreteOrMVar.concrete to be our simp normal form. -/
 @[simp]
-def instantiate_concrete_eq (as : Vector α φ) :
-  (ConcreteOrMVar.concrete w).instantiate as = w := by rfl
+def ofNat_eq_concrete (x : Nat) :
+    (OfNat.ofNat x) = (ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) := rfl
+
+@[simp]
+def instantiate_ofNat_eq (as : Vector Nat φ) (x : Nat) :
+   ConcreteOrMVar.instantiate as (OfNat.ofNat x) = x := rfl
 
 @[simp]
 lemma instantiate_mvar_zero {hφ : List.length (w :: ws) = φ} {h0 : 0 < φ} :

SSA/Projects/InstCombine/Tactic.lean

@@ -42,10 +42,12 @@ macro "simp_alive_meta" : tactic =>
       dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero]
       dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero']
       dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero'']
-      dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_concrete_eq]
       dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate]
       dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMTy]
       dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_mvar_zero'']
+      -- How can I avoid this `simp! only` and instead use a plain `simp only`?
+      dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.ofNat_eq_concrete]
+      simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_ofNat_eq]
    )
  )
 

SSA/Projects/InstCombine/Test.lean

@@ -386,3 +386,172 @@ def three_inst_macro_noreduc_proof (w : Nat) :
   simp_alive_meta
   simp_alive_ssa
   apply three_inst_stmt
+
+def one_inst_concrete_macro :=
+  [alive_icom ()|{
+  ^bb0(%arg0: i1):
+    %0 = "llvm.not" (%arg0) : (i1) -> (i1)
+    "llvm.return" (%0) : (i1) -> ()
+  }]
+
+set_option ssa.alive_icom_reduce false in
+def one_inst_concrete_macro_noreduce :=
+  [alive_icom ()|{
+  ^bb0(%arg0: i1):
+    %0 = "llvm.not" (%arg0) : (i1) -> (i1)
+    "llvm.return" (%0) : (i1) -> ()
+  }]
+
+def one_inst_concrete_com :
+    Com InstCombine.LLVM [InstCombine.Ty.bitvec 1] .pure (InstCombine.Ty.bitvec 1) :=
+  Com.lete (not 1 0) <|
+  Com.ret ⟨0, by simp [Ctxt.snoc]⟩
+
+def one_inst_concrete_stmt :
+    @BitVec.Refinement (BitVec 1) (LLVM.not e) (LLVM.not e) := by
+  simp
+
+def one_inst_concrete_com_proof :
+    one_inst_concrete_com ⊑ one_inst_concrete_com := by
+  unfold one_inst_concrete_com
+  simp only [simp_llvm_wrap]
+  simp_alive_meta
+  simp_alive_ssa
+  apply one_inst_concrete_stmt
+
+def one_inst_concrete_macro_proof :
+    one_inst_concrete_macro ⊑ one_inst_concrete_macro := by
+  unfold one_inst_concrete_macro
+  simp_alive_meta
+  simp_alive_ssa
+  apply one_inst_concrete_stmt
+
+def one_inst_concrete_macro_proof_noreduce :
+    one_inst_concrete_macro_noreduce ⊑ one_inst_concrete_macro_noreduce := by
+  unfold one_inst_concrete_macro_noreduce
+  simp_alive_meta
+  simp_alive_ssa
+  apply one_inst_concrete_stmt
+
+def two_inst_concrete_macro :=
+  [alive_icom ()|{
+  ^bb0(%arg0: i1):
+    %0 = "llvm.not" (%arg0) : (i1) -> (i1)
+    %1 = "llvm.not" (%arg0) : (i1) -> (i1)
+    "llvm.return" (%0) : (i1) -> ()
+  }]
+
+set_option ssa.alive_icom_reduce false in
+def two_inst_concrete_macro_noreduce :=
+  [alive_icom ()|{
+  ^bb0(%arg0: i1):
+    %0 = "llvm.not" (%arg0) : (i1) -> (i1)
+    %1 = "llvm.not" (%arg0) : (i1) -> (i1)
+    "llvm.return" (%0) : (i1) -> ()
+  }]
+
+def two_inst_concrete_com (w : ℕ) :
+  Com InstCombine.LLVM [InstCombine.Ty.bitvec w] .pure (InstCombine.Ty.bitvec w) :=
+  Com.lete (not w 0) <|
+  Com.lete (not w 1) <|
+  Com.ret ⟨1, by simp [Ctxt.snoc]⟩
+
+def two_inst_concrete_stmt (e : LLVM.IntW w) :
+    @BitVec.Refinement (BitVec w) (LLVM.not e) (LLVM.not e) := by
+  simp
+
+def two_inst_concrete_com_proof :
+    two_inst_concrete_com w ⊑ two_inst_concrete_com w := by
+  unfold two_inst_concrete_com
+  simp only [simp_llvm_wrap]
+  simp_alive_meta
+  simp_alive_ssa
+  apply two_inst_concrete_stmt
+
+def two_inst_concrete_macro_proof :
+    two_inst_concrete_macro ⊑ two_inst_concrete_macro := by
+  unfold two_inst_concrete_macro
+  simp_alive_meta
+  simp_alive_ssa
+  apply two_inst_concrete_stmt
+
+def two_inst_concrete_macro_noreduc_proof :
+    two_inst_concrete_macro_noreduce ⊑ two_inst_concrete_macro_noreduce := by
+  unfold two_inst_concrete_macro_noreduce
+  simp_alive_meta
+  simp_alive_ssa
+  apply two_inst_concrete_stmt
+
+def three_inst_concrete_macro :=
+  [alive_icom ()|{
+  ^bb0(%arg0: i1):
+    %0 = "llvm.not" (%arg0) : (i1) -> (i1)
+    %1 = "llvm.not" (%0) : (i1) -> (i1)
+    %2 = "llvm.not" (%1) : (i1) -> (i1)
+    "llvm.return" (%2) : (i1) -> ()
+  }]
+
+set_option ssa.alive_icom_reduce false in
+def three_inst_concrete_macro_noreduce :=
+  [alive_icom ()|{
+  ^bb0(%arg0: i1):
+    %0 = "llvm.not" (%arg0) : (i1) -> (i1)
+    %1 = "llvm.not" (%0) : (i1) -> (i1)
+    %2 = "llvm.not" (%1) : (i1) -> (i1)
+    "llvm.return" (%2) : (i1) -> ()
+  }]
+
+def three_inst_concrete_com :
+  Com InstCombine.LLVM [InstCombine.Ty.bitvec 1] .pure (InstCombine.Ty.bitvec 1) :=
+  Com.lete (not 1 0) <|
+  Com.lete (not 1 0) <|
+  Com.lete (not 1 0) <|
+  Com.ret ⟨0, by simp [Ctxt.snoc]⟩
+
+def three_inst_concrete_stmt (e : LLVM.IntW 1) :
+    @BitVec.Refinement (BitVec 1) (LLVM.not (LLVM.not (LLVM.not e)))
+      (LLVM.not (LLVM.not (LLVM.not e))) := by
+  simp
+
+def three_inst_concrete_com_proof :
+    three_inst_concrete_com ⊑ three_inst_concrete_com := by
+  unfold three_inst_concrete_com
+  simp only [simp_llvm_wrap]
+  simp_alive_meta
+  simp_alive_ssa
+  apply three_inst_concrete_stmt
+
+def three_inst_concrete_macro_proof :
+    three_inst_concrete_macro ⊑ three_inst_concrete_macro := by
+  unfold three_inst_concrete_macro
+  simp_alive_meta
+  simp_alive_ssa
+  apply three_inst_concrete_stmt
+
+def three_inst_concrete_macro_noreduc_proof :
+    three_inst_concrete_macro_noreduce ⊑ three_inst_concrete_macro_noreduce := by
+  unfold three_inst_concrete_macro_noreduce
+  simp_alive_meta
+  simp_alive_ssa
+  apply three_inst_concrete_stmt
+
+set_option ssa.alive_icom_reduce false in
+def two_ne_macro_noreduce (w : Nat) :=
+  [alive_icom (w)|{
+  ^bb0(%arg0: _, %arg1: _):
+    %0 = "llvm.icmp.ne" (%arg0, %arg1) : (_, _) -> (i1)
+    %1 = "llvm.icmp.ne" (%arg0, %arg1) : (_, _) -> (i1)
+    "llvm.return" (%1) : (i1) -> ()
+  }]
+
+def two_ne_stmt (a b : LLVM.IntW w) :
+    @BitVec.Refinement (BitVec 1) (LLVM.icmp LLVM.IntPredicate.ne b a)
+      (LLVM.icmp LLVM.IntPredicate.ne b a) := by
+  simp
+
+def two_ne_macro_noreduc_proof (w : Nat) :
+    two_ne_macro_noreduce w ⊑ two_ne_macro_noreduce w := by
+  unfold two_ne_macro_noreduce
+  simp_alive_meta
+  simp_alive_ssa
+  apply two_ne_stmt