Add adc -> sbb to arithmetic simplifer

After    | File Name                                            | Before   || Change
---------------------------------------------------------------------------------------
6m14.04s | Total                                                | 6m23.68s || -0m09.63s
---------------------------------------------------------------------------------------
0m26.28s | Compilers/Z/ArithmeticSimplifierWf                   | 0m48.67s || -0m22.39s
0m25.64s | Compilers/Z/ArithmeticSimplifierInterp               | 0m14.14s || +0m11.50s
2m17.60s | Specific/IntegrationTestLadderstep                   | 2m17.90s || -0m00.30s
0m56.48s | Compilers/Z/Named/RewriteAddToAdcInterp              | 0m55.76s || +0m00.71s
0m54.26s | Specific/IntegrationTestLadderstep130                | 0m54.53s || -0m00.27s
0m15.89s | Specific/IntegrationTestFreeze                       | 0m15.07s || +0m00.82s
0m11.69s | Specific/IntegrationTestMul                          | 0m11.78s || -0m00.08s
0m10.62s | Specific/ArithmeticSynthesisTest                     | 0m10.59s || +0m00.02s
0m10.54s | Specific/IntegrationTestSub                          | 0m10.55s || -0m00.01s
0m08.98s | Specific/IntegrationTestSquare                       | 0m09.04s || -0m00.05s
0m06.05s | Arithmetic/Saturated                                 | 0m06.02s || +0m00.03s
0m03.04s | Compilers/Z/RewriteAddToAdcInterp                    | 0m03.00s || +0m00.04s
0m02.60s | Compilers/Z/Bounds/Pipeline/Definition               | 0m02.25s || +0m00.35s
0m01.52s | Util/ZUtil/AddGetCarry                               | 0m01.50s || +0m00.02s
0m00.74s | Arithmetic/MontgomeryReduction/WordByWord/Definition | 0m00.71s || +0m00.03s
0m00.62s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics        | 0m00.78s || -0m00.16s
0m00.59s | Compilers/Z/ArithmeticSimplifier                     | 0m00.42s || +0m00.17s
0m00.57s | Compilers/Z/Bounds/Pipeline                          | 0m00.60s || -0m00.03s
0m00.34s | Compilers/Z/ArithmeticSimplifierUtil                 | 0m00.37s || -0m00.02s

5 files changed, 276 insertions, 36 deletions

diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v
index 7a2a73434..2690f2dfb 100644
--- a/src/Compilers/Z/ArithmeticSimplifier.v
+++ b/src/Compilers/Z/ArithmeticSimplifier.v
@@ -176,6 +176,110 @@ Section language.
                  | _
                    => Op opc args
                  end
+         | AddWithCarry TZ TZ TZ TZ as opc
+           => fun args
+              => match interp_as_expr_or_const args with
+                 | Some (const_of c, const_of x, const_of y)
+                   => Op (OpConst (interp_op _ _ opc (c, x, y))) TT
+                 | Some (c, gen_expr x, y)
+                   => let y' := match y with
+                                | const_of y => if (y <? 0)%Z
+                                                then Some (Op (OpConst (-y)) TT)
+                                                else None
+                                | neg_expr y => Some y
+                                | gen_expr _ => None
+                                end in
+                      match y' with
+                      | Some y => Op (SubWithBorrow TZ TZ TZ TZ)
+                                     (match c with
+                                      | const_of c => Op (OpConst (-c)) TT
+                                      | neg_expr c => c
+                                      | gen_expr c => Op (Opp TZ TZ) c
+                                      end,
+                                      x, y)%expr
+                      | None => Op opc args
+                      end
+                 | _ => Op opc args
+                 end
+         | AddWithGetCarry bw TZ TZ TZ TZ TZ as opc
+           => fun args
+              => match interp_as_expr_or_const args with
+                 | Some (const_of c, const_of x, const_of y)
+                   => let '(v, c) := interp_op _ _ opc (c, x, y) in
+                      (Op (OpConst v) TT, Op (OpConst c) TT)%expr
+                 | Some (c, gen_expr x, y)
+                   => let y' := match y with
+                                | const_of y => if (y <? 0)%Z
+                                                then Some (Op (OpConst (-y)) TT)
+                                                else None
+                                | neg_expr y => Some y
+                                | gen_expr _ => None
+                                end in
+                      match y' with
+                      | Some y => LetIn (Op (SubWithGetBorrow bw TZ TZ TZ TZ TZ)
+                                            (match c with
+                                             | const_of c => Op (OpConst (-c)) TT
+                                             | neg_expr c => c
+                                             | gen_expr c => Op (Opp TZ TZ) c
+                                             end,
+                                             x, y)%expr)
+                                        (fun '(v, c) => (Var v, Op (Opp TZ TZ) (Var c))%expr)
+                      | None => Op opc args
+                      end
+                 | _ => Op opc args
+                 end
+         | SubWithBorrow TZ TZ TZ TZ as opc
+           => fun args
+              => match interp_as_expr_or_const args with
+                 | Some (const_of c, const_of x, const_of y)
+                   => Op (OpConst (interp_op _ _ opc (c, x, y))) TT
+                 | Some (c, gen_expr x, y)
+                   => let y' := match y with
+                                | const_of y => if (y <? 0)%Z
+                                                then Some (Op (OpConst (-y)) TT)
+                                                else None
+                                | neg_expr y => Some y
+                                | gen_expr _ => None
+                                end in
+                      match y' with
+                      | Some y => Op (AddWithCarry TZ TZ TZ TZ)
+                                     (match c with
+                                      | const_of c => Op (OpConst (-c)) TT
+                                      | neg_expr c => c
+                                      | gen_expr c => Op (Opp TZ TZ) c
+                                      end,
+                                      x, y)%expr
+                      | None => Op opc args
+                      end
+                 | _ => Op opc args
+                 end
+         | SubWithGetBorrow bw TZ TZ TZ TZ TZ as opc
+           => fun args
+              => match interp_as_expr_or_const args with
+                 | Some (const_of c, const_of x, const_of y)
+                   => let '(v, c) := interp_op _ _ opc (c, x, y) in
+                      (Op (OpConst v) TT, Op (OpConst c) TT)%expr
+                 | Some (c, gen_expr x, y)
+                   => let y' := match y with
+                                | const_of y => if (y <? 0)%Z
+                                                then Some (Op (OpConst (-y)) TT)
+                                                else None
+                                | neg_expr y => Some y
+                                | gen_expr _ => None
+                                end in
+                      match y' with
+                      | Some y => LetIn (Op (AddWithGetCarry bw TZ TZ TZ TZ TZ)
+                                            (match c with
+                                             | const_of c => Op (OpConst (-c)) TT
+                                             | neg_expr c => c
+                                             | gen_expr c => Op (Opp TZ TZ) c
+                                             end,
+                                             x, y)%expr)
+                                        (fun '(v, c) => (Var v, Op (Opp TZ TZ) (Var c))%expr)
+                      | None => Op opc args
+                      end
+                 | _ => Op opc args
+                 end
          | Add _ _ _ as opc
          | Sub _ _ _ as opc
          | Mul _ _ _ as opc
diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v
index 6eec2f2a4..1f638c076 100644
--- a/src/Compilers/Z/ArithmeticSimplifierInterp.v
+++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v
@@ -10,6 +10,7 @@ Require Import Crypto.Compilers.Z.ArithmeticSimplifier.
 Require Import Crypto.Compilers.Z.ArithmeticSimplifierUtil.
 Require Import Crypto.Compilers.Z.Syntax.Equality.
 Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.AddGetCarry.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Sum.
@@ -36,6 +37,7 @@ Local Ltac break_t_step :=
         | progress inversion_prod
         | progress inversion_inverted_expr
         | progress inversion_flat_type
+        | progress subst_prod
         | progress destruct_head'_and
         | progress destruct_head'_prod
         | progress eliminate_hprop_eq
@@ -72,6 +74,12 @@ Proof.
                    | progress invert_op ]. }
 Qed.
 
+Local Ltac rewrite_interp_as_expr_or_const_correct_base _ :=
+  match goal with
+  | [ |- context[interpf _ ?e] ]
+    => erewrite !(@interp_as_expr_or_const_correct_base _ e) by eassumption; cbv beta iota
+  end.
+
 Lemma interp_as_expr_or_const_correct_prod_base {A B} e (v : _ * _)
   : @interp_as_expr_or_const interp_base_type (Prod (Tbase A) (Tbase B)) e = Some v
     -> interpf interp_op e = (match fst v with
@@ -90,9 +98,48 @@ Proof.
                  | progress simpl in *
                  | progress intros
                  | break_t_step
-                 | erewrite !interp_as_expr_or_const_correct_base by eassumption; cbv beta iota ].
+                 | rewrite_interp_as_expr_or_const_correct_base () ].
+Qed.
+
+Local Ltac rewrite_interp_as_expr_or_const_correct_prod_base _ :=
+  match goal with
+  | [ |- context[interpf _ ?e] ]
+    => erewrite !(@interp_as_expr_or_const_correct_prod_base _ _ e) by eassumption; cbv beta iota
+  end.
+
+Lemma interp_as_expr_or_const_correct_prod3_base {A B C} e (v : _ * _ * _)
+  : @interp_as_expr_or_const interp_base_type (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e = Some v
+    -> interpf interp_op e = (match fst (fst v) with
+                              | const_of z => cast_const (t1:=TZ) z
+                              | gen_expr e => interpf interp_op e
+                              | neg_expr e => interpf interp_op (Op (Opp _ _) e)
+                              end,
+                              match snd (fst v) with
+                              | const_of z => cast_const (t1:=TZ) z
+                              | gen_expr e => interpf interp_op e
+                              | neg_expr e => interpf interp_op (Op (Opp _ _) e)
+                              end,
+                              match snd v with
+                              | const_of z => cast_const (t1:=TZ) z
+                              | gen_expr e => interpf interp_op e
+                              | neg_expr e => interpf interp_op (Op (Opp _ _) e)
+                              end).
+Proof.
+  invert_expr;
+    repeat first [ fin_t
+                 | progress simpl in *
+                 | progress intros
+                 | break_t_step
+                 | rewrite_interp_as_expr_or_const_correct_base ()
+                 | rewrite_interp_as_expr_or_const_correct_prod_base () ].
 Qed.
 
+Local Ltac rewrite_interp_as_expr_or_const_correct_prod3_base _ :=
+  match goal with
+  | [ |- context[interpf _ ?e] ]
+    => erewrite !(@interp_as_expr_or_const_correct_prod3_base _ _ _ e) by eassumption; cbv beta iota
+  end.
+
 Local Arguments Z.mul !_ !_.
 Local Arguments Z.add !_ !_.
 Local Arguments Z.sub !_ !_.
@@ -104,17 +151,18 @@ Proof.
   apply InterpRewriteOp; intros; unfold simplify_op_expr.
   break_innermost_match;
     repeat first [ fin_t
+                 | progress cbv [LetIn.Let_In]
                  | progress simpl in *
                  | progress subst
-                 | erewrite !interp_as_expr_or_const_correct_prod_base by eassumption; cbv beta iota
-                 | erewrite !interp_as_expr_or_const_correct_base by eassumption; cbv beta iota
-                 | match goal with
-                   | [ |- context[interpf _ ?e] ]
-                     => erewrite !(@interp_as_expr_or_const_correct_base _ e) by eassumption; cbv beta iota
-                   end
+                 | progress subst_prod
+                 | rewrite_interp_as_expr_or_const_correct_base ()
+                 | rewrite_interp_as_expr_or_const_correct_prod_base ()
+                 | rewrite_interp_as_expr_or_const_correct_prod3_base ()
                  | progress unfold interp_op, lift_op
                  | progress Z.ltb_to_lt
-                 | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r ].
+                 | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r
+                 | rewrite !Z.sub_with_borrow_to_add_get_carry
+                 | progress autorewrite with zsimplify_fast ].
 Qed.
 
 Hint Rewrite @InterpSimplifyArith : reflective_interp.
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v
index 157cdfe8f..ff5068b89 100644
--- a/src/Compilers/Z/ArithmeticSimplifierWf.v
+++ b/src/Compilers/Z/ArithmeticSimplifierWf.v
@@ -28,7 +28,14 @@ Local Ltac fin_t :=
         | reflexivity
         | congruence
         | assumption
-        | exfalso; assumption ].
+        | exfalso; assumption
+        | match goal with
+          | [ |- _ /\ False ] => exfalso
+          | [ |- False /\ _ ] => exfalso
+          | [ |- _ /\ _ /\ False ] => exfalso
+          | [ |- _ /\ False /\ _ ] => exfalso
+          | [ |- False /\ _ /\ _ ] => exfalso
+          end ].
 Local Ltac break_t_step :=
   first [ progress subst
         | progress inversion_option
@@ -43,6 +50,7 @@ Local Ltac break_t_step :=
         | progress destruct_head'_sig
         | progress specialize_by reflexivity
         | progress eliminate_hprop_eq
+        | progress break_innermost_match_hyps_step
         | progress break_innermost_match_step
         | progress break_match_hyps
         | progress inversion_wf_constr ].
@@ -79,6 +87,18 @@ Proof.
   erewrite <- interp_as_expr_or_const_None_iff by eassumption; congruence.
 Qed.
 
+Local Ltac pret_step :=
+  first [ fin_t
+        | progress subst
+        | progress inversion_option
+        | progress inversion_prod
+        | progress simpl in *
+        | progress inversion_wf
+        | match goal with
+          | [ H : match interp_as_expr_or_const ?e with _ => _ end = Some _ |- _ ]
+            => is_var e; destruct (interp_as_expr_or_const e) eqn:?
+          end ].
+
 Lemma wff_interp_as_expr_or_const_base {var1 var2 t} {G e1 e2 v1 v2}
       (Hwf : @wff var1 var2 G (Tbase t) e1 e2)
   : @interp_as_expr_or_const var1 (Tbase t) e1 = Some v1
@@ -105,6 +125,12 @@ Proof.
                      end ].
 Qed.
 
+Local Ltac pose_wff_base :=
+  match goal with
+  | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
+    => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2
+  end.
+
 Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _ * _}
       (Hwf : wff G e1 e2)
   : @interp_as_expr_or_const var1 (Prod (Tbase A) (Tbase B)) e1 = Some v1
@@ -132,39 +158,96 @@ Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _
 Proof.
   invert_one_expr e1; intros; break_innermost_match; intros; try exact I;
     try invert_one_expr e2; intros; break_innermost_match; intros; try exact I;
-      repeat first [ fin_t
-                   | progress simpl in *
+      repeat first [ pret_step
+                   | pose_wff_base
                    | break_t_step
-                   | match goal with
-                     | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
-                       => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2
-                     | [ |- and _ _ ] => split
-                     end ].
+                   | apply conj ].
 Qed.
 
+Local Ltac pose_wff_prod :=
+  match goal with
+  | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
+    => pose proof (wff_interp_as_expr_or_const_prod_base Hwf H1 H2); clear H1 H2
+  end.
+
+Lemma wff_interp_as_expr_or_const_prod3_base {var1 var2 A B C} {G e1 e2} {v1 v2 : _ * _ * _}
+      (Hwf : wff G e1 e2)
+  : @interp_as_expr_or_const var1 (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e1 = Some v1
+    -> @interp_as_expr_or_const var2 (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e2 = Some v2
+    -> match fst (fst v1), fst (fst v2) with
+       | const_of z1, const_of z2 => z1 = z2
+       | gen_expr e1, gen_expr e2
+       | neg_expr e1, neg_expr e2
+         => wff G e1 e2
+       | const_of _, _
+       | gen_expr _, _
+       | neg_expr _, _
+         => False
+       end
+       /\ match snd (fst v1), snd (fst v2) with
+          | const_of z1, const_of z2 => z1 = z2
+          | gen_expr e1, gen_expr e2
+          | neg_expr e1, neg_expr e2
+            => wff G e1 e2
+          | const_of _, _
+          | gen_expr _, _
+          | neg_expr _, _
+            => False
+          end
+       /\ match snd v1, snd v2 with
+          | const_of z1, const_of z2 => z1 = z2
+          | gen_expr e1, gen_expr e2
+          | neg_expr e1, neg_expr e2
+            => wff G e1 e2
+          | const_of _, _
+          | gen_expr _, _
+          | neg_expr _, _
+            => False
+          end.
+Proof.
+  invert_one_expr e1; intros; break_innermost_match; intros; try exact I;
+    try invert_one_expr e2; intros; break_innermost_match; intros; try exact I;
+      repeat first [ pret_step
+                   | pose_wff_base
+                   | pose_wff_prod
+                   | break_t_step
+                   | apply conj ].
+Qed.
+
+Local Ltac pose_wff_prod3 :=
+  match goal with
+  | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
+    => pose proof (wff_interp_as_expr_or_const_prod3_base Hwf H1 H2); clear H1 H2
+  end.
+
 Lemma Wf_SimplifyArith {t} (e : Expr t)
       (Hwf : Wf e)
   : Wf (SimplifyArith e).
 Proof.
   apply Wf_RewriteOp; [ | assumption ].
   intros ???????? Hwf'; unfold simplify_op_expr;
-    break_innermost_match; repeat constructor; auto;
-      repeat first [ fin_t
-                   | progress simpl in *
-                   | progress subst
-                   | progress Z.ltb_to_lt
-                   | match goal with
-                     | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
-                       => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2
-                     | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
-                       => pose proof (wff_interp_as_expr_or_const_prod_base Hwf H1 H2); clear H1 H2
-                     | [ H1 : _ = Some _, H2 : _ = None, Hwf : wff _ _ _ |- _ ]
-                       => pose proof (interp_as_expr_or_const_Some_None Hwf H1 H2); clear H1 H2
-                     | [ H1 : _ = None, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
-                       => pose proof (interp_as_expr_or_const_None_Some Hwf H1 H2); clear H1 H2
-                     | [ |- wff _ _ _ ] => constructor
-                     end
-                   | break_t_step ].
+    repeat match goal with
+           | [ H : ?T |- ?T ] => exact H
+           | [ H : False |- _ ] => exfalso; assumption
+           | [ H : false = true |- _ ] => exfalso; clear -H; discriminate
+           | [ H : true = false |- _ ] => exfalso; clear -H; discriminate
+           | _ => pose_wff_base
+           | _ => pose_wff_prod
+           | _ => pose_wff_prod3
+           | _ => progress destruct_head'_and
+           | _ => progress subst
+           | [ H1 : _ = Some _, H2 : _ = None, Hwf : wff _ _ _ |- _ ]
+             => pose proof (interp_as_expr_or_const_Some_None Hwf H1 H2); clear H1 H2
+           | [ H1 : _ = None, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
+             => pose proof (interp_as_expr_or_const_None_Some Hwf H1 H2); clear H1 H2
+           | [ |- wff _ (Op _ _) (LetIn _ _) ] => exfalso
+           | [ |- wff _ (LetIn _ _) (Op _ _) ] => exfalso
+           | [ |- wff _ (Pair _ _) (LetIn _ _) ] => exfalso
+           | [ |- wff _ (LetIn _ _) (Pair _ _) ] => exfalso
+           | [ |- wff _ _ _ ] => constructor; intros
+           | [ |- List.In _ _ ] => progress (simpl; auto)
+           | _ => break_innermost_match_step; simpl in *
+           end.
 Qed.
 
 Hint Resolve Wf_SimplifyArith : wf.
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index 8a43a0ec7..b0ec96dbb 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -89,12 +89,13 @@ Definition PostWfPipeline
   := Build_ProcessedReflectivePackage_from_option_sigma
        e input_bounds
        (let e := InlineConst e in
-        let e := SimplifyArith e in
-        let e := InlineConst e in
-        let e := SimplifyArith e in
+        let e := InlineConst (SimplifyArith e) in
+        let e := InlineConst (SimplifyArith e) in
+        let e := InlineConst (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 := InlineConst (SimplifyArith e) in
         (*let e := CSE false e in*)
         let e := MapCast _ e input_bounds in
         option_map
diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v
index 0208207b3..34f5f2ea8 100644
--- a/src/Util/ZUtil/AddGetCarry.v
+++ b/src/Util/ZUtil/AddGetCarry.v
@@ -70,4 +70,8 @@ Module Z.
       reflexivity.
   Qed.
 
+  Lemma sub_with_borrow_to_add_get_carry c x y
+    : Z.sub_with_borrow c x y = Z.add_with_carry (-c) x (-y).
+  Proof. reflexivity. Qed.
+
 End Z.