From 6389e4bc4ea7f062bcffb93067d8aa24d4a55142 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 2 Dec 2023 20:55:51 -0800
Subject: [PATCH] Future-proof CompilersTestCases (#1762)

Also add some utility functions to ZRangeProofs

This is very minor progress towards avoiding replacing the abstract
state of higher order functions with bottom when we can avoid it, in
service of #1609.
---
 src/AbstractInterpretation/ZRangeProofs.v | 19 ++++++++++++++++++-
 src/CompilersTestCases.v                  | 20 ++++++++++----------
 2 files changed, 28 insertions(+), 11 deletions(-)

diff --git a/src/AbstractInterpretation/ZRangeProofs.v b/src/AbstractInterpretation/ZRangeProofs.v
index 3b34786c650..0a6cca2ef62 100644
--- a/src/AbstractInterpretation/ZRangeProofs.v
+++ b/src/AbstractInterpretation/ZRangeProofs.v
@@ -64,6 +64,23 @@ Module Compilers.
         : ZRange.type.option.is_bounded_by x v = true
           -> type.related_hetero (fun t x v => ZRange.type.base.option.is_bounded_by x v = true) x v.
         Proof. induction t; cbn in *; intuition congruence. Qed.
+
+        Lemma is_bounded_by_impl_eqv_refl t
+          (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
+          : ZRange.type.option.is_bounded_by x v = true
+            -> v == v.
+        Proof. induction t; cbn; try reflexivity; try congruence. Qed.
+
+        Lemma andb_bool_for_each_lhs_of_arrow_is_bounded_by_impl_and_for_each_lhs_of_arrow_eqv_refl t
+          (x : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (v : type.for_each_lhs_of_arrow (type.interp base.interp) t)
+          : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) x v = true
+            -> type.and_for_each_lhs_of_arrow (@type.eqv) v v.
+        Proof.
+          induction t; cbn; [ reflexivity | ].
+          rewrite Bool.andb_true_iff.
+          intros [H0 H1].
+          split; eauto using is_bounded_by_impl_eqv_refl.
+        Qed.
       End option.
     End type.
 
@@ -244,7 +261,7 @@ Module Compilers.
                 -- f_equal. assumption.
                 -- intros v H. apply IH2. assumption.
           Qed.
-          
+
           Local Ltac handle_lt_le_t_step_fast :=
             first [ match goal with
                     | [ H : (?a <= ?b)%Z, H' : (?b <= ?a)%Z |- _ ]
diff --git a/src/CompilersTestCases.v b/src/CompilersTestCases.v
index bc2f545ecf9..96a78ac6390 100644
--- a/src/CompilersTestCases.v
+++ b/src/CompilersTestCases.v
@@ -63,34 +63,34 @@ Module testrewrite.
                           ((\ x , expr_let y := ##5 in $$y + ($$y + (#ident.fst @ $$x + #ident.snd @ $$x)))
                              @ (##1, ##7))%expr).
 
-  Redirect "log" Eval cbv in partial.eval_with_bound partial.default_relax_zrange false (@ident.is_comment) false
+  Redirect "log" Eval cbv in partial.EvalWithBound partial.default_relax_zrange false (@ident.is_comment) false
                                       (RewriteRules.RewriteNBE RewriteRules.default_opts (fun var =>
                 (\z , ((\ x , expr_let y := ##5 in $$y + ($$z + (#ident.fst @ $$x + #ident.snd @ $$x)))
-                         @ (##1, ##7)))%expr) _)
+                         @ (##1, ##7)))%expr))
                 (Datatypes.Some r[0~>100]%zrange, Datatypes.tt).
 End testrewrite.
 Module testpartial.
   Import expr.
   Import ident.
 
-  Redirect "log" Eval compute in partial.eval
-                          (#ident.fst @ (expr_let x := ##10 in ($$x, $$x)))%expr.
+  Redirect "log" Eval compute in partial.Eval
+                          (fun _ => #ident.fst @ (expr_let x := ##10 in ($$x, $$x)))%expr.
 
   Notation "x + y" := (@expr.Ident base.type ident _ _ (ident.Z_add) @ x @ y)%expr : expr_scope.
 
-  Redirect "log" Eval compute in partial.eval
-                          ((\ x , expr_let y := ##5 in #ident.fst @ $$x + (#ident.fst @ $$x + ($$y + $$y)))
+  Redirect "log" Eval compute in partial.Eval
+                          (fun _ => (\ x , expr_let y := ##5 in #ident.fst @ $$x + (#ident.fst @ $$x + ($$y + $$y)))
                              @ (##1, ##1))%expr.
 
-  Redirect "log" Eval compute in partial.eval
-                          ((\ x , expr_let y := ##5 in $$y + ($$y + (#ident.fst @ $$x + #ident.snd @ $$x)))
+  Redirect "log" Eval compute in partial.Eval
+                          (fun _ => (\ x , expr_let y := ##5 in $$y + ($$y + (#ident.fst @ $$x + #ident.snd @ $$x)))
                              @ (##1, ##7))%expr.
 
 
-  Redirect "log" Eval cbv in partial.eval_with_bound
+  Redirect "log" Eval cbv in partial.EvalWithBound
                 partial.default_relax_zrange
                 false (@ident.is_comment) false
-                (\z , ((\ x , expr_let y := ##5 in $$y + ($$z + (#ident.fst @ $$x + #ident.snd @ $$x)))
+                (fun _ => \z , ((\ x , expr_let y := ##5 in $$y + ($$z + (#ident.fst @ $$x + #ident.snd @ $$x)))
                          @ (##1, ##7)))%expr
                 (Datatypes.Some r[0~>100]%zrange, Datatypes.tt).
 End testpartial.