Add correctness of Rewriter

2 files changed, 109 insertions, 0 deletions

diff --git a/src/Reflection/RewriterInterp.v b/src/Reflection/RewriterInterp.v
new file mode 100644
index 000000000..4de516dfd
--- /dev/null
+++ b/src/Reflection/RewriterInterp.v
@@ -0,0 +1,48 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Rewriter.
+Require Import Crypto.Util.Tactics.RewriteHyp.
+
+Section language.
+  Context {base_type_code : Type}
+          {interp_base_type : base_type_code -> Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}.
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Local Notation interp_type := (interp_type interp_base_type).
+  Local Notation interp_flat_type := (interp_flat_type interp_base_type).
+  Local Notation exprf := (@exprf base_type_code op interp_base_type).
+  Local Notation expr := (@expr base_type_code op interp_base_type).
+  Local Notation Expr := (@Expr base_type_code op).
+
+  Section specialized.
+    Context {rewrite_op_expr : forall src dst (opc : op src dst), exprf src -> exprf dst}
+            (Hrewrite : forall src dst opc args,
+                interpf interp_op (rewrite_op_expr src dst opc args)
+                = interp_op _ _ opc (interpf interp_op args)).
+
+    Lemma interpf_rewrite_opf {t} (e : exprf t)
+      : interpf interp_op (rewrite_opf rewrite_op_expr e) = interpf interp_op e.
+    Proof.
+      induction e; simpl; unfold LetIn.Let_In; rewrite_hyp ?*; reflexivity.
+    Qed.
+
+    Lemma interp_rewrite_op {t} (e : expr t)
+      : forall x, interp interp_op (rewrite_op rewrite_op_expr e) x = interp interp_op e x.
+    Proof.
+      destruct e; intro x; apply interpf_rewrite_opf.
+    Qed.
+  End specialized.
+
+  Lemma InterpRewriteOp
+        {rewrite_op_expr}
+        (Hrewrite : forall src dst opc args,
+            interpf interp_op (rewrite_op_expr interp_base_type src dst opc args)
+            = interp_op _ _ opc (interpf interp_op args))
+        {t} (e : Expr t)
+    : forall x, Interp interp_op (RewriteOp rewrite_op_expr e) x = Interp interp_op e x.
+  Proof.
+    apply interp_rewrite_op; assumption.
+  Qed.
+End language.
diff --git a/src/Reflection/RewriterWf.v b/src/Reflection/RewriterWf.v
new file mode 100644
index 000000000..f44832d29
--- /dev/null
+++ b/src/Reflection/RewriterWf.v
@@ -0,0 +1,61 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Reflection.WfInversion.
+Require Import Crypto.Reflection.Rewriter.
+
+Section language.
+  Context {base_type_code : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Local Notation wff := (@wff base_type_code op).
+  Local Notation wf := (@wf base_type_code op).
+  Local Notation Wf := (@Wf base_type_code op).
+  Local Notation exprf := (@exprf base_type_code op).
+  Local Notation expr := (@expr base_type_code op).
+  Local Notation Expr := (@Expr base_type_code op).
+
+  Section with_var.
+    Context {var1 var2 : base_type_code -> Type}
+            {rewrite_op_expr1 : forall src dst (opc : op src dst),
+                exprf (var:=var1) src -> exprf (var:=var1) dst}
+            {rewrite_op_expr2 : forall src dst (opc : op src dst),
+                exprf (var:=var2) src -> exprf (var:=var2) dst}
+            (Hrewrite_wf : forall G src dst opc args1 args2,
+                wff G args1 args2
+                -> wff G
+                       (rewrite_op_expr1 src dst opc args1)
+                       (rewrite_op_expr2 src dst opc args2)).
+
+    Lemma wff_rewrite_opf {t} G (e1 : @exprf var1 t) (e2 : @exprf var2 t)
+          (Hwf : wff G e1 e2)
+      : wff G (rewrite_opf rewrite_op_expr1 e1) (rewrite_opf rewrite_op_expr2 e2).
+    Proof.
+      induction Hwf; simpl; try constructor; auto.
+    Qed.
+
+    Lemma wf_rewrite_opf {t} (e1 : @expr var1 t) (e2 : @expr var2 t)
+          (Hwf : wf e1 e2)
+      : wf (rewrite_op rewrite_op_expr1 e1) (rewrite_op rewrite_op_expr2 e2).
+    Proof.
+      destruct Hwf; simpl; constructor; intros; apply wff_rewrite_opf; auto.
+    Qed.
+  End with_var.
+
+  Lemma Wf_InterpRewriteOp
+        {rewrite_op_expr}
+        (Hrewrite_wff : forall var1 var2 G src dst opc args1 args2,
+            wff G args1 args2
+            -> wff G
+                   (rewrite_op_expr var1 src dst opc args1)
+                   (rewrite_op_expr var2 src dst opc args2))
+        {t} (e : Expr t)
+        (Hwf : Wf e)
+    : Wf (RewriteOp rewrite_op_expr e).
+  Proof.
+    intros var1 var2; apply wf_rewrite_opf; auto.
+  Qed.
+End language.
+
+Hint Resolve Wf_InterpRewriteOp : wf.