From 37f9bf44900a931c52d10442f03d73cef7e819ff Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 12:56:19 +0100 Subject: [PATCH 01/43] feat: support short test case without a need for reduction --- SSA/Projects/InstCombine/Test.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index c11a8a1af..be70caab5 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -246,6 +246,14 @@ def one_inst_macro (w: Nat):= "llvm.return" (%0) : (_) -> () }] +set_option ssa.alive_icom_reduce false in +def one_inst_macro_noreduce (w: Nat):= + [alive_icom (w)|{ + ^bb0(%arg0: _): + %0 = "llvm.not" (%arg0) : (_, _) -> (_) + "llvm.return" (%0) : (_) -> () + }] + def one_inst_com (w : ℕ) : Com InstCombine.LLVM [InstCombine.Ty.bitvec w] .pure (InstCombine.Ty.bitvec w) := Com.lete (not w 0) <| @@ -269,6 +277,13 @@ def one_inst_macro_proof (w : Nat) : simp_alive_ssa apply one_inst_stmt +def one_inst_macro_proof_noreduce (w : Nat) : + one_inst_macro_noreduce w ⊑ one_inst_macro_noreduce w := by + unfold one_inst_macro_noreduce + simp_alive_meta + simp_alive_ssa + apply one_inst_stmt + def two_inst_macro (w: Nat):= [alive_icom (w)|{ ^bb0(%arg0: _): From 65675ca383007b23396e5bc028996a6c14f4738d Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 12:57:39 +0100 Subject: [PATCH 02/43] feat: add lemmas --- SSA/Core/Framework.lean | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean index ab095c395..57632a5e3 100644 --- a/SSA/Core/Framework.lean +++ b/SSA/Core/Framework.lean @@ -1327,6 +1327,12 @@ theorem DialectMorphism.preserves_effectKind (op : d.Op) : DialectSignature.effectKind (f.mapOp op) = DialectSignature.effectKind op := by simp only [DialectSignature.effectKind, Function.comp_apply, f.preserves_signature]; rfl +@[simp] lemma DialectMorphism.mapOp_mk (fOp : d.Op → d'.Op) (fTy) (h) : + mapOp ⟨fOp, fTy, h⟩ = fOp := rfl + +@[simp] lemma DialectMorphism.mapTy_mk (fOp : d.Op → d'.Op) (fTy) (h) : + mapTy ⟨fOp, fTy, h⟩ = fTy := rfl + mutual -- TODO: `map` is ambiguous, rename it to `changeDialect` (to mirror `changeVars`) @@ -1357,6 +1363,41 @@ def Lets.changeDialect : Lets d Γ_in eff Γ_out → Lets d' (f.mapTy <$> Γ_in) | nil => nil | lete body e => lete (changeDialect body) (e.changeDialect f) +section Lemmas + +/-! +There seems to be a bug with the `rfl` suggestion. When it fails, tt says: +``` +Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`. +``` +But `Eq.rfl` does not exist, it should be `exact Eq.refl _` +-/ + +@[simp] lemma Com.changeDialect_ret (f : DialectMorphism d d') (v : Var Γ t): + Com.changeDialect f (Com.ret v : Com d Γ eff t) = Com.ret v.toMap := by + cases eff <;> rfl + +@[simp] lemma Com.changeDialect_lete (f : DialectMorphism d d') + (e : Expr d Γ eff t) (body : Com d _ eff u) : + Com.changeDialect f (Com.lete e body) + = Com.lete (e.changeDialect f) (body.changeDialect f) := by + simp only [List.map_eq_map, changeDialect] + +@[simp] lemma Expr.changeDialect_mk (f : DialectMorphism d d') (op ty_eq eff_le args regArgs) : + Expr.changeDialect f (⟨op, ty_eq, eff_le, args, regArgs⟩ : Expr d Γ eff t) + = ⟨f.mapOp op, + ty_eq ▸ (f.preserves_outTy _).symm, + f.preserves_effectKind _ ▸ eff_le, + f.preserves_sig _ ▸ args.map' f.mapTy fun _ => Var.toMap (f:=f.mapTy), + f.preserves_regSig _ ▸ + HVector.changeDialect f regArgs⟩ := by + subst ty_eq; simp [Expr.changeDialect] + +@[simp] lemma HVector.changeDialect_nil (f : DialectMorphism d d') : + HVector.changeDialect (eff := eff) f nil = nil := rfl + +end Lemmas + end Map /-! From 3a2c10d00991d12865914fd59945ba545e3f0ad9 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 13:25:23 +0100 Subject: [PATCH 03/43] Make one_inst_macro_proof_noreduce work --- SSA/Projects/InstCombine/Test.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index be70caab5..cec8e3a7c 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -277,9 +277,19 @@ def one_inst_macro_proof (w : Nat) : simp_alive_ssa apply one_inst_stmt +set_option pp.proofs true in def one_inst_macro_proof_noreduce (w : Nat) : one_inst_macro_noreduce w ⊑ one_inst_macro_noreduce w := by unfold one_inst_macro_noreduce + simp only [Com.changeDialect_ret, Com.changeDialect_lete] + simp only [Com.changeDialect_ret, Com.changeDialect_lete, Expr.changeDialect, + (HVector.changeDialect_nil), InstcombineTransformDialect.MOp.instantiateCom] + dsimp! [] + dsimp only [DialectMorphism.mapOp_mk, DialectMorphism.mapTy_mk, + InstcombineTransformDialect.MOp.instantiateCom, + InstcombineTransformDialect.instantiateMOp, + InstcombineTransformDialect.instantiateMTy, + HVector.changeDialect_nil, HVector.map'] simp_alive_meta simp_alive_ssa apply one_inst_stmt From a70f2d776cc549b5abd8f8dc362285d1dedfd140 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 17:23:03 +0100 Subject: [PATCH 04/43] Make this end deterministically --- SSA/Projects/InstCombine/Test.lean | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index cec8e3a7c..e8201d633 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -277,6 +277,25 @@ def one_inst_macro_proof (w : Nat) : simp_alive_ssa apply one_inst_stmt +def aa : (instantiateMOp ⟨[w], one_inst_macro_noreduce.proof_1 w⟩ (MOp.unary (Width.mvar (0 : Fin (0 + 1))) MOp.UnaryOp.not)) = + (Op.unary w MOp.UnaryOp.not) := rfl + +def castA : +(@Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)] + (MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)) Ty + (instantiateMTy ⟨[w], one_inst_macro_noreduce.proof_1 w⟩) + (Ctxt.Var.last ∅ (MTy.bitvec (ConcreteOrMVar.mvar ⟨0, _⟩))) : (Ctxt.map (instantiateMTy ⟨[w], one_inst_macro_noreduce.proof_1 w⟩) + [MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)]).Var + (instantiateMTy ⟨[w], one_inst_macro_noreduce.proof_1 w⟩ + (MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)))) = + (Ctxt.Var.last [] (Ty.bitvec w)) := rfl + +def srf : (@Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] + _ Ty (instantiateMTy ⟨[w], one_inst_macro_noreduce.proof_1 w⟩) + (Ctxt.Var.last (MTy.bitvec (ConcreteOrMVar.mvar 0) :: ∅) (MTy.bitvec (ConcreteOrMVar.mvar 0)))) + = Ctxt.Var.last [Ty.bitvec w] (Ty.bitvec w) := rfl + + set_option pp.proofs true in def one_inst_macro_proof_noreduce (w : Nat) : one_inst_macro_noreduce w ⊑ one_inst_macro_noreduce w := by @@ -284,13 +303,14 @@ def one_inst_macro_proof_noreduce (w : Nat) : simp only [Com.changeDialect_ret, Com.changeDialect_lete] simp only [Com.changeDialect_ret, Com.changeDialect_lete, Expr.changeDialect, (HVector.changeDialect_nil), InstcombineTransformDialect.MOp.instantiateCom] - dsimp! [] dsimp only [DialectMorphism.mapOp_mk, DialectMorphism.mapTy_mk, InstcombineTransformDialect.MOp.instantiateCom, InstcombineTransformDialect.instantiateMOp, InstcombineTransformDialect.instantiateMTy, HVector.changeDialect_nil, HVector.map'] simp_alive_meta + dsimp [castA] + rw [srf] simp_alive_ssa apply one_inst_stmt From efaa15338f30e836804fe8bcf8839fa9737b2f91 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 21:52:44 +0100 Subject: [PATCH 05/43] generalize theorem thanks to Siddharth --- SSA/Projects/InstCombine/Test.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index e8201d633..5a98f11fb 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -290,11 +290,8 @@ def castA : (MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)))) = (Ctxt.Var.last [] (Ty.bitvec w)) := rfl -def srf : (@Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] - _ Ty (instantiateMTy ⟨[w], one_inst_macro_noreduce.proof_1 w⟩) - (Ctxt.Var.last (MTy.bitvec (ConcreteOrMVar.mvar 0) :: ∅) (MTy.bitvec (ConcreteOrMVar.mvar 0)))) - = Ctxt.Var.last [Ty.bitvec w] (Ty.bitvec w) := rfl - +@[simp] +theorem Ctxt.Var.toMap_last {Γ : Ctxt Ty2} {t : Ty2} : (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl set_option pp.proofs true in def one_inst_macro_proof_noreduce (w : Nat) : @@ -309,8 +306,8 @@ def one_inst_macro_proof_noreduce (w : Nat) : InstcombineTransformDialect.instantiateMTy, HVector.changeDialect_nil, HVector.map'] simp_alive_meta - dsimp [castA] - rw [srf] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] + simp_alive_meta simp_alive_ssa apply one_inst_stmt From 24344e4b60f1baf09021e02ce91be06ec18e2d2f Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 21:55:48 +0100 Subject: [PATCH 06/43] Add prefix --- SSA/Projects/InstCombine/Tactic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 86196e381..74c686bc3 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -22,8 +22,8 @@ macro "simp_alive_meta" : tactic => ( dsimp (config := {failIfUnchanged := false }) only [Functor.map] dsimp (config := {failIfUnchanged := false }) only [Ctxt.DerivedCtxt.snoc_ctxt_eq_ctxt_snoc] - dsimp (config := {failIfUnchanged := false }) only [Var.succ_eq_toSnoc] - dsimp (config := {failIfUnchanged := false }) only [Var.zero_eq_last] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.succ_eq_toSnoc] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.zero_eq_last] dsimp (config := {failIfUnchanged := false }) only [List.map] dsimp (config := {failIfUnchanged := false }) only [Width.mvar] dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_snoc, Ctxt.map_nil] From 9c8f4c04082eb8db6accbaac8351636cb9f95dbc Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 22:17:13 +0100 Subject: [PATCH 07/43] clean proof --- SSA/Core/ErasedContext.lean | 3 +++ SSA/Projects/InstCombine/Tactic.lean | 4 +++- SSA/Projects/InstCombine/Test.lean | 13 ------------- 3 files changed, 6 insertions(+), 14 deletions(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index cdc426054..1de4d2f97 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -140,6 +140,9 @@ def castCtxt {Γ : Ctxt Op} (h_eq : Γ = Δ) : Γ.Var ty → Δ.Var ty @[simp] lemma castCtxt_castCtxt (v : Var Γ t) (h₁ : Γ = Δ) (h₂ : Δ = Ξ) : (v.castCtxt h₁).castCtxt h₂ = v.castCtxt (by simp [*]) := by subst h₁ h₂; simp +@[simp] +theorem toMap_last {Γ : Ctxt Ty2} {t : Ty2} : (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl + /-- This is an induction principle that case splits on whether or not a variable is the last variable in a context. -/ @[elab_as_elim, cases_eliminator] diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 74c686bc3..94e9c5a7c 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -20,10 +20,12 @@ and all `Width.mvar` should be resolved into `Width.concrete`. -/ macro "simp_alive_meta" : tactic => `(tactic| ( + simp (config := {failIfUnchanged := false }) only [Com.changeDialect_ret, Com.changeDialect_lete, Expr.changeDialect] dsimp (config := {failIfUnchanged := false }) only [Functor.map] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.DerivedCtxt.snoc_ctxt_eq_ctxt_snoc] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.succ_eq_toSnoc] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.zero_eq_last] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.DerivedCtxt.snoc_ctxt_eq_ctxt_snoc] dsimp (config := {failIfUnchanged := false }) only [List.map] dsimp (config := {failIfUnchanged := false }) only [Width.mvar] dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_snoc, Ctxt.map_nil] diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 5a98f11fb..7adf7b1f5 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -290,23 +290,10 @@ def castA : (MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)))) = (Ctxt.Var.last [] (Ty.bitvec w)) := rfl -@[simp] -theorem Ctxt.Var.toMap_last {Γ : Ctxt Ty2} {t : Ty2} : (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl - set_option pp.proofs true in def one_inst_macro_proof_noreduce (w : Nat) : one_inst_macro_noreduce w ⊑ one_inst_macro_noreduce w := by unfold one_inst_macro_noreduce - simp only [Com.changeDialect_ret, Com.changeDialect_lete] - simp only [Com.changeDialect_ret, Com.changeDialect_lete, Expr.changeDialect, - (HVector.changeDialect_nil), InstcombineTransformDialect.MOp.instantiateCom] - dsimp only [DialectMorphism.mapOp_mk, DialectMorphism.mapTy_mk, - InstcombineTransformDialect.MOp.instantiateCom, - InstcombineTransformDialect.instantiateMOp, - InstcombineTransformDialect.instantiateMTy, - HVector.changeDialect_nil, HVector.map'] - simp_alive_meta - dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] simp_alive_meta simp_alive_ssa apply one_inst_stmt From a6b727e83e7b7f5d506fb8498544bc15f068da40 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 22:17:58 +0100 Subject: [PATCH 08/43] Clean up noise --- SSA/Projects/InstCombine/Test.lean | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 7adf7b1f5..3645c9549 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -277,19 +277,6 @@ def one_inst_macro_proof (w : Nat) : simp_alive_ssa apply one_inst_stmt -def aa : (instantiateMOp ⟨[w], one_inst_macro_noreduce.proof_1 w⟩ (MOp.unary (Width.mvar (0 : Fin (0 + 1))) MOp.UnaryOp.not)) = - (Op.unary w MOp.UnaryOp.not) := rfl - -def castA : -(@Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)] - (MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)) Ty - (instantiateMTy ⟨[w], one_inst_macro_noreduce.proof_1 w⟩) - (Ctxt.Var.last ∅ (MTy.bitvec (ConcreteOrMVar.mvar ⟨0, _⟩))) : (Ctxt.map (instantiateMTy ⟨[w], one_inst_macro_noreduce.proof_1 w⟩) - [MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)]).Var - (instantiateMTy ⟨[w], one_inst_macro_noreduce.proof_1 w⟩ - (MTy.bitvec (ConcreteOrMVar.mvar ⟨0, one_inst_macro_noreduce.proof_2⟩)))) = - (Ctxt.Var.last [] (Ty.bitvec w)) := rfl - set_option pp.proofs true in def one_inst_macro_proof_noreduce (w : Nat) : one_inst_macro_noreduce w ⊑ one_inst_macro_noreduce w := by From 970f6f2897a83d103dcc362f78828b2602675190 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 22:19:26 +0100 Subject: [PATCH 09/43] chore: do not pp proofs --- SSA/Projects/InstCombine/Test.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 3645c9549..be70caab5 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -277,7 +277,6 @@ def one_inst_macro_proof (w : Nat) : simp_alive_ssa apply one_inst_stmt -set_option pp.proofs true in def one_inst_macro_proof_noreduce (w : Nat) : one_inst_macro_noreduce w ⊑ one_inst_macro_noreduce w := by unfold one_inst_macro_noreduce From 5b1ff484a99eecfdcce83feea3285b682d654ddd Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 22:26:58 +0100 Subject: [PATCH 10/43] chore: use full context in simp_alive_meta This is helpful for debugging, when we copy the individual statements to the actual proof, which may not have Ctxt open. --- SSA/Projects/InstCombine/Tactic.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 86196e381..a9c223fdb 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -12,7 +12,6 @@ import Batteries.Data.BitVec import Mathlib.Data.BitVec.Lemmas open MLIR AST -open Ctxt /-- We eliminate our alive framework's metavarible machinery. At the end of this pass, all `InstcombineTransformDialect.instantiate*` must be eliminated, @@ -22,8 +21,8 @@ macro "simp_alive_meta" : tactic => ( dsimp (config := {failIfUnchanged := false }) only [Functor.map] dsimp (config := {failIfUnchanged := false }) only [Ctxt.DerivedCtxt.snoc_ctxt_eq_ctxt_snoc] - dsimp (config := {failIfUnchanged := false }) only [Var.succ_eq_toSnoc] - dsimp (config := {failIfUnchanged := false }) only [Var.zero_eq_last] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.succ_eq_toSnoc] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.zero_eq_last] dsimp (config := {failIfUnchanged := false }) only [List.map] dsimp (config := {failIfUnchanged := false }) only [Width.mvar] dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_snoc, Ctxt.map_nil] From 00394fdbabc41ced1d2ea7c91b8c91c2baf1137f Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 22:49:52 +0100 Subject: [PATCH 11/43] chore: drop unused things --- SSA/Core/Framework.lean | 27 --------------------------- 1 file changed, 27 deletions(-) diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean index 57632a5e3..c5617355e 100644 --- a/SSA/Core/Framework.lean +++ b/SSA/Core/Framework.lean @@ -1327,12 +1327,6 @@ theorem DialectMorphism.preserves_effectKind (op : d.Op) : DialectSignature.effectKind (f.mapOp op) = DialectSignature.effectKind op := by simp only [DialectSignature.effectKind, Function.comp_apply, f.preserves_signature]; rfl -@[simp] lemma DialectMorphism.mapOp_mk (fOp : d.Op → d'.Op) (fTy) (h) : - mapOp ⟨fOp, fTy, h⟩ = fOp := rfl - -@[simp] lemma DialectMorphism.mapTy_mk (fOp : d.Op → d'.Op) (fTy) (h) : - mapTy ⟨fOp, fTy, h⟩ = fTy := rfl - mutual -- TODO: `map` is ambiguous, rename it to `changeDialect` (to mirror `changeVars`) @@ -1365,14 +1359,6 @@ def Lets.changeDialect : Lets d Γ_in eff Γ_out → Lets d' (f.mapTy <$> Γ_in) section Lemmas -/-! -There seems to be a bug with the `rfl` suggestion. When it fails, tt says: -``` -Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`. -``` -But `Eq.rfl` does not exist, it should be `exact Eq.refl _` --/ - @[simp] lemma Com.changeDialect_ret (f : DialectMorphism d d') (v : Var Γ t): Com.changeDialect f (Com.ret v : Com d Γ eff t) = Com.ret v.toMap := by cases eff <;> rfl @@ -1383,19 +1369,6 @@ But `Eq.rfl` does not exist, it should be `exact Eq.refl _` = Com.lete (e.changeDialect f) (body.changeDialect f) := by simp only [List.map_eq_map, changeDialect] -@[simp] lemma Expr.changeDialect_mk (f : DialectMorphism d d') (op ty_eq eff_le args regArgs) : - Expr.changeDialect f (⟨op, ty_eq, eff_le, args, regArgs⟩ : Expr d Γ eff t) - = ⟨f.mapOp op, - ty_eq ▸ (f.preserves_outTy _).symm, - f.preserves_effectKind _ ▸ eff_le, - f.preserves_sig _ ▸ args.map' f.mapTy fun _ => Var.toMap (f:=f.mapTy), - f.preserves_regSig _ ▸ - HVector.changeDialect f regArgs⟩ := by - subst ty_eq; simp [Expr.changeDialect] - -@[simp] lemma HVector.changeDialect_nil (f : DialectMorphism d d') : - HVector.changeDialect (eff := eff) f nil = nil := rfl - end Lemmas end Map From 56b396e78aaa75a8371e268b8d5f61c562e04543 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 23:08:21 +0100 Subject: [PATCH 12/43] Update SSA/Core/Framework.lean Co-authored-by: Siddharth --- SSA/Core/Framework.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean index c5617355e..1f1cfa059 100644 --- a/SSA/Core/Framework.lean +++ b/SSA/Core/Framework.lean @@ -1359,7 +1359,7 @@ def Lets.changeDialect : Lets d Γ_in eff Γ_out → Lets d' (f.mapTy <$> Γ_in) section Lemmas -@[simp] lemma Com.changeDialect_ret (f : DialectMorphism d d') (v : Var Γ t): +@[simp] lemma Com.changeDialect_ret (f : DialectMorphism d d') (v : Var Γ t) : Com.changeDialect f (Com.ret v : Com d Γ eff t) = Com.ret v.toMap := by cases eff <;> rfl From 6d80b2e86c999486201c8bc1b04cb485b9c1d478 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 23:08:37 +0100 Subject: [PATCH 13/43] Update SSA/Core/Framework.lean Co-authored-by: Siddharth --- SSA/Core/Framework.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean index 1f1cfa059..b7d2c0bb1 100644 --- a/SSA/Core/Framework.lean +++ b/SSA/Core/Framework.lean @@ -1365,8 +1365,7 @@ section Lemmas @[simp] lemma Com.changeDialect_lete (f : DialectMorphism d d') (e : Expr d Γ eff t) (body : Com d _ eff u) : - Com.changeDialect f (Com.lete e body) - = Com.lete (e.changeDialect f) (body.changeDialect f) := by + (Com.lete e body).changeDialect f = Com.lete (e.changeDialect f) (body.changeDialect f) := by simp only [List.map_eq_map, changeDialect] end Lemmas From 140a063a0a31e024b01a0f859b7db97703dfcdfd Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 May 2024 23:11:15 +0100 Subject: [PATCH 14/43] Fix notation --- SSA/Core/ErasedContext.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index 1de4d2f97..9942c4274 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -141,7 +141,7 @@ def castCtxt {Γ : Ctxt Op} (h_eq : Γ = Δ) : Γ.Var ty → Δ.Var ty (v.castCtxt h₁).castCtxt h₂ = v.castCtxt (by simp [*]) := by subst h₁ h₂; simp @[simp] -theorem toMap_last {Γ : Ctxt Ty2} {t : Ty2} : (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl +theorem toMap_last {Γ : Ctxt Ty} {t : Ty} : (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl /-- This is an induction principle that case splits on whether or not a variable is the last variable in a context. -/ From cc9f5877c9dbb4b0a23851b15294b87c5d2666bf Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 07:34:15 +0100 Subject: [PATCH 15/43] feat: support equality-based rewriting for equation two operations --- SSA/Core/Framework.lean | 3 +++ SSA/Projects/InstCombine/Test.lean | 20 ++++++++++++++++++++ 2 files changed, 23 insertions(+) diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean index b7d2c0bb1..0ca131e99 100644 --- a/SSA/Core/Framework.lean +++ b/SSA/Core/Framework.lean @@ -1368,6 +1368,9 @@ section Lemmas (Com.lete e body).changeDialect f = Com.lete (e.changeDialect f) (body.changeDialect f) := by simp only [List.map_eq_map, changeDialect] +@[simp] lemma HVector.changeDialect_nil (f : DialectMorphism d d') : + HVector.changeDialect (eff := eff) f nil = nil := rfl + end Lemmas end Map diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index be70caab5..ca939967b 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -292,6 +292,15 @@ def two_inst_macro (w: Nat):= "llvm.return" (%0) : (_) -> () }] +set_option ssa.alive_icom_reduce false in +def two_inst_macro_noreduce (w: Nat):= + [alive_icom (w)|{ + ^bb0(%arg0: _): + %0 = "llvm.not" (%arg0) : (_, _) -> (_) + %1 = "llvm.not" (%arg0) : (_, _) -> (_) + "llvm.return" (%0) : (_) -> () + }] + def two_inst_com (w : ℕ) : Com InstCombine.LLVM [InstCombine.Ty.bitvec w] .pure (InstCombine.Ty.bitvec w) := Com.lete (not w 0) <| @@ -315,3 +324,14 @@ def two_inst_macro_proof (w : Nat) : simp_alive_meta simp_alive_ssa apply two_inst_stmt + +def two_inst_macro_noreduce_proof (w : Nat) : + two_inst_macro_noreduce w ⊑ two_inst_macro_noreduce w := by + unfold two_inst_macro_noreduce + simp_alive_meta + simp only [(HVector.changeDialect_nil)] + dsimp! [] + unfold Op.unary + simp_alive_meta + simp_alive_ssa + apply two_inst_stmt From 9ad56a4a938f545dd38ee4bb86210d06321e740e Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 08:04:22 +0100 Subject: [PATCH 16/43] chore: ensuer that simplification works end-to-end. Now we need to clean-up and extract general theorems --- SSA/Core/Tactic.lean | 2 +- SSA/Projects/InstCombine/Test.lean | 34 +++++++++++++++++++++++++++++- 2 files changed, 34 insertions(+), 2 deletions(-) diff --git a/SSA/Core/Tactic.lean b/SSA/Core/Tactic.lean index 2bf52f99a..f2b23aaaf 100644 --- a/SSA/Core/Tactic.lean +++ b/SSA/Core/Tactic.lean @@ -108,7 +108,7 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" Γv:ident only_goal simp (config := {failIfUnchanged := false}) only [Ctxt.Var.toSnoc, Ctxt.Var.last] repeat (generalize_or_fail at $Γv) - clear $Γv + try clear $Γv ) ) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index ca939967b..8abd00133 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -325,13 +325,45 @@ def two_inst_macro_proof (w : Nat) : simp_alive_ssa apply two_inst_stmt +-- theorem toMap_last {Γ : Ctxt Ty} {t : Ty} : +-- (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl + +theorem toMap_toMap {Γ : Ctxt Ty0} {t : Ty0} {f : Ty0 → Ty1} {var : (Γ.Var t)}: +@Ctxt.Var.toMap Ty0 Γ t Ty1 f var = +@Ctxt.Var.toMap Ty0 Γ t Ty1 f var := rfl + +theorem aa {w : Nat}: @Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] + (MTy.bitvec (ConcreteOrMVar.mvar 0)) Ty (instantiateMTy ⟨[w], by simp⟩) ⟨0 + 1, by simp⟩ = + ⟨1, by simp⟩ := rfl + +#reduce @Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] + (MTy.bitvec (ConcreteOrMVar.mvar 0)) Ty (instantiateMTy ⟨[], _⟩) ⟨0 + 1, _⟩ + def two_inst_macro_noreduce_proof (w : Nat) : two_inst_macro_noreduce w ⊑ two_inst_macro_noreduce w := by unfold two_inst_macro_noreduce simp_alive_meta simp only [(HVector.changeDialect_nil)] - dsimp! [] + dsimp [instantiateMOp] unfold Op.unary simp_alive_meta + /- + @Ctxt.Var.toMap (MTy 1) + [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] + (MTy.bitvec (ConcreteOrMVar.mvar 0)) Ty (instantiateMTy ⟨[w], ⋯⟩) ⟨0 + 1, ⋯⟩ + -/ + simp_alive_ssa + rw [aa] + simp only [Ctxt.map_cons, Ctxt.get?, Ctxt.Valuation.snoc_eval, Ctxt.Var.zero_eq_last, zero_add, + Ctxt.Var.succ_eq_toSnoc, implies_true] + simp_alive_meta + simp_alive_ssa + simp_alive_meta + unfold Ctxt.Var.toMap + dsimp only [Ctxt.map_cons, Nat.reduceAdd, Ctxt.get?, Ctxt.Var.succ_eq_toSnoc, List.map_cons, + List.map_nil, Ctxt.Var.zero_eq_last, Ctxt.Valuation.snoc_toSnoc] + simp_alive_meta + unfold Ctxt.Var.last + dsimp only [Ctxt.get?, Ctxt.Var.zero_eq_last, Ctxt.Valuation.snoc_last] apply two_inst_stmt From 9db80f6aaed384043949bf721cc736a3a1c1a637 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 08:37:06 +0100 Subject: [PATCH 17/43] cleanup --- SSA/Core/ErasedContext.lean | 3 +++ SSA/Projects/InstCombine/Test.lean | 30 ++++++++++-------------------- 2 files changed, 13 insertions(+), 20 deletions(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index 9942c4274..bc9f84762 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -140,6 +140,9 @@ def castCtxt {Γ : Ctxt Op} (h_eq : Γ = Δ) : Γ.Var ty → Δ.Var ty @[simp] lemma castCtxt_castCtxt (v : Var Γ t) (h₁ : Γ = Δ) (h₂ : Δ = Ξ) : (v.castCtxt h₁).castCtxt h₂ = v.castCtxt (by simp [*]) := by subst h₁ h₂; simp +variable {Γ : Ctxt Ty} {t : Ty} +#check (Ctxt.Var.last Γ t) + @[simp] theorem toMap_last {Γ : Ctxt Ty} {t : Ty} : (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 8abd00133..099b75909 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -332,6 +332,8 @@ theorem toMap_toMap {Γ : Ctxt Ty0} {t : Ty0} {f : Ty0 → Ty1} {var : (Γ.Var t @Ctxt.Var.toMap Ty0 Γ t Ty1 f var = @Ctxt.Var.toMap Ty0 Γ t Ty1 f var := rfl +⟨1, ⋯⟩ + theorem aa {w : Nat}: @Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] (MTy.bitvec (ConcreteOrMVar.mvar 0)) Ty (instantiateMTy ⟨[w], by simp⟩) ⟨0 + 1, by simp⟩ = ⟨1, by simp⟩ := rfl @@ -339,31 +341,19 @@ theorem aa {w : Nat}: @Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0 #reduce @Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] (MTy.bitvec (ConcreteOrMVar.mvar 0)) Ty (instantiateMTy ⟨[], _⟩) ⟨0 + 1, _⟩ +#reduce @Ctxt.Var.toSnoc (MTy 1) (MTy.bitvec (ConcreteOrMVar.mvar 0) :: ∅) (MTy.bitvec (ConcreteOrMVar.mvar 0)) + (MTy.bitvec (ConcreteOrMVar.mvar 0)) (Ctxt.Var.last ∅ (MTy.bitvec (ConcreteOrMVar.mvar 0))) + def two_inst_macro_noreduce_proof (w : Nat) : two_inst_macro_noreduce w ⊑ two_inst_macro_noreduce w := by unfold two_inst_macro_noreduce simp_alive_meta simp only [(HVector.changeDialect_nil)] - dsimp [instantiateMOp] + dsimp only [List.length_singleton, List.map_nil, Fin.zero_eta, instantiateMOp, + ConcreteOrMVar.instantiate_mvar_zero'', Nat.zero_eq] unfold Op.unary - simp_alive_meta - /- - @Ctxt.Var.toMap (MTy 1) - [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] - (MTy.bitvec (ConcreteOrMVar.mvar 0)) Ty (instantiateMTy ⟨[w], ⋯⟩) ⟨0 + 1, ⋯⟩ - -/ - - simp_alive_ssa - rw [aa] - simp only [Ctxt.map_cons, Ctxt.get?, Ctxt.Valuation.snoc_eval, Ctxt.Var.zero_eq_last, zero_add, - Ctxt.Var.succ_eq_toSnoc, implies_true] - simp_alive_meta - simp_alive_ssa - simp_alive_meta unfold Ctxt.Var.toMap - dsimp only [Ctxt.map_cons, Nat.reduceAdd, Ctxt.get?, Ctxt.Var.succ_eq_toSnoc, List.map_cons, - List.map_nil, Ctxt.Var.zero_eq_last, Ctxt.Valuation.snoc_toSnoc] - simp_alive_meta - unfold Ctxt.Var.last - dsimp only [Ctxt.get?, Ctxt.Var.zero_eq_last, Ctxt.Valuation.snoc_last] + unfold Ctxt.Var.toSnoc + dsimp! [] + simp_alive_ssa apply two_inst_stmt From 7b16657d15c1380d5efc5fdf9566017ccf8f400a Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 10:04:57 +0100 Subject: [PATCH 18/43] fix build --- SSA/Projects/InstCombine/Test.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 099b75909..cc018b4f5 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -325,15 +325,6 @@ def two_inst_macro_proof (w : Nat) : simp_alive_ssa apply two_inst_stmt --- theorem toMap_last {Γ : Ctxt Ty} {t : Ty} : --- (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Γ.map f) (f t) := rfl - -theorem toMap_toMap {Γ : Ctxt Ty0} {t : Ty0} {f : Ty0 → Ty1} {var : (Γ.Var t)}: -@Ctxt.Var.toMap Ty0 Γ t Ty1 f var = -@Ctxt.Var.toMap Ty0 Γ t Ty1 f var := rfl - -⟨1, ⋯⟩ - theorem aa {w : Nat}: @Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] (MTy.bitvec (ConcreteOrMVar.mvar 0)) Ty (instantiateMTy ⟨[w], by simp⟩) ⟨0 + 1, by simp⟩ = ⟨1, by simp⟩ := rfl From 605904db54156461895c33b81ef1d2df10d3055a Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 10:06:01 +0100 Subject: [PATCH 19/43] fix build --- SSA/Projects/InstCombine/Test.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index cc018b4f5..cafa796f7 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -345,6 +345,5 @@ def two_inst_macro_noreduce_proof (w : Nat) : unfold Op.unary unfold Ctxt.Var.toMap unfold Ctxt.Var.toSnoc - dsimp! [] simp_alive_ssa apply two_inst_stmt From bf48ddff0831b08478b58d4ddd0e5af73d2f6388 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 13:42:14 +0100 Subject: [PATCH 20/43] chore: make two operations work --- SSA/Core/ErasedContext.lean | 7 ++++--- SSA/Core/Tactic.lean | 2 +- SSA/Projects/InstCombine/Tactic.lean | 7 ++++++- SSA/Projects/InstCombine/Test.lean | 18 +----------------- 4 files changed, 12 insertions(+), 22 deletions(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index bc9f84762..1838705af 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -140,12 +140,13 @@ def castCtxt {Γ : Ctxt Op} (h_eq : Γ = Δ) : Γ.Var ty → Δ.Var ty @[simp] lemma castCtxt_castCtxt (v : Var Γ t) (h₁ : Γ = Δ) (h₂ : Δ = Ξ) : (v.castCtxt h₁).castCtxt h₂ = v.castCtxt (by simp [*]) := by subst h₁ h₂; simp -variable {Γ : Ctxt Ty} {t : Ty} -#check (Ctxt.Var.last Γ t) - @[simp] 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 → Ty2} : + @Ctxt.Var.toMap _ (Γ.snoc t) _ _ f var.toSnoc = var.toMap.toSnoc := rfl + /-- This is an induction principle that case splits on whether or not a variable is the last variable in a context. -/ @[elab_as_elim, cases_eliminator] diff --git a/SSA/Core/Tactic.lean b/SSA/Core/Tactic.lean index f2b23aaaf..2bf52f99a 100644 --- a/SSA/Core/Tactic.lean +++ b/SSA/Core/Tactic.lean @@ -108,7 +108,7 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" Γv:ident only_goal simp (config := {failIfUnchanged := false}) only [Ctxt.Var.toSnoc, Ctxt.Var.last] repeat (generalize_or_fail at $Γv) - try clear $Γv + clear $Γv ) ) diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index d3ce49a21..22f2f87ca 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -20,6 +20,7 @@ macro "simp_alive_meta" : tactic => `(tactic| ( simp (config := {failIfUnchanged := false }) only [Com.changeDialect_ret, Com.changeDialect_lete, Expr.changeDialect] + simp (config := {failIfUnchanged := false }) only [(HVector.changeDialect_nil)] dsimp (config := {failIfUnchanged := false }) only [Functor.map] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.succ_eq_toSnoc] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.zero_eq_last] @@ -29,13 +30,17 @@ macro "simp_alive_meta" : tactic => dsimp (config := {failIfUnchanged := false }) only [Width.mvar] dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_snoc, Ctxt.map_nil] dsimp (config := {failIfUnchanged := false }) only [Ctxt.get?] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.map, Ctxt.snoc] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toSnoc_toMap] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_cons] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.MOp.instantiateCom] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMTy] + dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMOp] 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 [Ctxt.map, Ctxt.snoc] dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate] ) ) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index cafa796f7..554b5704c 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -325,25 +325,9 @@ def two_inst_macro_proof (w : Nat) : simp_alive_ssa apply two_inst_stmt -theorem aa {w : Nat}: @Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] - (MTy.bitvec (ConcreteOrMVar.mvar 0)) Ty (instantiateMTy ⟨[w], by simp⟩) ⟨0 + 1, by simp⟩ = - ⟨1, by simp⟩ := rfl - -#reduce @Ctxt.Var.toMap (MTy 1) [MTy.bitvec (ConcreteOrMVar.mvar 0), MTy.bitvec (ConcreteOrMVar.mvar 0)] - (MTy.bitvec (ConcreteOrMVar.mvar 0)) Ty (instantiateMTy ⟨[], _⟩) ⟨0 + 1, _⟩ - -#reduce @Ctxt.Var.toSnoc (MTy 1) (MTy.bitvec (ConcreteOrMVar.mvar 0) :: ∅) (MTy.bitvec (ConcreteOrMVar.mvar 0)) - (MTy.bitvec (ConcreteOrMVar.mvar 0)) (Ctxt.Var.last ∅ (MTy.bitvec (ConcreteOrMVar.mvar 0))) - -def two_inst_macro_noreduce_proof (w : Nat) : +def two_inst_macro_noreduc'_proof (w : Nat) : two_inst_macro_noreduce w ⊑ two_inst_macro_noreduce w := by unfold two_inst_macro_noreduce simp_alive_meta - simp only [(HVector.changeDialect_nil)] - dsimp only [List.length_singleton, List.map_nil, Fin.zero_eta, instantiateMOp, - ConcreteOrMVar.instantiate_mvar_zero'', Nat.zero_eq] - unfold Op.unary - unfold Ctxt.Var.toMap - unfold Ctxt.Var.toSnoc simp_alive_ssa apply two_inst_stmt From 7b9fa09cf1169d8704dfd0c4a099a3b6734b07e1 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 13:57:49 +0100 Subject: [PATCH 21/43] fix typo --- SSA/Projects/InstCombine/Test.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 554b5704c..2526754c8 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -325,7 +325,7 @@ def two_inst_macro_proof (w : Nat) : simp_alive_ssa apply two_inst_stmt -def two_inst_macro_noreduc'_proof (w : Nat) : +def two_inst_macro_noreduc_proof (w : Nat) : two_inst_macro_noreduce w ⊑ two_inst_macro_noreduce w := by unfold two_inst_macro_noreduce simp_alive_meta From 4e0c66643e15e6ff6267a8b7e847ab2741d946d5 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 17:49:49 +0100 Subject: [PATCH 22/43] chore: make all work --- SSA/Projects/InstCombine/AliveAutoGenerated.lean | 2 +- SSA/Projects/InstCombine/Tactic.lean | 4 ++++ SSA/Projects/InstCombine/Test.lean | 12 +++++++----- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/SSA/Projects/InstCombine/AliveAutoGenerated.lean b/SSA/Projects/InstCombine/AliveAutoGenerated.lean index 47ea0c61b..b8ccc2371 100644 --- a/SSA/Projects/InstCombine/AliveAutoGenerated.lean +++ b/SSA/Projects/InstCombine/AliveAutoGenerated.lean @@ -16,7 +16,7 @@ set_option pp.proofs false set_option pp.proofs.withType false set_option linter.deprecated false - +set_option ssa.alive_icom_reduce false in -- Name:AddSub:1043 -- precondition: true diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 22f2f87ca..9985c185f 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -21,6 +21,7 @@ macro "simp_alive_meta" : tactic => ( simp (config := {failIfUnchanged := false }) only [Com.changeDialect_ret, Com.changeDialect_lete, Expr.changeDialect] simp (config := {failIfUnchanged := false }) only [(HVector.changeDialect_nil)] + dsimp (config := {failIfUnchanged := false }) only [HVector.map'] dsimp (config := {failIfUnchanged := false }) only [Functor.map] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.succ_eq_toSnoc] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.zero_eq_last] @@ -36,12 +37,15 @@ macro "simp_alive_meta" : tactic => dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_cons] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.MOp.instantiateCom] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMTy] + dsimp (config := {failIfUnchanged := false }) only [Fin.zero_eta, List.map_cons] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMOp] 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''] ) ) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 2526754c8..c8890e217 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -287,8 +287,8 @@ def one_inst_macro_proof_noreduce (w : Nat) : def two_inst_macro (w: Nat):= [alive_icom (w)|{ ^bb0(%arg0: _): - %0 = "llvm.not" (%arg0) : (_, _) -> (_) - %1 = "llvm.not" (%arg0) : (_, _) -> (_) + %0 = "llvm.not" (%arg0) : (_) -> (_) + %1 = "llvm.not" (%arg0) : (_) -> (_) "llvm.return" (%0) : (_) -> () }] @@ -296,9 +296,10 @@ set_option ssa.alive_icom_reduce false in def two_inst_macro_noreduce (w: Nat):= [alive_icom (w)|{ ^bb0(%arg0: _): - %0 = "llvm.not" (%arg0) : (_, _) -> (_) - %1 = "llvm.not" (%arg0) : (_, _) -> (_) - "llvm.return" (%0) : (_) -> () + %0 = "llvm.not" (%arg0) : (_) -> (_) + %1 = "llvm.not" (%0) : (_) -> (_) + %2 = "llvm.not" (%1) : (_) -> (_) + "llvm.return" (%2) : (_) -> () }] def two_inst_com (w : ℕ) : @@ -331,3 +332,4 @@ def two_inst_macro_noreduc_proof (w : Nat) : simp_alive_meta simp_alive_ssa apply two_inst_stmt +ß From 8ad4f2534dde008614c1d8110fd619772e60108a Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 19:11:03 +0100 Subject: [PATCH 23/43] WIP --- SSA/Projects/InstCombine/Test.lean | 58 +++++++++++++++++++++++++++--- 1 file changed, 54 insertions(+), 4 deletions(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 4b116ea74..d5de13577 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -297,9 +297,8 @@ def two_inst_macro_noreduce (w: Nat):= [alive_icom (w)|{ ^bb0(%arg0: _): %0 = "llvm.not" (%arg0) : (_) -> (_) - %1 = "llvm.not" (%0) : (_) -> (_) - %2 = "llvm.not" (%1) : (_) -> (_) - "llvm.return" (%2) : (_) -> () + %1 = "llvm.not" (%arg0) : (_) -> (_) + "llvm.return" (%0) : (_) -> () }] def two_inst_com (w : ℕ) : @@ -332,4 +331,55 @@ def two_inst_macro_noreduc_proof (w : Nat) : simp_alive_meta simp_alive_ssa apply two_inst_stmt -ß + +def three_inst_macro (w: Nat):= + [alive_icom (w)|{ + ^bb0(%arg0: _): + %0 = "llvm.not" (%arg0) : (_) -> (_) + %1 = "llvm.not" (%0) : (_) -> (_) + %2 = "llvm.not" (%1) : (_) -> (_) + "llvm.return" (%2) : (_) -> () + }] + +set_option ssa.alive_icom_reduce false in +def three_inst_macro_noreduce (w: Nat):= + [alive_icom (w)|{ + ^bb0(%arg0: _): + %0 = "llvm.not" (%arg0) : (_) -> (_) + %1 = "llvm.not" (%0) : (_) -> (_) + %2 = "llvm.not" (%1) : (_) -> (_) + "llvm.return" (%2) : (_) -> () + }] + +def three_inst_com (w : ℕ) : + Com InstCombine.LLVM [InstCombine.Ty.bitvec w] .pure (InstCombine.Ty.bitvec w) := + Com.lete (not w 0) <| + Com.lete (not w 0) <| + Com.lete (not w 0) <| + Com.ret ⟨0, by simp [Ctxt.snoc]⟩ + +def three_inst_stmt (e : LLVM.IntW w) : + @BitVec.Refinement (BitVec w) (LLVM.not (LLVM.not (LLVM.not e))) + (LLVM.not (LLVM.not (LLVM.not e))) := by simp + +def three_inst_com_proof (w : Nat) : + three_inst_com w ⊑ three_inst_com w := by + unfold three_inst_com + simp only [simp_llvm_wrap] + simp_alive_meta + simp_alive_ssa + apply three_inst_stmt + +def three_inst_macro_proof (w : Nat) : + three_inst_macro w ⊑ three_inst_macro w := by + unfold three_inst_macro + simp_alive_meta + simp_alive_ssa + apply three_inst_stmt + +def three_inst_macro_noreduc_proof (w : Nat) : + three_inst_macro_noreduce w ⊑ three_inst_macro_noreduce w := by + unfold three_inst_macro_noreduce + simp_alive_meta + simp_alive_ssa + apply three_inst_stmt From fc377680bfb09ef82a7d4b759ca36fd653db289c Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 25 May 2024 19:15:11 +0100 Subject: [PATCH 24/43] Drop set_option --- SSA/Projects/InstCombine/AliveAutoGenerated.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/AliveAutoGenerated.lean b/SSA/Projects/InstCombine/AliveAutoGenerated.lean index b8ccc2371..47ea0c61b 100644 --- a/SSA/Projects/InstCombine/AliveAutoGenerated.lean +++ b/SSA/Projects/InstCombine/AliveAutoGenerated.lean @@ -16,7 +16,7 @@ set_option pp.proofs false set_option pp.proofs.withType false set_option linter.deprecated false -set_option ssa.alive_icom_reduce false in + -- Name:AddSub:1043 -- precondition: true From f82125d25b54c70ccb0e9fdfaf6a4cdfe706f766 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 07:57:20 +0100 Subject: [PATCH 25/43] chore: try all of AliveAutoGenerated --- SSA/Core/ErasedContext.lean | 11 +++++++++-- SSA/Projects/InstCombine/AliveAutoGenerated.lean | 14 ++++++++------ SSA/Projects/InstCombine/Tactic.lean | 2 ++ 3 files changed, 19 insertions(+), 8 deletions(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index 1838705af..b44fef0e2 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -121,7 +121,6 @@ theorem succ_eq_toSnoc {Γ : Ctxt Ty} {t : Ty} {w} (h : (Γ.snoc t).get? (w+1) = rfl /-- Transport a variable from `Γ` to any mapped context `Γ.map f` -/ -@[coe] def toMap : Var Γ t → Var (Γ.map f) (f t) | ⟨i, h⟩ => ⟨i, by simp only [get?, map, List.get?_map, Option.map_eq_some'] @@ -145,7 +144,15 @@ theorem toMap_last {Γ : Ctxt Ty} {t : Ty} : (Ctxt.Var.last Γ t).toMap = Ctxt.V @[simp] theorem toSnoc_toMap {Γ : Ctxt Ty} {t : Ty } {var : Ctxt.Var Γ t} {f : Ty → Ty2} : - @Ctxt.Var.toMap _ (Γ.snoc t) _ _ f var.toSnoc = var.toMap.toSnoc := rfl + @Var.toMap _ (Γ.snoc t) _ _ f var.toSnoc = var.toMap.toSnoc := rfl + +@[simp] +theorem toSnoc_toMap' {Γ : Ctxt Ty} {t t': Ty } {var : Ctxt.Var Γ t} {f : Ty → Ty2} : + @Ctxt.Var.toMap _ ((Γ.snoc t).snoc t') _ _ f var.toSnoc.toSnoc = var.toMap.toSnoc.toSnoc := rfl + +@[simp] +theorem toSnoc_toMap'' {Γ : Ctxt Ty} {t t' t'': Ty } {var : Ctxt.Var Γ t} {f : Ty → Ty2} : + @Ctxt.Var.toMap _ (((Γ.snoc t).snoc t').snoc t'') _ _ f var.toSnoc.toSnoc.toSnoc = var.toMap.toSnoc.toSnoc.toSnoc := rfl /-- This is an induction principle that case splits on whether or not a variable is the last variable in a context. -/ diff --git a/SSA/Projects/InstCombine/AliveAutoGenerated.lean b/SSA/Projects/InstCombine/AliveAutoGenerated.lean index 47ea0c61b..ede09b742 100644 --- a/SSA/Projects/InstCombine/AliveAutoGenerated.lean +++ b/SSA/Projects/InstCombine/AliveAutoGenerated.lean @@ -16,7 +16,7 @@ set_option pp.proofs false set_option pp.proofs.withType false set_option linter.deprecated false - +set_option ssa.alive_icom_reduce false -- Name:AddSub:1043 -- precondition: true @@ -722,6 +722,7 @@ theorem alive_AndOrXor_144 (w : Nat) : alive_AndOrXor_144_src w ⊑ alive_An -/ -- MANUAL FIX: the translation script inferred some of the resulting types to be `i1` -- where they should be the meta-variable `_` (https://github.com/opencompl/ssa/issues/169) + def alive_AndOrXor_698_src (w : Nat) := [alive_icom ( w )| { ^bb0(%a : _, %b : _, %d : _): @@ -752,7 +753,10 @@ def alive_AndOrXor_698_tgt (w : Nat) := }] theorem alive_AndOrXor_698 (w : Nat) : alive_AndOrXor_698_src w ⊑ alive_AndOrXor_698_tgt w := by unfold alive_AndOrXor_698_src alive_AndOrXor_698_tgt + simp_alive_meta + simp_alive_meta simp_alive_peephole + apply bitvec_AndOrXor_698 @@ -870,17 +874,14 @@ def alive_AndOrXor_794_src (w : Nat) := ^bb0(%a : _, %b : _): %v1 = "llvm.icmp.sgt" (%a,%b) : (_, _) -> (i1) %v2 = "llvm.icmp.ne" (%a,%b) : (_, _) -> (i1) - %v3 = "llvm.and" (%v1,%v2) : (i1, i1) -> (i1) - "llvm.return" (%v3) : (i1) -> () + "llvm.return" (%v2) : (i1) -> () }] def alive_AndOrXor_794_tgt (w : Nat) := [alive_icom ( w )| { ^bb0(%a : _, %b : _): %v1 = "llvm.icmp.sgt" (%a,%b) : (_, _) -> (i1) - %v2 = "llvm.icmp.ne" (%a,%b) : (_, _) -> (i1) - %v3 = "llvm.icmp.sgt" (%a,%b) : (_, _) -> (i1) - "llvm.return" (%v3) : (i1) -> () + "llvm.return" (%v1) : (i1) -> () }] theorem alive_AndOrXor_794 (w : Nat) : alive_AndOrXor_794_src w ⊑ alive_AndOrXor_794_tgt w := by unfold alive_AndOrXor_794_src alive_AndOrXor_794_tgt @@ -1050,6 +1051,7 @@ def alive_AndOrXor_1241_AB__AB__AB_tgt (w : Nat) := }] theorem alive_AndOrXor_1241_AB__AB__AB (w : Nat) : alive_AndOrXor_1241_AB__AB__AB_src w ⊑ alive_AndOrXor_1241_AB__AB__AB_tgt w := by unfold alive_AndOrXor_1241_AB__AB__AB_src alive_AndOrXor_1241_AB__AB__AB_tgt + simp_alive_meta simp_alive_peephole apply bitvec_AndOrXor_1241_AB__AB__AB diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 9985c185f..705c71f98 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -33,6 +33,8 @@ macro "simp_alive_meta" : tactic => dsimp (config := {failIfUnchanged := false }) only [Ctxt.get?] dsimp (config := {failIfUnchanged := false }) only [Ctxt.map, Ctxt.snoc] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toSnoc_toMap] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toSnoc_toMap'] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toSnoc_toMap''] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_cons] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.MOp.instantiateCom] From 3a7b5d99ed98ccbfe5b56792d345b1f82ac36181 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 16:30:15 +0100 Subject: [PATCH 26/43] minimized test case --- SSA/Projects/InstCombine/Test.lean | 147 ++++++++++++++++++++++++++++- 1 file changed, 146 insertions(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index d5de13577..a78163cee 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -377,9 +377,154 @@ def three_inst_macro_proof (w : Nat) : simp_alive_ssa apply three_inst_stmt -def three_inst_macro_noreduc_proof (w : Nat) : +def three_inst_macro_noreduc_proof : three_inst_macro_noreduce w ⊑ three_inst_macro_noreduce w := by unfold three_inst_macro_noreduce 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 (w : ℕ) : + Com InstCombine.LLVM [InstCombine.Ty.bitvec w] .pure (InstCombine.Ty.bitvec w) := + Com.lete (not w 0) <| + Com.lete (not w 0) <| + Com.lete (not w 0) <| + Com.ret ⟨0, by simp [Ctxt.snoc]⟩ + +def three_inst_concrete_stmt (e : LLVM.IntW w) : + @BitVec.Refinement (BitVec w) (LLVM.not (LLVM.not (LLVM.not e))) + (LLVM.not (LLVM.not (LLVM.not e))) := by simp + +def three_inst_concrete_com_proof (w : Nat) : + three_inst_concrete_com w ⊑ three_inst_concrete_com w := 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 (w : Nat) : + three_inst_concrete_macro w ⊑ three_inst_concrete_macro w := by + unfold three_inst_concrete_macro + simp_alive_meta + simp_alive_ssa + apply three_inst_concrete_stmt + +def three_inst_concrete_macro_noreduc_proof (w : Nat) : + three_inst_concrete_macro_noreduce w ⊑ three_inst_concrete_macro_noreduce w := by + unfold three_inst_concrete_macro_noreduce + simp_alive_meta + simp_alive_ssa + apply three_inst_concrete_stmt From 0fbaf31fc585e905f5d1501284779169db617ea5 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 16:52:33 +0100 Subject: [PATCH 27/43] reduce test case --- SSA/Projects/InstCombine/Test.lean | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index a78163cee..08061a93f 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -496,34 +496,34 @@ def three_inst_concrete_macro_noreduce := "llvm.return" (%2) : (i1) -> () }] -def three_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 0) <| - Com.lete (not w 0) <| +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 w) : - @BitVec.Refinement (BitVec w) (LLVM.not (LLVM.not (LLVM.not e))) +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 (w : Nat) : - three_inst_concrete_com w ⊑ three_inst_concrete_com w := by +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 (w : Nat) : - three_inst_concrete_macro w ⊑ three_inst_concrete_macro w := by +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 (w : Nat) : - three_inst_concrete_macro_noreduce w ⊑ three_inst_concrete_macro_noreduce w := by +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 From b97bdaf018f175e9756d550441e174793ef46095 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 17:07:42 +0100 Subject: [PATCH 28/43] WIP --- SSA/Core/Util/ConcreteOrMVar.lean | 4 ++++ SSA/Projects/InstCombine/Test.lean | 6 ++++++ 2 files changed, 10 insertions(+) diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean index 37cd85aaf..8e8f02cf6 100644 --- a/SSA/Core/Util/ConcreteOrMVar.lean +++ b/SSA/Core/Util/ConcreteOrMVar.lean @@ -52,6 +52,10 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α def instantiate_concrete_eq (as : Vector α φ) : (ConcreteOrMVar.concrete w).instantiate as = w := by rfl +@[simp] +def instantiate_list (x : Nat) (as : List Nat) : + ConcreteOrMVar.instantiate ⟨as, by rfl⟩ x = x := rfl + @[simp] lemma instantiate_mvar_zero {hφ : List.length (w :: ws) = φ} {h0 : 0 < φ} : ConcreteOrMVar.instantiate (Subtype.mk (w :: ws) hφ) (ConcreteOrMVar.mvar ⟨0, h0⟩) = w := by diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 08061a93f..0ae6fde55 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -522,9 +522,15 @@ def three_inst_concrete_macro_proof : simp_alive_ssa apply three_inst_concrete_stmt +@[simp] +def ainstantiate_list (x : Nat) (as : List Nat) : + ConcreteOrMVar.instantiate ll x = x := rfl + +#check ConcreteOrMVar.instantiate_concrete_eq 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! only [ainstantiate_list] simp_alive_ssa apply three_inst_concrete_stmt From 4454b712409d4ba8a21694dec6dd96f764f18190 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 17:18:18 +0100 Subject: [PATCH 29/43] WIP --- SSA/Core/Util/ConcreteOrMVar.lean | 4 ++-- SSA/Projects/InstCombine/Test.lean | 8 ++------ 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean index 8e8f02cf6..d9e3a1672 100644 --- a/SSA/Core/Util/ConcreteOrMVar.lean +++ b/SSA/Core/Util/ConcreteOrMVar.lean @@ -53,8 +53,8 @@ def instantiate_concrete_eq (as : Vector α φ) : (ConcreteOrMVar.concrete w).instantiate as = w := by rfl @[simp] -def instantiate_list (x : Nat) (as : List Nat) : - ConcreteOrMVar.instantiate ⟨as, by rfl⟩ x = x := rfl +def instantiate_list (as : Vector Nat φ) (x : Nat) : + ConcreteOrMVar.instantiate as x = x := rfl @[simp] lemma instantiate_mvar_zero {hφ : List.length (w :: ws) = φ} {h0 : 0 < φ} : diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index e54b05b53..4c25f5f4e 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -522,15 +522,11 @@ def three_inst_concrete_macro_proof : simp_alive_ssa apply three_inst_concrete_stmt -@[simp] -def ainstantiate_list (x : Nat) (as : List Nat) : - ConcreteOrMVar.instantiate ll x = x := rfl - -#check ConcreteOrMVar.instantiate_concrete_eq 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! only [ainstantiate_list] + -- How can I avoid the `simp! only`and use a plain `simp only`? + simp! only [ConcreteOrMVar.instantiate_list] simp_alive_ssa apply three_inst_concrete_stmt From 523c1ddba061cbf6b15a953d33dab6f6ee8e99af Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 17:33:48 +0100 Subject: [PATCH 30/43] two more reduced test cases --- SSA/Projects/InstCombine/Test.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 4c25f5f4e..fdb6be772 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -530,3 +530,27 @@ def three_inst_concrete_macro_noreduc_proof : simp! only [ConcreteOrMVar.instantiate_list] simp_alive_ssa apply three_inst_concrete_stmt + +@[simp] +theorem toSnoc_toMap {Γ : Ctxt Ty1} {t1 t2 : Ty1} {var : Ctxt.Var Γ t} {f : Ty1 → Ty2} : + var.toSnoc.toSnoc.toMap (Γ := ((Γ.snoc t1).snoc t2)) (f := f) = + var.toMap.toSnoc.toSnoc := rfl + +set_option ssa.alive_icom_reduce false in +def three_inst_concrete_macro_noreduce_ne (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 three_inst_concrete_macro_noreduc_proof_ne : + three_inst_concrete_macro_noreduce_ne w ⊑ three_inst_concrete_macro_noreduce_ne w := by + unfold three_inst_concrete_macro_noreduce_ne + simp_alive_meta + -- There remains a 'toMap' in the following expression: + -- (↑↑(Ctxt.Var.last ∅ (MTy.bitvec (ConcreteOrMVar.mvar 0)))).toMap + -- I am unsure why + simp_alive_ssa + apply three_inst_concrete_stmt From 36c78f0c0763cd32a9becc98ac3b7732ad9c1c82 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 20:06:05 +0100 Subject: [PATCH 31/43] make it work --- SSA/Core/ErasedContext.lean | 20 +++++++++++++++++++ .../InstCombine/AliveAutoGenerated.lean | 2 +- SSA/Projects/InstCombine/Tactic.lean | 1 + SSA/Projects/InstCombine/Test.lean | 16 ++++++++------- 4 files changed, 31 insertions(+), 8 deletions(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index c0f088511..59619a613 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -146,6 +146,26 @@ theorem toMap_last {Γ : Ctxt Ty} {t : Ty} : (Ctxt.Var.last Γ t).toMap = Ctxt.V 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 +@[simp] +theorem toSnoc_toMap' {Γ : Ctxt Ty1} {t1 t2 : Ty1} {var : Ctxt.Var Γ t} {f : Ty1 → Ty2} : + var.toSnoc.toSnoc.toMap (Γ := ((Γ.snoc t1).snoc t2)) (f := f) = + var.toMap.toSnoc.toSnoc := rfl + +@[simp] +theorem toSnoc_toMap'' {Γ : Ctxt Ty1} {t1 t2 t3: Ty1} {var : Ctxt.Var Γ t} {f : Ty1 → Ty2} : + var.toSnoc.toSnoc.toSnoc.toMap (Γ := ((Γ.snoc t1).snoc t2).snoc t3) (f := f) = + var.toMap.toSnoc.toSnoc.toSnoc := rfl + +@[simp] +theorem toSnoc_toMap''' {Γ : Ctxt Ty1} {t1 t2 t3 t4: Ty1} {var : Ctxt.Var Γ t} {f : Ty1 → Ty2} : + var.toSnoc.toSnoc.toSnoc.toSnoc.toMap (Γ := (((Γ.snoc t1).snoc t2).snoc t3).snoc t4) (f := f) = + var.toMap.toSnoc.toSnoc.toSnoc.toSnoc := rfl + +@[simp] +theorem last_toSnoc_toMap {Γ : Ctxt Ty1} {t t2: Ty1} {f : Ty1 → Ty2} : + (Ctxt.Var.last Γ t).toSnoc.toMap (f := f) (Γ := ((Γ.snoc t).snoc t2)) + = (Ctxt.Var.last (Ctxt.map f Γ) (f t)).toSnoc := rfl + /-- This is an induction principle that case splits on whether or not a variable is the last variable in a context. -/ @[elab_as_elim, cases_eliminator] diff --git a/SSA/Projects/InstCombine/AliveAutoGenerated.lean b/SSA/Projects/InstCombine/AliveAutoGenerated.lean index ede09b742..20ef167fe 100644 --- a/SSA/Projects/InstCombine/AliveAutoGenerated.lean +++ b/SSA/Projects/InstCombine/AliveAutoGenerated.lean @@ -16,7 +16,7 @@ set_option pp.proofs false set_option pp.proofs.withType false set_option linter.deprecated false -set_option ssa.alive_icom_reduce false +set_option ssa.alive_icom_reduce true -- Name:AddSub:1043 -- precondition: true diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 9985c185f..6e8dcc6dd 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -34,6 +34,7 @@ macro "simp_alive_meta" : tactic => dsimp (config := {failIfUnchanged := false }) only [Ctxt.map, Ctxt.snoc] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toSnoc_toMap] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] + dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.last_toSnoc_toMap] dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_cons] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.MOp.instantiateCom] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMTy] diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index fdb6be772..2c12fb351 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -531,11 +531,6 @@ def three_inst_concrete_macro_noreduc_proof : simp_alive_ssa apply three_inst_concrete_stmt -@[simp] -theorem toSnoc_toMap {Γ : Ctxt Ty1} {t1 t2 : Ty1} {var : Ctxt.Var Γ t} {f : Ty1 → Ty2} : - var.toSnoc.toSnoc.toMap (Γ := ((Γ.snoc t1).snoc t2)) (f := f) = - var.toMap.toSnoc.toSnoc := rfl - set_option ssa.alive_icom_reduce false in def three_inst_concrete_macro_noreduce_ne (w : Nat) := [alive_icom (w)|{ @@ -545,12 +540,19 @@ def three_inst_concrete_macro_noreduce_ne (w : Nat) := "llvm.return" (%1) : (i1) -> () }] +def three_inst_concrete_stmt_ne {a b : LLVM.IntW w} : + @BitVec.Refinement (BitVec 1) (LLVM.icmp LLVM.IntPredicate.ne a b) + (LLVM.icmp LLVM.IntPredicate.ne a b) := by simp + def three_inst_concrete_macro_noreduc_proof_ne : - three_inst_concrete_macro_noreduce_ne w ⊑ three_inst_concrete_macro_noreduce_ne w := by + three_inst_concrete_macro_noreduce_ne x ⊑ three_inst_concrete_macro_noreduce_ne x := by unfold three_inst_concrete_macro_noreduce_ne simp_alive_meta -- There remains a 'toMap' in the following expression: -- (↑↑(Ctxt.Var.last ∅ (MTy.bitvec (ConcreteOrMVar.mvar 0)))).toMap -- I am unsure why + simp only [Ctxt.Var.toSnoc_toMap'] + simp_alive_meta simp_alive_ssa - apply three_inst_concrete_stmt + intros -- Why do I need an intros? + apply three_inst_concrete_stmt_ne From 15a08dae2326a0593746b0faa26d0a66946f6bea Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 20:07:27 +0100 Subject: [PATCH 32/43] Remove diff on AliveAutoGenerated --- SSA/Projects/InstCombine/AliveAutoGenerated.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/SSA/Projects/InstCombine/AliveAutoGenerated.lean b/SSA/Projects/InstCombine/AliveAutoGenerated.lean index 20ef167fe..47ea0c61b 100644 --- a/SSA/Projects/InstCombine/AliveAutoGenerated.lean +++ b/SSA/Projects/InstCombine/AliveAutoGenerated.lean @@ -16,7 +16,7 @@ set_option pp.proofs false set_option pp.proofs.withType false set_option linter.deprecated false -set_option ssa.alive_icom_reduce true + -- Name:AddSub:1043 -- precondition: true @@ -722,7 +722,6 @@ theorem alive_AndOrXor_144 (w : Nat) : alive_AndOrXor_144_src w ⊑ alive_An -/ -- MANUAL FIX: the translation script inferred some of the resulting types to be `i1` -- where they should be the meta-variable `_` (https://github.com/opencompl/ssa/issues/169) - def alive_AndOrXor_698_src (w : Nat) := [alive_icom ( w )| { ^bb0(%a : _, %b : _, %d : _): @@ -753,10 +752,7 @@ def alive_AndOrXor_698_tgt (w : Nat) := }] theorem alive_AndOrXor_698 (w : Nat) : alive_AndOrXor_698_src w ⊑ alive_AndOrXor_698_tgt w := by unfold alive_AndOrXor_698_src alive_AndOrXor_698_tgt - simp_alive_meta - simp_alive_meta simp_alive_peephole - apply bitvec_AndOrXor_698 @@ -874,14 +870,17 @@ def alive_AndOrXor_794_src (w : Nat) := ^bb0(%a : _, %b : _): %v1 = "llvm.icmp.sgt" (%a,%b) : (_, _) -> (i1) %v2 = "llvm.icmp.ne" (%a,%b) : (_, _) -> (i1) - "llvm.return" (%v2) : (i1) -> () + %v3 = "llvm.and" (%v1,%v2) : (i1, i1) -> (i1) + "llvm.return" (%v3) : (i1) -> () }] def alive_AndOrXor_794_tgt (w : Nat) := [alive_icom ( w )| { ^bb0(%a : _, %b : _): %v1 = "llvm.icmp.sgt" (%a,%b) : (_, _) -> (i1) - "llvm.return" (%v1) : (i1) -> () + %v2 = "llvm.icmp.ne" (%a,%b) : (_, _) -> (i1) + %v3 = "llvm.icmp.sgt" (%a,%b) : (_, _) -> (i1) + "llvm.return" (%v3) : (i1) -> () }] theorem alive_AndOrXor_794 (w : Nat) : alive_AndOrXor_794_src w ⊑ alive_AndOrXor_794_tgt w := by unfold alive_AndOrXor_794_src alive_AndOrXor_794_tgt @@ -1051,7 +1050,6 @@ def alive_AndOrXor_1241_AB__AB__AB_tgt (w : Nat) := }] theorem alive_AndOrXor_1241_AB__AB__AB (w : Nat) : alive_AndOrXor_1241_AB__AB__AB_src w ⊑ alive_AndOrXor_1241_AB__AB__AB_tgt w := by unfold alive_AndOrXor_1241_AB__AB__AB_src alive_AndOrXor_1241_AB__AB__AB_tgt - simp_alive_meta simp_alive_peephole apply bitvec_AndOrXor_1241_AB__AB__AB From c47e7639adacd6014287db90981e1e12bb34b40e Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 21:22:42 +0100 Subject: [PATCH 33/43] chore: fix toSnoc_toMap --- SSA/Core/ErasedContext.lean | 17 +---------------- SSA/Projects/InstCombine/Tactic.lean | 2 ++ SSA/Projects/InstCombine/Test.lean | 7 ------- 3 files changed, 3 insertions(+), 23 deletions(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index 59619a613..c28c5c998 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -143,24 +143,9 @@ 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 -@[simp] -theorem toSnoc_toMap' {Γ : Ctxt Ty1} {t1 t2 : Ty1} {var : Ctxt.Var Γ t} {f : Ty1 → Ty2} : - var.toSnoc.toSnoc.toMap (Γ := ((Γ.snoc t1).snoc t2)) (f := f) = - var.toMap.toSnoc.toSnoc := rfl - -@[simp] -theorem toSnoc_toMap'' {Γ : Ctxt Ty1} {t1 t2 t3: Ty1} {var : Ctxt.Var Γ t} {f : Ty1 → Ty2} : - var.toSnoc.toSnoc.toSnoc.toMap (Γ := ((Γ.snoc t1).snoc t2).snoc t3) (f := f) = - var.toMap.toSnoc.toSnoc.toSnoc := rfl - -@[simp] -theorem toSnoc_toMap''' {Γ : Ctxt Ty1} {t1 t2 t3 t4: Ty1} {var : Ctxt.Var Γ t} {f : Ty1 → Ty2} : - var.toSnoc.toSnoc.toSnoc.toSnoc.toMap (Γ := (((Γ.snoc t1).snoc t2).snoc t3).snoc t4) (f := f) = - var.toMap.toSnoc.toSnoc.toSnoc.toSnoc := rfl - @[simp] theorem last_toSnoc_toMap {Γ : Ctxt Ty1} {t t2: Ty1} {f : Ty1 → Ty2} : (Ctxt.Var.last Γ t).toSnoc.toMap (f := f) (Γ := ((Γ.snoc t).snoc t2)) diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 6e8dcc6dd..34038239c 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -47,6 +47,8 @@ macro "simp_alive_meta" : tactic => 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 the `simp! only`and use a plain `simp only`? + simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_list] ) ) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 2c12fb351..e2aae7168 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -526,8 +526,6 @@ 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 - -- How can I avoid the `simp! only`and use a plain `simp only`? - simp! only [ConcreteOrMVar.instantiate_list] simp_alive_ssa apply three_inst_concrete_stmt @@ -548,11 +546,6 @@ def three_inst_concrete_macro_noreduc_proof_ne : three_inst_concrete_macro_noreduce_ne x ⊑ three_inst_concrete_macro_noreduce_ne x := by unfold three_inst_concrete_macro_noreduce_ne simp_alive_meta - -- There remains a 'toMap' in the following expression: - -- (↑↑(Ctxt.Var.last ∅ (MTy.bitvec (ConcreteOrMVar.mvar 0)))).toMap - -- I am unsure why - simp only [Ctxt.Var.toSnoc_toMap'] - simp_alive_meta simp_alive_ssa intros -- Why do I need an intros? apply three_inst_concrete_stmt_ne From b692c7b7b8fe825cea0d018cc1f607b7e89604b0 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 21:39:00 +0100 Subject: [PATCH 34/43] remove unnecessary theorem --- SSA/Core/ErasedContext.lean | 5 ----- SSA/Projects/InstCombine/Tactic.lean | 1 - 2 files changed, 6 deletions(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index c28c5c998..2e9aea2f1 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -146,11 +146,6 @@ theorem toMap_last {Γ : Ctxt Ty} {t : Ty} : (Ctxt.Var.last Γ t).toMap = Ctxt.V 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 -@[simp] -theorem last_toSnoc_toMap {Γ : Ctxt Ty1} {t t2: Ty1} {f : Ty1 → Ty2} : - (Ctxt.Var.last Γ t).toSnoc.toMap (f := f) (Γ := ((Γ.snoc t).snoc t2)) - = (Ctxt.Var.last (Ctxt.map f Γ) (f t)).toSnoc := rfl - /-- This is an induction principle that case splits on whether or not a variable is the last variable in a context. -/ @[elab_as_elim, cases_eliminator] diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 34038239c..cdf56b8ad 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -34,7 +34,6 @@ macro "simp_alive_meta" : tactic => dsimp (config := {failIfUnchanged := false }) only [Ctxt.map, Ctxt.snoc] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toSnoc_toMap] dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.toMap_last] - dsimp (config := {failIfUnchanged := false }) only [Ctxt.Var.last_toSnoc_toMap] dsimp (config := {failIfUnchanged := false }) only [Ctxt.map_cons] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.MOp.instantiateCom] dsimp (config := {failIfUnchanged := false }) only [InstcombineTransformDialect.instantiateMTy] From e3ef5db8724c4f5a5a0bbe0c4a8a3e32dafcbb73 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 21:39:54 +0100 Subject: [PATCH 35/43] fix typo --- SSA/Projects/InstCombine/Tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index cdf56b8ad..e61128cd0 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -46,7 +46,7 @@ macro "simp_alive_meta" : tactic => 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 the `simp! only`and use a plain `simp only`? + -- How can I avoid this `simp! only` and instead use a plain `simp only`? simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_list] ) ) From c100fe1986fb321d4f898f7a5628948efa3391b7 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 21:52:39 +0100 Subject: [PATCH 36/43] Fix the intro case --- SSA/Projects/InstCombine/Test.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index e2aae7168..cb7a0f1d9 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -538,14 +538,13 @@ def three_inst_concrete_macro_noreduce_ne (w : Nat) := "llvm.return" (%1) : (i1) -> () }] -def three_inst_concrete_stmt_ne {a b : LLVM.IntW w} : - @BitVec.Refinement (BitVec 1) (LLVM.icmp LLVM.IntPredicate.ne a b) - (LLVM.icmp LLVM.IntPredicate.ne a b) := by simp +def three_inst_concrete_stmt_ne (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 three_inst_concrete_macro_noreduc_proof_ne : - three_inst_concrete_macro_noreduce_ne x ⊑ three_inst_concrete_macro_noreduce_ne x := by +def three_inst_concrete_macro_noreduc_proof_ne (w : Nat) : + three_inst_concrete_macro_noreduce_ne w ⊑ three_inst_concrete_macro_noreduce_ne w := by unfold three_inst_concrete_macro_noreduce_ne simp_alive_meta simp_alive_ssa - intros -- Why do I need an intros? apply three_inst_concrete_stmt_ne From e1b7bcf4dbf386e8ff97a5892cc87932ca97dd7b Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 26 May 2024 22:17:35 +0100 Subject: [PATCH 37/43] improve formatting --- SSA/Projects/InstCombine/Test.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 4184846e2..b0190ba5d 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -470,7 +470,7 @@ def two_inst_concrete_macro_proof : simp_alive_ssa apply two_inst_concrete_stmt -def two_inst_concrete_macro_noreduc_proof : +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 @@ -530,7 +530,7 @@ def three_inst_concrete_macro_noreduc_proof : apply three_inst_concrete_stmt set_option ssa.alive_icom_reduce false in -def three_inst_concrete_macro_noreduce_ne (w : Nat) := +def two_ne_macro_noreduce (w : Nat) := [alive_icom (w)|{ ^bb0(%arg0: _, %arg1: _): %0 = "llvm.icmp.ne" (%arg0, %arg1) : (_, _) -> (i1) @@ -538,13 +538,13 @@ def three_inst_concrete_macro_noreduce_ne (w : Nat) := "llvm.return" (%1) : (i1) -> () }] -def three_inst_concrete_stmt_ne (a b : LLVM.IntW w) : +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 three_inst_concrete_macro_noreduc_proof_ne (w : Nat) : - three_inst_concrete_macro_noreduce_ne w ⊑ three_inst_concrete_macro_noreduce_ne w := by - unfold three_inst_concrete_macro_noreduce_ne +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 three_inst_concrete_stmt_ne + apply two_ne_stmt From 66928091efa8b6ca9fe133628fdf0e122c3929a1 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 27 May 2024 12:50:31 +0100 Subject: [PATCH 38/43] chore: canonicalize to ConcreteOrMVar.concrete into OfNat.ofNat --- SSA/Core/Util/ConcreteOrMVar.lean | 9 +++++---- SSA/Projects/InstCombine/AliveAutoGenerated.lean | 2 +- SSA/Projects/InstCombine/Tactic.lean | 4 ++-- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean index d9e3a1672..705d8ce91 100644 --- a/SSA/Core/Util/ConcreteOrMVar.lean +++ b/SSA/Core/Util/ConcreteOrMVar.lean @@ -48,13 +48,14 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α | .concrete w => w | .mvar i => as.get i +/-- We choose OfNat.ofNat to be our simp normal form. -/ @[simp] -def instantiate_concrete_eq (as : Vector α φ) : - (ConcreteOrMVar.concrete w).instantiate as = w := by rfl +def concrete_eq_ofNat (x : Nat) : + (ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) = (OfNat.ofNat x) := rfl @[simp] -def instantiate_list (as : Vector Nat φ) (x : Nat) : - ConcreteOrMVar.instantiate as x = x := rfl +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 < φ} : diff --git a/SSA/Projects/InstCombine/AliveAutoGenerated.lean b/SSA/Projects/InstCombine/AliveAutoGenerated.lean index 47ea0c61b..88149c27e 100644 --- a/SSA/Projects/InstCombine/AliveAutoGenerated.lean +++ b/SSA/Projects/InstCombine/AliveAutoGenerated.lean @@ -16,7 +16,7 @@ set_option pp.proofs false set_option pp.proofs.withType false set_option linter.deprecated false - +set_option ssa.alive_icom_reduce false -- Name:AddSub:1043 -- precondition: true diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index e61128cd0..0145122ac 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -42,12 +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`? - simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_list] + dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.concrete_eq_ofNat] + simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_ofNat_eq] ) ) From ffa83ab83d779a42c1c14665b7ac04a4beb08349 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 27 May 2024 13:54:11 +0100 Subject: [PATCH 39/43] remove option --- SSA/Projects/InstCombine/AliveAutoGenerated.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/AliveAutoGenerated.lean b/SSA/Projects/InstCombine/AliveAutoGenerated.lean index 88149c27e..47ea0c61b 100644 --- a/SSA/Projects/InstCombine/AliveAutoGenerated.lean +++ b/SSA/Projects/InstCombine/AliveAutoGenerated.lean @@ -16,7 +16,7 @@ set_option pp.proofs false set_option pp.proofs.withType false set_option linter.deprecated false -set_option ssa.alive_icom_reduce false + -- Name:AddSub:1043 -- precondition: true From 26826518bd8227bb08ead75ba4382bedb025f72e Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 27 May 2024 19:06:35 +0100 Subject: [PATCH 40/43] Improve formatting --- SSA/Projects/InstCombine/Test.lean | 38 +++++++++++++++++------------- 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index 8ae37061c..a20400870 100644 --- a/SSA/Projects/InstCombine/Test.lean +++ b/SSA/Projects/InstCombine/Test.lean @@ -403,15 +403,16 @@ def one_inst_concrete_macro_noreduce := }] def one_inst_concrete_com : - Com InstCombine.LLVM [InstCombine.Ty.bitvec 1] .pure (InstCombine.Ty.bitvec 1) := + 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 + @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 + one_inst_concrete_com ⊑ one_inst_concrete_com := by unfold one_inst_concrete_com simp only [simp_llvm_wrap] simp_alive_meta @@ -419,14 +420,14 @@ def one_inst_concrete_com_proof : apply one_inst_concrete_stmt def one_inst_concrete_macro_proof : - one_inst_concrete_macro ⊑ one_inst_concrete_macro := by + 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 + one_inst_concrete_macro_noreduce ⊑ one_inst_concrete_macro_noreduce := by unfold one_inst_concrete_macro_noreduce simp_alive_meta simp_alive_ssa @@ -456,10 +457,11 @@ def two_inst_concrete_com (w : ℕ) : 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 + @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 + two_inst_concrete_com w ⊑ two_inst_concrete_com w := by unfold two_inst_concrete_com simp only [simp_llvm_wrap] simp_alive_meta @@ -467,14 +469,14 @@ def two_inst_concrete_com_proof : apply two_inst_concrete_stmt def two_inst_concrete_macro_proof : - two_inst_concrete_macro ⊑ two_inst_concrete_macro := by + 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 + two_inst_concrete_macro_noreduce ⊑ two_inst_concrete_macro_noreduce := by unfold two_inst_concrete_macro_noreduce simp_alive_meta simp_alive_ssa @@ -507,11 +509,12 @@ def three_inst_concrete_com : 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 + @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 + three_inst_concrete_com ⊑ three_inst_concrete_com := by unfold three_inst_concrete_com simp only [simp_llvm_wrap] simp_alive_meta @@ -519,14 +522,14 @@ def three_inst_concrete_com_proof : apply three_inst_concrete_stmt def three_inst_concrete_macro_proof : - three_inst_concrete_macro ⊑ three_inst_concrete_macro := by + 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 + three_inst_concrete_macro_noreduce ⊑ three_inst_concrete_macro_noreduce := by unfold three_inst_concrete_macro_noreduce simp_alive_meta simp_alive_ssa @@ -542,11 +545,12 @@ def two_ne_macro_noreduce (w : Nat) := }] 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 + @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 + two_ne_macro_noreduce w ⊑ two_ne_macro_noreduce w := by unfold two_ne_macro_noreduce simp_alive_meta simp_alive_ssa From 24f47c82e824e38a5f5105b706ab9c3aa14551ee Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 27 May 2024 19:08:01 +0100 Subject: [PATCH 41/43] Improve formatting --- SSA/Core/Util/ConcreteOrMVar.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean index 705d8ce91..14d1aaa7f 100644 --- a/SSA/Core/Util/ConcreteOrMVar.lean +++ b/SSA/Core/Util/ConcreteOrMVar.lean @@ -51,11 +51,11 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α /-- We choose OfNat.ofNat to be our simp normal form. -/ @[simp] def concrete_eq_ofNat (x : Nat) : - (ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) = (OfNat.ofNat x) := rfl + (ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) = (OfNat.ofNat x) := rfl @[simp] def instantiate_ofNat_eq (as : Vector Nat φ) (x : Nat) : - ConcreteOrMVar.instantiate as (OfNat.ofNat x) = x := rfl + ConcreteOrMVar.instantiate as (OfNat.ofNat x) = x := rfl @[simp] lemma instantiate_mvar_zero {hφ : List.length (w :: ws) = φ} {h0 : 0 < φ} : From ec9ba5df002b08b194bf76bac3c404d14d88f4e8 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 27 May 2024 19:19:48 +0100 Subject: [PATCH 42/43] Flip canonical form --- SSA/Core/Util/ConcreteOrMVar.lean | 4 ++-- SSA/Projects/InstCombine/Tactic.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean index 14d1aaa7f..acbbaa8ed 100644 --- a/SSA/Core/Util/ConcreteOrMVar.lean +++ b/SSA/Core/Util/ConcreteOrMVar.lean @@ -50,8 +50,8 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α /-- We choose OfNat.ofNat to be our simp normal form. -/ @[simp] -def concrete_eq_ofNat (x : Nat) : - (ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) = (OfNat.ofNat x) := 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) : diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean index 0145122ac..bdc93176a 100644 --- a/SSA/Projects/InstCombine/Tactic.lean +++ b/SSA/Projects/InstCombine/Tactic.lean @@ -46,7 +46,7 @@ macro "simp_alive_meta" : tactic => 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.concrete_eq_ofNat] + dsimp (config := {failIfUnchanged := false }) only [ConcreteOrMVar.ofNat_eq_concrete] simp! (config := {failIfUnchanged := false }) only [ConcreteOrMVar.instantiate_ofNat_eq] ) ) From 8a7a6a859ac2e42ef23fe5d89cbe581036e79aa5 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 28 May 2024 10:34:59 +0100 Subject: [PATCH 43/43] Update SSA/Core/Util/ConcreteOrMVar.lean --- SSA/Core/Util/ConcreteOrMVar.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean index acbbaa8ed..93ff0ec9c 100644 --- a/SSA/Core/Util/ConcreteOrMVar.lean +++ b/SSA/Core/Util/ConcreteOrMVar.lean @@ -48,7 +48,7 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α | .concrete w => w | .mvar i => as.get i -/-- We choose OfNat.ofNat to be our simp normal form. -/ +/-- We choose ConcreteOrMVar.concrete to be our simp normal form. -/ @[simp] def ofNat_eq_concrete (x : Nat) : (OfNat.ofNat x) = (ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) := rfl