1 files changed, 43 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
new file mode 100644
index 000000000..560f89199
--- /dev/null
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -0,0 +1,43 @@
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.Sum.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Experiments.NewPipeline.Language.
+Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation.
+Local Open Scope Z_scope.
+
+Module Compilers.
+  Export Language.Compilers.
+  Export UnderLets.Compilers.
+  Export AbstractInterpretation.Compilers.
+  Import invert_expr.
+  Import defaults.
+
+  Axiom admit_pf : False.
+  Local Notation admit := (match admit_pf with end).
+
+  Theorem CheckedPartialEvaluateWithBounds_Correct
+          (relax_zrange : zrange -> option zrange)
+          (Hrelax : forall r r' z, is_tighter_than_bool z r = true
+                                   -> relax_zrange r = Some r'
+                                   -> is_tighter_than_bool z r' = true)
+          {t} (E : Expr t)
+          (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+          (b_out : ZRange.type.base.option.interp (type.final_codomain t))
+          rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange E b_in b_out = inl rv)
+    : forall arg
+             (Harg : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg = true),
+      ZRange.type.base.option.is_bounded_by b_out (type.app_curried (Interp rv) arg) = true
+      /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg
+                                 = type.app_curried (Interp E) arg.
+  Proof.
+    cbv [CheckedPartialEvaluateWithBounds CheckPartialEvaluateWithBounds Let_In] in *;
+      break_innermost_match_hyps; inversion_sum; subst.
+    intros arg Harg.
+    split.
+    { eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ].
+      revert Harg.
+      exact admit. (* boundedness *) }
+    { exact admit. (* correctness of interp *) }
+  Qed.
+End Compilers.