Add CSE correctness files for Z-specialization

They depend on admitted proofs, currently

4 files changed, 82 insertions, 1 deletions

diff --git a/src/Compilers/CommonSubexpressionEliminationInterp.v b/src/Compilers/CommonSubexpressionEliminationInterp.v
index 2d9115eb6..e0ebf71a4 100644
--- a/src/Compilers/CommonSubexpressionEliminationInterp.v
+++ b/src/Compilers/CommonSubexpressionEliminationInterp.v
@@ -215,3 +215,5 @@ Check @symbolize_exprf.
     apply interp_cse; auto.
   Qed.
 End symbolic.
+
+Hint Rewrite @InterpCSE using solve_wf_side_condition : reflective_interp.
diff --git a/src/Compilers/Z/CommonSubexpressionElimination.v b/src/Compilers/Z/CommonSubexpressionElimination.v
index fa7fd8c4c..d88438b1f 100644
--- a/src/Compilers/Z/CommonSubexpressionElimination.v
+++ b/src/Compilers/Z/CommonSubexpressionElimination.v
@@ -61,6 +61,29 @@ Definition symbolize_op s d (opc : op s d) : symbolic_op
      | Opp T Tout => SOpp
      end.
 
+Definition denote_symbolic_op s d (opc : symbolic_op) : option (op s d)
+  := match opc, s, d with
+     | SOpConst z, Unit, Tbase T => Some (OpConst z)
+     | SAdd, Prod (Tbase _) (Tbase _), Tbase _ => Some (Add _ _ _)
+     | SSub, Prod (Tbase _) (Tbase _), Tbase _ => Some (Sub _ _ _)
+     | SMul, Prod (Tbase _) (Tbase _), Tbase _ => Some (Mul _ _ _)
+     | SShl, Prod (Tbase _) (Tbase _), Tbase _ => Some (Shl _ _ _)
+     | SShr, Prod (Tbase _) (Tbase _), Tbase _ => Some (Shr _ _ _)
+     | SLand, Prod (Tbase _) (Tbase _), Tbase _ => Some (Land _ _ _)
+     | SLor, Prod (Tbase _) (Tbase _), Tbase _ => Some (Lor _ _ _)
+     | SOpp, Tbase _, Tbase _ => Some (Opp _ _)
+     | SAdd, _, _
+     | SSub, _, _
+     | SMul, _, _
+     | SShl, _, _
+     | SShr, _, _
+     | SLand, _, _
+     | SLor, _, _
+     | SOpp, _, _
+     | SOpConst _, _, _
+       => None
+     end.
+
 Lemma symbolic_op_leb_total
   : forall a1 a2, symbolic_op_leb a1 a2 = true \/ symbolic_op_leb a2 a1 = true.
 Proof.
@@ -138,9 +161,13 @@ Definition cse {var} (prefix : list _) {t} (v : expr _ _ t) xs
           normalize_symbolic_expr_mod_c
           var prefix t v xs.
 
-Definition CSE {t} (e : Expr _ _ t) (prefix : forall var, list { t : flat_type base_type & exprf _ _ t })
+Definition CSE_gen {t} (e : Expr _ _ t) (prefix : forall var, list { t : flat_type base_type & exprf _ _ t })
   : Expr _ _ t
   := @CSE base_type symbolic_op base_type_beq symbolic_op_beq
           internal_base_type_dec_bl op symbolize_op
           normalize_symbolic_expr_mod_c
           t e prefix.
+
+Definition CSE {t} (e : Expr _ _ t)
+  : Expr _ _ t
+  := @CSE_gen t e (fun _ => nil).
diff --git a/src/Compilers/Z/CommonSubexpressionEliminationInterp.v b/src/Compilers/Z/CommonSubexpressionEliminationInterp.v
new file mode 100644
index 000000000..6552084d9
--- /dev/null
+++ b/src/Compilers/Z/CommonSubexpressionEliminationInterp.v
@@ -0,0 +1,23 @@
+(** * Common Subexpression Elimination for PHOAS Syntax *)
+Require Import Coq.Lists.List.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.CommonSubexpressionEliminationInterp.
+Require Import Crypto.Compilers.Z.CommonSubexpressionElimination.
+
+Lemma InterpCSE_gen t (e : Expr _ _ t) prefix
+      (Hwf : Wf e)
+  : forall x, Interp interp_op (@CSE_gen t e prefix) x = Interp interp_op e x.
+Proof.
+  apply InterpCSE;
+    auto using internal_base_type_dec_bl, internal_base_type_dec_lb, internal_symbolic_op_dec_bl, internal_symbolic_op_dec_lb, denote_symbolic_op.
+Qed.
+
+Lemma InterpCSE t (e : Expr _ _ t) (Hwf : Wf e)
+  : forall x, Interp interp_op (@CSE t e) x = Interp interp_op e x.
+Proof.
+  apply InterpCSE_gen; auto.
+Qed.
+
+Hint Rewrite @InterpCSE using solve_wf_side_condition : reflective_interp.
diff --git a/src/Compilers/Z/CommonSubexpressionEliminationWf.v b/src/Compilers/Z/CommonSubexpressionEliminationWf.v
new file mode 100644
index 000000000..4f46f9454
--- /dev/null
+++ b/src/Compilers/Z/CommonSubexpressionEliminationWf.v
@@ -0,0 +1,29 @@
+(** * Common Subexpression Elimination for PHOAS Syntax *)
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.CommonSubexpressionEliminationWf.
+Require Import Crypto.Compilers.Z.CommonSubexpressionElimination.
+
+Lemma Wf_CSE_gen t (e : Expr _ _ t)
+      prefix
+      (Hlen : forall var1 var2, length (prefix var1) = length (prefix var2))
+      (Hprefix : forall var1 var2 n t1 t2 e1 e2,
+          List.nth_error (prefix var1) n = Some (existT _ t1 e1)
+          -> List.nth_error (prefix var2) n = Some (existT _ t2 e2)
+          -> exists pf : t1 = t2, wff nil (eq_rect _ (@exprf _ _ _) e1 _ pf) e2)
+      (Hwf : Wf e)
+  : Wf (@CSE_gen t e prefix).
+Proof.
+  apply Wf_CSE; auto using internal_base_type_dec_bl, internal_base_type_dec_lb, internal_symbolic_op_dec_bl, internal_symbolic_op_dec_lb.
+Qed.
+
+Lemma Wf_CSE t (e : Expr _ _ t)
+      (Hwf : Wf e)
+  : Wf (@CSE t e).
+Proof.
+  apply Wf_CSE_gen; simpl; auto.
+  { destruct n; simpl; try congruence. }
+Qed.
+
+Hint Resolve Wf_CSE : wf.