Handle r[0~>0] casts on Z.mul_split

For mit-plv#1358 Note that we need to work around mit-plv/rewriter#84
JasonGross · Oct 23, 2022 · 9d4e513 · 9d4e513
1 parent b797484
commit 9d4e513
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 2 deletions.
diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v
@@ -928,7 +928,8 @@ Section with_bitwidth.
   Context (bitwidth : Z)
           (lgcarrymax : Z).
 
-  Local Notation singlewidth_range := r[0~>2^bitwidth - 1]%zrange.
+  Local Notation singlewidth_upperbound := (2^bitwidth - 1).
+  Local Notation singlewidth_range := r[0~>singlewidth_upperbound]%zrange.
   Local Notation doublewidth := (cstZ r[0~>2^(2*bitwidth) - 1]).
   Local Notation singlewidth := (cstZ singlewidth_range).
   Local Notation carrymax := (2^lgcarrymax-1).
@@ -1183,6 +1184,15 @@ Section with_bitwidth.
                do_again
                [ (* [do_again], so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *)
                  (forall rx ry x y, cstZZ rx ry (x, y) = (cstZ rx x, cstZ ry y))
+                 ; (* handle things other than pairsinglewidth on Z.mul_split, most importantly r[0~>0] *)
+                 (* N.B. we need to abstract over ranges, not just their upper bounds, due to https://github.com/mit-plv/rewriter/issues/84 *)
+                 (forall r1 r2 s x y,
+                     lower r1 = 0 -> lower r2 = 0 -> 0 <= singlewidth_upperbound -> 0 <= upper r1 -> 0 <= upper r2
+                     -> ((upper r1+1) | (singlewidth_upperbound+1))
+                     -> ((upper r2+1) | (singlewidth_upperbound+1))
+                     -> (upper r1 <> singlewidth_upperbound \/ upper r2 <> singlewidth_upperbound)
+                     -> cstZZ r1 r2 (Z.mul_split s x y)
+                        = cstZZ r1 r2 (pairsinglewidth (Z.mul_split s x y)))
                ]
           ]%Z%zrange.
 

diff --git a/src/Rewriter/RulesProofs.v b/src/Rewriter/RulesProofs.v
@@ -1,5 +1,5 @@
 Require Import Coq.micromega.Lia.
-Require Import Coq.ZArith.ZArith.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ZRange.Operations.
@@ -9,6 +9,7 @@ Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModDivide.
 Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute.
 Require Import Crypto.Util.ZUtil.Hints.
@@ -31,6 +32,7 @@ Require Import Crypto.Util.ZUtil.Land.
 Require Import Crypto.Util.ZUtil.Lor.
 Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
 Require Import Crypto.Util.ZUtil.Shift.
+Require Import Crypto.Util.ZUtil.Divide.Bool.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.ZRange.BasicLemmas.
@@ -798,6 +800,7 @@ Proof using Type.
   all: repeat interp_good_t_step_related.
   all: systematically_handle_casts; autorewrite with zsimplify_fast; try reflexivity.
   all: rewrite !ident.platform_specific_cast_0_is_mod, ?Z.sub_add, ?Z.mod_mod by lia; try reflexivity.
+  all: autorewrite with zsimplify_fast in *; Z.rewrite_mod_divide_in_all; try reflexivity.
   all: progress specialize_by lia.
   all: try match goal with
            | H : ?x = 2 ^ Z.log2 ?x |- _ =>