From 0e4a562018ec8ab47aad8b92777759019a1f5753 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 25 Oct 2023 12:22:01 +0100 Subject: [PATCH 1/2] feat: add examples from paper as a project --- SSA.lean | 1 + SSA/Core/ErasedContext.lean | 5 +- SSA/Core/Framework.lean | 8 +- SSA/Projects/PaperExamples/PaperExamples.lean | 209 ++++++++++++++++++ SSA/Projects/PaperExamples/README.md | 5 + 5 files changed, 223 insertions(+), 5 deletions(-) create mode 100644 SSA/Projects/PaperExamples/PaperExamples.lean create mode 100644 SSA/Projects/PaperExamples/README.md diff --git a/SSA.lean b/SSA.lean index 595aca576..4323deb1d 100644 --- a/SSA.lean +++ b/SSA.lean @@ -12,6 +12,7 @@ import SSA.Projects.Tensor1D.Tensor1D import SSA.Projects.Tensor2D.Tensor2D import SSA.Projects.Holor.Holor import SSA.Projects.DCE.DCE +import SSA.Projects.PaperExamples.PaperExamples -- EXPERIMENTAL diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index af8b51091..589f0e666 100644 --- a/SSA/Core/ErasedContext.lean +++ b/SSA/Core/ErasedContext.lean @@ -206,7 +206,10 @@ def Valuation (Γ : Ctxt Ty) : Type := def Valuation.eval {Γ : Ctxt Ty} (VAL : Valuation Γ) ⦃t : Ty⦄ (v : Γ.Var t) : toType t := VAL v -instance : Inhabited (Ctxt.Valuation (∅ : Ctxt Ty)) := ⟨fun _ v => v.emptyElim⟩ +/-- Make a valuation for the empty context. -/ +def Valuation.nil : Ctxt.Valuation (∅ : Ctxt Ty) := fun _ v => v.emptyElim + +instance : Inhabited (Ctxt.Valuation (∅ : Ctxt Ty)) := ⟨Valuation.nil⟩ /-- Make a valuation for `Γ.snoc t` from a valuation for `Γ` and an element of `t.toType`. -/ def Valuation.snoc {Γ : Ctxt Ty} {t : Ty} (s : Γ.Valuation) (x : toType t) : diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean index d3f151d0f..0fb9f546f 100644 --- a/SSA/Core/Framework.lean +++ b/SSA/Core/Framework.lean @@ -1162,8 +1162,8 @@ leaving behind a bare Lean level proposition to be proven. macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" ll:ident : tactic => `(tactic| ( - try simp only [ICom.denote, IExpr.denote, HVector.denote, Var.zero_eq_last, Var.succ_eq_toSnoc, - Ctxt.snoc, Ctxt.Valuation.snoc_last, Ctxt.ofList, Ctxt.Valuation.snoc_toSnoc, + try simp (config := {decide := false}) only [ICom.denote, IExpr.denote, HVector.denote, Var.zero_eq_last, Var.succ_eq_toSnoc, + Ctxt.empty, Ctxt.snoc, Ctxt.Valuation.nil, Ctxt.Valuation.snoc', Ctxt.Valuation.snoc_last, Ctxt.ofList, Ctxt.Valuation.snoc_toSnoc, HVector.map, HVector.toPair, HVector.toTuple, OpDenote.denote, IExpr.op_mk, IExpr.args_mk, $ts,*] generalize $ll { val := 0, property := _ } = a; generalize $ll { val := 1, property := _ } = b; @@ -1171,7 +1171,7 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" ll:ident : generalize $ll { val := 3, property := _ } = d; generalize $ll { val := 4, property := _ } = e; generalize $ll { val := 5, property := _ } = f; - simp [Goedel.toType] at a b c d e f; + try simp (config := {decide := false}) [Goedel.toType] at a b c d e f; try clear f; try clear e; try clear d; @@ -1217,7 +1217,7 @@ inductive ExOp : Type | add : ExOp | beq : ExOp | cst : ℕ → ExOp - deriving DecidableEq + deriving DecidableEq, Repr instance : OpSignature ExOp ExTy where signature diff --git a/SSA/Projects/PaperExamples/PaperExamples.lean b/SSA/Projects/PaperExamples/PaperExamples.lean new file mode 100644 index 000000000..4517685d9 --- /dev/null +++ b/SSA/Projects/PaperExamples/PaperExamples.lean @@ -0,0 +1,209 @@ +import Mathlib.Logic.Function.Iterate +import SSA.Core.Framework +import SSA.Core.Util + +set_option pp.proofs false +set_option pp.proofs.withType false + +open Std (BitVec) +open Ctxt(Var) + +namespace ToyNoRegion + +inductive Ty + | int + deriving DecidableEq, Repr + +@[reducible] +instance : Goedel Ty where + toType + | .int => BitVec 32 + +inductive Op : Type + | add : Op + | const : (val : ℤ) → Op + deriving DecidableEq, Repr + +instance : OpSignature Op Ty where + signature + | .const _ => ⟨[], [], .int⟩ + | .add => ⟨[.int, .int], [], .int⟩ + +@[reducible] +instance : OpDenote Op Ty where + denote + | .const n, _, _ => BitVec.ofInt 32 n + | .add, .cons (a : BitVec 32) (.cons (b : BitVec 32) .nil), _ => a + b + +def cst {Γ : Ctxt _} (n : ℤ) : IExpr Op Γ .int := + IExpr.mk + (op := .const n) + (ty_eq := rfl) + (args := .nil) + (regArgs := .nil) + +def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int := + IExpr.mk + (op := .add) + (ty_eq := rfl) + (args := .cons e₁ <| .cons e₂ .nil) + (regArgs := .nil) + +attribute [local simp] Ctxt.snoc + +/-- x + 0 -/ +def lhs : ICom Op (Ctxt.ofList [.int]) .int := + -- %c0 = 0 + ICom.lete (cst 0) <| + -- %out = %x + %c0 + ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| + -- return %out + ICom.ret ⟨0, by simp [Ctxt.snoc]⟩ + +/-- x -/ +def rhs : ICom Op (Ctxt.ofList [.int]) .int := + ICom.ret ⟨0, by simp⟩ + +def p1 : PeepholeRewrite Op [.int] .int := + { lhs := lhs, rhs := rhs, correct := + by + rw [lhs, rhs] + /- + ICom.denote + (ICom.lete (cst 0) + (ICom.lete (add { val := 1, property := _ } { val := 0, property := _ }) + (ICom.ret { val := 0, property := ex1.proof_3 }))) = + ICom.denote (ICom.ret { val := 0, property := _ }) + -/ + funext Γv + simp_peephole [add, cst] at Γv + /- ⊢ ∀ (a : BitVec 32), a + BitVec.ofInt 32 0 = a -/ + intros a + ring + /- goals accomplished 🎉 -/ + sorry + } + +def ex1' : ICom Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs + + +theorem EX1' : ex1' = ( + -- %c0 = 0 + ICom.lete (cst 0) <| + -- %out_dead = %x + %c0 + ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0 + -- ret %c0 + ICom.ret ⟨2, by simp [Ctxt.snoc]⟩) + := by rfl + +end ToyNoRegion + +namespace ToyRegion + +inductive Ty + | int + deriving DecidableEq, Repr + +@[reducible] +instance : Goedel Ty where + toType + | .int => BitVec 32 + +inductive Op : Type + | add : Op + | const : (val : ℤ) → Op + | iterate (k : ℕ) : Op + deriving DecidableEq, Repr + +instance : OpSignature Op Ty where + signature + | .const _ => ⟨[], [], .int⟩ + | .add => ⟨[.int, .int], [], .int⟩ + | .iterate _k => ⟨[.int], [([.int], .int)], .int⟩ + +@[reducible] +instance : OpDenote Op Ty where + denote + | .const n, _, _ => BitVec.ofInt 32 n + | .add, .cons (a : BitVec 32) (.cons (b : BitVec 32) .nil), _ => a + b + | .iterate k, (.cons (x : BitVec 32) .nil), (.cons (f : _ → BitVec 32) .nil) => + let f' (v : BitVec 32) : BitVec 32 := f (Ctxt.Valuation.nil.snoc' v) + k.iterate f' x + -- let f_k := Nat.iterate f' k + -- f_k x + +def cst {Γ : Ctxt _} (n : ℤ) : IExpr Op Γ .int := + IExpr.mk + (op := .const n) + (ty_eq := rfl) + (args := .nil) + (regArgs := .nil) + +def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int := + IExpr.mk + (op := .add) + (ty_eq := rfl) + (args := .cons e₁ <| .cons e₂ .nil) + (regArgs := .nil) + +def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : ICom Op [.int] .int) : IExpr Op Γ .int := + IExpr.mk + (op := .iterate k) + (ty_eq := rfl) + (args := .cons input .nil) + (regArgs := HVector.cons body HVector.nil) + +attribute [local simp] Ctxt.snoc + +/-- running `f(x) = x + x` 0 times is the identity. -/ +def lhs : ICom Op [.int] .int := + ICom.lete (iterate (k := 0) ⟨0, by simp[Ctxt.snoc]⟩ ( + ICom.lete (add ⟨0, by simp[Ctxt.snoc]⟩ ⟨0, by simp[Ctxt.snoc]⟩) -- fun x => (x + x) + <| ICom.ret ⟨0, by simp[Ctxt.snoc]⟩ + )) <| + ICom.ret ⟨0, by simp[Ctxt.snoc]⟩ + +def rhs : ICom Op [.int] .int := + ICom.ret ⟨0, by simp[Ctxt.snoc]⟩ + +attribute [local simp] Ctxt.snoc + +@[simp] +theorem Ctxt.Valuation.snoc_last [Goedel Ty] {ty : Ty} (Γ : Ctxt Ty) (V : Γ.Valuation) (v : Goedel.toType ty): + (Ctxt.Valuation.snoc V v) (Ctxt.Var.last _ _) = v := rfl +set_option pp.proofs false in +set_option pp.proofs.withType false in +def p1 : PeepholeRewrite Op [.int] .int:= + { lhs := lhs, rhs := rhs, correct := by + rw [lhs, rhs] + funext Γv + /- + ICom.denote + (ICom.lete + (iterate 0 { val := 0, property := lhs.proof_1 } + (ICom.lete (add { val := 0, property := lhs.proof_1 } { val := 0, property := lhs.proof_1 }) + (ICom.ret { val := 0, property := lhs.proof_2 }))) + (ICom.ret { val := 0, property := lhs.proof_2 })) + Γv = + ICom.denote (ICom.ret { val := 0, property := rhs.proof_1 }) Γv + -/ + simp_peephole [add, iterate] at Γv + /- ∀ (a : BitVec 32), (fun v => v + v)^[0] a = a -/ + simp [Function.iterate_zero] + done + } + +/- +def ex1' : ICom Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs + +theorem EX1' : ex1' = ( + -- %c0 = 0 + ICom.lete (cst 0) <| + -- %out_dead = %x + %c0 + ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0 + -- ret %c0 + ICom.ret ⟨2, by simp [Ctxt.snoc]⟩) + := by rfl +-/ + +end ToyRegion diff --git a/SSA/Projects/PaperExamples/README.md b/SSA/Projects/PaperExamples/README.md new file mode 100644 index 000000000..9a1a6aedf --- /dev/null +++ b/SSA/Projects/PaperExamples/README.md @@ -0,0 +1,5 @@ +# Paper Examples + +This folder has the simple examples we use in the paper to motivate +the framework. + From f04071cf7bd57d9095a06b92ef9f318ce4f07093 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Goens?= Date: Thu, 26 Oct 2023 17:44:16 +0200 Subject: [PATCH 2/2] ICom/IExpr -> Com/Expr --- SSA/Projects/PaperExamples/PaperExamples.lean | 84 +++++++++---------- 1 file changed, 42 insertions(+), 42 deletions(-) diff --git a/SSA/Projects/PaperExamples/PaperExamples.lean b/SSA/Projects/PaperExamples/PaperExamples.lean index 4517685d9..575c6a594 100644 --- a/SSA/Projects/PaperExamples/PaperExamples.lean +++ b/SSA/Projects/PaperExamples/PaperExamples.lean @@ -35,15 +35,15 @@ instance : OpDenote Op Ty where | .const n, _, _ => BitVec.ofInt 32 n | .add, .cons (a : BitVec 32) (.cons (b : BitVec 32) .nil), _ => a + b -def cst {Γ : Ctxt _} (n : ℤ) : IExpr Op Γ .int := - IExpr.mk +def cst {Γ : Ctxt _} (n : ℤ) : Expr Op Γ .int := + Expr.mk (op := .const n) (ty_eq := rfl) (args := .nil) (regArgs := .nil) -def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int := - IExpr.mk +def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : Expr Op Γ .int := + Expr.mk (op := .add) (ty_eq := rfl) (args := .cons e₁ <| .cons e₂ .nil) @@ -52,28 +52,28 @@ def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int := attribute [local simp] Ctxt.snoc /-- x + 0 -/ -def lhs : ICom Op (Ctxt.ofList [.int]) .int := +def lhs : Com Op (Ctxt.ofList [.int]) .int := -- %c0 = 0 - ICom.lete (cst 0) <| + Com.lete (cst 0) <| -- %out = %x + %c0 - ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| + Com.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- return %out - ICom.ret ⟨0, by simp [Ctxt.snoc]⟩ + Com.ret ⟨0, by simp [Ctxt.snoc]⟩ /-- x -/ -def rhs : ICom Op (Ctxt.ofList [.int]) .int := - ICom.ret ⟨0, by simp⟩ +def rhs : Com Op (Ctxt.ofList [.int]) .int := + Com.ret ⟨0, by simp⟩ def p1 : PeepholeRewrite Op [.int] .int := { lhs := lhs, rhs := rhs, correct := by rw [lhs, rhs] /- - ICom.denote - (ICom.lete (cst 0) - (ICom.lete (add { val := 1, property := _ } { val := 0, property := _ }) - (ICom.ret { val := 0, property := ex1.proof_3 }))) = - ICom.denote (ICom.ret { val := 0, property := _ }) + Com.denote + (Com.lete (cst 0) + (Com.lete (add { val := 1, property := _ } { val := 0, property := _ }) + (Com.ret { val := 0, property := ex1.proof_3 }))) = + Com.denote (Com.ret { val := 0, property := _ }) -/ funext Γv simp_peephole [add, cst] at Γv @@ -84,16 +84,16 @@ def p1 : PeepholeRewrite Op [.int] .int := sorry } -def ex1' : ICom Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs +def ex1' : Com Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs theorem EX1' : ex1' = ( -- %c0 = 0 - ICom.lete (cst 0) <| + Com.lete (cst 0) <| -- %out_dead = %x + %c0 - ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0 + Com.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0 -- ret %c0 - ICom.ret ⟨2, by simp [Ctxt.snoc]⟩) + Com.ret ⟨2, by simp [Ctxt.snoc]⟩) := by rfl end ToyNoRegion @@ -132,22 +132,22 @@ instance : OpDenote Op Ty where -- let f_k := Nat.iterate f' k -- f_k x -def cst {Γ : Ctxt _} (n : ℤ) : IExpr Op Γ .int := - IExpr.mk +def cst {Γ : Ctxt _} (n : ℤ) : Expr Op Γ .int := + Expr.mk (op := .const n) (ty_eq := rfl) (args := .nil) (regArgs := .nil) -def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : IExpr Op Γ .int := - IExpr.mk +def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : Expr Op Γ .int := + Expr.mk (op := .add) (ty_eq := rfl) (args := .cons e₁ <| .cons e₂ .nil) (regArgs := .nil) -def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : ICom Op [.int] .int) : IExpr Op Γ .int := - IExpr.mk +def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : Com Op [.int] .int) : Expr Op Γ .int := + Expr.mk (op := .iterate k) (ty_eq := rfl) (args := .cons input .nil) @@ -156,15 +156,15 @@ def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Ty.int) (body : ICom Op [.in attribute [local simp] Ctxt.snoc /-- running `f(x) = x + x` 0 times is the identity. -/ -def lhs : ICom Op [.int] .int := - ICom.lete (iterate (k := 0) ⟨0, by simp[Ctxt.snoc]⟩ ( - ICom.lete (add ⟨0, by simp[Ctxt.snoc]⟩ ⟨0, by simp[Ctxt.snoc]⟩) -- fun x => (x + x) - <| ICom.ret ⟨0, by simp[Ctxt.snoc]⟩ +def lhs : Com Op [.int] .int := + Com.lete (iterate (k := 0) ⟨0, by simp[Ctxt.snoc]⟩ ( + Com.lete (add ⟨0, by simp[Ctxt.snoc]⟩ ⟨0, by simp[Ctxt.snoc]⟩) -- fun x => (x + x) + <| Com.ret ⟨0, by simp[Ctxt.snoc]⟩ )) <| - ICom.ret ⟨0, by simp[Ctxt.snoc]⟩ + Com.ret ⟨0, by simp[Ctxt.snoc]⟩ -def rhs : ICom Op [.int] .int := - ICom.ret ⟨0, by simp[Ctxt.snoc]⟩ +def rhs : Com Op [.int] .int := + Com.ret ⟨0, by simp[Ctxt.snoc]⟩ attribute [local simp] Ctxt.snoc @@ -178,14 +178,14 @@ def p1 : PeepholeRewrite Op [.int] .int:= rw [lhs, rhs] funext Γv /- - ICom.denote - (ICom.lete + Com.denote + (Com.lete (iterate 0 { val := 0, property := lhs.proof_1 } - (ICom.lete (add { val := 0, property := lhs.proof_1 } { val := 0, property := lhs.proof_1 }) - (ICom.ret { val := 0, property := lhs.proof_2 }))) - (ICom.ret { val := 0, property := lhs.proof_2 })) + (Com.lete (add { val := 0, property := lhs.proof_1 } { val := 0, property := lhs.proof_1 }) + (Com.ret { val := 0, property := lhs.proof_2 }))) + (Com.ret { val := 0, property := lhs.proof_2 })) Γv = - ICom.denote (ICom.ret { val := 0, property := rhs.proof_1 }) Γv + Com.denote (Com.ret { val := 0, property := rhs.proof_1 }) Γv -/ simp_peephole [add, iterate] at Γv /- ∀ (a : BitVec 32), (fun v => v + v)^[0] a = a -/ @@ -194,15 +194,15 @@ def p1 : PeepholeRewrite Op [.int] .int:= } /- -def ex1' : ICom Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs +def ex1' : Com Op (Ctxt.ofList [.int]) .int := rewritePeepholeAt p1 1 lhs theorem EX1' : ex1' = ( -- %c0 = 0 - ICom.lete (cst 0) <| + Com.lete (cst 0) <| -- %out_dead = %x + %c0 - ICom.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0 + Com.lete (add ⟨1, by simp [Ctxt.snoc]⟩ ⟨0, by simp [Ctxt.snoc]⟩ ) <| -- %out = %x + %c0 -- ret %c0 - ICom.ret ⟨2, by simp [Ctxt.snoc]⟩) + Com.ret ⟨2, by simp [Ctxt.snoc]⟩) := by rfl -/