From 5eb370497b4f92febe8dfe69b8f5093c5a8743b0 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 7 Dec 2023 21:15:28 -0500
Subject: [PATCH] Augment rewrite rule proving tactics for saturated arithmetic

For https://github.com/mit-plv/fiat-crypto/pull/1609 and
https://github.com/mit-plv/fiat-crypto/pull/1777
---
 rewriter                   |  2 +-
 src/Rewriter/RulesProofs.v | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/rewriter b/rewriter
index 90549d8f09..3a0a5f7337 160000
--- a/rewriter
+++ b/rewriter
@@ -1 +1 @@
-Subproject commit 90549d8f0910d4d5c7a28bfd0266e5dc719a51dd
+Subproject commit 3a0a5f73379174ce1232f6e656c27d146cccd3c7
diff --git a/src/Rewriter/RulesProofs.v b/src/Rewriter/RulesProofs.v
index 55c96c2888..1eb8f63004 100644
--- a/src/Rewriter/RulesProofs.v
+++ b/src/Rewriter/RulesProofs.v
@@ -263,6 +263,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
@@ -288,6 +295,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
@@ -399,6 +407,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 :=