From ce6329c031fa98cd385356608a872965fa5e65f9 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Tue, 16 Apr 2024 16:50:27 +0200
Subject: [PATCH 01/22] chore: drop unnecessary open

This is factored out from https://github.com/opencompl/ssa/pull/191 to minimize
the diff to main.
---
 SSA/Projects/InstCombine/Tactic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
index 36e524687..1136b7bfb 100644
--- a/SSA/Projects/InstCombine/Tactic.lean
+++ b/SSA/Projects/InstCombine/Tactic.lean
@@ -9,7 +9,6 @@ import Std.Data.BitVec
 import Mathlib.Data.BitVec.Lemmas
 
 open MLIR AST
-open Std (BitVec)
 open Ctxt
 
 /--

From 4a3fb48252975f92aefff5437f2867b1709445c0 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 16 Apr 2024 16:38:24 +0100
Subject: [PATCH 02/22] feat: add Op.denote as a OpDenote instance for FHE
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Andrés Goens <andres@goens.org>
---
 .../FullyHomomorphicEncryption/Basic.lean     | 27 +++++++++----------
 1 file changed, 13 insertions(+), 14 deletions(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
index 96165aa11..272de42e9 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
@@ -9,6 +9,7 @@ For the rationale behind this, see:
  Junfeng Fan and Frederik Vercauteren, Somewhat Practical Fully Homomorphic Encryption
 https://eprint.iacr.org/2012/144
 
+Authors: Andrés Goens<andres@goens.org>, Siddharth Bhat<siddu.druid@gmail.com>
 -/
 import Mathlib.RingTheory.Polynomial.Quotient
 import Mathlib.RingTheory.Ideal.Quotient
@@ -696,17 +697,15 @@ def Op.signature : Op q n → Signature (Ty q n) :=
 instance : OpSignature (Op q n) (Ty q n) := ⟨Op.signature q n⟩
 
 @[simp]
-noncomputable def Op.denote (o : Op q n)
-   (arg : HVector toType (OpSignature.sig o))
-   : (toType <| OpSignature.outTy o) :=
-    match o with
-    | Op.add => (fun args : R q n × R q n => args.1 + args.2) arg.toPair
-    | Op.sub => (fun args : R q n × R q n => args.1 - args.2) arg.toPair
-    | Op.mul => (fun args : R q n × R q n => args.1 * args.2) arg.toPair
-    | Op.mul_constant => (fun args : R q n × Int => args.1 * ↑(args.2)) arg.toPair
-    | Op.leading_term => R.leadingTerm arg.toSingle
-    | Op.monomial => (fun args => R.monomial ↑(args.1) args.2) arg.toPair
-    | Op.monomial_mul => (fun args : R q n × Nat => args.1 * R.monomial 1 args.2) arg.toPair
-    | Op.from_tensor => R.fromTensor arg.toSingle
-    | Op.to_tensor => R.toTensor' arg.toSingle
-    | Op.const c => c
+noncomputable instance : OpDenote (Op q n) (Ty q n) where
+    denote
+    | Op.add, arg, _ => (fun args : R q n × R q n => args.1 + args.2) arg.toPair
+    | Op.sub, arg, _ => (fun args : R q n × R q n => args.1 - args.2) arg.toPair
+    | Op.mul, arg, _ => (fun args : R q n × R q n => args.1 * args.2) arg.toPair
+    | Op.mul_constant, arg, _ => (fun args : R q n × Int => args.1 * ↑(args.2)) arg.toPair
+    | Op.leading_term, arg, _ => R.leadingTerm arg.toSingle
+    | Op.monomial, arg, _ => (fun args => R.monomial ↑(args.1) args.2) arg.toPair
+    | Op.monomial_mul, arg, _ => (fun args : R q n × Nat => args.1 * R.monomial 1 args.2) arg.toPair
+    | Op.from_tensor, arg, _ => R.fromTensor arg.toSingle
+    | Op.to_tensor, arg, _ => R.toTensor' arg.toSingle
+    | Op.const c, _arg, _ => c

From 6a4c3ef7fadcb267d3aa82aba8807b34167fc3d3 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 16 Apr 2024 13:56:20 +0100
Subject: [PATCH 03/22] refactor: generalize `simp_alive_case_bash` to an
 arbitrary number of variables

Also, introduce a new simp-set, and squeeze the simp used in
`simp_alive_case_bash`
---
 SSA/Projects/InstCombine/LLVM/SimpSet.lean |  3 ++
 SSA/Projects/InstCombine/Tactic.lean       | 61 ++++++++++------------
 2 files changed, 30 insertions(+), 34 deletions(-)

diff --git a/SSA/Projects/InstCombine/LLVM/SimpSet.lean b/SSA/Projects/InstCombine/LLVM/SimpSet.lean
index b053fdae4..34aabd6ab 100644
--- a/SSA/Projects/InstCombine/LLVM/SimpSet.lean
+++ b/SSA/Projects/InstCombine/LLVM/SimpSet.lean
@@ -4,3 +4,6 @@ import Lean.LabelAttribute
 
 register_simp_attr simp_llvm
 register_simp_attr simp_llvm_option
+
+/-- The simp-set used in `simp_alive_case_bash` to attempt to discharge trivial `none` cases -/
+register_simp_attr simp_llvm_case_bash
diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
index 1136b7bfb..b13ca3767 100644
--- a/SSA/Projects/InstCombine/Tactic.lean
+++ b/SSA/Projects/InstCombine/Tactic.lean
@@ -1,4 +1,5 @@
 import SSA.Projects.InstCombine.LLVM.EDSL
+import SSA.Projects.InstCombine.LLVM.SimpSet
 import SSA.Projects.InstCombine.AliveStatements
 import SSA.Projects.InstCombine.Refinement
 import SSA.Projects.InstCombine.ForStd
@@ -11,49 +12,41 @@ import Mathlib.Data.BitVec.Lemmas
 open MLIR AST
 open Ctxt
 
+attribute [simp_llvm_case_bash]
+  BitVec.Refinement.refl BitVec.Refinement.some_some BitVec.Refinement.none_left
+  bind_assoc forall_const
+  Option.bind_eq_bind Option.none_bind Option.bind_none Option.some_bind Option.pure_def
+  BitVec.reduceOfInt Nat.cast_one
+/- `reduceOfInt` and `Nat.cast_one` are somewhat questionable additions to this simp-set.
+   They are not needed for the case-bashing to succeed, but they are simp-lemmas that were
+   previously being applied in `AliveAutoGenerated`, where they closed a few trivial goals,
+   so they've been preserved to not change this existing behaviour of `simp_alive_case_bash` -/
+
 /--
 `simp_alive_case_bash` transforms a goal of the form
   `∀ (x₁ : Option (BitVec _)) ... (xₙ : Option (BitVec _)), ...`
-(for some number of variables `n ≤ 5`, following the hack in `simp_peephole`)
 into a goal about just `BitVec`s, by doing a case distinction on each `Option`.
 
 Then, we `simp`lify each goal, following the assumption that the `none` cases
 should generally be trivial, hopefully leaving us with just a single goal:
 the one where each option is `some`. -/
-macro "simp_alive_case_bash" : tactic =>
-  `(tactic|
-    (
-      /- Attempt to introduce up to 5 variables (using `try` because the intro might fail if
-         the goal has less than 5 universal quantifiers)
-
-        case split on them, and simp
-          through the monadic bind on `Option` (in the generally true assumption that the `none`
-            case becomes trivial and is closed by `simp`). -/
-      try intros v0; try intros v1; try intros v2; try intros v3; try intros v4
-
-      /- Then, case split on each variable, and `simp` through the monadic bind on `Option`
-         (in the hope that the `none` case becomes trivial and is immediately closed) -/
-      try cases' v0 with x0 <;> simp [Option.bind, bind, Monad.toBind]
-          <;> try cases' v1 with x1 <;> simp [Option.bind, bind, Monad.toBind]
-          <;> try cases' v2 with x2 <;> simp [Option.bind, bind, Monad.toBind]
-          <;> try cases' v3 with x3 <;> simp [Option.bind, bind, Monad.toBind]
-          <;> try cases' v4 with x4 <;> simp [Option.bind, bind, Monad.toBind]
-          <;> try cases' v5 with x5 <;> simp [Option.bind, bind, Monad.toBind]
-          <;> dsimp [Option.bind, bind, Monad.toBind]
-
-      /- Revert the variables introduced in the `some` cases, so that we are left with
-         a universally quantified goal of the form:
-         `∀ (x₁ : BitVec _) ... (xₙ : BitVec _), ...` -/
-      try revert x5
-      try revert x4
-      try revert x3
-      try revert x2
-      try revert x1
-      try revert x0
-
-      try revert w
+syntax "simp_alive_case_bash" : tactic
+macro_rules
+  | `(tactic| simp_alive_case_bash) => `(tactic|
+    first
+    | fail_if_success (intro (v : Option (_)))
+      -- If there is no variable to introduce, `intro` fails, so the first branch succeeds,
+      -- but does nothing. This is similar to `try`, except `first ...` does not swallow any errors
+      -- that occur in the later tactics
+    | intro (v : Option (_))    -- Introduce the variable,
+      rcases v with _|x         -- Do the case distinction
+      <;> simp (config:={failIfUnchanged := false}) only [simp_llvm_case_bash]
+      --  ^^^^^^^^^^^^^^^^^^^^^^^^ Simplify, in the hopes that the `none` case is trivially closed
+      <;> simp_alive_case_bash  -- Recurse, to case bash the next variable (if it exists)
+      <;> (try revert x)        -- Finally, revert the variable we got in the `some` case, so that
+                                --   we are left with a universally quantified goal of the form:
+                                --   `∀ (x₁ : BitVec _) ... (xₙ : BitVec _), ...`
     )
-  )
 
 /-- Eliminate the SSA structure of the program
 - We first simplify `Com.refinement` to see the context `Γv`.

From be19f03db72f2ec74f7e38cc4b9511b1aada9f49 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 16 Apr 2024 17:05:58 +0100
Subject: [PATCH 04/22] feat: Implement [fhe_icom|...] to write FHE examples
 with sugar.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Andrés Goens <andres@goens.org>

Code peeled from pre-paper submission PR: https://github.com/opencompl/ssa/pull/196.
Code stacked on: https://github.com/opencompl/ssa/pull/230.
---
 SSA/Projects/FullyHomomorphicEncryption.lean  |   4 +-
 .../FullyHomomorphicEncryption/Basic.lean     |   2 +-
 .../FullyHomomorphicEncryption/Rewrites.lean  |  81 +++++++----
 .../FullyHomomorphicEncryption/Syntax.lean    | 127 ++++++++++++++++++
 4 files changed, 187 insertions(+), 27 deletions(-)
 create mode 100644 SSA/Projects/FullyHomomorphicEncryption/Syntax.lean

diff --git a/SSA/Projects/FullyHomomorphicEncryption.lean b/SSA/Projects/FullyHomomorphicEncryption.lean
index 22ca1cd7b..2d3707dba 100644
--- a/SSA/Projects/FullyHomomorphicEncryption.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption.lean
@@ -1,2 +1,4 @@
 import SSA.Projects.FullyHomomorphicEncryption.Basic
-import SSA.Projects.FullyHomomorphicEncryption.Statements
\ No newline at end of file
+import SSA.Projects.FullyHomomorphicEncryption.Rewrites
+import SSA.Projects.FullyHomomorphicEncryption.Statements
+import SSA.Projects.FullyHomomorphicEncryption.Syntax
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
index 272de42e9..8924b60da 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
@@ -640,7 +640,7 @@ inductive Ty (q : Nat) (n : Nat) [Fact (q > 1)]
   | integer : Ty q n
   | tensor : Ty q n
   | polynomialLike : Ty q n
-  deriving DecidableEq
+  deriving DecidableEq, Repr
 
 instance : Inhabited (Ty q n) := ⟨Ty.index⟩
 instance : TyDenote (Ty q n) where
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
index 05d65dd03..8aaee5a2d 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -1,43 +1,74 @@
+/-
+End-to-end showcase of the framework for verifying rewrites about FHE semantics.
+
+Authors: Andrés Goens<andres@goens.org>
+-/
+import SSA.Projects.MLIRSyntax.EDSL
+import SSA.Core.Tactic
 import SSA.Projects.FullyHomomorphicEncryption.Basic
 import SSA.Projects.FullyHomomorphicEncryption.Statements
-import SSA.Projects.MLIRSyntax.EDSL
+import SSA.Projects.FullyHomomorphicEncryption.Syntax
 
-theorem dialect_mul_comm :
-[mlir_icom| {
-^bb0(%A : P, %B : P):
-  %v1 = "poly.mul" (%A,%B) : (P, P) -> (P)
-  "poly.return" (%v1) : (P) -> ()
-}] = 
-[mlir_icom| {
-^bb0(%A : P, %B : P):
-  %v1 = "poly.mul" (%A,%B) : (P, P) -> (P)
-  "poly.return" (%v1) : (P) -> ()
-}]=  := by
-  simp_mlir
-  apply poly_mul_comm
-
-theorem dialect_add_comm : a + b = b + a := by
-  ring
+open Ctxt (Var Valuation DerivedCtxt)
 
+open MLIR AST -- need this to support the unhygenic macros in the EDSL
+
+/- Lemmas about the elements of the quotient ring. -/
+namespace RingLemmas
+
+/-- In the quotient ring, (f q n) = 0. -/
 theorem dialect_f_eq_zero : (f q n) = (0 : R q n) := by
   apply Ideal.Quotient.eq_zero_iff_mem.2
   rw [Ideal.mem_span_singleton]
 
-theorem dialect_mul_f_eq_zero : a * (f q n) = 0 := by
+/-- Since (f q n) = 0, anything multiplied by it is also zero. -/
+theorem dialect_mul_f_eq_zero (a : R q n) : a * (f q n) = 0 := by
   rw [dialect_f_eq_zero]; ring
 
-theorem dialect_mul_one_eq : 1 * a = a := by
-  ring
-
-theorem dialect_add_f_eq : a + (f q n) = a := by
-  rw [← dialect_mul_one_eq q n (f q n), dialect_mul_f_eq_zero _ _ 1]; ring
+/-- Since (f q n) = 0, adding it to any element gives the element itself. -/
+theorem dialect_add_f_eq (a : R q n) : a + (f q n) = a := by
+  rw [← one_mul a, dialect_f_eq_zero]; ring
 
-theorem dialect_add_zero_eq : a + 0 = a := by
-  ring
+end RingLemmas
 
 
+namespace ExampleComm
 
+variable {q : Nat} {n : Nat} [hq : Fact (q > 1)]
 
+def lhs :=
+[fhe_com q, n, hq| {
+^bb0(%A : ! R, %B : ! R):
+  %v1 = "poly.add" (%A,%B) : (! R, ! R) -> (! R)
+  "return" (%v1) : (! R) -> ()
+}]
 
+def rhs :=
+[fhe_com q, n, hq| {
+^bb0(%A : ! R, %B : ! R):
+  %v1 = "poly.add" (%B,%A) : (! R, ! R) -> (! R)
+  "return" (%v1) : (! R) -> ()
+}]
 
+open MLIR AST in
+noncomputable def p1 : PeepholeRewrite (Op q n) [.polynomialLike, .polynomialLike] .polynomialLike :=
+  { lhs := lhs, rhs := rhs, correct :=
+    by
+      rw [lhs, rhs]
+      /-:
+      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 [] at Γv
+      /- ⊢ ∀ (a b : R 2 3), b + a = a + b -/
+      intros a b
+      rw [add_comm]
+      /- No goals-/
+      done
+    }
 
+end ExampleComm
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
new file mode 100644
index 000000000..6a056e616
--- /dev/null
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -0,0 +1,127 @@
+/-
+Syntax definitions for FHE, providing a custom [fhe_com|...] with syntax sugar.
+
+Authors: Andrés Goens<andres@goens.org>
+-/
+import SSA.Projects.InstCombine.LLVM.Transform
+import SSA.Projects.MLIRSyntax.AST
+import SSA.Projects.MLIRSyntax.EDSL
+import SSA.Projects.FullyHomomorphicEncryption.Basic
+
+open MLIR AST Ctxt
+open Polynomial -- for R[X] notation
+
+section MkFuns
+variable {q : Nat} {n : Nat} [Fact (q > 1)]
+
+def mkTy : MLIR.AST.MLIRType φ → MLIR.AST.ExceptM (Op q n) (Ty q n)
+  | MLIR.AST.MLIRType.undefined "R" => do
+    return .polynomialLike
+  | MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless _ => do
+    return .integer
+  | MLIR.AST.MLIRType.index  => do
+    return .index
+  | _ => throw .unsupportedType
+
+instance instTransformTy : MLIR.AST.TransformTy (Op q n) (Ty q n) 0 where
+  mkTy := mkTy
+
+def add {Γ : Ctxt (Ty q n)} (e₁ e₂ : Var Γ .polynomialLike) : Expr (Op q n) Γ .polynomialLike :=
+  Expr.mk
+    (op := .add)
+    (ty_eq := rfl)
+    (args := .cons e₁ <| .cons e₂ .nil)
+    (regArgs := .nil)
+
+def mul {Γ : Ctxt (Ty q n)} (e₁ e₂ : Var Γ .polynomialLike) : Expr (Op q n) Γ .polynomialLike :=
+  Expr.mk
+    (op := .mul)
+    (ty_eq := rfl)
+    (args := .cons e₁ <| .cons e₂ .nil)
+    (regArgs := .nil)
+
+def mon {Γ : Ctxt (Ty q n)} (a : Var Γ .integer) (i : Var Γ .index) : Expr (Op q n) Γ .polynomialLike :=
+  Expr.mk
+    (op := .monomial)
+    (ty_eq := rfl)
+    (args := .cons a <| .cons i .nil)
+    (regArgs := .nil)
+
+def mkExpr (Γ : Ctxt (Ty q n)) (opStx : MLIR.AST.Op 0) :
+    MLIR.AST.ReaderM (Op q n) (Σ ty, Expr (Op q n) Γ ty) := do
+  match opStx.name with
+  | "poly.monomial" =>
+    match opStx.args with
+    | v₁Stx::v₂Stx::[] =>
+      let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx
+      let ⟨ty₂, v₂⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₂Stx
+      match ty₁, ty₂ with
+        | .integer, .index => return ⟨.polynomialLike, mon v₁ v₂⟩
+        | _, _ => throw <| .generic s!"expected operands to be of types `integer` and `index` for `monomial`. Got: {repr ty₁}, {repr ty₂}"
+    | _ => throw <| .generic s!"expected two operands for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'"
+  | "poly.add" =>
+    match opStx.args with
+    | v₁Stx::v₂Stx::[] =>
+      let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx
+      let ⟨ty₂, v₂⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₂Stx
+      match ty₁, ty₂ with
+        | .polynomialLike, .polynomialLike => return ⟨.polynomialLike, add v₁ v₂⟩
+        | _, _ => throw <| .generic s!"expected both operands to be of type 'polynomialLike'"
+    | _ => throw <| .generic s!"expected two operands for `add`, found #'{opStx.args.length}' in '{repr opStx.args}'"
+  | _ => throw <| .unsupportedOp s!"unsupported operation {repr opStx}"
+
+instance : MLIR.AST.TransformExpr (Op q n) (Ty q n) 0 where
+  mkExpr := mkExpr
+
+def mkReturn (Γ : Ctxt (Ty q n)) (opStx : MLIR.AST.Op 0) : MLIR.AST.ReaderM (Op q n) (Σ ty, Com (Op q n) Γ ty) :=
+  if opStx.name == "return"
+  then match opStx.args with
+  | vStx::[] => do
+    let ⟨ty, v⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ vStx
+    return ⟨ty, Com.ret v⟩
+  | _ => throw <| .generic s!"Ill-formed return statement (wrong arity, expected 1, got {opStx.args.length})"
+  else throw <| .generic s!"Tried to build return out of non-return statement {opStx.name}"
+
+instance : MLIR.AST.TransformReturn (Op q n) (Ty q n) 0 where
+  mkReturn := mkReturn
+
+def mlir2fhe (reg : MLIR.AST.Region 0) :
+    MLIR.AST.ExceptM (Op q n) (Σ (Γ : Ctxt (Ty q n)) (ty : (Ty q n)), Com (Op q n) Γ ty) := MLIR.AST.mkCom reg
+
+end MkFuns -- we don't want q and i here anymore
+
+open Qq MLIR AST Lean Elab Term Meta in
+/--
+NOTE: Wanting Stuck Terms During Strong Normalization of Com
+
+See that we unfold with `TransparencyMode.all`. We do this so we can expose Com.denote
+fully. This is a crazy hack, and interacts extremely poorly with complex definitions found in FHE.
+
+One neater solution is a `match goal` like tactic to match on the proof state
+and run the correct equation.
+-/
+elab "[fhe_com" qi:term "," ni:term "," hq:term " | " reg:mlir_region "]" : term => do
+  let ast_stx ← `([mlir_region| $reg])
+  let ast ← elabTermEnsuringTypeQ ast_stx q(Region 0)
+  let qval : Q(Nat) ← elabTermEnsuringTypeQ qi q(Nat)
+  let nval : Q(Nat) ← elabTermEnsuringTypeQ ni q(Nat)
+  -- We need this for building `R  later
+  -- I would like to synthesize this at elaboration time, not sure how
+  let _factval ← elabTermEnsuringTypeQ hq q(Fact ($qval > 1))
+  let com := q(mlir2fhe (q := $qval) (n := $nval) $ast)
+  synthesizeSyntheticMVarsNoPostponing
+  let com : Q(MLIR.AST.ExceptM (Op 2 3) (Σ (Γ' : Ctxt (Ty 2 3)) (ty : Ty 2 3), Com (Op 2 3) Γ' ty)) ←
+    withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
+      withTransparency (mode := TransparencyMode.default) <|
+        return ←reduce com
+  let comExpr : Expr := com
+  match comExpr.app3? ``Except.ok with
+  | .some (_εexpr, _αexpr, aexpr) =>
+      match aexpr.app4? ``Sigma.mk with
+      | .some (_αexpr, _βexpr, _fstexpr, sndexpr) =>
+        match sndexpr.app4? ``Sigma.mk with
+        | .some (_αexpr, _βexpr, _fstexpr, sndexpr) =>
+            return sndexpr
+        | .none => throwError "Found `Except.ok (Sigma.mk _ WRONG)`, Expected (Except.ok (Sigma.mk _ (Sigma.mk _ _))"
+      | .none => throwError "Found `Except.ok WRONG`, Expected (Except.ok (Sigma.mk _ _))"
+  | .none => throwError "Expected `Except.ok`, found {comExpr}"

From e3252536fa79a65c96b00132416bf91c2dd04e4a Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 16 Apr 2024 17:18:11 +0100
Subject: [PATCH 05/22] chore: delete dead comment

---
 SSA/Projects/FullyHomomorphicEncryption/Syntax.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index 6a056e616..961bd0ec4 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -91,15 +91,6 @@ def mlir2fhe (reg : MLIR.AST.Region 0) :
 end MkFuns -- we don't want q and i here anymore
 
 open Qq MLIR AST Lean Elab Term Meta in
-/--
-NOTE: Wanting Stuck Terms During Strong Normalization of Com
-
-See that we unfold with `TransparencyMode.all`. We do this so we can expose Com.denote
-fully. This is a crazy hack, and interacts extremely poorly with complex definitions found in FHE.
-
-One neater solution is a `match goal` like tactic to match on the proof state
-and run the correct equation.
--/
 elab "[fhe_com" qi:term "," ni:term "," hq:term " | " reg:mlir_region "]" : term => do
   let ast_stx ← `([mlir_region| $reg])
   let ast ← elabTermEnsuringTypeQ ast_stx q(Region 0)

From 20a57be9e779416abd7f1b2f1033a62af6a92d7e Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 10:49:15 +0100
Subject: [PATCH 06/22] feat: add const_int and const_idx operations to FHE
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Andrés Goens <andres@goens.org>

Code peeled from pre-paper submission PR: https://github.com/opencompl/ssa/pull/196.
Code stacked on: https://github.com/opencompl/ssa/pull/231.
---
 SSA/Projects/FullyHomomorphicEncryption/Basic.lean | 11 +++++++++++
 .../FullyHomomorphicEncryption/Syntax.lean         | 14 ++++++++++++++
 2 files changed, 25 insertions(+)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
index 8924b60da..401857a20 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
@@ -667,6 +667,9 @@ inductive Op (q : Nat) (n : Nat) [Fact (q > 1)]
   | from_tensor : Op q n-- interpret values as coefficients of a representative
   | to_tensor : Op q n-- give back coefficients from `R.representative`
   | const (c : R q n) : Op q n
+  | const_int (c : Int) : Op q n
+  | const_idx (i : Nat) : Op q n
+
 
 open TyDenote (toType)
 
@@ -683,12 +686,17 @@ def Op.sig : Op  q n → List (Ty q n)
 | Op.from_tensor => [Ty.tensor]
 | Op.to_tensor => [Ty.polynomialLike]
 | Op.const _ => []
+| Op.const_int _ => []
+| Op.const_idx _ => []
+
 
 @[simp, reducible]
 def Op.outTy : Op q n → Ty q n
 | Op.add | Op.sub | Op.mul | Op.mul_constant | Op.leading_term | Op.monomial
 | Op.monomial_mul | Op.from_tensor | Op.const _  => Ty.polynomialLike
 | Op.to_tensor => Ty.tensor
+| Op.const_int _ => Ty.integer
+| Op.const_idx _ => Ty.index
 
 @[simp, reducible]
 def Op.signature : Op q n → Signature (Ty q n) :=
@@ -709,3 +717,6 @@ noncomputable instance : OpDenote (Op q n) (Ty q n) where
     | Op.from_tensor, arg, _ => R.fromTensor arg.toSingle
     | Op.to_tensor, arg, _ => R.toTensor' arg.toSingle
     | Op.const c, _arg, _ => c
+    | Op.const_int c, _, _ => c
+    | Op.const_idx c, _, _ => c
+
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index 961bd0ec4..625ca28c0 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -26,6 +26,20 @@ def mkTy : MLIR.AST.MLIRType φ → MLIR.AST.ExceptM (Op q n) (Ty q n)
 instance instTransformTy : MLIR.AST.TransformTy (Op q n) (Ty q n) 0 where
   mkTy := mkTy
 
+def cstInt {Γ : Ctxt _} (z :Int) : Expr (Op q n) Γ .integer  :=
+  Expr.mk
+    (op := .const_int z)
+    (ty_eq := rfl)
+    (args := .nil)
+    (regArgs := .nil)
+
+def cstIdx {Γ : Ctxt _} (i : Nat) : Expr (Op q n) Γ .index :=
+  Expr.mk
+    (op := .const_idx i)
+    (ty_eq := rfl)
+    (args := .nil)
+    (regArgs := .nil)
+
 def add {Γ : Ctxt (Ty q n)} (e₁ e₂ : Var Γ .polynomialLike) : Expr (Op q n) Γ .polynomialLike :=
   Expr.mk
     (op := .add)

From 593e0fc16e7e0e5d8e931f016da3253619524816 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 17 Apr 2024 13:26:42 +0100
Subject: [PATCH 07/22] refactor: move `MLIRSyntax` project into `Core`

---
 SSA/{Projects => Core/DSL}/MLIRSyntax/AST.lean      |  5 +++++
 .../EDSL.lean => Core/DSL/MLIRSyntax/Parser.lean}   | 13 +++++++++++--
 SSA/Core/Framework.lean                             |  3 ---
 .../FullyHomomorphicEncryption/Rewrites.lean        |  2 +-
 SSA/Projects/FullyHomomorphicEncryption/Syntax.lean |  4 ++--
 SSA/Projects/InstCombine/LLVM/EDSL.lean             |  4 ++--
 SSA/Projects/InstCombine/LLVM/Transform.lean        |  2 +-
 .../InstCombine/LLVM/Transform/TransformError.lean  |  2 +-
 SSA/Projects/InstCombine/Test.lean                  |  3 +--
 SSA/Projects/PaperExamples/PaperExamples.lean       |  4 ++--
 10 files changed, 26 insertions(+), 16 deletions(-)
 rename SSA/{Projects => Core/DSL}/MLIRSyntax/AST.lean (99%)
 rename SSA/{Projects/MLIRSyntax/EDSL.lean => Core/DSL/MLIRSyntax/Parser.lean} (98%)

diff --git a/SSA/Projects/MLIRSyntax/AST.lean b/SSA/Core/DSL/MLIRSyntax/AST.lean
similarity index 99%
rename from SSA/Projects/MLIRSyntax/AST.lean
rename to SSA/Core/DSL/MLIRSyntax/AST.lean
index 31b5894bf..9120b0c40 100644
--- a/SSA/Projects/MLIRSyntax/AST.lean
+++ b/SSA/Core/DSL/MLIRSyntax/AST.lean
@@ -1,6 +1,11 @@
 import SSA.Core.Util.ConcreteOrMVar
 open Lean PrettyPrinter
 
+/-!
+# MLIR Syntax AST
+This file contains the AST datastructures for generic MLIR syntax
+-/
+
 namespace MLIR.AST
 
 -- variable (MCtxt : Type*)
diff --git a/SSA/Projects/MLIRSyntax/EDSL.lean b/SSA/Core/DSL/MLIRSyntax/Parser.lean
similarity index 98%
rename from SSA/Projects/MLIRSyntax/EDSL.lean
rename to SSA/Core/DSL/MLIRSyntax/Parser.lean
index 681e8de67..86723bb20 100644
--- a/SSA/Projects/MLIRSyntax/EDSL.lean
+++ b/SSA/Core/DSL/MLIRSyntax/Parser.lean
@@ -6,7 +6,16 @@ import Lean.PrettyPrinter
 import Lean.PrettyPrinter.Formatter
 import Lean.Parser
 import Lean.Parser.Extra
-import SSA.Projects.MLIRSyntax.AST
+import SSA.Core.DSL.MLIRSyntax.AST
+
+/-!
+# MLIR Syntax Parsing
+This file uses Lean's parser extensions to parse generic MLIR syntax into datastructures defined
+in `MLIRSyntax.AST`.
+
+Key definitions are the `[mlir_op| ...]` and `[mlir_region| ...]` term elaborators
+
+-/
 
 open Lean
 open Lean.Parser
@@ -102,7 +111,7 @@ partial def balancedBracketsFnAux (startPos: String.Pos)
   | ']' => consumeCloseBracket Bracket.Square startPos i input bs ctx s
   | '>' => consumeCloseBracket Bracket.Angle startPos i input bs ctx s
   | '}' => consumeCloseBracket Bracket.Curly startPos i input bs ctx s
-  | c => balancedBracketsFnAux startPos (input.next i) input bs ctx s
+  | _c => balancedBracketsFnAux startPos (input.next i) input bs ctx s
 
 end
 
diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean
index 04d01f6b5..f5d8bb07c 100644
--- a/SSA/Core/Framework.lean
+++ b/SSA/Core/Framework.lean
@@ -5,9 +5,6 @@ import SSA.Core.HVector
 import Mathlib.Data.List.AList
 import Mathlib.Data.Finset.Piecewise
 
-import SSA.Projects.MLIRSyntax.AST -- TODO post-merge: bring into Core
-import SSA.Projects.MLIRSyntax.EDSL -- TODO post-merge: bring into Core
-
 open Ctxt (Var VarSet Valuation)
 open TyDenote (toType)
 
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
index 8aaee5a2d..777fd131a 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -3,7 +3,7 @@ End-to-end showcase of the framework for verifying rewrites about FHE semantics.
 
 Authors: Andrés Goens<andres@goens.org>
 -/
-import SSA.Projects.MLIRSyntax.EDSL
+import SSA.Core.DSL.MLIRSyntax.Parser
 import SSA.Core.Tactic
 import SSA.Projects.FullyHomomorphicEncryption.Basic
 import SSA.Projects.FullyHomomorphicEncryption.Statements
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index 625ca28c0..e615bac7a 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -4,8 +4,8 @@ Syntax definitions for FHE, providing a custom [fhe_com|...] with syntax sugar.
 Authors: Andrés Goens<andres@goens.org>
 -/
 import SSA.Projects.InstCombine.LLVM.Transform
-import SSA.Projects.MLIRSyntax.AST
-import SSA.Projects.MLIRSyntax.EDSL
+import SSA.Core.DSL.MLIRSyntax.AST
+import SSA.Core.DSL.MLIRSyntax.Parser
 import SSA.Projects.FullyHomomorphicEncryption.Basic
 
 open MLIR AST Ctxt
diff --git a/SSA/Projects/InstCombine/LLVM/EDSL.lean b/SSA/Projects/InstCombine/LLVM/EDSL.lean
index 57e1cbe1c..cb86076d2 100644
--- a/SSA/Projects/InstCombine/LLVM/EDSL.lean
+++ b/SSA/Projects/InstCombine/LLVM/EDSL.lean
@@ -1,8 +1,8 @@
 import Qq
 import SSA.Projects.InstCombine.Base
 import Std.Data.BitVec
-import SSA.Projects.MLIRSyntax.AST
-import SSA.Projects.MLIRSyntax.EDSL
+import SSA.Core.DSL.MLIRSyntax.AST
+import SSA.Core.DSL.MLIRSyntax.Parser
 import SSA.Projects.InstCombine.LLVM.Transform
 import SSA.Projects.InstCombine.LLVM.CLITests
 
diff --git a/SSA/Projects/InstCombine/LLVM/Transform.lean b/SSA/Projects/InstCombine/LLVM/Transform.lean
index f297b3f85..b21801f77 100644
--- a/SSA/Projects/InstCombine/LLVM/Transform.lean
+++ b/SSA/Projects/InstCombine/LLVM/Transform.lean
@@ -1,5 +1,5 @@
 -- should replace with Lean import once Pure is upstream
-import SSA.Projects.MLIRSyntax.AST
+import SSA.Core.DSL.MLIRSyntax.AST
 import SSA.Projects.InstCombine.LLVM.Transform.NameMapping
 import SSA.Projects.InstCombine.LLVM.Transform.TransformError
 import SSA.Core.Framework
diff --git a/SSA/Projects/InstCombine/LLVM/Transform/TransformError.lean b/SSA/Projects/InstCombine/LLVM/Transform/TransformError.lean
index eadaed68b..9edf16c76 100644
--- a/SSA/Projects/InstCombine/LLVM/Transform/TransformError.lean
+++ b/SSA/Projects/InstCombine/LLVM/Transform/TransformError.lean
@@ -1,4 +1,4 @@
-import SSA.Projects.MLIRSyntax.AST
+import SSA.Core.DSL.MLIRSyntax.AST
 
 namespace MLIR.AST
 
diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean
index 44bb67198..e654a0462 100644
--- a/SSA/Projects/InstCombine/Test.lean
+++ b/SSA/Projects/InstCombine/Test.lean
@@ -1,4 +1,4 @@
-import SSA.Projects.MLIRSyntax.EDSL
+import SSA.Core.DSL.MLIRSyntax.Parser
 import SSA.Projects.InstCombine.LLVM.Transform
 import SSA.Projects.InstCombine.LLVM.EDSL
 open MLIR AST
@@ -138,4 +138,3 @@ example : bb0IcomGeneric 32 = bb0IcomConcrete := by rfl
 -/
 example (w Γv) : (GenericWidth w).denote Γv = some (Bitvec.ofNat w 0) := by
   rfl
-
diff --git a/SSA/Projects/PaperExamples/PaperExamples.lean b/SSA/Projects/PaperExamples/PaperExamples.lean
index ee241e87a..4736b9c79 100644
--- a/SSA/Projects/PaperExamples/PaperExamples.lean
+++ b/SSA/Projects/PaperExamples/PaperExamples.lean
@@ -4,9 +4,9 @@ import Mathlib.Logic.Function.Iterate
 import SSA.Core.Framework
 import SSA.Core.Tactic
 import SSA.Core.Util
+import SSA.Core.DSL.MLIRSyntax.AST
+import SSA.Core.DSL.MLIRSyntax.Parser
 import SSA.Projects.InstCombine.LLVM.Transform
-import SSA.Projects.MLIRSyntax.AST
-import SSA.Projects.MLIRSyntax.EDSL
 import Std.Data.BitVec
 import Mathlib.Data.BitVec.Lemmas
 import Mathlib.Tactic.Ring

From 6fa8664755f4b67c38e8f96c8fe243ba37e5f773 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 17 Apr 2024 13:37:38 +0100
Subject: [PATCH 08/22] refactor: move `Transform` into core

---
 .../InstCombine/LLVM => Core/DSL}/Transform.lean     | 12 ++++++++----
 .../LLVM => Core/DSL}/Transform/NameMapping.lean     |  0
 .../LLVM => Core/DSL}/Transform/TransformError.lean  |  0
 SSA/Projects/FullyHomomorphicEncryption/Syntax.lean  |  2 +-
 SSA/Projects/InstCombine/LLVM/CLITests.lean          |  2 +-
 SSA/Projects/InstCombine/LLVM/EDSL.lean              |  2 +-
 SSA/Projects/InstCombine/Test.lean                   |  2 +-
 SSA/Projects/PaperExamples/PaperExamples.lean        |  2 +-
 8 files changed, 13 insertions(+), 9 deletions(-)
 rename SSA/{Projects/InstCombine/LLVM => Core/DSL}/Transform.lean (95%)
 rename SSA/{Projects/InstCombine/LLVM => Core/DSL}/Transform/NameMapping.lean (100%)
 rename SSA/{Projects/InstCombine/LLVM => Core/DSL}/Transform/TransformError.lean (100%)

diff --git a/SSA/Projects/InstCombine/LLVM/Transform.lean b/SSA/Core/DSL/Transform.lean
similarity index 95%
rename from SSA/Projects/InstCombine/LLVM/Transform.lean
rename to SSA/Core/DSL/Transform.lean
index b21801f77..7a7fbc7bb 100644
--- a/SSA/Projects/InstCombine/LLVM/Transform.lean
+++ b/SSA/Core/DSL/Transform.lean
@@ -1,17 +1,21 @@
 -- should replace with Lean import once Pure is upstream
 import SSA.Core.DSL.MLIRSyntax.AST
-import SSA.Projects.InstCombine.LLVM.Transform.NameMapping
-import SSA.Projects.InstCombine.LLVM.Transform.TransformError
+import SSA.Core.DSL.Transform.NameMapping
+import SSA.Core.DSL.Transform.TransformError
 import SSA.Core.Framework
 import SSA.Core.ErasedContext
 
-import Std.Data.BitVec
+/-!
+# `Transform*` typeclasses
+This file defines `TransformTy`, `TransformExpr`, and `TransformReturn` typeclasses,
+which dictate how generic MLIR syntax (as defined in `MLIRSyntax.AST`) can be transformed into
+an instance of `Com` or `Expr` for a specific dialect.
+-/
 
 universe u
 
 namespace MLIR.AST
 
-open Std (BitVec)
 open Ctxt
 
 instance {Op Ty : Type} [OpSignature Op Ty] {t : Ty} {Γ : Ctxt Ty} {Γ' : DerivedCtxt Γ} : Coe (Expr Op Γ t) (Expr Op Γ'.ctxt t) where
diff --git a/SSA/Projects/InstCombine/LLVM/Transform/NameMapping.lean b/SSA/Core/DSL/Transform/NameMapping.lean
similarity index 100%
rename from SSA/Projects/InstCombine/LLVM/Transform/NameMapping.lean
rename to SSA/Core/DSL/Transform/NameMapping.lean
diff --git a/SSA/Projects/InstCombine/LLVM/Transform/TransformError.lean b/SSA/Core/DSL/Transform/TransformError.lean
similarity index 100%
rename from SSA/Projects/InstCombine/LLVM/Transform/TransformError.lean
rename to SSA/Core/DSL/Transform/TransformError.lean
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index e615bac7a..dc136f6d1 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -3,7 +3,7 @@ Syntax definitions for FHE, providing a custom [fhe_com|...] with syntax sugar.
 
 Authors: Andrés Goens<andres@goens.org>
 -/
-import SSA.Projects.InstCombine.LLVM.Transform
+import SSA.Core.DSL.Transform
 import SSA.Core.DSL.MLIRSyntax.AST
 import SSA.Core.DSL.MLIRSyntax.Parser
 import SSA.Projects.FullyHomomorphicEncryption.Basic
diff --git a/SSA/Projects/InstCombine/LLVM/CLITests.lean b/SSA/Projects/InstCombine/LLVM/CLITests.lean
index 9fda7695c..40049a19b 100644
--- a/SSA/Projects/InstCombine/LLVM/CLITests.lean
+++ b/SSA/Projects/InstCombine/LLVM/CLITests.lean
@@ -2,7 +2,7 @@ import SSA.Core.Util
 import Std
 import Lean.Environment
 import Cli
-import SSA.Projects.InstCombine.LLVM.Transform
+import SSA.Core.DSL.Transform
 import SSA.Projects.InstCombine.Base
 
 open Lean TyDenote InstCombine
diff --git a/SSA/Projects/InstCombine/LLVM/EDSL.lean b/SSA/Projects/InstCombine/LLVM/EDSL.lean
index cb86076d2..259afc68d 100644
--- a/SSA/Projects/InstCombine/LLVM/EDSL.lean
+++ b/SSA/Projects/InstCombine/LLVM/EDSL.lean
@@ -3,7 +3,7 @@ import SSA.Projects.InstCombine.Base
 import Std.Data.BitVec
 import SSA.Core.DSL.MLIRSyntax.AST
 import SSA.Core.DSL.MLIRSyntax.Parser
-import SSA.Projects.InstCombine.LLVM.Transform
+import SSA.Core.DSL.Transform
 import SSA.Projects.InstCombine.LLVM.CLITests
 
 open Qq Lean Meta Elab.Term Elab Command
diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean
index e654a0462..1eb1cf74a 100644
--- a/SSA/Projects/InstCombine/Test.lean
+++ b/SSA/Projects/InstCombine/Test.lean
@@ -1,5 +1,5 @@
 import SSA.Core.DSL.MLIRSyntax.Parser
-import SSA.Projects.InstCombine.LLVM.Transform
+import SSA.Core.DSL.Transform
 import SSA.Projects.InstCombine.LLVM.EDSL
 open MLIR AST
 
diff --git a/SSA/Projects/PaperExamples/PaperExamples.lean b/SSA/Projects/PaperExamples/PaperExamples.lean
index 4736b9c79..e7b69689a 100644
--- a/SSA/Projects/PaperExamples/PaperExamples.lean
+++ b/SSA/Projects/PaperExamples/PaperExamples.lean
@@ -6,7 +6,7 @@ import SSA.Core.Tactic
 import SSA.Core.Util
 import SSA.Core.DSL.MLIRSyntax.AST
 import SSA.Core.DSL.MLIRSyntax.Parser
-import SSA.Projects.InstCombine.LLVM.Transform
+import SSA.Core.DSL.Transform
 import Std.Data.BitVec
 import Mathlib.Data.BitVec.Lemmas
 import Mathlib.Tactic.Ring

From 189c7a3d66ac95ded5100dc65cb05e4681559379 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 17 Apr 2024 13:49:20 +0100
Subject: [PATCH 09/22] refactor: flatten `DSL.MLirSyntax` hierarchy into just
 `MLIRSyntax`

---
 SSA/Core/{DSL => }/MLIRSyntax/AST.lean                      | 0
 .../Parser.lean => MLIRSyntax/GenericParser.lean}           | 2 +-
 SSA/Core/{DSL => MLIRSyntax}/Transform.lean                 | 6 +++---
 SSA/Core/{DSL => MLIRSyntax}/Transform/NameMapping.lean     | 0
 SSA/Core/{DSL => MLIRSyntax}/Transform/TransformError.lean  | 2 +-
 SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean       | 2 +-
 SSA/Projects/FullyHomomorphicEncryption/Syntax.lean         | 6 +++---
 SSA/Projects/InstCombine/LLVM/CLITests.lean                 | 2 +-
 SSA/Projects/InstCombine/LLVM/EDSL.lean                     | 6 +++---
 SSA/Projects/InstCombine/Test.lean                          | 4 ++--
 SSA/Projects/PaperExamples/PaperExamples.lean               | 6 +++---
 11 files changed, 18 insertions(+), 18 deletions(-)
 rename SSA/Core/{DSL => }/MLIRSyntax/AST.lean (100%)
 rename SSA/Core/{DSL/MLIRSyntax/Parser.lean => MLIRSyntax/GenericParser.lean} (99%)
 rename SSA/Core/{DSL => MLIRSyntax}/Transform.lean (98%)
 rename SSA/Core/{DSL => MLIRSyntax}/Transform/NameMapping.lean (100%)
 rename SSA/Core/{DSL => MLIRSyntax}/Transform/TransformError.lean (97%)

diff --git a/SSA/Core/DSL/MLIRSyntax/AST.lean b/SSA/Core/MLIRSyntax/AST.lean
similarity index 100%
rename from SSA/Core/DSL/MLIRSyntax/AST.lean
rename to SSA/Core/MLIRSyntax/AST.lean
diff --git a/SSA/Core/DSL/MLIRSyntax/Parser.lean b/SSA/Core/MLIRSyntax/GenericParser.lean
similarity index 99%
rename from SSA/Core/DSL/MLIRSyntax/Parser.lean
rename to SSA/Core/MLIRSyntax/GenericParser.lean
index 86723bb20..2742ab2d1 100644
--- a/SSA/Core/DSL/MLIRSyntax/Parser.lean
+++ b/SSA/Core/MLIRSyntax/GenericParser.lean
@@ -6,7 +6,7 @@ import Lean.PrettyPrinter
 import Lean.PrettyPrinter.Formatter
 import Lean.Parser
 import Lean.Parser.Extra
-import SSA.Core.DSL.MLIRSyntax.AST
+import SSA.Core.MLIRSyntax.AST
 
 /-!
 # MLIR Syntax Parsing
diff --git a/SSA/Core/DSL/Transform.lean b/SSA/Core/MLIRSyntax/Transform.lean
similarity index 98%
rename from SSA/Core/DSL/Transform.lean
rename to SSA/Core/MLIRSyntax/Transform.lean
index 7a7fbc7bb..da76385d0 100644
--- a/SSA/Core/DSL/Transform.lean
+++ b/SSA/Core/MLIRSyntax/Transform.lean
@@ -1,7 +1,7 @@
 -- should replace with Lean import once Pure is upstream
-import SSA.Core.DSL.MLIRSyntax.AST
-import SSA.Core.DSL.Transform.NameMapping
-import SSA.Core.DSL.Transform.TransformError
+import SSA.Core.MLIRSyntax.AST
+import SSA.Core.MLIRSyntax.Transform.NameMapping
+import SSA.Core.MLIRSyntax.Transform.TransformError
 import SSA.Core.Framework
 import SSA.Core.ErasedContext
 
diff --git a/SSA/Core/DSL/Transform/NameMapping.lean b/SSA/Core/MLIRSyntax/Transform/NameMapping.lean
similarity index 100%
rename from SSA/Core/DSL/Transform/NameMapping.lean
rename to SSA/Core/MLIRSyntax/Transform/NameMapping.lean
diff --git a/SSA/Core/DSL/Transform/TransformError.lean b/SSA/Core/MLIRSyntax/Transform/TransformError.lean
similarity index 97%
rename from SSA/Core/DSL/Transform/TransformError.lean
rename to SSA/Core/MLIRSyntax/Transform/TransformError.lean
index 9edf16c76..95cdf5a87 100644
--- a/SSA/Core/DSL/Transform/TransformError.lean
+++ b/SSA/Core/MLIRSyntax/Transform/TransformError.lean
@@ -1,4 +1,4 @@
-import SSA.Core.DSL.MLIRSyntax.AST
+import SSA.Core.MLIRSyntax.AST
 
 namespace MLIR.AST
 
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
index 777fd131a..78251ec0a 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -3,7 +3,7 @@ End-to-end showcase of the framework for verifying rewrites about FHE semantics.
 
 Authors: Andrés Goens<andres@goens.org>
 -/
-import SSA.Core.DSL.MLIRSyntax.Parser
+import SSA.Core.MLIRSyntax.GenericParser
 import SSA.Core.Tactic
 import SSA.Projects.FullyHomomorphicEncryption.Basic
 import SSA.Projects.FullyHomomorphicEncryption.Statements
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index dc136f6d1..7f04fad56 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -3,9 +3,9 @@ Syntax definitions for FHE, providing a custom [fhe_com|...] with syntax sugar.
 
 Authors: Andrés Goens<andres@goens.org>
 -/
-import SSA.Core.DSL.Transform
-import SSA.Core.DSL.MLIRSyntax.AST
-import SSA.Core.DSL.MLIRSyntax.Parser
+import SSA.Core.MLIRSyntax.Transform
+import SSA.Core.MLIRSyntax.AST
+import SSA.Core.MLIRSyntax.GenericParser
 import SSA.Projects.FullyHomomorphicEncryption.Basic
 
 open MLIR AST Ctxt
diff --git a/SSA/Projects/InstCombine/LLVM/CLITests.lean b/SSA/Projects/InstCombine/LLVM/CLITests.lean
index 40049a19b..42d124247 100644
--- a/SSA/Projects/InstCombine/LLVM/CLITests.lean
+++ b/SSA/Projects/InstCombine/LLVM/CLITests.lean
@@ -2,7 +2,7 @@ import SSA.Core.Util
 import Std
 import Lean.Environment
 import Cli
-import SSA.Core.DSL.Transform
+import SSA.Core.MLIRSyntax.Transform
 import SSA.Projects.InstCombine.Base
 
 open Lean TyDenote InstCombine
diff --git a/SSA/Projects/InstCombine/LLVM/EDSL.lean b/SSA/Projects/InstCombine/LLVM/EDSL.lean
index 259afc68d..e33fcedd3 100644
--- a/SSA/Projects/InstCombine/LLVM/EDSL.lean
+++ b/SSA/Projects/InstCombine/LLVM/EDSL.lean
@@ -1,9 +1,9 @@
 import Qq
 import SSA.Projects.InstCombine.Base
 import Std.Data.BitVec
-import SSA.Core.DSL.MLIRSyntax.AST
-import SSA.Core.DSL.MLIRSyntax.Parser
-import SSA.Core.DSL.Transform
+import SSA.Core.MLIRSyntax.AST
+import SSA.Core.MLIRSyntax.GenericParser
+import SSA.Core.MLIRSyntax.Transform
 import SSA.Projects.InstCombine.LLVM.CLITests
 
 open Qq Lean Meta Elab.Term Elab Command
diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean
index 1eb1cf74a..46ee78aac 100644
--- a/SSA/Projects/InstCombine/Test.lean
+++ b/SSA/Projects/InstCombine/Test.lean
@@ -1,5 +1,5 @@
-import SSA.Core.DSL.MLIRSyntax.Parser
-import SSA.Core.DSL.Transform
+import SSA.Core.MLIRSyntax.GenericParser
+import SSA.Core.MLIRSyntax.Transform
 import SSA.Projects.InstCombine.LLVM.EDSL
 open MLIR AST
 
diff --git a/SSA/Projects/PaperExamples/PaperExamples.lean b/SSA/Projects/PaperExamples/PaperExamples.lean
index e7b69689a..728e60f53 100644
--- a/SSA/Projects/PaperExamples/PaperExamples.lean
+++ b/SSA/Projects/PaperExamples/PaperExamples.lean
@@ -4,9 +4,9 @@ import Mathlib.Logic.Function.Iterate
 import SSA.Core.Framework
 import SSA.Core.Tactic
 import SSA.Core.Util
-import SSA.Core.DSL.MLIRSyntax.AST
-import SSA.Core.DSL.MLIRSyntax.Parser
-import SSA.Core.DSL.Transform
+import SSA.Core.MLIRSyntax.AST
+import SSA.Core.MLIRSyntax.GenericParser
+import SSA.Core.MLIRSyntax.Transform
 import Std.Data.BitVec
 import Mathlib.Data.BitVec.Lemmas
 import Mathlib.Tactic.Ring

From a28f1b078143cd0eade1604c8f61fab176d7fa64 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 17 Apr 2024 15:13:03 +0100
Subject: [PATCH 10/22] refactor: make `change_mlir_context` reduce less
 aggressively

In particular, don't needlessly reduce individual types in a context
---
 SSA/Core/Tactic.lean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/SSA/Core/Tactic.lean b/SSA/Core/Tactic.lean
index 1a2e37cbe..d895ebebd 100644
--- a/SSA/Core/Tactic.lean
+++ b/SSA/Core/Tactic.lean
@@ -12,6 +12,18 @@ section
 
 open Lean Meta Elab.Tactic Qq
 
+/-- `ctxtNf` reduces an expression of type `Ctxt _` to something in between whnf and normal form.
+`ctxtNf` recursively calls `whnf` on the tail of the list, so that the result is of the form
+  `a₀ :: a₁ :: ... :: aₙ :: [] `
+where each element `aᵢ` is not further reduced -/
+private partial def ctxtNf {α : Q(Type)} (as : Q(Ctxt $α)) : MetaM Q(Ctxt $α) := do
+  let as : Q(List $α) ← whnf as
+  match as with
+    | ~q($a :: $as) =>
+        let as ← ctxtNf as
+        return q($a :: $as)
+    | as => return as
+
 /-- Given a `V : Valuation Γ`, fully reduce the context `Γ` in the type of `V` -/
 elab "change_mlir_context " V:ident : tactic => do
   let V : Name := V.getId
@@ -28,7 +40,7 @@ elab "change_mlir_context " V:ident : tactic => do
     let _  ← assertDefEqQ Vdecl.type q(@Ctxt.Valuation $Ty $G $Γ)
 
     -- Reduce the context `Γ`
-    let Γr ← reduce Γ
+    let Γr ← ctxtNf Γ
     let Γr : Q(Ctxt $Ty) := Γr
 
     let goal ← getMainGoal

From 6f5b9580cccaf67929f5d759a32350a94d86bf7a Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 14:00:09 +0100
Subject: [PATCH 11/22] feat: add example from paper for FHE.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

To make this example work, we need a definition of `R.ofZ` that is
computable, and which is not agressively unfolded. This is ensured by
our `axiom` trick.

Code peeled from pre-paper submission PR: https://github.com/opencompl/ssa/pull/196.
Code stacked on: https://github.com/opencompl/ssa/pull/234

Co-authored-by: Andrés Goens <andres@goens.org>
---
 .../FullyHomomorphicEncryption/Rewrites.lean  | 80 +++++++++++++++++++
 .../FullyHomomorphicEncryption/Syntax.lean    | 76 ++++++++++++++++++
 2 files changed, 156 insertions(+)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
index 78251ec0a..b6c732427 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -72,3 +72,83 @@ noncomputable def p1 : PeepholeRewrite (Op q n) [.polynomialLike, .polynomialLik
     }
 
 end ExampleComm
+
+section ExampleModulo
+
+@[irreducible]
+def irreduciblePow (q n : Nat) : Nat := q^n
+infixl:50 "**" => irreduciblePow
+
+
+variable {q : Nat} {n : Nat} [hq : Fact (q > 1)]
+
+-- code generator does not support recursor 'Decidable.rec' yet, consider using 'match ... with' and/or structural recursion
+noncomputable def lhs := [fhe_com q, n, hq| {
+^bb0(%a : ! R):
+  %one_int = "arith.const" () {value = 1}: () -> (i16)
+  %two_to_the_n = "arith.const" () {value = $((2**n : Int))}: () -> (index)
+  %x2n = "poly.monomial" (%one_int,%two_to_the_n) : (i16, index) -> (! R)
+  %oner = "poly.const" () {value = 1}: () -> (! R)
+  %p = "poly.add" (%x2n, %oner) : (! R, ! R) -> (! R)
+  %v1 = "poly.add" (%a, %p) : (! R, ! R) -> (! R)
+  "return" (%v1) : (! R) -> ()
+}]
+
+def rhs := [fhe_com q, n, hq | {
+^bb0(%a : ! R):
+  "return" (%a) : (! R) -> ()
+}]
+
+/- 'lhs' depends on axioms: [propext, Quot.sound, Classical.choice, ROfZComputable_stuck_term] -/
+#print axioms lhs
+
+/-  `x^(2^n) + a = a`, since we quotient the polynomial ring with x^(2^n) -/
+open MLIR AST in
+noncomputable def p1 : PeepholeRewrite (Op q n) [.polynomialLike] .polynomialLike :=
+  { lhs := lhs,
+     rhs := rhs
+  , correct :=
+    by
+      funext Γv
+      unfold lhs rhs
+       /-
+      Com.denote
+          (Com.lete (Expr.mk (Op.const_int (Int.ofNat 1)) lhs.proof_2 HVector.nil HVector.nil)
+            (Com.lete (Expr.mk (Op.const_idx 1) lhs.proof_3 HVector.nil HVector.nil)
+              (Com.lete
+                (Expr.mk Op.monomial lhs.proof_4
+                  ({ val := 1, property := lhs.proof_5 }::ₕ({ val := 0, property := lhs.proof_6 }::ₕHVector.nil)) HVector.nil)
+                (Com.lete
+                  (Expr.mk (Op.const (ROfZComputable_stuck_term 2 3 (Int.ofNat 1))) lhs.proof_7 HVector.nil HVector.nil)
+                  (Com.lete
+                    (Expr.mk Op.add lhs.proof_8
+                      ({ val := 1, property := lhs.proof_9 }::ₕ({ val := 0, property := lhs.proof_10 }::ₕHVector.nil))
+                      HVector.nil)
+                    (Com.lete
+                      (Expr.mk Op.add lhs.proof_8
+                        ({ val := 5, property := lhs.proof_11 }::ₕ({ val := 0, property := lhs.proof_12 }::ₕHVector.nil))
+                        HVector.nil)
+                      (Com.ret { val := 0, property := lhs.proof_13 })))))))
+          Γv =
+        Com.denote (Com.ret { val := 0, property := rhs.proof_2 }) Γv
+       -/
+      simp_peephole [Nat.cast_one, Int.cast_one, ROfZComputable_def] at Γv
+      /- ⊢ ∀ (a : ⟦Ty.polynomialLike⟧), a + (R.monomial q n 1 (2**n) + 1) = a -/
+      simp [R.fromPoly, R.monomial]
+      /- ⊢ a + ((Ideal.Quotient.mk (Ideal.span {f q n})) ((Polynomial.monomial (2**n)) 1) + 1) = a -/
+      intros a
+      unfold irreduciblePow
+      --have hgenerator : f 2 3 = (Polynomial.monomial 8 1) + 1  := by simp [f, Polynomial.X_pow_eq_monomial]
+      have hgenerator : f q n - (1 : Polynomial (ZMod q)) = (Polynomial.monomial (R := ZMod q) (2^n : Nat) 1)  := by simp  [f, Polynomial.X_pow_eq_monomial]
+      --set_option pp.all true in
+      -- `rw` bug? or because of the workaround?
+      -- tactic 'rewrite' failed, motive is not type correct
+      rw [← hgenerator]
+      have add_congr_quotient : ((Ideal.Quotient.mk (Ideal.span {f q n})) (f q n - 1) + 1)  = ((Ideal.Quotient.mk (Ideal.span {f q n})) (f q n )) := by simp
+      rw [add_congr_quotient]
+      apply Poly.add_f_eq
+      done
+    }
+/- 'p1' depends on axioms: [propext, Classical.choice, Quot.sound, ROfZComputable_stuck_term, ROfZComputable_def] -/
+#print axioms p1
+end ExampleModulo
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index 7f04fad56..3a7eeb259 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -61,9 +61,85 @@ def mon {Γ : Ctxt (Ty q n)} (a : Var Γ .integer) (i : Var Γ .index) : Expr (O
     (args := .cons a <| .cons i .nil)
     (regArgs := .nil)
 
+
+section CstComputable
+
+
+/-- This definition is subtle.
+
+1.  We make this an axiom so we can strongly normalize terms without lean
+  unfolding the definition
+2. We give it an implemented_by so we can use it in computable code that is used
+   to create the expression in Meta code
+3. We give it an equation lemma to make it what we *really* want in proof mode, which is the coe.
+
+This ensures three properties simultaneously:
+1. We can run it at meta time giving us the `ìmplemented_by` value
+2. It strongly normalizes creating stuck term (`ROfZComputable`)
+3. We can then `simp`it to become the value we really want (`coe z`).
+4. The `theorem ROfZComputable_eq` tells us that this is safe to do.
+-/
+
+def ROfZComputable_impl (z : ℤ) : R q n :=
+  let zq : ZMod q := z
+  let p : (ZMod q)[X] := {
+      toFinsupp := Finsupp.mk
+        (support := List.toFinset (if zq = 0 then  [] else [0]))
+        (toFun := fun i => if i = 0 then z else 0)
+        (mem_support_toFun := by
+          intros a
+          constructor
+          · intros ha
+            simp at ha
+            split at ha
+            case mp.inl hz =>
+              simp at ha
+            case mp.inr hz =>
+              simp at ha
+              subst ha
+              simp [hz]
+          · intros hb
+            simp at hb
+            obtain ⟨ha, hz⟩ := hb
+            subst ha
+            simp [hz]
+        )
+      : (ZMod q)[X]
+  }
+  R.fromPoly p
+
+@[implemented_by ROfZComputable_impl]
+axiom ROfZComputable_stuck_term (q n : Nat) (z : ℤ) : R q n
+
+@[simp]
+axiom ROfZComputable_def (q n :Nat) (z : ℤ) : ROfZComputable_stuck_term  q n z = (↑ z : R q n)
+
+def cstComputable {Γ : Ctxt _} (z : Int) : Expr (Op q n) Γ .polynomialLike :=
+  Expr.mk
+    (op := Op.const (ROfZComputable_stuck_term q n z))
+    (ty_eq := rfl)
+    (args := .nil)
+    (regArgs := .nil)
+end CstComputable
+
 def mkExpr (Γ : Ctxt (Ty q n)) (opStx : MLIR.AST.Op 0) :
     MLIR.AST.ReaderM (Op q n) (Σ ty, Expr (Op q n) Γ ty) := do
   match opStx.name with
+  | "poly.const" =>
+    match opStx.attrs.find_int "value" with
+    | .some (v, _ty) =>
+      -- throw <| .generic s!"expected 'const' to have int attr 'value', found: {repr opStx}"
+      return ⟨.polynomialLike, cstComputable v⟩
+    | .none => throw <| .generic s!"expected 'const' to have int attr 'value', found: {repr opStx}"
+  | "arith.const" =>
+    match opStx.attrs.find_int "value" with
+    | .some (v, vty) => match vty with
+        | .int _ _ => match opStx.res with
+          | [(_,MLIR.AST.MLIRType.int MLIR.AST.Signedness.Signless _)] => return ⟨.integer, cstInt v⟩
+          | [(_,MLIR.AST.MLIRType.index)] => return ⟨.index, cstIdx v.toNat⟩
+          | _ => throw <| .generic s!"unsupported result type {repr opStx.res} for arith.const"
+        | _ => throw <| .generic s!"unsupported constant type {repr vty} for arith.const"
+    | .none => throw <| .generic s!"expected 'const' to have int attr 'value', found: {repr opStx}"
   | "poly.monomial" =>
     match opStx.args with
     | v₁Stx::v₂Stx::[] =>

From 5c460063d2bf0f32d274e29932f7063c109a6832 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 14:04:19 +0100
Subject: [PATCH 12/22] feat: minor proof cleanup

---
 SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
index b6c732427..7fd28d57a 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -138,11 +138,7 @@ noncomputable def p1 : PeepholeRewrite (Op q n) [.polynomialLike] .polynomialLik
       /- ⊢ a + ((Ideal.Quotient.mk (Ideal.span {f q n})) ((Polynomial.monomial (2**n)) 1) + 1) = a -/
       intros a
       unfold irreduciblePow
-      --have hgenerator : f 2 3 = (Polynomial.monomial 8 1) + 1  := by simp [f, Polynomial.X_pow_eq_monomial]
       have hgenerator : f q n - (1 : Polynomial (ZMod q)) = (Polynomial.monomial (R := ZMod q) (2^n : Nat) 1)  := by simp  [f, Polynomial.X_pow_eq_monomial]
-      --set_option pp.all true in
-      -- `rw` bug? or because of the workaround?
-      -- tactic 'rewrite' failed, motive is not type correct
       rw [← hgenerator]
       have add_congr_quotient : ((Ideal.Quotient.mk (Ideal.span {f q n})) (f q n - 1) + 1)  = ((Ideal.Quotient.mk (Ideal.span {f q n})) (f q n )) := by simp
       rw [add_congr_quotient]

From def5b88533ac0fbfbd9abd967442a3fe73f097e1 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 14:05:13 +0100
Subject: [PATCH 13/22] chore: delete dead comment

---
 SSA/Projects/FullyHomomorphicEncryption/Syntax.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index 3a7eeb259..85f8f9baf 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -128,7 +128,6 @@ def mkExpr (Γ : Ctxt (Ty q n)) (opStx : MLIR.AST.Op 0) :
   | "poly.const" =>
     match opStx.attrs.find_int "value" with
     | .some (v, _ty) =>
-      -- throw <| .generic s!"expected 'const' to have int attr 'value', found: {repr opStx}"
       return ⟨.polynomialLike, cstComputable v⟩
     | .none => throw <| .generic s!"expected 'const' to have int attr 'value', found: {repr opStx}"
   | "arith.const" =>

From a0a7e13c766de51567ebf450b15a6d185a307c67 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 14:09:53 +0100
Subject: [PATCH 14/22] chore: drop dead, misleading comment about a theorem
 that we never quite proved

---
 SSA/Projects/FullyHomomorphicEncryption/Syntax.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index 85f8f9baf..fff76fe7d 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -77,7 +77,6 @@ This ensures three properties simultaneously:
 1. We can run it at meta time giving us the `ìmplemented_by` value
 2. It strongly normalizes creating stuck term (`ROfZComputable`)
 3. We can then `simp`it to become the value we really want (`coe z`).
-4. The `theorem ROfZComputable_eq` tells us that this is safe to do.
 -/
 
 def ROfZComputable_impl (z : ℤ) : R q n :=

From 37aa559377ad4f832be8bd3effe4353dc172348f Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 17:25:07 +0100
Subject: [PATCH 15/22] Update
 SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean

Co-authored-by: Alex Keizer <alex@keizer.dev>
---
 SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
index 7fd28d57a..10d9ad27a 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -99,8 +99,8 @@ def rhs := [fhe_com q, n, hq | {
   "return" (%a) : (! R) -> ()
 }]
 
-/- 'lhs' depends on axioms: [propext, Quot.sound, Classical.choice, ROfZComputable_stuck_term] -/
-#print axioms lhs
+/--info: 'lhs' depends on axioms: [propext, Quot.sound, Classical.choice, ROfZComputable_stuck_term] -/
+#guard_msgs in #print axioms lhs
 
 /-  `x^(2^n) + a = a`, since we quotient the polynomial ring with x^(2^n) -/
 open MLIR AST in

From fd78e5c7cea63e92e6d374f5ef616a61d557e1e2 Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 17:25:13 +0100
Subject: [PATCH 16/22] Update
 SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean

Co-authored-by: Alex Keizer <alex@keizer.dev>
---
 SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
index 10d9ad27a..7704714d1 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -145,6 +145,6 @@ noncomputable def p1 : PeepholeRewrite (Op q n) [.polynomialLike] .polynomialLik
       apply Poly.add_f_eq
       done
     }
-/- 'p1' depends on axioms: [propext, Classical.choice, Quot.sound, ROfZComputable_stuck_term, ROfZComputable_def] -/
-#print axioms p1
+/--info: 'p1' depends on axioms: [propext, Classical.choice, Quot.sound, ROfZComputable_stuck_term, ROfZComputable_def] -/
+#guard_msgs in #print axioms p1
 end ExampleModulo

From 2a331919bc6b5dc38b22b93418fe047218562547 Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 17:37:10 +0100
Subject: [PATCH 17/22] Better explain why lhs is marked noncomputable

---
 SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
index 7704714d1..2c07717e5 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -82,7 +82,8 @@ infixl:50 "**" => irreduciblePow
 
 variable {q : Nat} {n : Nat} [hq : Fact (q > 1)]
 
--- code generator does not support recursor 'Decidable.rec' yet, consider using 'match ... with' and/or structural recursion
+-- We mark this as noncomputable due to the presence of poly.const, which creates a value of type R.
+-- This operation is noncomputable, as we use `coe` from `Int` to `R`, which is a noncomputable instance. 
 noncomputable def lhs := [fhe_com q, n, hq| {
 ^bb0(%a : ! R):
   %one_int = "arith.const" () {value = 1}: () -> (i16)

From 394a1833812676bcd31f9439622c8c9561173f8d Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 17 Apr 2024 14:11:49 +0100
Subject: [PATCH 18/22] refactor: generic building block for dialect edsl

---
 SSA/Core/MLIRSyntax/EDSL.lean                 | 57 +++++++++++++++++++
 SSA/Projects/PaperExamples/PaperExamples.lean | 33 +----------
 2 files changed, 60 insertions(+), 30 deletions(-)
 create mode 100644 SSA/Core/MLIRSyntax/EDSL.lean

diff --git a/SSA/Core/MLIRSyntax/EDSL.lean b/SSA/Core/MLIRSyntax/EDSL.lean
new file mode 100644
index 000000000..a3045e944
--- /dev/null
+++ b/SSA/Core/MLIRSyntax/EDSL.lean
@@ -0,0 +1,57 @@
+import SSA.Core.MLIRSyntax.GenericParser
+import SSA.Core.MLIRSyntax.Transform
+
+/-!
+# MLIR Dialect Domain Specific Language
+This file sets up generic glue meta-code to tie together the generic MLIR parser with the
+`Transform` mechanism, to obtain an easy way to specify a DSL that elaborates into `Com`/`Expr`
+instances for a specific dialect.
+-/
+
+namespace SSA
+
+open Qq Lean Meta Elab Term
+open MLIR.AST
+
+/--
+`elabIntoCom` is a building block for defining a dialect-specific DSL based on the geneeric MLIR
+syntax parser.
+
+For example, if `FooOp` is the type of operations of a "Foo" dialect, we can build a term elaborator
+for this dialect as follows:
+```
+elab "[foo_com| " reg:mlir_region "]" : term => SSA.elabIntoCom reg q(FooOp)
+--     ^^^^^^^                                                        ^^^^^
+```
+-/
+def elabIntoCom (region : TSyntax `mlir_region) (Op : Q(Type)) {Ty : Q(Type)}
+    (_opSignature : Q(OpSignature $Op $Ty) := by exact q(by infer_instance))
+    (φ : Q(Nat) := q(0))
+    (_transformTy      : Q(TransformTy $Op $Ty $φ)     := by exact q(by infer_instance))
+    (_transformExpr    : Q(TransformExpr $Op $Ty $φ)   := by exact q(by infer_instance))
+    (_transformReturn  : Q(TransformReturn $Op $Ty $φ) := by exact q(by infer_instance))
+    :
+    TermElabM Expr := do
+  let ast_stx ← `([mlir_region| $region])
+  let ast ← elabTermEnsuringTypeQ ast_stx q(Region $φ)
+  let com : Q(MLIR.AST.ExceptM $Op (Σ (Γ' : Ctxt $Ty) (ty : $Ty), Com $Op Γ' ty)) :=
+    q(MLIR.AST.mkCom $ast)
+  synthesizeSyntheticMVarsNoPostponing
+  let com : Q(MLIR.AST.ExceptM $Op (Σ (Γ' : Ctxt $Ty) (ty : $Ty), Com $Op Γ' ty)) ←
+    withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
+      withTransparency (mode := TransparencyMode.all) <|
+        return ←reduce com
+  let comExpr : Expr := com
+  trace[Meta] com
+  trace[Meta] comExpr
+
+  match comExpr.app3? ``Except.ok with
+  | .some (_εexpr, _αexpr, aexpr) =>
+      match aexpr.app4? ``Sigma.mk with
+      | .some (_αexpr, _βexpr, _fstexpr, sndexpr) =>
+        match sndexpr.app4? ``Sigma.mk with
+        | .some (_αexpr, _βexpr, _fstexpr, sndexpr) =>
+            return sndexpr
+        | .none => throwError "Found `Except.ok (Sigma.mk _ WRONG)`, Expected (Except.ok (Sigma.mk _ (Sigma.mk _ _))"
+      | .none => throwError "Found `Except.ok WRONG`, Expected (Except.ok (Sigma.mk _ _))"
+  | .none => throwError "Expected `Except.ok`, found {comExpr}"
diff --git a/SSA/Projects/PaperExamples/PaperExamples.lean b/SSA/Projects/PaperExamples/PaperExamples.lean
index 728e60f53..a9e5b7ca0 100644
--- a/SSA/Projects/PaperExamples/PaperExamples.lean
+++ b/SSA/Projects/PaperExamples/PaperExamples.lean
@@ -4,9 +4,8 @@ import Mathlib.Logic.Function.Iterate
 import SSA.Core.Framework
 import SSA.Core.Tactic
 import SSA.Core.Util
-import SSA.Core.MLIRSyntax.AST
 import SSA.Core.MLIRSyntax.GenericParser
-import SSA.Core.MLIRSyntax.Transform
+import SSA.Core.MLIRSyntax.EDSL
 import Std.Data.BitVec
 import Mathlib.Data.BitVec.Lemmas
 import Mathlib.Tactic.Ring
@@ -106,34 +105,8 @@ def mkReturn (Γ : Ctxt Ty) (opStx : MLIR.AST.Op 0) : MLIR.AST.ReaderM Op (Σ ty
 instance : MLIR.AST.TransformReturn Op Ty 0 where
   mkReturn := mkReturn
 
-def mlir2simple (reg : MLIR.AST.Region 0) :
-    MLIR.AST.ExceptM Op (Σ (Γ : Ctxt Ty) (ty : Ty), Com Op Γ ty) := MLIR.AST.mkCom reg
-
-open Qq MLIR AST Lean Elab Term Meta in
-elab "[simple_com| " reg:mlir_region "]" : term => do
-  let ast_stx ← `([mlir_region| $reg])
-  let ast ← elabTermEnsuringTypeQ ast_stx q(Region 0)
-  let mvalues ← `(⟨[], by rfl⟩)
-  -- let mvalues : Q(Vector Nat 0) ← elabTermEnsuringType mvalues q(Vector Nat 0)
-  let com := q(ToyNoRegion.MLIR2Simple.mlir2simple $ast)
-  synthesizeSyntheticMVarsNoPostponing
-  let com : Q(MLIR.AST.ExceptM Op (Σ (Γ' : Ctxt Ty) (ty : Ty), Com Op Γ' ty)) ←
-    withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
-      withTransparency (mode := TransparencyMode.all) <|
-        return ←reduce com
-  let comExpr : Expr := com
-  trace[Meta] com
-  trace[Meta] comExpr
-  match comExpr.app3? ``Except.ok with
-  | .some (_εexpr, _αexpr, aexpr) =>
-      match aexpr.app4? ``Sigma.mk with
-      | .some (_αexpr, _βexpr, _fstexpr, sndexpr) =>
-        match sndexpr.app4? ``Sigma.mk with
-        | .some (_αexpr, _βexpr, _fstexpr, sndexpr) =>
-            return sndexpr
-        | .none => throwError "Found `Except.ok (Sigma.mk _ WRONG)`, Expected (Except.ok (Sigma.mk _ (Sigma.mk _ _))"
-      | .none => throwError "Found `Except.ok WRONG`, Expected (Except.ok (Sigma.mk _ _))"
-  | .none => throwError "Expected `Except.ok`, found {comExpr}"
+open Qq in
+elab "[simple_com| " reg:mlir_region "]" : term => SSA.elabIntoCom reg q(Op)
 
 end MLIR2Simple
 

From 5a4b6f0525c3d6f0dae089396335b18a824ac8d9 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 17 Apr 2024 19:02:18 +0100
Subject: [PATCH 19/22] refactor: redefine `fhe_com` in terms of generic
 `elabIntoCom`

Also drop the reduction from using `.all` transparency to only `.default` (i.e., don't reduce `irreducible` defs)
---
 SSA/Core/MLIRSyntax/EDSL.lean                 |  2 +-
 .../FullyHomomorphicEncryption/Syntax.lean    | 36 ++++---------------
 SSA/Projects/InstCombine/LLVM/EDSL.lean       |  2 +-
 3 files changed, 8 insertions(+), 32 deletions(-)

diff --git a/SSA/Core/MLIRSyntax/EDSL.lean b/SSA/Core/MLIRSyntax/EDSL.lean
index a3045e944..da0562cf9 100644
--- a/SSA/Core/MLIRSyntax/EDSL.lean
+++ b/SSA/Core/MLIRSyntax/EDSL.lean
@@ -39,7 +39,7 @@ def elabIntoCom (region : TSyntax `mlir_region) (Op : Q(Type)) {Ty : Q(Type)}
   synthesizeSyntheticMVarsNoPostponing
   let com : Q(MLIR.AST.ExceptM $Op (Σ (Γ' : Ctxt $Ty) (ty : $Ty), Com $Op Γ' ty)) ←
     withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
-      withTransparency (mode := TransparencyMode.all) <|
+      withTransparency (mode := .default) <|
         return ←reduce com
   let comExpr : Expr := com
   trace[Meta] com
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index fff76fe7d..0d0cd203f 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -3,9 +3,7 @@ Syntax definitions for FHE, providing a custom [fhe_com|...] with syntax sugar.
 
 Authors: Andrés Goens<andres@goens.org>
 -/
-import SSA.Core.MLIRSyntax.Transform
-import SSA.Core.MLIRSyntax.AST
-import SSA.Core.MLIRSyntax.GenericParser
+import SSA.Core.MLIRSyntax.EDSL
 import SSA.Projects.FullyHomomorphicEncryption.Basic
 
 open MLIR AST Ctxt
@@ -173,34 +171,12 @@ def mkReturn (Γ : Ctxt (Ty q n)) (opStx : MLIR.AST.Op 0) : MLIR.AST.ReaderM (Op
 instance : MLIR.AST.TransformReturn (Op q n) (Ty q n) 0 where
   mkReturn := mkReturn
 
-def mlir2fhe (reg : MLIR.AST.Region 0) :
-    MLIR.AST.ExceptM (Op q n) (Σ (Γ : Ctxt (Ty q n)) (ty : (Ty q n)), Com (Op q n) Γ ty) := MLIR.AST.mkCom reg
-
 end MkFuns -- we don't want q and i here anymore
 
 open Qq MLIR AST Lean Elab Term Meta in
 elab "[fhe_com" qi:term "," ni:term "," hq:term " | " reg:mlir_region "]" : term => do
-  let ast_stx ← `([mlir_region| $reg])
-  let ast ← elabTermEnsuringTypeQ ast_stx q(Region 0)
-  let qval : Q(Nat) ← elabTermEnsuringTypeQ qi q(Nat)
-  let nval : Q(Nat) ← elabTermEnsuringTypeQ ni q(Nat)
-  -- We need this for building `R  later
-  -- I would like to synthesize this at elaboration time, not sure how
-  let _factval ← elabTermEnsuringTypeQ hq q(Fact ($qval > 1))
-  let com := q(mlir2fhe (q := $qval) (n := $nval) $ast)
-  synthesizeSyntheticMVarsNoPostponing
-  let com : Q(MLIR.AST.ExceptM (Op 2 3) (Σ (Γ' : Ctxt (Ty 2 3)) (ty : Ty 2 3), Com (Op 2 3) Γ' ty)) ←
-    withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
-      withTransparency (mode := TransparencyMode.default) <|
-        return ←reduce com
-  let comExpr : Expr := com
-  match comExpr.app3? ``Except.ok with
-  | .some (_εexpr, _αexpr, aexpr) =>
-      match aexpr.app4? ``Sigma.mk with
-      | .some (_αexpr, _βexpr, _fstexpr, sndexpr) =>
-        match sndexpr.app4? ``Sigma.mk with
-        | .some (_αexpr, _βexpr, _fstexpr, sndexpr) =>
-            return sndexpr
-        | .none => throwError "Found `Except.ok (Sigma.mk _ WRONG)`, Expected (Except.ok (Sigma.mk _ (Sigma.mk _ _))"
-      | .none => throwError "Found `Except.ok WRONG`, Expected (Except.ok (Sigma.mk _ _))"
-  | .none => throwError "Expected `Except.ok`, found {comExpr}"
+  let q : Q(Nat) ← elabTermEnsuringTypeQ qi q(Nat)
+  let n : Q(Nat) ← elabTermEnsuringTypeQ ni q(Nat)
+  let _factval ← elabTermEnsuringTypeQ hq q(Fact ($q > 1))
+
+  SSA.elabIntoCom reg q(Op $q $n)
diff --git a/SSA/Projects/InstCombine/LLVM/EDSL.lean b/SSA/Projects/InstCombine/LLVM/EDSL.lean
index e33fcedd3..2cfe07f18 100644
--- a/SSA/Projects/InstCombine/LLVM/EDSL.lean
+++ b/SSA/Projects/InstCombine/LLVM/EDSL.lean
@@ -218,7 +218,7 @@ elab "[alive_icom (" mvars:term,* ")| " reg:mlir_region "]" : term => do
   synthesizeSyntheticMVarsNoPostponing
   let com : Q(MLIR.AST.ExceptM (MOp $φ) (Σ (Γ' : Ctxt (MTy $φ)) (ty : (MTy $φ)), Com (MOp $φ) Γ' ty)) ←
     withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
-      withTransparency (mode := TransparencyMode.all) <|
+      withTransparency (mode := TransparencyMode.default) <|
         return ←reduce com
   let comExpr : Expr := com
   trace[Meta] com

From 1a06f33e31337008b857b0b983c3701fe0460dfe Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 17 Apr 2024 19:10:57 +0100
Subject: [PATCH 20/22] chore: document reduction

---
 SSA/Core/MLIRSyntax/EDSL.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/SSA/Core/MLIRSyntax/EDSL.lean b/SSA/Core/MLIRSyntax/EDSL.lean
index da0562cf9..acd7468a2 100644
--- a/SSA/Core/MLIRSyntax/EDSL.lean
+++ b/SSA/Core/MLIRSyntax/EDSL.lean
@@ -37,6 +37,12 @@ def elabIntoCom (region : TSyntax `mlir_region) (Op : Q(Type)) {Ty : Q(Type)}
   let com : Q(MLIR.AST.ExceptM $Op (Σ (Γ' : Ctxt $Ty) (ty : $Ty), Com $Op Γ' ty)) :=
     q(MLIR.AST.mkCom $ast)
   synthesizeSyntheticMVarsNoPostponing
+  /-  Now reduce the term. We do this so that the resulting term will be of the form
+        `Com.lete _ <| Com.lete _ <| ... <| Com.ret _`,
+      rather than still containing the `Transform` machinery applied to a raw AST.
+      This has the side-effect of also fully reducing the expressions involved.
+      We reduce with mode `.default` so that a dialect can prevent reduction of specific parts
+      by marking those `irreducible` -/
   let com : Q(MLIR.AST.ExceptM $Op (Σ (Γ' : Ctxt $Ty) (ty : $Ty), Com $Op Γ' ty)) ←
     withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
       withTransparency (mode := .default) <|

From ae86b8820be3d940e66e998183a9e97cc43f221e Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 21:00:48 +0100
Subject: [PATCH 21/22] chore: remove uses of axiom

Closes https://github.com/opencompl/ssa/issues/240

https://github.com/opencompl/ssa/pull/239 toned down how
aggressive our unfolding is (to be Reducibility.default).
Thus, we can now use `irreducible_def` to hide the implementation of `R.ofZComputable`.
This eliminates our reliance on axioms.
This generally improves the trustworthiness of our development.
---
 .../FullyHomomorphicEncryption/Rewrites.lean  |  4 +-
 .../FullyHomomorphicEncryption/Syntax.lean    | 50 ++++++++++++-------
 2 files changed, 34 insertions(+), 20 deletions(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
index 2c07717e5..3d9357e45 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -100,7 +100,7 @@ def rhs := [fhe_com q, n, hq | {
   "return" (%a) : (! R) -> ()
 }]
 
-/--info: 'lhs' depends on axioms: [propext, Quot.sound, Classical.choice, ROfZComputable_stuck_term] -/
+/--info: 'lhs' depends on axioms: [propext, Quot.sound, Classical.choice] -/
 #guard_msgs in #print axioms lhs
 
 /-  `x^(2^n) + a = a`, since we quotient the polynomial ring with x^(2^n) -/
@@ -146,6 +146,6 @@ noncomputable def p1 : PeepholeRewrite (Op q n) [.polynomialLike] .polynomialLik
       apply Poly.add_f_eq
       done
     }
-/--info: 'p1' depends on axioms: [propext, Classical.choice, Quot.sound, ROfZComputable_stuck_term, ROfZComputable_def] -/
+/--info: 'p1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms p1
 end ExampleModulo
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index 0d0cd203f..b560c8530 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -1,10 +1,11 @@
-/-
+/- := rfl
 Syntax definitions for FHE, providing a custom [fhe_com|...] with syntax sugar.
 
 Authors: Andrés Goens<andres@goens.org>
 -/
 import SSA.Core.MLIRSyntax.EDSL
 import SSA.Projects.FullyHomomorphicEncryption.Basic
+import Mathlib.Tactic.IrreducibleDef
 
 open MLIR AST Ctxt
 open Polynomial -- for R[X] notation
@@ -62,21 +63,6 @@ def mon {Γ : Ctxt (Ty q n)} (a : Var Γ .integer) (i : Var Γ .index) : Expr (O
 
 section CstComputable
 
-
-/-- This definition is subtle.
-
-1.  We make this an axiom so we can strongly normalize terms without lean
-  unfolding the definition
-2. We give it an implemented_by so we can use it in computable code that is used
-   to create the expression in Meta code
-3. We give it an equation lemma to make it what we *really* want in proof mode, which is the coe.
-
-This ensures three properties simultaneously:
-1. We can run it at meta time giving us the `ìmplemented_by` value
-2. It strongly normalizes creating stuck term (`ROfZComputable`)
-3. We can then `simp`it to become the value we really want (`coe z`).
--/
-
 def ROfZComputable_impl (z : ℤ) : R q n :=
   let zq : ZMod q := z
   let p : (ZMod q)[X] := {
@@ -105,11 +91,39 @@ def ROfZComputable_impl (z : ℤ) : R q n :=
   }
   R.fromPoly p
 
+/-#
+Explanation of what's going on:
+- We want to have a `cstComputable : Z -> R`, which achieves three properties:
+1. It is computable, since the meta code needs it to be computable for `[fhe_icom|..]` to elaborate.
+2. It is equal to the noncomputable definition `(coe z : R q n)`
+3. It does not unfold when using `simp_peephole`, so we can rewrite using the equation
+     `ROfZComputable_def` after calling `simp_peephole`.
+
+What we really want is to have the following:
+
+```lean
 @[implemented_by ROfZComputable_impl]
-axiom ROfZComputable_stuck_term (q n : Nat) (z : ℤ) : R q n
+irreducible_noncomputable_def ROfZComputable_stuck_term (q n : Nat) (z : ℤ) :=
+  (↑ z : R q n)
+
+@[simp]
+lemma ROfZComputable_def (q n :Nat) (z : ℤ) : ROfZComputable_stuck_term  q n z = (↑ z : R q n) :=
+  ROfZComputable_stuck_term_def
+```
+
+However, the problem is that `irreducible_noncomputable_def` does not exist, so we fake it,
+by creating a computable `_implemented_by_shim`, and then making this shim an `irreducible_def`.
+-/
+
+@[implemented_by ROfZComputable_impl]
+def ROfZ_computable_stuck_term_implemented_by_shim (q n : Nat) (z : ℤ) := (↑ z : R q n)
+
+irreducible_def ROfZComputable_stuck_term (q n : Nat) (z : ℤ) :=
+  ROfZ_computable_stuck_term_implemented_by_shim q n z
 
 @[simp]
-axiom ROfZComputable_def (q n :Nat) (z : ℤ) : ROfZComputable_stuck_term  q n z = (↑ z : R q n)
+lemma ROfZComputable_def (q n :Nat) (z : ℤ) : ROfZComputable_stuck_term  q n z = (↑ z : R q n) := by
+  simp [ROfZComputable_stuck_term, ROfZ_computable_stuck_term_implemented_by_shim]
 
 def cstComputable {Γ : Ctxt _} (z : Int) : Expr (Op q n) Γ .polynomialLike :=
   Expr.mk

From 0e05c32ac18ca24bfa9be0cd84cf033c8550d028 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 17 Apr 2024 21:44:24 +0100
Subject: [PATCH 22/22] feat: refactor according to @tobiasgrosser, @alexkeizer
 suggestions

---
 .../FullyHomomorphicEncryption/Syntax.lean    | 32 +++++++------------
 1 file changed, 11 insertions(+), 21 deletions(-)

diff --git a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
index b560c8530..821231abc 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Syntax.lean
@@ -1,11 +1,10 @@
-/- := rfl
+/-
 Syntax definitions for FHE, providing a custom [fhe_com|...] with syntax sugar.
 
-Authors: Andrés Goens<andres@goens.org>
+Authors: Andrés Goens<andres@goens.org>, Siddharth Bhat<siddu.druid@gmail.com>
 -/
 import SSA.Core.MLIRSyntax.EDSL
 import SSA.Projects.FullyHomomorphicEncryption.Basic
-import Mathlib.Tactic.IrreducibleDef
 
 open MLIR AST Ctxt
 open Polynomial -- for R[X] notation
@@ -99,31 +98,22 @@ Explanation of what's going on:
 3. It does not unfold when using `simp_peephole`, so we can rewrite using the equation
      `ROfZComputable_def` after calling `simp_peephole`.
 
-What we really want is to have the following:
+We achieve this by the following means:
 
-```lean
-@[implemented_by ROfZComputable_impl]
-irreducible_noncomputable_def ROfZComputable_stuck_term (q n : Nat) (z : ℤ) :=
-  (↑ z : R q n)
-
-@[simp]
-lemma ROfZComputable_def (q n :Nat) (z : ℤ) : ROfZComputable_stuck_term  q n z = (↑ z : R q n) :=
-  ROfZComputable_stuck_term_def
-```
-
-However, the problem is that `irreducible_noncomputable_def` does not exist, so we fake it,
-by creating a computable `_implemented_by_shim`, and then making this shim an `irreducible_def`.
+1. computable => implemented_by.
+2. equal to the noncomputable defn => make this the lean definition.
+3. does not unfold => irreducible, allow using the definition with the lemma `ROfZComputable_def`.
 -/
 
-@[implemented_by ROfZComputable_impl]
-def ROfZ_computable_stuck_term_implemented_by_shim (q n : Nat) (z : ℤ) := (↑ z : R q n)
 
-irreducible_def ROfZComputable_stuck_term (q n : Nat) (z : ℤ) :=
-  ROfZ_computable_stuck_term_implemented_by_shim q n z
+@[irreducible, implemented_by ROfZComputable_impl]
+def ROfZComputable_stuck_term (q n : Nat) (z : ℤ) :=
+  (↑ z : R q n)
 
 @[simp]
 lemma ROfZComputable_def (q n :Nat) (z : ℤ) : ROfZComputable_stuck_term  q n z = (↑ z : R q n) := by
-  simp [ROfZComputable_stuck_term, ROfZ_computable_stuck_term_implemented_by_shim]
+  unfold ROfZComputable_stuck_term
+  rfl
 
 def cstComputable {Γ : Ctxt _} (z : Int) : Expr (Op q n) Γ .polynomialLike :=
   Expr.mk