Get sbb conversion working in the pipeline

After    | File Name                                     | Before   || Change
--------------------------------------------------------------------------------
4m56.46s | Total                                         | 4m54.81s || +0m01.64s
--------------------------------------------------------------------------------
2m19.22s | Specific/IntegrationTestLadderstep            | 2m18.29s || +0m00.93s
0m53.92s | Specific/IntegrationTestLadderstep130         | 0m53.83s || +0m00.09s
0m26.24s | Compilers/Z/ArithmeticSimplifierWf            | 0m25.65s || +0m00.58s
0m24.93s | Compilers/Z/ArithmeticSimplifierInterp        | 0m24.87s || +0m00.05s
0m15.38s | Specific/IntegrationTestFreeze                | 0m15.97s || -0m00.58s
0m11.83s | Specific/IntegrationTestMul                   | 0m11.82s || +0m00.00s
0m10.57s | Specific/IntegrationTestSub                   | 0m10.50s || +0m00.07s
0m09.18s | Specific/IntegrationTestSquare                | 0m09.07s || +0m00.10s
0m02.80s | Compilers/Z/Bounds/Pipeline/Definition        | 0m02.57s || +0m00.23s
0m00.78s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.64s || +0m00.14s
0m00.64s | Compilers/Z/ArithmeticSimplifier              | 0m00.66s || -0m00.02s
0m00.62s | Compilers/Z/Bounds/Pipeline                   | 0m00.59s || +0m00.03s
0m00.35s | Compilers/Z/ArithmeticSimplifierUtil          | 0m00.36s || -0m00.01s

4 files changed, 112 insertions, 103 deletions

diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v
index 2690f2dfb..8f63e815b 100644
--- a/src/Compilers/Z/ArithmeticSimplifier.v
+++ b/src/Compilers/Z/ArithmeticSimplifier.v
@@ -5,6 +5,7 @@ Require Import Crypto.Compilers.Rewriter.
 Require Import Crypto.Compilers.Z.Syntax.
 
 Section language.
+  Context (convert_adc_to_sbb : bool).
   Local Notation exprf := (@exprf base_type op).
   Local Notation Expr := (@Expr base_type op).
 
@@ -178,108 +179,116 @@ Section language.
                  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
+              => if convert_adc_to_sbb
+                 then 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
-                 | _ => Op opc args
-                 end
+                 else Op opc args
          | 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
+              => if convert_adc_to_sbb
+                 then 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
-                 | _ => Op opc args
-                 end
+                 else Op opc args
          | 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
+              => if convert_adc_to_sbb
+                 then 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
-                 | _ => Op opc args
-                 end
+                 else Op opc args
          | 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
+              => if convert_adc_to_sbb
+                 then 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
-                 | _ => Op opc args
-                 end
+                 else Op opc args
          | Add _ _ _ as opc
          | Sub _ _ _ as opc
          | Mul _ _ _ as opc
diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v
index 1f638c076..3dc11aa9e 100644
--- a/src/Compilers/Z/ArithmeticSimplifierInterp.v
+++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v
@@ -145,8 +145,8 @@ Local Arguments Z.add !_ !_.
 Local Arguments Z.sub !_ !_.
 Local Arguments Z.opp !_.
 
-Lemma InterpSimplifyArith {t} (e : Expr t)
-  : forall x, Interp interp_op (SimplifyArith e) x = Interp interp_op e x.
+Lemma InterpSimplifyArith {convert_adc_to_sbb} {t} (e : Expr t)
+  : forall x, Interp interp_op (SimplifyArith convert_adc_to_sbb e) x = Interp interp_op e x.
 Proof.
   apply InterpRewriteOp; intros; unfold simplify_op_expr.
   break_innermost_match;
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v
index ff5068b89..ba5dd39cd 100644
--- a/src/Compilers/Z/ArithmeticSimplifierWf.v
+++ b/src/Compilers/Z/ArithmeticSimplifierWf.v
@@ -220,9 +220,9 @@ Local Ltac pose_wff_prod3 :=
     => pose proof (wff_interp_as_expr_or_const_prod3_base Hwf H1 H2); clear H1 H2
   end.
 
-Lemma Wf_SimplifyArith {t} (e : Expr t)
+Lemma Wf_SimplifyArith {convert_adc_to_sbb} {t} (e : Expr t)
       (Hwf : Wf e)
-  : Wf (SimplifyArith e).
+  : Wf (SimplifyArith convert_adc_to_sbb e).
 Proof.
   apply Wf_RewriteOp; [ | assumption ].
   intros ???????? Hwf'; unfold simplify_op_expr;
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index b0ec96dbb..5aadc8dfd 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -34,7 +34,7 @@ Require Import Crypto.Compilers.Z.ArithmeticSimplifierInterp.
 (** *** Definition of the Pre-Wf Pipeline *)
 (** Do not change the name or the type of this definition *)
 Definition PreWfPipeline {t} (e : Expr base_type op t) : Expr base_type op _
-  := ExprEta (SimplifyArith (Linearize e)).
+  := ExprEta (SimplifyArith false (Linearize e)).
 
 (** *** Correctness proof of the Pre-Wf Pipeline *)
 (** Do not change the statement of this lemma.  You shouldn't need to
@@ -89,13 +89,13 @@ Definition PostWfPipeline
   := Build_ProcessedReflectivePackage_from_option_sigma
        e input_bounds
        (let e := InlineConst 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 := InlineConst (SimplifyArith false e) in
+        let e := InlineConst (SimplifyArith false e) in
+        let e := InlineConst (SimplifyArith false e) in
+        let e := if opts.(anf) then InlineConst (ANormal e) else e in
         let e := RewriteAdc e in
-        let e := InlineConst (SimplifyArith e) in
+        let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in
+        let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in
         (*let e := CSE false e in*)
         let e := MapCast _ e input_bounds in
         option_map