Fix a wrong bound computation (on negatives), fix a proof

2 files changed, 6 insertions, 1 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index 3391c741b..bec6434a1 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -429,7 +429,11 @@ Module Compilers.
                => fun v m
                  => match to_literal m, to_literal v with
                    | Some m, Some v => of_literal (ident.interp idc v m)
-                   | Some m, None => Some r[0 ~> m]
+                   | Some m, None => Some (if (0 <? m)%Z
+                                           then r[0 ~> m-1]
+                                           else if (m =? 0)%Z
+                                                then r[0 ~> 0]
+                                                else r[m+1 ~> 0])
                    | _, _ => None
                    end
              | ident.bool_rect _
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 626fb04f1..727426082 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -1782,6 +1782,7 @@ Module Import UnsaturatedSolinas.
         { rewrite !map_app in *; cbn [map] in *.
           erewrite !eval_snoc by (distr_length; eauto).
           cbn [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by] in *.
+          cbv [is_bounded_by_bool] in *.
           specialize_by (intros; auto with omega).
           specialize (Hwt n); specialize_by omega.
           repeat first [ progress Bool.split_andb