Fix some bounds analysis

3 files changed, 21 insertions, 10 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index bec6434a1..858832f5d 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -521,10 +521,11 @@ Module Compilers.
              | ident.Z_add as idc
              | ident.Z_mul as idc
              | ident.Z_sub as idc
+               => fun x y => x <- x; y <- y; Some (ZRange.four_corners (ident.interp idc) x y)
              | ident.Z_div as idc
              | ident.Z_shiftr as idc
              | ident.Z_shiftl as idc
-               => fun x y => x <- x; y <- y; Some (ZRange.four_corners (ident.interp idc) x y)
+               => fun x y => x <- x; y <- y; Some (ZRange.four_corners_and_zero (ident.interp idc) x y)
              | ident.Z_add_with_carry as idc
                => fun x y z => x <- x; y <- y; z <- z; Some (ZRange.eight_corners (ident.interp idc) x y z)
              | ident.Z_cc_m as idc
diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v
index 6b5a430c4..1245bfe3f 100644
--- a/src/Util/ZRange/BasicLemmas.v
+++ b/src/Util/ZRange/BasicLemmas.v
@@ -89,16 +89,22 @@ Module ZRange.
     rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *; repeat apply conj; etransitivity; destruct_head'_and; eassumption.
   Qed.
 
-  Lemma is_bounded_by_bool_Proper_if_sumbool_union {A B} (b : sumbool A B) x y rx ry
-    : is_bounded_by_bool x rx = true
-      -> is_bounded_by_bool y ry = true
+  Lemma is_bounded_by_bool_Proper_if_sumbool_union_dep {A B} (b : sumbool A B) x y rx ry
+    : (A -> is_bounded_by_bool x rx = true)
+      -> (B -> is_bounded_by_bool y ry = true)
       -> is_bounded_by_bool (if b then x else y) (Operations.ZRange.union rx ry) = true.
   Proof.
     destruct b; cbv [Operations.ZRange.union is_bounded_by_bool];
-      intros; Bool.split_andb; rewrite Bool.andb_true_iff; split; Z.ltb_to_lt; cbn [lower upper] in *; split_min_max.
+      intros; specialize_by_assumption; Bool.split_andb; rewrite Bool.andb_true_iff; split; Z.ltb_to_lt; cbn [lower upper] in *; split_min_max.
     all: lia.
   Qed.
 
+  Lemma is_bounded_by_bool_Proper_if_sumbool_union {A B} (b : sumbool A B) x y rx ry
+    : is_bounded_by_bool x rx = true
+      -> is_bounded_by_bool y ry = true
+      -> is_bounded_by_bool (if b then x else y) (Operations.ZRange.union rx ry) = true.
+  Proof. intros; apply is_bounded_by_bool_Proper_if_sumbool_union_dep; auto. Qed.
+
   Lemma is_bounded_by_bool_opp x r : is_bounded_by_bool (Z.opp x) (ZRange.opp r) = is_bounded_by_bool x r.
   Proof.
     cbv [is_bounded_by_bool andb opp]; cbn [lower upper]; break_match; Z.ltb_to_lt; break_match; Z.ltb_to_lt;
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index 95f32869c..32af62ee5 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -43,20 +43,24 @@ Module ZRange.
     := let (l, u) := eta v in
        r[ f l ~> f u ].
 
-  Definition split_range_at_0 (x : zrange) : option zrange (* < 0 *) * option zrange (* >= 0 *)
+  Definition split_range_at_0 (x : zrange) : option zrange (* < 0 *) * option zrange (* = 0 *) * option zrange (* >= 0 *)
     := let (l, u) := eta x in
        (if (0 <=? l)%Z
         then None
         else Some r[l ~> Z.min u (-1)],
+        if ((0 <? l)%Z || (u <? 0)%Z)%bool
+        then None
+        else Some r[0 ~> 0],
         if (0 <=? u)%Z
-        then Some r[Z.max 0 l ~> u]
+        then Some r[Z.max 1 l ~> u]
         else None).
 
   Definition apply_to_split_range (f : zrange -> zrange) (v : zrange) : zrange
     := match split_range_at_0 v with
-       | (Some n, Some p) => union (f n) (f p)
-       | (Some v, None) | (None, Some v) => f v
-       | (None, None) => f v
+       | (Some n, Some z, Some p) => union (union (f n) (f p)) (f z)
+       | (Some v1, Some v2, None) | (Some v1, None, Some v2) | (None, Some v1, Some v2) => union (f v1) (f v2)
+       | (Some v, None, None) | (None, Some v, None) | (None, None, Some v) => f v
+       | (None, None, None) => f v
        end.
 
   Definition apply_to_range (f : BinInt.Z -> zrange) (v : zrange) : zrange