put the new rewrite rule in its own pass

Author: OwenConoly

fiat-c/src/secp256k1_dettman_64.c

@@ -806,7 +806,8 @@ Module Pipeline.
       match E' with
         (* rewrites after bounds relaxation---add a new one named arithWithRelaxedCasts or something. *)
       | inl E
-        => (E <- match split_mul_to with
+        => (E <- RewriteAndEliminateDeadAndInline "RewriteArithWithRelaxedCasts" (RewriteRules.RewriteArithWithRelaxedCasts opts) with_dead_code_elimination with_subst01 with_let_bind_return E;
+            E <- match split_mul_to with
                  | Some (max_bitwidth, lgcarrymax)
                    => wrap_debug_rewrite "RewriteMulSplit" (RewriteRules.RewriteMulSplit max_bitwidth lgcarrymax opts) E
                  | None => Debug.ret E

src/BoundsPipeline.v

@@ -2,6 +2,7 @@ Require Import Crypto.Rewriter.Passes.NBE.
 Require Import Crypto.Rewriter.Passes.AddAssocLeft.
 Require Import Crypto.Rewriter.Passes.Arith.
 Require Import Crypto.Rewriter.Passes.ArithWithCasts.
+Require Import Crypto.Rewriter.Passes.ArithWithRelaxedCasts.
 Require Import Crypto.Rewriter.Passes.StripLiteralCasts.
 Require Import Crypto.Rewriter.Passes.FlattenThunkedRects.
 Require Import Crypto.Rewriter.Passes.MulSplit.
@@ -17,6 +18,7 @@ Module Compilers.
   Export AddAssocLeft.Compilers.
   Export Arith.Compilers.
   Export ArithWithCasts.Compilers.
+  Export ArithWithRelaxedCasts.Compilers.
   Export StripLiteralCasts.Compilers.
   Export FlattenThunkedRects.Compilers.
   Export MulSplit.Compilers.
@@ -32,6 +34,7 @@ Module Compilers.
     Export AddAssocLeft.Compilers.RewriteRules.
     Export Arith.Compilers.RewriteRules.
     Export ArithWithCasts.Compilers.RewriteRules.
+    Export ArithWithRelaxedCasts.Compilers.RewriteRules.
     Export StripLiteralCasts.Compilers.RewriteRules.
     Export FlattenThunkedRects.Compilers.RewriteRules.
     Export MulSplit.Compilers.RewriteRules.

src/Rewriter/All.v

@@ -0,0 +1,43 @@
+Require Import Rewriter.Language.Language.
+Require Import Crypto.Language.API.
+Require Import Rewriter.Language.Wf.
+Require Import Crypto.Language.WfExtra.
+Require Import Crypto.Rewriter.AllTacticsExtra.
+Require Import Crypto.Rewriter.RulesProofs.
+
+Module Compilers.
+  Import Language.Compilers.
+  Import Language.API.Compilers.
+  Import Language.Wf.Compilers.
+  Import Language.WfExtra.Compilers.
+  Import Rewriter.AllTacticsExtra.Compilers.RewriteRules.GoalType.
+  Import Rewriter.AllTactics.Compilers.RewriteRules.Tactic.
+  Import Compilers.Classes.
+
+  Module Import RewriteRules.
+    Section __.
+      Definition VerifiedRewriterArithWithRelaxedCasts : VerifiedRewriter_with_args false false true arith_with_relaxed_casts_rewrite_rules_proofs.
+      Proof using All. make_rewriter. Defined.
+
+      Definition default_opts := Eval hnf in @default_opts VerifiedRewriterArithWithRelaxedCasts.
+      Let optsT := Eval hnf in optsT VerifiedRewriterArithWithRelaxedCasts.
+
+      Definition RewriteArithWithRelaxedCasts (opts : optsT) {t : API.type} := Eval hnf in @Rewrite VerifiedRewriterArithWithRelaxedCasts opts t.
+
+      Lemma Wf_RewriteArithWithRelaxedCasts opts {t} e (Hwf : Wf e) : Wf (@RewriteArithWithRelaxedCasts opts t e).
+      Proof. now apply VerifiedRewriterArithWithRelaxedCasts. Qed.
+
+      Lemma Interp_RewriteArithWithRelaxedCasts opts {t} e (Hwf : Wf e) : API.Interp (@RewriteArithWithRelaxedCasts opts t e) == API.Interp e.
+      Proof. now apply VerifiedRewriterArithWithRelaxedCasts. Qed.
+    End __.
+  End RewriteRules.
+
+  Module Export Hints.
+#[global]
+    Hint Resolve Wf_RewriteArithWithRelaxedCasts : wf wf_extra.
+#[global]
+    Hint Opaque RewriteArithWithRelaxedCasts : wf wf_extra interp interp_extra rewrite.
+#[global]
+    Hint Rewrite @Interp_RewriteArithWithRelaxedCasts : interp interp_extra.
+  End Hints.
+End Compilers.

src/Rewriter/Passes/ArithWithRelaxedCasts.v

@@ -561,6 +561,30 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list (
              ]
         ]%Z%zrange.
 
+Definition arith_with_relaxed_casts_rewrite_rulesT : list (bool * Prop)
+  := Eval cbv [myapp mymap myflatten] in
+    myflatten
+      [mymap
+         dont_do_again
+         [(forall rland rm1 rv v,
+              rland.(upper) ∈ rm1
+              -> rland.(upper) = Z.ones (Z.succ (Z.log2 rland.(upper)))
+              -> 0 = rland.(lower)
+              -> 0 = rv.(lower)
+              -> 0 <= rv.(upper)
+              -> (rv.(upper) + 1) mod (rland.(upper) + 1) = 0
+              -> cstZ rland (Z.land (cstZ rv v) (cstZ rm1 ('rland.(upper)))) = cstZ rland v)
+          ; (forall rland rm1 rv v,
+                rland.(upper) ∈ rm1
+                -> rland.(upper) = Z.ones (Z.succ (Z.log2 rland.(upper)))
+                -> 0 = rland.(lower)
+                -> 0 = rv.(lower)
+                -> 0 <= rv.(upper)
+                -> (rv.(upper) + 1) mod (rland.(upper) + 1) = 0
+                -> cstZ rland (Z.land (cstZ rm1 ('rland.(upper))) (cstZ rv v)) = cstZ rland v)
+         ]
+      ]%Z%zrange.
+
 Definition strip_literal_casts_rewrite_rulesT : list (bool * Prop)
   := [dont_do_again (forall rx x, x ∈ rx -> cstZ rx ('x) = 'x)]%Z%zrange.
 
@@ -1060,17 +1084,7 @@ Section with_bitwidth.
           [mymap dont_do_again []
            ; mymap
                do_again
-               [
-                 (* owen put this here, and he needs to remove it. *)
-                 (forall rland rm1 rv v,
-                       rland.(upper) ∈ rm1
-                       -> rland.(upper) = Z.ones (Z.succ (Z.log2 rland.(upper)))
-                       -> 0 = rland.(lower)
-                       -> 0 = rv.(lower)
-                       -> 0 <= rv.(upper)
-                       -> (rv.(upper) + 1) mod (rland.(upper) + 1) = 0
-                       -> cstZ rland (Z.land (cstZ rv v) (cstZ rm1 ('rland.(upper)))) = cstZ rland v)
-                ; (forall A B x y, @fst A B (x, y) = x)
+               [(forall A B x y, @fst A B (x, y) = x)
                 ; (forall A B x y, @snd A B (x, y) = y)
                     (** In order to avoid tautological compares, we need to deal with carry/borrows being 0 *)
                 ; (forall r0 s x y r1 r2,