Update the post-bounds rewrite rules

They are all proven, and they work!

To make this possible, we had to make casting commute with negation.

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
32m30.13s | Total                                                                | 32m17.70s || +0m12.42s | +0.64%
--------------------------------------------------------------------------------------------------------------------
1m38.96s  | Experiments/NewPipeline/RewriterRulesGood.vo                         | 1m23.70s  || +0m15.26s | +18.23%
4m44.45s  | Experiments/NewPipeline/Toplevel1.vo                                 | 4m58.41s  || -0m13.95s | -4.67%
2m08.47s  | Experiments/NewPipeline/RewriterRulesInterpGood.vo                   | 1m56.27s  || +0m12.19s | +10.49%
6m36.50s  | p384_32.c                                                            | 6m42.34s  || -0m05.84s | -1.45%
6m19.09s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo                | 6m15.11s  || +0m03.97s | +1.06%
1m24.28s  | Experiments/NewPipeline/Rewriter.vo                                  | 1m20.87s  || +0m03.40s | +4.21%
0m40.26s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m43.07s  || -0m02.81s | -6.52%
1m57.38s  | Experiments/NewPipeline/RewriterWf2.vo                               | 1m59.36s  || -0m01.98s | -1.65%
1m40.57s  | Experiments/NewPipeline/Toplevel2.vo                                 | 1m41.68s  || -0m01.11s | -1.09%
0m42.80s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m41.59s  || +0m01.20s | +2.90%
0m25.06s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m26.26s  || -0m01.20s | -4.56%
0m18.78s  | p256_32.c                                                            | 0m17.12s  || +0m01.66s | +9.69%
0m18.49s  | secp256k1_32.c                                                       | 0m17.05s  || +0m01.43s | +8.44%
0m15.98s  | Experiments/NewPipeline/RewriterWf1.vo                               | 0m17.00s  || -0m01.01s | -5.99%
0m08.04s  | p224_32.c                                                            | 0m07.03s  || +0m01.00s | +14.36%
0m39.70s  | p521_32.c                                                            | 0m40.46s  || -0m00.75s | -1.87%
0m33.03s  | p521_64.c                                                            | 0m33.98s  || -0m00.94s | -2.79%
0m23.34s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m22.79s  || +0m00.55s | +2.41%
0m18.64s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m17.70s  || +0m00.94s | +5.31%
0m14.98s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m14.20s  || +0m00.78s | +5.49%
0m11.58s  | p384_64.c                                                            | 0m11.49s  || +0m00.08s | +0.78%
0m09.16s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m09.29s  || -0m00.12s | -1.39%
0m06.04s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m06.01s  || +0m00.03s | +0.49%
0m05.80s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.85s  || -0m00.04s | -0.85%
0m04.74s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.36s  || +0m00.37s | +8.71%
0m04.57s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m04.91s  || -0m00.33s | -6.92%
0m03.66s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.55s  || +0m00.11s | +3.09%
0m02.24s  | curve25519_32.c                                                      | 0m02.29s  || -0m00.04s | -2.18%
0m02.04s  | p224_64.c                                                            | 0m01.86s  || +0m00.17s | +9.67%
0m01.98s  | secp256k1_64.c                                                       | 0m02.45s  || -0m00.47s | -19.18%
0m01.97s  | p256_64.c                                                            | 0m01.88s  || +0m00.09s | +4.78%
0m01.49s  | curve25519_64.c                                                      | 0m01.55s  || -0m00.06s | -3.87%
0m01.40s  | Experiments/NewPipeline/CLI.vo                                       | 0m01.49s  || -0m00.09s | -6.04%
0m01.30s  | Experiments/NewPipeline/StandaloneHaskellMain.vo                     | 0m01.34s  || -0m00.04s | -2.98%
0m01.26s  | Experiments/NewPipeline/StandaloneOCamlMain.vo                       | 0m01.31s  || -0m00.05s | -3.81%
0m01.10s  | Experiments/NewPipeline/CompilersTestCases.vo                        | 0m01.12s  || -0m00.02s | -1.78%
0m01.00s  | Experiments/NewPipeline/RewriterProofs.vo                            | 0m00.97s  || +0m00.03s | +3.09%

1 files changed, 59 insertions, 116 deletions

diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index b205acec1..e5d0e040f 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -172,9 +172,28 @@ Module Compilers.
                   => rewrite ident.cast_normalize
                 | [ H : context[ident.cast (ZRange.normalize ?r)] |- _ ]
                   => rewrite ident.cast_normalize in H
+                | [ H : ?T, H' : ?T |- _ ] => clear H'
+                | [ H : context[is_bounded_by_bool _ (ZRange.normalize (-_))] |- _ ]
+                  => rewrite ZRange.is_bounded_by_bool_move_opp_normalize in H
+                | [ |- context[is_bounded_by_bool _ (ZRange.normalize (-_))] ]
+                  => rewrite ZRange.is_bounded_by_bool_move_opp_normalize
+                | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ ?r ?v] ]
+                  => rewrite (@ident.cast_in_normalized_bounds _ r v) by exact H
+                | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ (-?r) (-?v)] ]
+                  => rewrite (@ident.cast_in_normalized_bounds _ (-r) (-v));
+                     [ | clear -H ]
+                | [ |- context[ident.cast _ ?r (-ident.cast _ (-?r) ?v)] ]
+                  => rewrite (ident.cast_in_normalized_bounds r (-ident.cast _ (-r) v))
+                    by (rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize; apply ident.cast_always_bounded)
+                | [ |- context[ident.cast _ ?r (ident.cast _ ?r _)] ]
+                  => rewrite (@ident.cast_idempotent _ _ r)
+                | [ H : is_bounded_by_bool _ ?r = true |- _]
+                  => is_var r; unique pose proof (ZRange.is_bounded_by_normalize _ _ H)
+                | [ H : zrange * zrange |- _ ] => destruct H
                 end
               | progress intros
               | progress subst
+              | assumption
               | progress inversion_option
               | progress destruct_head'_and
               | progress Z.ltb_to_lt
@@ -294,6 +313,7 @@ Module Compilers.
               | break_innermost_match_hyps_step
               | progress destruct_head'_or
               | match goal with
+                | [ |- context[-ident.cast _ (-?r) (-?v)] ] => rewrite (ident.cast_opp' r v)
                 | [ |- context[ident.cast ?coor ?r ?v] ]
                   => is_var v;
                      pose proof (@ident.cast_always_bounded coor r v);
@@ -304,6 +324,18 @@ Module Compilers.
                      generalize dependent (ident.cast coor r v); intros
                 | [ H : is_bounded_by_bool ?v ?r = true, H' : is_tighter_than_bool ?r ?r' = true |- _ ]
                   => unique assert (is_bounded_by_bool v r' = true) by (eauto 2 using ZRange.is_bounded_by_of_is_tighter_than)
+                | [ H : is_bounded_by_bool (-?v) ?r = true, H' : (-?r <=? ?r')%zrange = true |- _ ]
+                  => unique assert (is_bounded_by_bool v r' = true)
+                    by (apply (@ZRange.is_bounded_by_of_is_tighter_than _ _ H');
+                        rewrite <- ZRange.is_bounded_by_bool_opp, ZRange.opp_involutive; exact H)
+                | [ H : is_bounded_by_bool ?v (-?r) = true |- _ ]
+                  => is_var v;
+                     unique assert (is_bounded_by_bool (-v) r = true)
+                       by now rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize, ZRange.normalize_opp
+                | [ H : is_bounded_by_bool ?x r[0~>?v-1] = true |- _ ]
+                  => progress (try unique assert (0 <= x); try unique assert (x <= v - 1));
+                     [ clear -H; cbv [is_bounded_by_bool] in H; cbn [lower upper] in H; Bool.split_andb; Z.ltb_to_lt; lia..
+                     | ]
                 end
               | match goal with
                 | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))]
@@ -312,6 +344,7 @@ Module Compilers.
                 | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith
                 | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith
                 | [ |- context[Z.shiftl _ (-_)] ] => rewrite Z.shiftl_opp_r
+                | [ |- context[- - _] ] => rewrite Z.opp_involutive
                 | [ H : ?x = 2^Z.log2 ?x |- context[2^Z.log2 ?x] ] => rewrite <- H
                 | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ]
                   => rewrite !Z.sub_1_r, H, <- Z.ones_equiv, Z.land_ones by auto with zarith
@@ -323,11 +356,33 @@ Module Compilers.
                 | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_const
                 | [ |- ?f (?g (nat_rect _ _ _ ?n ?v)) = nat_rect _ _ _ ?n _ ]
                   => revert v; is_var n; induction n; intro v; cbn [nat_rect]
+                | [ H : 0 <= ?x, H' : ?x <= ?r - 1 |- context[?x mod ?r] ]
+                  => rewrite (Z.mod_small x r) by (clear -H H'; lia)
+                | [ H : 0 <= ?x, H' : ?x <= ?y - 1 |- context[?x / ?y] ]
+                  => rewrite (Z.div_small x y) by (clear -H H'; lia)
                 | [ |- _ mod ?x = _ mod ?x ]
                   => progress (push_Zmod; pull_Zmod)
                 | [ |- _ mod ?x = _ mod ?x ]
                   => apply f_equal2; (lia + nia)
+                | [ |- context[-?x + ?y] ] => rewrite !Z.add_opp_l
+                | [ |- context[?n + - ?m] ] => rewrite !Z.add_opp_r
+                | [ |- context[?n - - ?m] ] => rewrite !Z.sub_opp_r
+                | [ |- ?f (?a mod ?r) = ?f (?b mod ?r) ] => apply f_equal; apply f_equal2; lia
+                | [ |- context[-?a - ?b + ?c] ] => replace (-a - b + c) with (c - a - b) by (clear; lia)
+                | [ |- context[?x - ?y + ?z] ]
+                  => lazymatch goal with
+                     | [ |- context[z - y + x] ]
+                       => progress replace (z - y + x) with (x - y + z) by (clear; lia)
+                     end
+                | [ |- context[?x - ?y - ?z] ]
+                  => lazymatch goal with
+                     | [ |- context[x - z - y] ]
+                       => progress replace (x - z - y) with (x - y - z) by (clear; lia)
+                     end
+                | [ |- - ident.cast _ (-?r) (- (?x / ?y)) = ident.cast _ ?r (?x' / ?y) ]
+                  => tryif constr_eq x x' then fail else replace x with x' by lia
                 | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast
+                | [ |- ident.cast _ ?r _ = ident.cast _ ?r _ ] => apply f_equal; Z.div_mod_to_quot_rem; nia
                 end ].
 
       Lemma nbe_rewrite_rules_interp_good
@@ -337,9 +392,6 @@ Module Compilers.
         Time all: repeat interp_good_t_step.
       Qed.
 
-      Axiom proof_admitted : False.
-      Local Notation admit := (match proof_admitted with end).
-
       Lemma arith_rewrite_rules_interp_good max_const
         : rewrite_rules_interp_goodT (arith_rewrite_rules max_const).
       Proof using Type.
@@ -351,119 +403,7 @@ Module Compilers.
         : rewrite_rules_interp_goodT arith_with_casts_rewrite_rules.
       Proof using Type.
         Time start_interp_good.
-        Time all: try solve [ repeat interp_good_t_step; (lia + nia) ].
-        (* This is mainly for display *)
-        all: repeat first [ progress cbn [Compile.value' Compile.reify] in *
-                          | progress subst
-                          | match goal with
-                            | [ H : context[expr.interp ?ii ?v] |- _ ]
-                              => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
-                            | [ |- context[expr.interp ?ii ?v] ]
-                              => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
-                            end ].
-        (* 9 subgoals (ID 32915)
-
-  cast_outside_of_range : zrange -> Z -> Z
-  max_const, x, x0 : Z
-  v1 : expr (type.base base.type.Z)
-  ============================
-  match
-    (x1 <- rwhen (Some (v1, (##0)%expr)%expr_pat) (x0 =? 1);
-     Some (UnderLets.Base x1))%option
-  with
-  | Some v0 =>
-      expr.interp ident_interp (UnderLets.interp ident_interp v0) =
-      Z.mul_split x x0 (expr.interp ident_interp v1)
-  | None => True
-  end
-
-subgoal 2 (ID 32967) is:
- match
-   (x1 <- rwhen (Some (v1, (##0)%expr)%expr_pat) (x0 =? 1);
-    Some (UnderLets.Base x1))%option
- with
- | Some v0 =>
-     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
-     Z.mul_split x (expr.interp ident_interp v1) x0
- | None => True
- end
-subgoal 3 (ID 33019) is:
- match
-   (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1);
-    Some (UnderLets.Base x1))%option
- with
- | Some v0 =>
-     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
-     Z.mul_split x x0 (expr.interp ident_interp v1)
- | None => True
- end
-subgoal 4 (ID 33071) is:
- match
-   (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1);
-    Some (UnderLets.Base x1))%option
- with
- | Some v0 =>
-     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
-     Z.mul_split x (expr.interp ident_interp v1) x0
- | None => True
- end
-subgoal 5 (ID 33168) is:
- match
-   (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0);
-    Some (UnderLets.Base x0))%option
- with
- | Some v1 =>
-     expr.interp ident_interp (UnderLets.interp ident_interp v1) =
-     Z.add_get_carry_full v2 x (expr.interp ident_interp v0)
- | None => True
- end
-subgoal 6 (ID 33265) is:
- match
-   (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0);
-    Some (UnderLets.Base x0))%option
- with
- | Some v1 =>
-     expr.interp ident_interp (UnderLets.interp ident_interp v1) =
-     Z.add_get_carry_full v2 (expr.interp ident_interp v0) x
- | None => True
- end
-subgoal 7 (ID 33320) is:
- match
-   (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0));
-    Some (UnderLets.Base x2))%option
- with
- | Some v0 =>
-     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
-     Z.add_with_get_carry_full x x0 x1 (expr.interp ident_interp v1)
- | None => True
- end
-subgoal 8 (ID 33376) is:
- match
-   (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0));
-    Some (UnderLets.Base x2))%option
- with
- | Some v0 =>
-     expr.interp ident_interp (UnderLets.interp ident_interp v0) =
-     Z.add_with_get_carry_full x x0 (expr.interp ident_interp v1) x1
- | None => True
- end
-subgoal 9 (ID 33473) is:
- match
-   rwhenl
-     (Some
-        (UnderLets.UnderLet
-           (#(ident.Z_add_with_get_carry)%expr @ v1 @ v0 @ (##x)%expr @ (##x0)%expr)%expr_pat
-           (fun vc : Z * Z =>
-            UnderLets.Base (#(ident.fst)%expr @ ($vc)%expr, (##0)%expr)%expr_pat)))
-     ((x =? 0) && (x0 =? 0))
- with
- | Some v2 =>
-     expr.interp ident_interp (UnderLets.interp ident_interp v2) =
-     Z.add_with_get_carry_full (expr.interp ident_interp v1) (expr.interp ident_interp v0) x x0
- | None => True
- end
-         *)
-        1-9: exact admit.
+        Time all: try solve [ repeat interp_good_t_step; Z.div_mod_to_quot_rem; (lia + nia) ].
       Qed.
 
       Local Ltac fancy_local_t :=
@@ -473,6 +413,9 @@ subgoal 9 (ID 33473) is:
                        end
                      | progress autorewrite with zsimplify in * ].
 
+      Axiom proof_admitted : False.
+      Local Notation admit := (match proof_admitted with end).
+
       Lemma fancy_rewrite_rules_interp_good
             (invert_low invert_high : Z -> Z -> option Z)
             (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))