Add compiler optimization for add-with-carry

This closes #171.

It's unfortunately a bit fragile, and takes a really long time (about
60s) to prove correct, because Coq is bad at deep dependent pattern
matching.

We enable a-normal form for the freeze test, because the rewriter only
works when the arguments to adc are var or const.

7 files changed, 547 insertions, 1 deletions

diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index e7c267d65..8a43a0ec7 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -65,6 +65,9 @@ Require Import Crypto.Compilers.LinearizeWf.
 Require Import Crypto.Compilers.Z.CommonSubexpressionEliminationInterp.
 Require Import Crypto.Compilers.Z.CommonSubexpressionEliminationWf.*)
 Require Import Crypto.Compilers.Z.ArithmeticSimplifierWf.
+Require Import Crypto.Compilers.Z.RewriteAddToAdc.
+Require Import Crypto.Compilers.Z.RewriteAddToAdcWf.
+Require Import Crypto.Compilers.Z.RewriteAddToAdcInterp.
 Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn.
 Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnInterp.
 Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnWf.
@@ -91,6 +94,7 @@ Definition PostWfPipeline
         let e := SimplifyArith e in
         let e := if opts.(anf) then ANormal e else e in
         let e := InlineConst e in
+        let e := RewriteAdc e in
         (*let e := CSE false e in*)
         let e := MapCast _ e input_bounds in
         option_map
diff --git a/src/Compilers/Z/Named/RewriteAddToAdc.v b/src/Compilers/Z/Named/RewriteAddToAdc.v
new file mode 100644
index 000000000..c64663c8b
--- /dev/null
+++ b/src/Compilers/Z/Named/RewriteAddToAdc.v
@@ -0,0 +1,97 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Compilers.Named.Context.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Named.GetNames.
+Require Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Notations.
+
+Local Open Scope Z_scope.
+
+Section named.
+  Context {Name : Type}
+          (name_beq : Name -> Name -> bool).
+  Import Named.Syntax.
+  Local Notation flat_type := (flat_type base_type).
+  Local Notation type := (type base_type).
+  Local Notation exprf := (@exprf base_type op Name).
+  Local Notation expr := (@expr base_type op Name).
+
+  Local Notation tZ := (Tbase TZ).
+  Local Notation ADC bw c x y := (Op (@AddWithGetCarry bw TZ TZ TZ TZ TZ)
+                                     (Pair (Pair (t1:=tZ) c (t2:=tZ) x) (t2:=tZ) y)).
+  Local Notation ADD bw x y := (ADC bw (Op (OpConst 0) TT) x y).
+  Local Notation ADX x y := (Op (@Add TZ TZ TZ) (Pair (t1:=tZ) x (t2:=tZ) y)).
+  Local Infix "=Z?" := Z.eqb.
+  Local Infix "=n?" := name_beq.
+
+  Definition is_const_or_var {t} (v : exprf t)
+    := match v with
+       | Var _ _ => true
+       | Op _ _ (OpConst _ _) TT => true
+       | _ => false
+       end.
+
+  Fixpoint name_list_has_duplicate (ls : list Name) : bool
+    := match ls with
+       | nil => false
+       | cons n ns
+         => orb (name_list_has_duplicate ns)
+                (List.fold_left orb (List.map (name_beq n) ns) false)
+       end.
+
+  Definition do_rewrite
+             {t} (e : exprf t)
+    : option (exprf t)
+    := match e in Named.exprf _ _ _ t return option (exprf t) with
+       |           (nlet (a2, c1) : tZ * tZ := (ADD bw1 a b as ex0) in P0)
+         => match P0 in Named.exprf _ _ _ t return option (exprf t) with
+            |      (nlet (s , c2) : tZ * tZ := (ADD bw2 c0 (Var _ a2') as ex1) in P1)
+              => match P1 in Named.exprf _ _ _ t return option (exprf t) with
+                 | (nlet c        : tZ      := (ADX (Var _ c1') (Var _ c2') as ex2) in P)
+                   => if (((bw1 =Z? bw2) && (a2 =n? a2') && (c1 =n? c1') && (c2 =n? c2'))
+                            && (is_const_or_var c0 && is_const_or_var a && is_const_or_var b)
+                            && negb (name_list_has_duplicate (a2::c1::s::c2::c::nil ++ get_namesf c0 ++ get_namesf a ++ get_namesf b)%list))
+                      then Some (nlet (a2, c1) : tZ * tZ := ex0 in
+                                 nlet (s , c2) : tZ * tZ := ex1 in
+                                 nlet c        : tZ      := ex2 in
+                                 nlet (s, c)   : tZ * tZ := ADC bw1 c0 a b in
+                                 P)
+                      else None
+                 | P1' => None
+                 end
+            | P0' => None
+            end
+       | _ => None
+       end%core%nexpr%bool.
+
+  Definition do_rewriteo {t} (e : exprf t) : exprf t
+    := match do_rewrite e with
+       | Some e' => e'
+       | None => e
+       end.
+
+  Definition rewrite_exprf_prestep
+             (rewrite_exprf : forall {t} (e : exprf t), exprf t)
+             {t} (e : exprf t)
+    : exprf t
+    := match e in Named.exprf _ _ _ t return exprf t with
+       | TT => TT
+       | Var _ n => Var n
+       | Op _ _ opc args
+         => Op opc (@rewrite_exprf _ args)
+       | (nlet nx := ex in eC)
+         => (nlet nx := @rewrite_exprf _ ex in @rewrite_exprf _ eC)
+       | Pair tx ex ty ey
+         => Pair (@rewrite_exprf tx ex) (@rewrite_exprf ty ey)
+       end%nexpr.
+
+  Fixpoint rewrite_exprf {t} (e : exprf t) : exprf t
+    := do_rewriteo (@rewrite_exprf_prestep (@rewrite_exprf) t e).
+
+  Definition rewrite_expr {t} (e : expr t) : expr t
+    := match e in Named.expr _ _ _ t return expr t with
+       | Abs _ _ n f => Abs n (rewrite_exprf f)
+       end.
+End named.
diff --git a/src/Compilers/Z/Named/RewriteAddToAdcInterp.v b/src/Compilers/Z/Named/RewriteAddToAdcInterp.v
new file mode 100644
index 000000000..91a73cfc6
--- /dev/null
+++ b/src/Compilers/Z/Named/RewriteAddToAdcInterp.v
@@ -0,0 +1,281 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Compilers.Named.Context.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.Proper.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Equality.
+Require Import Crypto.Compilers.Z.Named.RewriteAddToAdc.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.ZUtil.AddGetCarry.
+Require Import Crypto.Util.Decidable.
+
+Local Open Scope Z_scope.
+
+Section named.
+  Context {Name : Type}
+          {InterpContext : Context Name interp_base_type}
+          {InterpContextOk : ContextOk InterpContext}
+          (Name_beq : Name -> Name -> bool)
+          (Name_bl : forall n1 n2, Name_beq n1 n2 = true -> n1 = n2)
+          (Name_lb : forall n1 n2, n1 = n2 -> Name_beq n1 n2 = true).
+
+  Local Notation exprf := (@exprf base_type op Name).
+  Local Notation expr := (@expr base_type op Name).
+  Local Notation do_rewrite := (@do_rewrite Name Name_beq).
+  Local Notation do_rewriteo := (@do_rewriteo Name Name_beq).
+  Local Notation rewrite_exprf := (@rewrite_exprf Name Name_beq).
+  Local Notation rewrite_exprf_prestep := (@rewrite_exprf_prestep Name).
+  Local Notation rewrite_expr := (@rewrite_expr Name Name_beq).
+
+  Local Instance Name_dec : DecidableRel (@eq Name)
+    := dec_rel_of_bool_dec_rel Name_beq Name_bl Name_lb.
+
+  Local Notation retT e re :=
+    (forall (ctx : InterpContext)
+            v,
+        Named.interpf (interp_op:=interp_op) (ctx:=ctx) re = Some v
+        -> Named.interpf (interp_op:=interp_op) (ctx:=ctx) e = Some v)
+      (only parsing).
+  Local Notation tZ := (Tbase TZ).
+  Local Notation ADC bw c x y := (Op (@AddWithGetCarry bw TZ TZ TZ TZ TZ)
+                                     (Pair (Pair (t1:=tZ) c (t2:=tZ) x) (t2:=tZ) y)).
+  Local Notation ADD bw x y := (ADC bw (Op (OpConst 0) TT) x y).
+  Local Notation ADX x y := (Op (@Add TZ TZ TZ) (Pair (t1:=tZ) x (t2:=tZ) y)).
+
+  Local Ltac simple_t_step :=
+    first [ discriminate
+          | exact I
+          | progress intros
+          | progress subst
+          | progress inversion_option ].
+  Local Ltac destruct_t_step :=
+    first [ break_innermost_match_hyps_step
+          | break_innermost_match_step ].
+  Local Ltac do_small_inversion e :=
+    is_var e;
+    lazymatch type of e with
+    | exprf ?T
+      => revert dependent e;
+         let P := match goal with |- forall e, @?P e => P end in
+         intro e;
+         lazymatch T with
+         | Unit
+           => refine match e in Named.exprf _ _ _ t return match t return Named.exprf _ _ _ t -> _ with Unit => P | _ => fun _ => True end e with TT => _ | _ => _ end
+         | tZ
+           => refine match e in Named.exprf _ _ _ t return match t return Named.exprf _ _ _ t -> _ with tZ => P | _ => fun _ => True end e with TT => _ | _ => _ end
+         | (tZ * tZ)%ctype
+           => refine match e in Named.exprf _ _ _ t return match t return Named.exprf _ _ _ t -> _ with (tZ * tZ)%ctype => P | _ => fun _ => True end e with TT => _ | _ => _ end
+         | (tZ * tZ * tZ)%ctype
+           => refine match e in Named.exprf _ _ _ t return match t return Named.exprf _ _ _ t -> _ with (tZ * tZ * tZ)%ctype => P | _ => fun _ => True end e with TT => _ | _ => _ end
+         end;
+         try exact I
+    | op ?a ?T
+      => first [ is_var a;
+                 move e at top;
+                 revert dependent a;
+                 let P := match goal with |- forall a e, @?P a e => P end in
+                 intros a e;
+                 lazymatch T with
+                 | tZ
+                   => refine match e in op a t return match t return op a t -> _ with tZ => P a | _ => fun _ => True end e with OpConst _ _ => _ | _ => _ end
+                 | (tZ * tZ)%ctype
+                   => refine match e in op a t return match t return op a t -> _ with (tZ * tZ)%ctype => P a | _ => fun _ => True end e with OpConst _ _ => _ | _ => _ end
+                 end ];
+         try exact I
+    end.
+  Local Ltac small_inversion_step _ :=
+    match goal with
+    | [ H : match ?e with _ => _ end = Some _ |- _ ] => do_small_inversion e
+    | [ H : match ?e with _ => _ end = true |- _ ] => do_small_inversion e
+    | [ H : match ?e with _ => _ end _ = Some _ |- _ ] => do_small_inversion e
+    end.
+
+  Local Ltac rewrite_lookupb_step :=
+    first [ rewrite !lookupb_extendb_different in * by (assumption || congruence)
+          | rewrite !lookupb_extendb_same in * by assumption
+          | rewrite !lookupb_extendb_wrong_type in * by (assumption || congruence)
+          | match goal with
+            | [ H : context[lookupb (extendb _ _ _) _] |- _ ] => revert H
+            | [ |- context[lookupb (extendb _ ?n _) ?n'] ]
+              => (tryif constr_eq n n' then fail else idtac);
+                 lazymatch goal with
+                 | [ H : n = n' |- _ ] => fail
+                 | [ H : n' = n |- _ ] => fail
+                 | [ H : n <> n' |- _ ] => fail
+                 | [ H : n' <> n |- _ ] => fail
+                 | _ => destruct (dec (n = n')); subst
+                 end
+            | [ |- context[lookupb (t:=?t0) (extendb (t:=?t1) _ _ _) _] ]
+              => (tryif constr_eq t0 t1 then fail else idtac);
+                 lazymatch goal with
+                 | [ H : t0 = t1 |- _ ] => fail
+                 | [ H : t1 = t0 |- _ ] => fail
+                 | [ H : t0 <> t1 |- _ ] => fail
+                 | [ H : t1 <> t0 |- _ ] => fail
+                 | _ => destruct (dec (t0 = t1)); subst
+                 end
+            end ].
+  Local Ltac rewrite_lookupb := repeat rewrite_lookupb_step.
+
+  Local Ltac do_rewrite_adc' P :=
+    let lem := open_constr:(Z.add_get_carry_to_add_with_get_carry_cps _ _ _ _ P) in
+    let T := type of lem in
+    let T := (eval cbv [Let_In Definitions.Z.add_with_get_carry Definitions.Z.add_with_get_carry Definitions.Z.get_carry Definitions.Z.add_get_carry] in T) in
+    etransitivity; [ | eapply (lem : T) ];
+    try reflexivity.
+  Local Ltac do_rewrite_adc :=
+    first [ do_rewrite_adc' uconstr:(fun a b => Some b)
+          | do_rewrite_adc' uconstr:(fun a b => Some a) ].
+
+  Lemma interpf_do_rewrite
+        {t} {e e' : exprf t}
+        (H : do_rewrite e = Some e')
+    : retT e e'.
+  Proof.
+    unfold do_rewrite in H;
+      repeat first [ simple_t_step
+                   | small_inversion_step ()
+                   | destruct_t_step ].
+    Time all:match goal with
+             | [ H : _ = ?x |- _ = ?x ] => rewrite <- H; clear H
+             end.
+    Time all:split_andb.
+    Time all:progress simpl @negb in *.
+    Time all:repeat match goal with
+                    | [ H : Name_beq _ _ = true |- _ ] => apply Name_bl in H
+                    | [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H
+                    end.
+    Time all:subst.
+    Local Ltac do_small_inversion_ctx :=
+      repeat match goal with
+             | [ H : is_const_or_var ?e = true |- _ ]
+               => do_small_inversion e; break_innermost_match; intros; try exact I;
+                  simpl in H; try solve [ clear -H; discriminate ]
+             | [ H : match ?e with _ => _ end = true |- _ ]
+               => do_small_inversion e; break_innermost_match; intros; try exact I;
+                  simpl in H; try solve [ clear -H; discriminate ]
+             | [ H : match ?e with _ => _ end _ = true |- _ ]
+               => do_small_inversion e; break_innermost_match; intros; try exact I;
+                  simpl in H; try solve [ clear -H; discriminate ]
+             end.
+    Time all:do_small_inversion_ctx.
+    Time all:simpl @negb in *.
+    Time all:rewrite !Bool.negb_orb in *.
+    Time all:split_andb.
+    Time all:rewrite !Bool.negb_true_iff in *.
+    Time all:repeat
+               match goal with
+               | [ H : Name_beq ?x ?y = false |- _ ]
+                 => assert (x <> y) by (clear -H Name_lb; intro; rewrite Name_lb in H by assumption; congruence);
+                      clear H
+               end.
+    Time all:subst.
+    Time all:simpl @interpf in *.
+    Time all:cbv [interp_op option_map lift_op Zinterp_op] in *; simpl in *.
+    Time all:unfold Let_In in * |- .
+    Time all:break_innermost_match; try reflexivity.
+    Local Ltac t_fin_step :=
+      match goal with
+      | [ |- ?x = ?x ] => reflexivity
+      | [ H : ?x = Some _ |- context[?x] ] => rewrite H
+      | [ H : ?x = None |- context[?x] ] => rewrite H
+      | [ H : ?x = Some ?a, H' : ?x = Some ?b |- _ ]
+        => assert (a = b) by congruence; (subst a || subst b)
+      | _ => progress rewrite_lookupb
+      | _ => progress simpl in *
+      | _ => progress intros
+      | _ => progress subst
+      | _ => progress inversion_option
+      | [ |- (dlet x := _ in _) = (dlet y := _ in _) ]
+        => apply Proper_Let_In_nd_changebody_eq; intros ??
+      | _ => progress unfold Let_In
+      | [ |- interpf ?x = interpf ?x ]
+        => eapply @interpf_Proper; [ eauto with typeclass_instances.. | intros ?? | reflexivity ]
+      | _ => progress break_innermost_match; try reflexivity
+      | _ => progress break_innermost_match_hyps; try reflexivity
+      | _ => progress break_match; try reflexivity
+      end.
+    Local Ltac t_fin :=
+      repeat t_fin_step;
+      try do_rewrite_adc.
+    { Time t_fin. }
+    { Time t_fin. }
+    { Time t_fin. }
+    { Time t_fin. }
+    { Time t_fin. }
+    { Time t_fin. }
+    { Time t_fin. }
+    { Time t_fin. }
+  Time Qed.
+
+  Lemma interpf_do_rewriteo
+        {t} {e : exprf t}
+    : retT e (do_rewriteo e).
+  Proof.
+    unfold do_rewriteo; intros *; break_innermost_match; try congruence.
+    apply interpf_do_rewrite; assumption.
+  Qed.
+
+  Local Opaque RewriteAddToAdc.do_rewriteo.
+  Lemma interpf_rewrite_exprf
+        {t} (e : exprf t)
+    : retT e (rewrite_exprf e).
+  Proof.
+    pose t as T.
+    pose (rewrite_exprf_prestep (@rewrite_exprf) e) as E.
+    induction e; simpl in *;
+      intros ctx v H;
+      pose proof (interpf_do_rewriteo (t:=T) (e:=E) ctx v H); clear H;
+      subst T E;
+      repeat first [ assumption
+                   | progress unfold option_map, Let_In in *
+                   | progress simpl in *
+                   | progress subst
+                   | progress inversion_option
+                   | apply (f_equal (@Some _))
+                   | break_innermost_match_step
+                   | break_innermost_match_hyps_step
+                   | congruence
+                   | solve [ eauto ]
+                   | match goal with
+                     | [ IH : forall ctx v, interpf ?e = Some v -> _ = Some _, H' : interpf ?e = Some _ |- _ ]
+                       => specialize (IH _ _ H')
+                     | [ H : ?x = Some ?a, H' : ?x = Some ?b |- _ ]
+                       => assert (a = b) by congruence; (subst a || subst b)
+                     | [ |- ?rhs = Some _ ]
+                       => lazymatch rhs with
+                          | Some _ => fail
+                          | None => fail
+                          | _ => destruct rhs eqn:?
+                          end
+                     end ].
+  Qed.
+
+  Lemma interp_rewrite_expr
+        {t} (e : expr t)
+    : forall (ctx : InterpContext)
+             v x,
+      Named.interp (interp_op:=interp_op) (ctx:=ctx) (rewrite_expr e) x = Some v
+      -> Named.interp (interp_op:=interp_op) (ctx:=ctx) e x = Some v.
+  Proof.
+    unfold Named.interp, rewrite_expr; destruct e; simpl.
+    intros *; apply interpf_rewrite_exprf.
+  Qed.
+
+  Lemma Interp_rewrite_expr
+        {t} (e : expr t)
+    : forall v x,
+      Named.Interp (Context:=InterpContext) (interp_op:=interp_op) (rewrite_expr e) x = Some v
+      -> Named.Interp (Context:=InterpContext) (interp_op:=interp_op) e x = Some v.
+  Proof.
+    intros *; apply interp_rewrite_expr.
+  Qed.
+End named.
diff --git a/src/Compilers/Z/RewriteAddToAdc.v b/src/Compilers/Z/RewriteAddToAdc.v
new file mode 100644
index 000000000..5f3fc05c5
--- /dev/null
+++ b/src/Compilers/Z/RewriteAddToAdc.v
@@ -0,0 +1,58 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Compilers.Named.Context.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.InterpretToPHOAS.
+Require Import Crypto.Compilers.Named.Compile.
+Require Import Crypto.Compilers.Named.Wf.
+Require Import Crypto.Compilers.Named.CountLets.
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.PositiveContext.Defaults.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Named.DeadCodeElimination.
+Require Import Crypto.Compilers.Z.Named.RewriteAddToAdc.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Decidable.
+
+(** N.B. This procedure only works when there are no nested lets,
+    i.e., nothing like [let x := let y := z in w] in the PHOAS syntax
+    tree.  This is a limitation of [compile]. *)
+
+Local Open Scope bool_scope.
+
+Section language.
+  Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl).
+
+  Definition RewriteAdc {t} (e : Expr base_type op t)
+    : Expr base_type op t
+    := let is_good e' := match option_map (wf_unit (Context:=PContext _) empty) e' with
+                         | Some (Some trivial) => true
+                         | _ => false
+                         end in
+       let interp_to_phoas := InterpToPHOAS (Context:=fun var => PContext var)
+                                            (fun _ t => Op (OpConst 0%Z) TT) in
+       let e' := compile (e _) (DefaultNamesFor e) in
+       let e' := option_map (rewrite_expr Pos.eqb) e' in
+       let good := is_good e' in
+       let e' := match e' with
+                 | Some e'
+                   => let ls := Named.default_names_for e' in
+                      match EliminateDeadCode (Context:=PContext _) e' ls with
+                      | Some e'' => Some e''
+                      | None => Some e'
+                      end
+                 | None => None
+                 end in
+       let good := good && is_good e' in
+       if good
+       then let e' := option_map interp_to_phoas e' in
+            match e' with
+            | Some e'
+              => match t return Expr _ _ (Arrow (domain t) (codomain t)) -> Expr _ _ t with
+                 | Arrow _ _ => fun x => x
+                 end e'
+            | None => e
+            end
+       else e.
+End language.
diff --git a/src/Compilers/Z/RewriteAddToAdcInterp.v b/src/Compilers/Z/RewriteAddToAdcInterp.v
new file mode 100644
index 000000000..4269cf09c
--- /dev/null
+++ b/src/Compilers/Z/RewriteAddToAdcInterp.v
@@ -0,0 +1,71 @@
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.PositiveContext.DefaultsProperties.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.InterpretToPHOASInterp.
+Require Import Crypto.Compilers.Named.CompileWf.
+Require Import Crypto.Compilers.Named.CompileInterp.
+Require Import Crypto.Compilers.Named.WfFromUnit.
+Require Import Crypto.Compilers.Named.DeadCodeEliminationInterp.
+Require Import Crypto.Compilers.Named.WfInterp.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.RewriteAddToAdc.
+Require Import Crypto.Compilers.Z.Named.RewriteAddToAdcInterp.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Bool.
+
+Section language.
+  Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl).
+
+  Lemma InterpRewriteAdc
+        {t} (e : Expr base_type op t) (Hwf : Wf e)
+  : forall x, Interp interp_op (RewriteAdc e) x = Interp interp_op e x.
+  Proof.
+    intro x; unfold RewriteAdc, option_map; break_innermost_match; try reflexivity;
+      match goal with |- ?x = ?y => cut (Some x = Some y); [ congruence | ] end;
+      (etransitivity; [ symmetry; eapply @Interp_InterpToPHOAS with (t:=Arrow _ _) | ]);
+      repeat
+        repeat
+        first [ lazymatch goal with
+                | [ H : DeadCodeElimination.EliminateDeadCode _ _ = Some ?e |- Syntax.Named.Interp ?e _ = Some _ ]
+                  => let lhs := match goal with |- ?lhs = _ => lhs end in
+                     let v := fresh in
+                     (destruct lhs as [v|] eqn:?);
+                     [ apply f_equal; eapply @InterpEliminateDeadCode with (Name_beq:=BinPos.Pos.eqb);
+                       [ .. | eassumption | try eassumption | try eassumption ]; clear H | ]
+                | [ |- Syntax.Named.Interp (RewriteAddToAdc.rewrite_expr _ ?e) _ = Some _ ]
+                  => let lhs := match goal with |- ?lhs = _ => lhs end in
+                     let H := fresh in
+                     destruct lhs eqn:H; [ apply (f_equal (@Some _)); eapply @Interp_rewrite_expr in H | ]
+                | [ H : Compile.compile (?e _) _ = Some ?e'', H' : Syntax.Named.Interp ?e'' ?x = Some ?v' |- ?v' = Interp ?interp_op' ?e ?x ]
+                  => eapply @Interp_compile with (v:=x) (interp_op:=interp_op') in H
+                end
+              | intros; eapply (@PositiveContextOk _ _ base_type_beq internal_base_type_dec_bl internal_base_type_dec_lb)
+              | progress split_andb
+              | congruence
+              | tauto
+              | solve [ auto | eapply @BinPos.Pos.eqb_eq; auto ]
+              | eapply @Wf_from_unit
+              | eapply @dec_rel_of_bool_dec_rel
+              | eapply @internal_base_type_dec_lb
+              | eapply @internal_base_type_dec_bl
+              | eapply @InterpEliminateDeadCode; [ .. | eassumption | eassumption | ]
+              | apply name_list_unique_DefaultNamesFor
+              | progress intros
+              | rewrite !@lookupb_empty
+              | eapply @wf_from_unit with (uContext:=PContext _); [ .. | eassumption ]
+              | match goal with
+                | [ H : Syntax.Named.Interp ?e ?x = Some ?a, H' : Syntax.Named.Interp ?e ?x = Some ?b |- _ ]
+                  => assert (a = b) by congruence; (subst a || subst b)
+                end
+              | lazymatch goal with
+                | [ |- Some _ = Some _ ] => fail
+                | [ |- None = Some _ ] => exfalso; eapply @wf_interp_not_None; [ .. | unfold Syntax.Named.Interp in *; eassumption ]
+                | [ |- ?x = Some _ ] => destruct x eqn:?; [ apply f_equal | ]
+                end ].
+  Qed.
+End language.
+
+Hint Rewrite @InterpRewriteAdc using solve_wf_side_condition : reflective_interp.
diff --git a/src/Compilers/Z/RewriteAddToAdcWf.v b/src/Compilers/Z/RewriteAddToAdcWf.v
new file mode 100644
index 000000000..3b9fb1ff5
--- /dev/null
+++ b/src/Compilers/Z/RewriteAddToAdcWf.v
@@ -0,0 +1,35 @@
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.InterpretToPHOASWf.
+Require Import Crypto.Compilers.Named.CompileWf.
+Require Import Crypto.Compilers.Named.WfFromUnit.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.RewriteAddToAdc.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Bool.
+
+Section language.
+  Local Hint Resolve internal_base_type_dec_lb internal_base_type_dec_lb dec_rel_of_bool_dec_rel : typeclass_instances.
+
+  Lemma Wf_RewriteAdc {t} (e : Expr base_type op t) (Hwf : Wf e)
+  : Wf (RewriteAdc e).
+  Proof.
+    unfold RewriteAdc, option_map; break_innermost_match;
+      [ .. | solve [ intros var1 var2; destruct (Hwf var1 var2); auto with wf ] ];
+      repeat first [ eapply @Wf_InterpToPHOAS with (t:=Arrow _ _)
+                   | progress split_andb
+                   | congruence
+                   | intros; eapply @PositiveContextOk
+                   | solve [ auto | eapply @BinPos.Pos.eqb_eq ]
+                   | eapply @Wf_from_unit
+                   | eapply @dec_rel_of_bool_dec_rel
+                   | eapply @internal_base_type_dec_lb
+                   | eapply @internal_base_type_dec_bl
+                   | intros var1 var2; specialize (Hwf var1 var2); destruct Hwf;
+                     constructor; assumption ].
+  Qed.
+End language.
+
+Hint Resolve Wf_RewriteAdc : wf.
diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v
index 12f107be6..74731f6c6 100644
--- a/src/Specific/IntegrationTestFreeze.v
+++ b/src/Specific/IntegrationTestFreeze.v
@@ -71,7 +71,7 @@ Section BoundedField25p5.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
     (* jgross start here! *)
     (*Set Ltac Profiling.*)
-    Time refine_reflectively. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *)
+    Time refine_reflectively_with anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *)
     (*Show Ltac Profile.*)
     (* total time:      5.680s