Unobjectionable rewrite rules for saturated arithmetic

For mit-plv#1609

We don't yet include the ones that are higher-order-than 3, those need
more debugging.

Co-authored-by: Andres Erbsen <[email protected]>

Author: JasonGross

src/Rewriter/Rules.v

@@ -288,18 +288,35 @@ Definition arith_rewrite_rulesT (max_const_val : Z) : list (bool * Prop)
             ; (forall s y x,
                   Z.add_get_carry_full s (- y) x
                   = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb))
+            ; (forall s y x k,
+                  Z.add_get_carry_full s x (-y * k)
+                  = dlet vb := Z.sub_get_borrow_full s x (y * k) in (fst vb, - snd vb))
+            ; (forall s y x k,
+                  Z.add_get_carry_full s (-y * k) x
+                  = dlet vb := Z.sub_get_borrow_full s x (y * k) in (fst vb, - snd vb))
             ; (forall s y x,
                   Z.add_with_get_carry_full s 0 x (- y)
                   = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb))
             ; (forall s y x,
                   Z.add_with_get_carry_full s 0 (- y) x
                   = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb))
+
+            ; (forall s c x,
+                  Z.add_with_get_carry_full s (- c) x 0
+                  = dlet vb := Z.sub_with_get_borrow_full s c x 0 in (fst vb, - snd vb))
+
             ; (forall s c y x,
                   Z.add_with_get_carry_full s (- c) (- y) x
                   = dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb))
             ; (forall s c y x,
                   Z.add_with_get_carry_full s (- c) x (- y)
                   = dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb))
+            ; (forall s c y x k,
+                  Z.add_with_get_carry_full s c x (-y * k)
+                  = dlet vb := Z.sub_with_get_borrow_full s (-c) x (y * k) in (fst vb, - snd vb))
+            ; (forall s c y x k,
+                  Z.add_with_get_carry_full s c (-y * k) x
+                  = dlet vb := Z.sub_with_get_borrow_full s (-c) x (y * k) in (fst vb, - snd vb))
             ; (forall b x, (* inline negation when the rewriter wouldn't already inline it *)
                   ident.gets_inlined b x = false
                   -> -x = dlet v := x in -v)
@@ -395,6 +412,16 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list (
                    y ∈ ry -> y = Z.ones (Z.succ (Z.log2 y))
                    -> cstZ rv (cstZ ry ('y) &' cstZ rx x) = cstZ rx x)
              ]%Z%zrange
+         ; mymap
+             do_again
+             [ (forall x y, cstZ r[0~>1] x * y = Z.zselect (cstZ r[0~>1] x) (cstZ r[0~>0] (' 0)) y)
+             ; (forall x y, y * cstZ r[0~>1] x = Z.zselect (cstZ r[0~>1] x) (cstZ r[0~>0] (' 0)) y)
+             ; (forall c M rv r0 rM, 0 ∈ r0 -> M ∈ rM -> M ∈ rv -> 2^Z.log2 (M+1) = M + 1 -> 1 <= M ->
+                  cstZ rv (Z.zselect (cstZ r[0~>1] c) (cstZ r0 ('0)) (cstZ rM ('M)))
+                  = (dlet vc := cstZZ rv r[0~>1] (Z.sub_with_get_borrow_full ('(M+1)) (cstZ r[0~>1] c) 0 0) in
+                     cstZ rv (fst vc)))
+              ; (forall rv c x y, cstZ rv (Z.zselect c x y) = dlet v := cstZ rv (Z.zselect c x y) in cstZ rv v)
+                  ]
          ; mymap
              do_again
              [ (* [do_again], so that we can trigger add/sub rules on the output *)
@@ -415,6 +442,11 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list (
                      adc_no_carry_to_add = true -> s ∈ rs -> (n rx - n ry - n rc <= r[0~>s-1])%zrange
                      -> cstZZ rv r[0~>0] (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ rc c) (cstZ rx x) (cstZ ry y))
                         = (cstZ rv (cstZ rx x - cstZ ry y - cstZ rc c), (cstZ r[0~>0] ('0))))
+               (* 0-0-c passes through the carry *)
+               ; (forall rv rs s c rx ry,
+                     s ∈ rs -> 0 ∈ rx -> 0 ∈ ry -> -1 / s = -1
+                     -> cstZZ rv r[0~>1] (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ r[0~>1] c) (cstZ rx ('0)) (cstZ ry ('0)))
+                        = (cstZ rv (-(cstZ r[0~>1]c) mod 's), (cstZ r[0~>1] c)))
              ]%Z%zrange
          ; mymap
              dont_do_again

src/Rewriter/RulesProofs.v

@@ -258,6 +258,13 @@ Local Ltac interp_good_t_step_arith :=
             => cbv [Z.ltz];
                apply unfold_is_bounded_by_bool in Hx;
                apply unfold_is_bounded_by_bool in Hy
+          | [ H : is_bounded_by_bool _ (ZRange.normalize r[0 ~> 1]) = true |- _ ]
+            => change (ZRange.normalize r[0 ~> 1]) with r[0 ~> 1]%zrange in *;
+               cbv [is_bounded_by_bool] in H; cbn [upper lower] in H
+          | [ H : ?x <> ?a, H' : ?a <= ?x |- _ ] => assert (a < x) by lia; clear H H'
+          | [ H : 0 < ?x, H' : ?x <= 1 |- _ ] => assert (x = 1) by lia; clear H H'
+          | [ H : ?x <= 1, H' : 0 <= ?x |- _ ] => assert (x = 0 \/ x = 1) by lia; clear H H'
+          | [ H : ?x = Z.neg _ |- context[?x] ] => rewrite H
           | [ |- context[ident.cast r[0~>0] ?v] ]
             => rewrite (ident.platform_specific_cast_0_is_mod 0 v) by reflexivity
           | [ H : ?x = Z.ones _ |- context [Z.land _ ?x] ] => rewrite H
@@ -283,6 +290,7 @@ Local Ltac interp_good_t_step_arith :=
         | progress destruct_head'_and
         | progress Z.ltb_to_lt
         | progress split_andb
+        | progress change (0 - 1) with (-1) in *
         | match goal with
           | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia
           | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia
@@ -394,6 +402,9 @@ Local Ltac interp_good_t_step_arith :=
             => tryif constr_eq x x' then fail else replace x with x' by lia
           | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast
           end
+        | match goal with
+          | [ |- context[(- _) mod _] ] => rewrite Z.mod_opp_small by lia
+          end
         | saturate_add_sub_bounds_step ].
 
 Local Ltac remove_casts :=
@@ -598,17 +609,17 @@ Proof.
       -- rewrite <- Z.mod_divide_full. assumption.
     + rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia.
     + lia.
-    + rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia.  
+    + rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia.
 Qed.
-      
+
 Lemma arith_with_relaxed_casts_rewrite_rules_proofs
   : PrimitiveHList.hlist (@snd bool Prop) arith_with_relaxed_casts_rewrite_rulesT.
 Proof using Type.
   start_proof; auto; intros; try lia.
   - apply relaxed_rules_work; assumption.
   - rewrite Z.land_comm. apply relaxed_rules_work; assumption.
 Qed.
-      
+
 Lemma strip_literal_casts_rewrite_rules_proofs
   : PrimitiveHList.hlist (@snd bool Prop) strip_literal_casts_rewrite_rulesT.
 Proof using Type.