Add compiler optimization for [Zselect (-x) _ _]

Since x = 0 <-> -x = 0, we can eliminate the negative on the borrow-bit
in freeze.

After    | File Name                                     | Before   || Change
--------------------------------------------------------------------------------
5m01.81s | Total                                         | 4m55.75s || +0m06.05s
--------------------------------------------------------------------------------
0m29.05s | Compilers/Z/ArithmeticSimplifierInterp        | 0m24.85s || +0m04.19s
0m28.68s | Compilers/Z/ArithmeticSimplifierWf            | 0m25.88s || +0m02.80s
2m18.19s | Specific/IntegrationTestLadderstep            | 2m19.51s || -0m01.31s
0m53.86s | Specific/IntegrationTestLadderstep130         | 0m53.64s || +0m00.21s
0m15.40s | Specific/IntegrationTestFreeze                | 0m15.30s || +0m00.09s
0m11.85s | Specific/IntegrationTestMul                   | 0m11.72s || +0m00.12s
0m10.72s | Specific/IntegrationTestSub                   | 0m10.47s || +0m00.25s
0m08.97s | Specific/IntegrationTestSquare                | 0m09.15s || -0m00.17s
0m02.78s | Compilers/Z/Bounds/Pipeline/Definition        | 0m02.81s || -0m00.03s
0m00.75s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.75s || +0m00.00s
0m00.60s | Compilers/Z/Bounds/Pipeline                   | 0m00.62s || -0m00.02s
0m00.60s | Compilers/Z/ArithmeticSimplifier              | 0m00.65s || -0m00.05s
0m00.36s | Compilers/Z/ArithmeticSimplifierUtil          | 0m00.41s || -0m00.04s

2 files changed, 37 insertions, 2 deletions

diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v
index 8f63e815b..a1775011d 100644
--- a/src/Compilers/Z/ArithmeticSimplifier.v
+++ b/src/Compilers/Z/ArithmeticSimplifier.v
@@ -48,6 +48,19 @@ Section language.
               end
          end.
 
+    Fixpoint uninterp_expr_or_const {t} : interp_flat_type inverted_expr t -> exprf (var:=var) t
+      := match t with
+         | Tbase T => fun e => match e with
+                               | const_of v => Op (OpConst v) TT
+                               | gen_expr e => e
+                               | neg_expr e => Op (Opp _ _) e
+                               end
+         | Unit => fun _ => TT
+         | Prod A B => fun (ab : interp_flat_type _ A * interp_flat_type _ B)
+                       => Pair (@uninterp_expr_or_const A (fst ab))
+                               (@uninterp_expr_or_const B (snd ab))
+         end.
+
     Definition simplify_op_expr {src dst} (opc : op src dst)
       : exprf (var:=var) src -> exprf (var:=var) dst
       := match opc in op src dst return exprf src -> exprf dst with
@@ -177,6 +190,27 @@ Section language.
                  | _
                    => Op opc args
                  end
+         | Zselect TZ TZ TZ TZ as opc
+           => fun args
+              => match interp_as_expr_or_const args with
+                 | Some (const_of c, x, y)
+                   => match (c =? 0)%Z, x, y with
+                      | true, const_of c, _
+                      | false, _, const_of c
+                        => Op (OpConst c) TT
+                      | true, gen_expr e, _
+                      | false, _, gen_expr e
+                        => e
+                      | true, neg_expr e, _
+                      | false, _, neg_expr e
+                        => Op (Opp TZ TZ) e
+                      end
+                 | Some (neg_expr e, x, y)
+                   => let x := uninterp_expr_or_const (t:=Tbase _) x in
+                      let y := uninterp_expr_or_const (t:=Tbase _) y in
+                      Op (Zselect TZ TZ TZ TZ) (e, x, y)%expr
+                 | _ => Op opc args
+                 end
          | AddWithCarry TZ TZ TZ TZ as opc
            => fun args
               => if convert_adc_to_sbb
diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v
index 3dc11aa9e..6db34f1b8 100644
--- a/src/Compilers/Z/ArithmeticSimplifierInterp.v
+++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v
@@ -151,7 +151,7 @@ Proof.
   apply InterpRewriteOp; intros; unfold simplify_op_expr.
   break_innermost_match;
     repeat first [ fin_t
-                 | progress cbv [LetIn.Let_In]
+                 | progress cbv [LetIn.Let_In Z.zselect]
                  | progress simpl in *
                  | progress subst
                  | progress subst_prod
@@ -162,7 +162,8 @@ Proof.
                  | progress Z.ltb_to_lt
                  | 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 ].
+                 | progress autorewrite with zsimplify_fast
+                 | break_innermost_match_step ].
 Qed.
 
 Hint Rewrite @InterpSimplifyArith : reflective_interp.