Add InlineConstAndOpByRewrite

10 files changed, 480 insertions, 2 deletions

diff --git a/src/Compilers/InlineConstAndOpByRewrite.v b/src/Compilers/InlineConstAndOpByRewrite.v
new file mode 100644
index 000000000..d1d610f8b
--- /dev/null
+++ b/src/Compilers/InlineConstAndOpByRewrite.v
@@ -0,0 +1,93 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.Rewriter.
+
+Module Export Rewrite.
+  Section language.
+    Context {base_type_code : Type}
+            {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+            {interp_base_type : base_type_code -> Type}
+            (interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d).
+    Local Notation flat_type := (flat_type base_type_code).
+    Local Notation type := (type base_type_code).
+    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 {var : base_type_code -> Type}
+              (invert_Const : forall s d, op s d -> @exprf var s -> option (interp_flat_type interp_base_type d))
+              (Const : forall t, interp_base_type t -> @exprf var (Tbase t)).
+
+      Local Notation invert_PairsConst' T
+        := (@invert_PairsConst base_type_code interp_base_type op var invert_Const T).
+      Local Notation invert_PairsConst
+        := (invert_PairsConst' _).
+
+      Definition rewrite_for_const_and_op src dst (opc : op src dst) (args : @exprf var src)
+        : @exprf var dst
+        := match invert_PairsConst args with
+           | Some argsv
+             => SmartPairf (SmartVarfMap Const (interp_op _ _ opc argsv))
+           | None => Op opc args
+           end.
+
+      Definition inline_const_and_op_genf {t} (e : @exprf var t) : @exprf var t
+        := @rewrite_opf base_type_code op var rewrite_for_const_and_op t e.
+      Definition inline_const_and_op_gen {t} (e : @expr var t) : @expr var t
+        := @rewrite_op base_type_code op var rewrite_for_const_and_op t e.
+    End with_var.
+
+
+    Section const_unit.
+      Context {var : base_type_code -> Type}
+              (OpConst : forall t, interp_base_type t -> op Unit (Tbase t)).
+
+      Definition invert_ConstUnit' {s d} : op s d -> option (interp_flat_type interp_base_type d)
+        := match s with
+           | Unit
+             => fun opv => Some (interp_op _ _ opv tt)
+           | _ => fun _ => None
+           end.
+      Definition invert_ConstUnit {s d} (opv : op s d) (e : @exprf var s)
+        : option (interp_flat_type interp_base_type d)
+        := invert_ConstUnit' opv.
+
+      Definition Const {t} v := Op (var:=var) (OpConst t v) TT.
+
+      Definition inline_const_and_opf {t}
+        := @inline_const_and_op_genf var (@invert_ConstUnit) (@Const) t.
+      Definition inline_const_and_op {t}
+        := @inline_const_and_op_gen var (@invert_ConstUnit) (@Const) t.
+    End const_unit.
+
+    Definition InlineConstAndOpGen
+               (invert_Const : forall var s d, op s d -> @exprf var s -> option (interp_flat_type interp_base_type d))
+               (Const : forall var t, interp_base_type t -> @exprf var (Tbase t))
+               {t} (e : Expr t)
+      : Expr t
+      := @RewriteOp
+           base_type_code op
+           (fun var => @rewrite_for_const_and_op var (invert_Const _) (Const _))
+           t
+           e.
+
+    Definition InlineConstAndOp
+               (OpConst : forall t, interp_base_type t -> op Unit (Tbase t))
+               {t} (e : Expr t)
+      : Expr t
+      := @RewriteOp
+           base_type_code op
+           (fun var => @rewrite_for_const_and_op var (@invert_ConstUnit _) (@Const _ OpConst))
+           t
+           e.
+  End language.
+
+  Global Arguments inline_const_and_op_genf {_ _ _} interp_op {var} invert_Const Const {t} _ : assert.
+  Global Arguments inline_const_and_op_gen {_ _ _} interp_op {var} invert_Const Const {t} _ : assert.
+  Global Arguments inline_const_and_opf {_ _ _} interp_op {var} OpConst {t} _ : assert.
+  Global Arguments inline_const_and_op {_ _ _} interp_op {var} OpConst {t} _ : assert.
+  Global Arguments InlineConstAndOpGen {_ _ _} interp_op invert_Const Const {t} _ var : assert.
+  Global Arguments InlineConstAndOp {_ _ _} interp_op OpConst {t} _ var : assert.
+End Rewrite.
diff --git a/src/Compilers/InlineConstAndOpByRewriteInterp.v b/src/Compilers/InlineConstAndOpByRewriteInterp.v
new file mode 100644
index 000000000..33e525ed4
--- /dev/null
+++ b/src/Compilers/InlineConstAndOpByRewriteInterp.v
@@ -0,0 +1,136 @@
+(** * Inline: Remove some [Let] expressions, inline constants, interpret constant operations *)
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.Rewriter.
+Require Import Crypto.Compilers.RewriterInterp.
+Require Import Crypto.Compilers.InlineConstAndOpByRewrite.
+Require Import Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Option.
+Require Import Crypto.Util.Tactics.BreakMatch.
+
+Module Export Rewrite.
+  Local Open Scope ctype_scope.
+  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).
+    Local Notation expr := (@expr base_type_code op).
+    Local Notation Expr := (@Expr base_type_code op).
+
+    Section with_invert.
+      Context (invert_Const : forall s d, op s d -> @exprf interp_base_type s -> option (interp_flat_type d))
+              (Const : forall t, interp_base_type t -> @exprf interp_base_type (Tbase t))
+              (Hinvert_Const
+               : forall s d opc e v, invert_Const s d opc e = Some v
+                                     -> interp_op s d opc (interpf interp_op e) = v)
+              (interpf_Const : forall t v, interpf interp_op (Const t v) = v).
+
+      Lemma interpf_rewrite_for_const_and_op s d opc args
+        : interpf interp_op (rewrite_for_const_and_op interp_op invert_Const Const s d opc args)
+          = interp_op _ _ opc (interpf interp_op args).
+      Proof using Hinvert_Const interpf_Const.
+        cbv [rewrite_for_const_and_op].
+        repeat first [ break_innermost_match_step
+                     | reflexivity
+                     | progress cbn [interpf exprf_of_inline_directive interpf_step LetIn.Let_In SmartVarVarf fst snd] in *
+                     | rewrite interpf_SmartPairf
+                     | rewrite SmartVarfMap_compose
+                     | rewrite SmartVarfMap_id
+                     | setoid_rewrite interpf_Const
+                     | erewrite interpf_invert_PairsConst by eassumption ].
+      Qed.
+
+      Lemma interpf_inline_const_and_op_genf
+            {t} e
+        : interpf interp_op (inline_const_and_op_genf (t:=t) interp_op invert_Const Const e)
+          = interpf interp_op e.
+      Proof.
+        unfold inline_const_and_op_genf;
+          eapply interpf_rewrite_opf; eauto using interpf_rewrite_for_const_and_op.
+      Qed.
+
+      Lemma interpf_inline_const_and_op_gen
+            {t} e
+        : forall x,
+          interp interp_op (inline_const_and_op_gen (t:=t) interp_op invert_Const Const e) x
+          = interp interp_op e x.
+      Proof.
+        unfold inline_const_and_op_gen;
+          eapply interp_rewrite_op; eauto using interpf_rewrite_for_const_and_op.
+      Qed.
+    End with_invert.
+
+    Section const_unit.
+      Context (OpConst : forall t, interp_base_type t -> op Unit (Tbase t))
+              (interp_op_OpConst : forall t v, interp_op _ _ (OpConst t v) tt = v).
+
+      Lemma interpf_invert_ConstUnit s d opc e v
+            (H : invert_ConstUnit interp_op opc e = Some v)
+        : interp_op s d opc (interpf interp_op e) = v.
+      Proof using Type.
+        destruct s; simpl in *; inversion_option; subst.
+        edestruct interpf; reflexivity.
+      Qed.
+
+      Lemma interpf_Const t v
+        : interpf interp_op (Const OpConst (t:=t) v) = v.
+      Proof using interp_op_OpConst.
+        apply interp_op_OpConst.
+      Qed.
+
+      Lemma interpf_inline_const_and_opf
+            {t} e
+        : interpf interp_op (inline_const_and_opf (t:=t) interp_op OpConst e)
+          = interpf interp_op e.
+      Proof.
+        unfold inline_const_and_opf;
+          eapply interpf_rewrite_opf; eauto using interpf_rewrite_for_const_and_op, interpf_invert_ConstUnit, interpf_Const.
+      Qed.
+
+      Lemma interpf_inline_const_and_op
+            {t} e
+        : forall x,
+          interp interp_op (inline_const_and_op (t:=t) interp_op OpConst e) x
+          = interp interp_op e x.
+      Proof.
+        unfold inline_const_and_op;
+          eapply interp_rewrite_op; eauto using interpf_rewrite_for_const_and_op, interpf_invert_ConstUnit, interpf_Const.
+      Qed.
+    End const_unit.
+
+    Lemma InterpInlineConstAndOpGen
+          (invert_Const : forall var s d, op s d -> @exprf var s -> option (interp_flat_type d))
+          (Const : forall var t, interp_base_type t -> @exprf var (Tbase t))
+
+          {t} (e : Expr t)
+          (Hinvert_Const
+           : forall s d opc e v,
+              invert_Const _ s d opc e = Some v
+              -> interp_op s d opc (interpf interp_op e) = v)
+          (interpf_Const : forall t v, interpf interp_op (Const _ t v) = v)
+      : forall x, Interp interp_op (InlineConstAndOpGen interp_op invert_Const Const e) x = Interp interp_op e x.
+    Proof using Type.
+      eapply InterpRewriteOp;
+        eauto using interpf_rewrite_for_const_and_op, interpf_invert_ConstUnit, interpf_Const.
+    Qed.
+
+    Lemma InterpInlineConstAndOp
+          (OpConst : forall t, interp_base_type t -> op Unit (Tbase t))
+          {t} (e : Expr t)
+          (interp_op_OpConst : forall t v, interp_op _ _ (OpConst t v) tt = v)
+      : forall x, Interp interp_op (InlineConstAndOp interp_op OpConst e) x = Interp interp_op e x.
+    Proof using Type.
+      eapply InterpRewriteOp;
+        eauto using interpf_rewrite_for_const_and_op, interpf_invert_ConstUnit, interpf_Const.
+    Qed.
+  End language.
+
+  Hint Rewrite @InterpInlineConstAndOp @InterpInlineConstAndOpGen using assumption : reflective_interp.
+End Rewrite.
diff --git a/src/Compilers/InlineConstAndOpByRewriteWf.v b/src/Compilers/InlineConstAndOpByRewriteWf.v
new file mode 100644
index 000000000..c1d06be99
--- /dev/null
+++ b/src/Compilers/InlineConstAndOpByRewriteWf.v
@@ -0,0 +1,171 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.WfProofs.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfInversion.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.Rewriter.
+Require Import Crypto.Compilers.RewriterWf.
+Require Import Crypto.Compilers.InlineConstAndOpByRewrite.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Option.
+
+Module Export Rewrite.
+  Section language.
+    Context {base_type_code : Type}
+            {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+            {interp_base_type : base_type_code -> Type}.
+
+    Local Notation flat_type := (flat_type base_type_code).
+    Local Notation type := (type base_type_code).
+    Local Notation Tbase := (@Tbase base_type_code).
+    Local Notation exprf := (@exprf base_type_code op).
+    Local Notation expr := (@expr base_type_code op).
+    Local Notation Expr := (@Expr base_type_code op).
+    Local Notation wff := (@wff base_type_code op).
+    Local Notation wf := (@wf base_type_code op).
+
+    Local Hint Constructors Wf.wff.
+
+    Section with_var.
+      Context {interp_op1 : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}
+              {interp_op2 : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}
+              {var1 var2 : base_type_code -> Type}
+              {invert_Const1 : forall s d, op s d -> @exprf var1 s -> option (interp_flat_type interp_base_type d)}
+              {invert_Const2 : forall s d, op s d -> @exprf var2 s -> option (interp_flat_type interp_base_type d)}
+              {Const1 : forall t, interp_base_type t -> @exprf var1 (Tbase t)}
+              {Const2 : forall t, interp_base_type t -> @exprf var2 (Tbase t)}
+              (Hinterp_op : forall s d opv args, interp_op1 s d opv args = interp_op2 s d opv args)
+              (Hinvert_Const : forall s d opv G e1 e2, wff G e1 e2 -> invert_Const1 s d opv e1 = invert_Const2 s d opv e2)
+              (HConst : forall t v G, wff G (Const1 t v) (Const2 t v)).
+
+
+      Local Ltac t_fin :=
+        repeat first [ intro
+                     | exfalso; assumption
+                     | exact I
+                     | progress destruct_head'_prod
+                     | progress destruct_head'_and
+                     | progress destruct_head'_sig
+                     | progress subst
+                     | rewrite Hinterp_op
+                     | rewrite SmartPairf_Pair
+                     | tauto
+                     | solve [ auto with nocore
+                             | apply wff_SmartPairf_SmartVarfMap_same; auto ]
+                     | progress simpl in *
+                     | constructor
+                     | solve [ eauto ]
+                     | progress inversion_wf_constr
+                     | match goal with
+                       | [ H : invert_PairsConst _ _ = ?x, H' : invert_PairsConst _ _ = ?y |- _ ]
+                         => assert (x = y)
+                           by (rewrite <- H, <- H'; eapply wff_invert_PairsConst; [ eauto | eassumption ]);
+                            inversion_option;
+                            progress (subst || congruence)
+                       end
+                     | break_innermost_match_hyps_step
+                     | break_innermost_match_step ].
+      Lemma wff_rewrite_for_const_and_op G s d opc args1 args2
+            (Hwf : wff G (var1:=var1) (var2:=var2) args1 args2)
+        : wff G
+              (rewrite_for_const_and_op interp_op1 invert_Const1 Const1 s d opc args1)
+              (rewrite_for_const_and_op interp_op2 invert_Const2 Const2 s d opc args2).
+      Proof using HConst Hinterp_op Hinvert_Const. cbv [rewrite_for_const_and_op]; t_fin. Qed.
+
+      Lemma wff_inline_const_and_op_genf {t} e1 e2 G
+            (wf : wff G e1 e2)
+        : @wff var1 var2 G t
+               (inline_const_and_op_genf interp_op1 invert_Const1 Const1 e1)
+               (inline_const_and_op_genf interp_op2 invert_Const2 Const2 e2).
+      Proof using HConst Hinvert_Const Hinterp_op.
+        unfold inline_const_and_op_genf;
+          eauto using wff_rewrite_opf, wff_rewrite_for_const_and_op.
+      Qed.
+
+      Lemma wff_inline_const_and_op_gen {t} e1 e2
+            (Hwf : wf e1 e2)
+        : @wf var1 var2 t
+              (inline_const_and_op_gen interp_op1 invert_Const1 Const1 e1)
+              (inline_const_and_op_gen interp_op2 invert_Const2 Const2 e2).
+      Proof using HConst Hinvert_Const Hinterp_op.
+        unfold inline_const_and_op_gen;
+          eauto using wf_rewrite_op, wff_rewrite_for_const_and_op.
+      Qed.
+    End with_var.
+
+    Section const_unit.
+      Context {interp_op1 : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}
+              {interp_op2 : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}
+              {var1 var2 : base_type_code -> Type}
+              (OpConst1 OpConst2 : forall t, interp_base_type t -> op Unit (Tbase t))
+              (HOpConst : forall t v, OpConst1 t v = OpConst2 t v)
+              (Hinterp_op : forall s d opv args, interp_op1 s d opv args = interp_op2 s d opv args).
+
+      Lemma wff_invert_ConstUnit
+            s d opv e1 e2
+        : @invert_ConstUnit _ _ _ interp_op1 var1 s d opv e1
+          = @invert_ConstUnit _ _ _ interp_op2 var2 s d opv e2.
+      Proof using Hinterp_op.
+        cbv [invert_ConstUnit invert_ConstUnit']; destruct s; f_equal; auto.
+      Qed.
+
+      Lemma wff_Const {t} v G
+        : wff G (@Const _ _ _ var1 OpConst1 t v) (@Const _ _ _ var2 OpConst2 t v).
+      Proof using HOpConst.
+        cbv [Const]; rewrite HOpConst; auto.
+      Qed.
+
+      Lemma wff_inline_const_and_opf {t} e1 e2 G
+            (wf : wff G e1 e2)
+        : @wff var1 var2 G t
+               (inline_const_and_opf interp_op1 OpConst1 e1)
+               (inline_const_and_opf interp_op2 OpConst2 e2).
+      Proof using HOpConst Hinterp_op.
+        unfold inline_const_and_opf;
+          eauto using wff_inline_const_and_op_genf, wff_invert_ConstUnit, wff_Const.
+      Qed.
+
+      Lemma wff_inline_const_and_op {t} e1 e2
+            (Hwf : wf e1 e2)
+        : @wf var1 var2 t (inline_const_and_op interp_op1 OpConst1 e1) (inline_const_and_op interp_op2 OpConst2 e2).
+      Proof using HOpConst Hinterp_op.
+        unfold inline_const_and_op;
+          eauto using wff_inline_const_and_op_gen, wff_invert_ConstUnit, wff_Const.
+      Qed.
+    End const_unit.
+
+    Lemma Wf_InlineConstAndOpGen
+          {interp_op}
+          (invert_Const : forall var s d, op s d -> @exprf var s -> option (interp_flat_type interp_base_type d))
+          (Const : forall var t, interp_base_type t -> @exprf var (Tbase t))
+          (Hinvert_Const
+           : forall var1 var2 s d opv G e1 e2,
+              wff G e1 e2
+              -> invert_Const var1 s d opv e1 = invert_Const var2 s d opv e2)
+          (HConst
+           : forall var1 var2 t v G,
+              wff G (Const var1 t v) (Const var2 t v))
+          {t} (e : Expr t)
+          (Hwf : Wf e)
+      : Wf (InlineConstAndOpGen interp_op invert_Const Const e).
+    Proof using Type.
+      unfold InlineConstAndOpGen;
+        eauto using Wf_RewriteOp, wff_rewrite_for_const_and_op.
+    Qed.
+
+    Lemma Wf_InlineConstAndOp
+          {interp_op}
+          (OpConst : forall t, interp_base_type t -> op Unit (Tbase t))
+          {t} (e : Expr t)
+          (Hwf : Wf e)
+      : Wf (InlineConstAndOp interp_op OpConst e).
+    Proof using Type.
+      unfold InlineConstAndOp;
+        eauto using Wf_RewriteOp, wff_rewrite_for_const_and_op, wff_Const.
+    Qed.
+  End language.
+
+  Hint Resolve Wf_InlineConstAndOpGen Wf_InlineConstAndOp : wf.
+End Rewrite.
diff --git a/src/Compilers/RewriterWf.v b/src/Compilers/RewriterWf.v
index 0dfdbaab6..22c135d00 100644
--- a/src/Compilers/RewriterWf.v
+++ b/src/Compilers/RewriterWf.v
@@ -35,7 +35,7 @@ Section language.
       induction Hwf; simpl; try constructor; auto.
     Qed.
 
-    Lemma wf_rewrite_opf {t} (e1 : @expr var1 t) (e2 : @expr var2 t)
+    Lemma wf_rewrite_op {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 using Type*.
@@ -54,7 +54,7 @@ Section language.
         (Hwf : Wf e)
     : Wf (RewriteOp rewrite_op_expr e).
   Proof using Type.
-    intros var1 var2; apply wf_rewrite_opf; auto.
+    intros var1 var2; apply wf_rewrite_op; auto.
   Qed.
 End language.
 
diff --git a/src/Compilers/Z/InlineConstAndOpByRewrite.v b/src/Compilers/Z/InlineConstAndOpByRewrite.v
new file mode 100644
index 000000000..f4403e12b
--- /dev/null
+++ b/src/Compilers/Z/InlineConstAndOpByRewrite.v
@@ -0,0 +1,13 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InlineConstAndOpByRewrite.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+
+Module Export Rewrite.
+  Definition inline_const_and_opf {var} {t} (e : exprf _ _ t) : @exprf base_type op var t
+    := @inline_const_and_opf base_type op interp_base_type (@interp_op) var make_const t e.
+  Definition inline_const_and_op {var} {t} (e : expr _ _ t) : @expr base_type op var t
+    := @inline_const_and_op base_type op interp_base_type (@interp_op) var make_const t e.
+  Definition InlineConstAndOp {t} (e : Expr t) : Expr t
+    := @InlineConstAndOp base_type op interp_base_type interp_op make_const t e.
+End Rewrite.
diff --git a/src/Compilers/Z/InlineConstAndOpByRewriteInterp.v b/src/Compilers/Z/InlineConstAndOpByRewriteInterp.v
new file mode 100644
index 000000000..e67442c71
--- /dev/null
+++ b/src/Compilers/Z/InlineConstAndOpByRewriteInterp.v
@@ -0,0 +1,12 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InlineConstAndOpByRewriteInterp.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.InlineConstAndOpByRewrite.
+
+Module Export Rewrite.
+  Definition InterpInlineConstAndOp {t} (e : Expr t)
+  : forall x, Interp (InlineConstAndOp e) x = Interp e x
+    := @InterpInlineConstAndOp _ _ _ _ _ t e Syntax.Util.make_const_correct.
+
+  Hint Rewrite @InterpInlineConstAndOp : reflective_interp.
+End Rewrite.
diff --git a/src/Compilers/Z/InlineConstAndOpByRewriteWf.v b/src/Compilers/Z/InlineConstAndOpByRewriteWf.v
new file mode 100644
index 000000000..aa883f5e7
--- /dev/null
+++ b/src/Compilers/Z/InlineConstAndOpByRewriteWf.v
@@ -0,0 +1,13 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.InlineConstAndOpByRewriteWf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.InlineConstAndOpByRewrite.
+
+Module Export Rewrite.
+  Definition Wf_InlineConstAndOp {t} (e : Expr t) (Hwf : Wf e)
+  : Wf (InlineConstAndOp e)
+    := @Wf_InlineConstAndOp _ _ _ _ _ t e Hwf.
+
+  Hint Resolve Wf_InlineConstAndOp : wf.
+End Rewrite.
diff --git a/src/Compilers/ZExtended/InlineConstAndOpByRewrite.v b/src/Compilers/ZExtended/InlineConstAndOpByRewrite.v
new file mode 100644
index 000000000..418a0e0f3
--- /dev/null
+++ b/src/Compilers/ZExtended/InlineConstAndOpByRewrite.v
@@ -0,0 +1,12 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InlineConstAndOpByRewrite.
+Require Import Crypto.Compilers.ZExtended.Syntax.
+
+Module Export Rewrite.
+  Definition inline_const_and_opf {var} {t} (e : exprf _ _ t) : @exprf base_type op var t
+    := @inline_const_and_opf base_type op interp_base_type (@interp_op) var (@Const) t e.
+  Definition inline_const_and_op {var} {t} (e : expr _ _ t) : @expr base_type op var t
+    := @inline_const_and_op base_type op interp_base_type (@interp_op) var (@Const) t e.
+  Definition InlineConstAndOp {t} (e : Expr t) : Expr t
+    := @InlineConstAndOp base_type op interp_base_type (@interp_op) (@Const) t e.
+End Rewrite.
diff --git a/src/Compilers/ZExtended/InlineConstAndOpByRewriteInterp.v b/src/Compilers/ZExtended/InlineConstAndOpByRewriteInterp.v
new file mode 100644
index 000000000..64d5263a7
--- /dev/null
+++ b/src/Compilers/ZExtended/InlineConstAndOpByRewriteInterp.v
@@ -0,0 +1,15 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InlineConstAndOpByRewriteInterp.
+Require Import Crypto.Compilers.ZExtended.Syntax.
+Require Import Crypto.Compilers.ZExtended.InlineConstAndOpByRewrite.
+
+Module Export Rewrite.
+  Lemma InterpInlineConstAndOp {t} (e : Expr t)
+  : forall x, Interp (InlineConstAndOp e) x = Interp e x.
+  Proof.
+    refine (@InterpInlineConstAndOp _ _ _ _ _ t e _).
+    clear; abstract (intros []; intros; reflexivity).
+  Defined.
+
+  Hint Rewrite @InterpInlineConstAndOp : reflective_interp.
+End Rewrite.
diff --git a/src/Compilers/ZExtended/InlineConstAndOpByRewriteWf.v b/src/Compilers/ZExtended/InlineConstAndOpByRewriteWf.v
new file mode 100644
index 000000000..281bee6ab
--- /dev/null
+++ b/src/Compilers/ZExtended/InlineConstAndOpByRewriteWf.v
@@ -0,0 +1,13 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.InlineConstAndOpByRewriteWf.
+Require Import Crypto.Compilers.ZExtended.Syntax.
+Require Import Crypto.Compilers.ZExtended.InlineConstAndOpByRewrite.
+
+Module Export Rewrite.
+  Definition Wf_InlineConstAndOp {t} (e : Expr t) (Hwf : Wf e)
+  : Wf (InlineConstAndOp e)
+    := @Wf_InlineConstAndOp _ _ _ _ _ t e Hwf.
+
+  Hint Resolve Wf_InlineConstAndOp : wf.
+End Rewrite.