Restrict [ident.cast] a bit more

We now enforce that [ident.cast] commutes appropriately with [Z.opp] /
[ZRange.opp].  In particular, we perform normalization to ensure that
more of the range is positive than negative (and if we have a range like
`r[-x ~> x]`, then we ensure that the value being casted is
non-negative), before using the given cast-outside-of-range function.
Afterwards, we perform the relevant negation to set it back.

This makes a number of rewrite rules simpler and easier to prove,
because we won't have to ensure that the casts are the same pre- and
post- negation; it's guaranteed that we can mess around with negation as
much as we want and still have things work out fine.

2 files changed, 147 insertions, 17 deletions

diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index a0fc9ade5..cc8dcff86 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -914,11 +914,24 @@ Module Compilers.
       Section gen.
         Context (cast_outside_of_range : zrange -> BinInt.Z -> BinInt.Z).
 
+        Definition is_more_pos_than_neg (r : zrange) (v : BinInt.Z) : bool
+          := ((Z.abs (lower r) <? Z.abs (upper r)) (* if more of the range is above 0 than below 0 *)
+              || ((lower r =? upper r) && (0 <=? lower r))
+              || ((Z.abs (lower r) =? Z.abs (upper r)) && (0 <=? v))).
+
+        (** We ensure that [ident.cast] is symmetric under [Z.opp], as
+            this makes some rewrite rules much, much easier to
+            prove. *)
+        Let cast_outside_of_range' (r : zrange) (v : BinInt.Z) : BinInt.Z
+          := ((cast_outside_of_range r v - lower r) mod (upper r - lower r + 1)) + lower r.
+
         Definition cast (r : zrange) (x : BinInt.Z)
           := let r := ZRange.normalize r in
              if (lower r <=? x) && (x <=? upper r)
              then x
-             else ((cast_outside_of_range r x - lower r) mod (upper r - lower r + 1)) + lower r.
+             else if is_more_pos_than_neg r x
+                  then cast_outside_of_range' r x
+                  else -cast_outside_of_range' (-r) (-x).
 
         Local Notation wordmax log2wordmax := (2 ^ log2wordmax).
         Local Notation half_bits log2wordmax := (log2wordmax / 2).
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 1a90024e4..4ed42814d 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -235,6 +235,60 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
 
       Local Notation cast := (@ident.cast cast_outside_of_range).
 
+      Lemma cast_opp' r v : (-cast (-r) (-v) = cast r v)%Z.
+      Proof.
+        pose proof (ZRange.goodb_normalize r); cbv [ZRange.goodb] in *.
+        cbv [cast ident.is_more_pos_than_neg]; rewrite !ZRange.normalize_opp, !ZRange.opp_involutive, !Z.opp_involutive.
+        repeat change (lower (-?r)) with (-upper r)%Z.
+        repeat change (upper (-?r)) with (-lower r)%Z.
+        destruct (ZRange.normalize r) as [l u]; clear r; cbn [lower upper] in *.
+        rewrite !Z.abs_opp.
+        repeat first [ progress split_andb
+                     | progress rewrite ?Bool.andb_false_iff in *
+                     | progress rewrite ?Bool.orb_true_iff in *
+                     | progress rewrite ?Bool.orb_false_iff in *
+                     | progress destruct_head'_and
+                     | progress Z.ltb_to_lt
+                     | progress subst
+                     | rewrite !Z.sub_opp_r
+                     | rewrite !Z.opp_involutive
+                     | rewrite !Z.add_0_r
+                     | rewrite !Z.sub_0_r
+                     | rewrite !Z.sub_diag
+                     | rewrite !Z.mod_1_r
+                     | progress change (- (-1))%Z with 1%Z
+                     | progress change (0 - 1)%Z with (-1)%Z
+                     | progress change (-0)%Z with 0%Z
+                     | lia
+                     | match goal with
+                       | [ H : ?x = ?x |- _ ] => clear H
+                       | [ H : (?x <= ?x)%Z |- _ ] => clear H
+                       | [ H : ?T, H' : ?T |- _ ] => clear H'
+                       | [ H : (-?x = -?y)%Z |- _ ] => assert (x = y) by lia; clear H
+                       | [ H : (0 <= - ?x)%Z |- _ ] => assert (x <= 0)%Z by lia; clear H
+                       | [ H : (?x > ?y)%Z |- _ ] => assert (y < x)%Z by lia; clear H
+                       | [ H : (?x >= ?y)%Z |- _ ] => assert (y <= x)%Z by lia; clear H
+                       | [ H : (- ?y < -?x)%Z |- _ ] => assert (x < y)%Z by lia; clear H
+                       | [ H : (?x <= ?y)%Z, H' : (?y <= ?x)%Z |- _ ] => assert (x = y) by lia; clear H H'
+                       (*| [ H : Z.abs ?l = Z.abs ?u |- _ ] => progress cbv [ZRange.opp]; cbn [lower upper]*)
+                       | [ H : (?l <= ?u)%Z, H' : (?u < 0)%Z, H'' : context[Z.abs ?l] |- _ ]
+                         => rewrite (Z.abs_neq l), (Z.abs_neq u) in * by lia
+                       | [ H : (?l <= ?u)%Z, H' : (0 < ?l)%Z, H'' : context[Z.abs ?l] |- _ ]
+                         => rewrite (Z.abs_eq l), (Z.abs_eq u) in * by lia
+                       | [ |- context[(?x mod (-?a + ?b + 1))%Z] ]
+                         => replace (x mod (-a + b + 1))%Z with (-((-x) mod (- - (a - b - 1))))%Z
+                           by (rewrite !Zmod_opp_opp, !Z.opp_involutive; apply f_equal2; lia)
+                       | [ |- context[(?x mod (?a - ?b + 1))%Z] ]
+                         => replace (x mod (a - b + 1))%Z with (-((-x) mod (- - (b - a - 1))))%Z
+                           by (rewrite !Zmod_opp_opp, !Z.opp_involutive; apply f_equal2; lia)
+                       | [ |- context[(?x mod (-1))%Z] ]
+                         => replace ((x mod (-1)))%Z with (-((-x) mod (- - 1)))%Z
+                           by (rewrite !Zmod_opp_opp, !Z.opp_involutive; apply f_equal2; lia)
+                       end
+                     | progress destruct_head'_or
+                     | break_innermost_match_step ].
+      Qed.
+
       Lemma cast_in_normalized_bounds r v : is_bounded_by_bool v (ZRange.normalize r) = true -> cast r v = v.
       Proof. cbv [cast is_bounded_by_bool]; break_innermost_match; congruence. Qed.
 
@@ -245,11 +299,14 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
 
       Lemma cast_always_bounded r v : is_bounded_by_bool (cast r v) (ZRange.normalize r) = true.
       Proof.
-        cbv [is_bounded_by_bool ZRange.normalize lower upper cast]; break_innermost_match; intros;
-          rewrite ?Bool.andb_true_iff, ?Bool.andb_false_iff in *;
-          destruct_head'_and; destruct_head'_or; repeat apply conj; Z.ltb_to_lt.
-        all: split_min_max.
-        all: Z.div_mod_to_quot_rem; nia.
+        pose proof (ZRange.goodb_normalize r); cbv [ZRange.goodb] in *.
+        cbv [cast]; break_innermost_match; Z.div_mod_to_quot_rem.
+        all: destruct (ZRange.normalize r) as [l u]; clear r; cbn [lower upper ZRange.opp] in *.
+        all: cbv [is_bounded_by_bool]; cbn [lower upper].
+        all: repeat first [ progress rewrite ?Bool.andb_true_iff, ?Bool.andb_false_iff in *
+                          | rewrite !Z.leb_le in *
+                          | progress destruct_head'_and
+                          | lia ].
       Qed.
 
       Lemma cast_bounded r v : (lower r <= upper r)%Z -> is_bounded_by_bool (cast r v) r = true.
@@ -268,14 +325,33 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
         edestruct is_bounded_by_bool; tauto.
       Qed.
 
-      Lemma cast_out_of_bounds_in_range r v
-        : is_bounded_by_bool v (ZRange.normalize r) = false
+      Lemma cast_out_of_bounds_in_range_pos r v
+        : ident.is_more_pos_than_neg (ZRange.normalize r) v = true
+          -> is_bounded_by_bool v (ZRange.normalize r) = false
           -> is_bounded_by_bool (cast_outside_of_range (ZRange.normalize r) v) (ZRange.normalize r) = true
           -> cast r v = cast_outside_of_range (ZRange.normalize r) v.
       Proof.
         cbv [cast is_bounded_by_bool]; break_innermost_match; try congruence; intros.
         pose proof (ZRange.goodb_normalize r); cbv [ZRange.goodb] in *.
-        split_andb; Z.ltb_to_lt.
+        split_andb; Z.ltb_to_lt; try lia.
+        match goal with
+        | [ |- context[(?a mod ?b)%Z] ]
+          => cut ((a / b) = 0)%Z
+        end.
+        all: Z.div_mod_to_quot_rem; nia.
+      Qed.
+
+      Lemma cast_out_of_bounds_in_range_neg r v
+        : ident.is_more_pos_than_neg (ZRange.normalize r) v = false
+          -> is_bounded_by_bool v (ZRange.normalize r) = false
+          -> is_bounded_by_bool (-cast_outside_of_range (-ZRange.normalize r) (-v)) (ZRange.normalize r) = true
+          -> cast r v = (-cast_outside_of_range (-ZRange.normalize r) (-v))%Z.
+      Proof.
+        cbv [cast is_bounded_by_bool]; break_innermost_match; try congruence; intros.
+        pose proof (ZRange.goodb_normalize r); cbv [ZRange.goodb] in *.
+        split_andb; Z.ltb_to_lt; try lia.
+        repeat change (lower (-?r)) with (-upper r)%Z.
+        repeat change (upper (-?r)) with (-lower r)%Z.
         match goal with
         | [ |- context[(?a mod ?b)%Z] ]
           => cut ((a / b) = 0)%Z
@@ -283,14 +359,51 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
         all: Z.div_mod_to_quot_rem; nia.
       Qed.
 
+      Lemma cast_out_of_bounds_in_range r v
+        : is_bounded_by_bool v (ZRange.normalize r) = false
+          -> (ident.is_more_pos_than_neg (ZRange.normalize r) v = true -> is_bounded_by_bool (cast_outside_of_range (ZRange.normalize r) v) (ZRange.normalize r) = true)
+          -> (ident.is_more_pos_than_neg (ZRange.normalize r) v = false -> is_bounded_by_bool (-cast_outside_of_range (-ZRange.normalize r) (-v)) (ZRange.normalize r) = true)
+          -> cast r v = if ident.is_more_pos_than_neg (ZRange.normalize r) v
+                        then cast_outside_of_range (ZRange.normalize r) v
+                        else (-cast_outside_of_range (-ZRange.normalize r) (-v))%Z.
+      Proof.
+        pose proof (cast_out_of_bounds_in_range_pos r v).
+        pose proof (cast_out_of_bounds_in_range_neg r v).
+        break_innermost_match; intros; auto.
+      Qed.
+
       Lemma cast_out_of_bounds_simple r v
         : (is_bounded_by_bool v (ZRange.normalize r) = true -> cast_outside_of_range (ZRange.normalize r) v = v)
-          -> is_bounded_by_bool (cast_outside_of_range (ZRange.normalize r) v) (ZRange.normalize r) = true
-          -> cast r v = cast_outside_of_range (ZRange.normalize r) v.
+          -> (ident.is_more_pos_than_neg (ZRange.normalize r) v = false -> (is_bounded_by_bool (-v) (-ZRange.normalize r))%Z = true -> (-cast_outside_of_range (-ZRange.normalize r) (-v) = v)%Z)
+          -> (ident.is_more_pos_than_neg (ZRange.normalize r) v = true -> is_bounded_by_bool (cast_outside_of_range (ZRange.normalize r) v) (ZRange.normalize r) = true)
+          -> (ident.is_more_pos_than_neg (ZRange.normalize r) v = false -> is_bounded_by_bool (-cast_outside_of_range (-ZRange.normalize r) (-v)) (ZRange.normalize r) = true)
+          -> cast r v = if ident.is_more_pos_than_neg (ZRange.normalize r) v
+                        then cast_outside_of_range (ZRange.normalize r) v
+                        else (-cast_outside_of_range (-ZRange.normalize r) (-v))%Z.
       Proof.
+        pose proof (cast_out_of_bounds_in_range r v).
+        assert (is_bounded_by_bool (-v) (-ZRange.normalize r) = is_bounded_by_bool v (ZRange.normalize r)).
+        { cbv [is_bounded_by_bool].
+          repeat change (lower (-?r)) with (-upper r)%Z.
+          repeat change (upper (-?r)) with (-lower r)%Z.
+          cbv [andb]; break_innermost_match; Z.ltb_to_lt; break_match; Z.ltb_to_lt; try lia; try reflexivity.
+          symmetry; Z.ltb_to_lt; lia. }
         destruct (is_bounded_by_bool v (ZRange.normalize r)) eqn:?.
-        { rewrite cast_in_normalized_bounds by assumption; intros; symmetry; auto. }
-        { auto using cast_out_of_bounds_in_range. }
+        { rewrite cast_in_normalized_bounds by assumption; intros; symmetry; break_innermost_match; auto. }
+        { auto. }
+      Qed.
+
+      Lemma is_more_pos_then_neg_0_u u v
+        : (0 <= u)%Z
+          -> ident.is_more_pos_than_neg (ZRange.normalize r[0~>u]) v = true.
+      Proof using Type.
+        intro.
+        cbv [ident.is_more_pos_than_neg]; cbn [upper lower].
+        rewrite (proj1 ZRange.normalize_id_iff_goodb)
+          by (cbv [ZRange.goodb lower upper]; Z.ltb_to_lt; assumption).
+        cbn [lower upper].
+        rewrite Z.abs_0, Z.abs_eq by assumption.
+        cbv [andb orb]; break_innermost_match; Z.ltb_to_lt; try lia; reflexivity.
       Qed.
 
       Lemma cast_out_of_bounds_simple_0 u v
@@ -300,11 +413,13 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
           -> cast r[0~>u] v = cast_outside_of_range r[0~>u] v.
       Proof.
         pose proof (cast_out_of_bounds_simple r[0~>u] v) as H.
-        intro.
+        intro H0.
+        pose proof (is_more_pos_then_neg_0_u u v H0) as H1.
+        rewrite H1 in *.
         rewrite (proj1 ZRange.normalize_id_iff_goodb) in H
           by (cbv [ZRange.goodb lower upper]; Z.ltb_to_lt; assumption).
-        cbv [is_bounded_by_bool] in *; rewrite ?Bool.andb_true_iff in *.
-        intros; apply H; intros; destruct_head'_and; repeat apply conj; Z.ltb_to_lt; auto.
+        cbv [is_bounded_by_bool ZRange.opp] in *; cbn [lower upper] in *; rewrite ?Bool.andb_true_iff, ?Z.leb_le in *.
+        intros; apply H; intros; destruct_head'_and; repeat apply conj; Z.ltb_to_lt; auto; try congruence.
       Qed.
 
       Lemma cast_out_of_bounds_simple_0_mod u v
@@ -312,7 +427,9 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
           -> ((0 <= v <= u)%Z -> cast_outside_of_range r[0~>u] v = v)
           -> (cast r[0~>u] v = (cast_outside_of_range r[0~>u] v) mod (u + 1))%Z.
       Proof.
-        cbv [cast]; intro.
+        intro H0.
+        pose proof (is_more_pos_then_neg_0_u u v H0) as H1.
+        cbv [cast]; rewrite H1.
         rewrite (proj1 ZRange.normalize_id_iff_goodb)
           by (cbv [ZRange.goodb lower upper]; Z.ltb_to_lt; assumption).
         cbn [lower upper].