From a7bc3fde287c451d2b0e77602cd9fab560d62a43 Mon Sep 17 00:00:00 2001
From: jadep <jadep@mit.edu>
Date: Fri, 15 Feb 2019 13:18:37 -0500
Subject: fix cast admits in Fancy

---
 src/Fancy/Barrett256.v    | 12 ++----------
 src/Fancy/Montgomery256.v | 16 ++--------------
 2 files changed, 4 insertions(+), 24 deletions(-)

(limited to 'src/Fancy')

diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v
index 2ac904cc9..58a9efd2d 100644
--- a/src/Fancy/Barrett256.v
+++ b/src/Fancy/Barrett256.v
@@ -47,7 +47,7 @@ Module Barrett256.
     forall (xLow xHigh : Z),
       0 <= xLow < 2 ^ machine_wordsize ->
       0 <= xHigh < M ->
-      expr.Interp (@ident.interp) barrett_red256 xLow xHigh = (xLow + 2 ^ machine_wordsize * xHigh) mod M.
+      expr.Interp (@ident.gen_interp cast_oor) barrett_red256 xLow xHigh = (xLow + 2 ^ machine_wordsize * xHigh) mod M.
   Proof.
     intros.
     rewrite <-barrett_reduce_correct_specialized by assumption.
@@ -97,12 +97,6 @@ Module Barrett256.
            | |- of_prefancy_scalar _ _ _ _ = _ => cbn; solve [eauto]
            end.
 
-  Lemma swap_casts xLow xHigh :
-    expr.interp (@ident.gen_interp cast_oor)
-                (invert_expr.smart_App_curried (barrett_red256 (type.interp base.interp)) (xLow, (xHigh, tt))) =
-    defaults.Interp barrett_red256 xLow xHigh.
-  Admitted.
-
   Lemma barrett_red256_fancy_correct :
     forall xLow xHigh error,
       0 <= xLow < 2 ^ machine_wordsize ->
@@ -155,9 +149,7 @@ Module Barrett256.
     { cbn. cbv [muLow M].
       repeat (econstructor; [ solve [valid_expr_subgoal] | intros ]).
       econstructor. valid_expr_subgoal. }
-    { cbn - [barrett_red256]. cbv [id].
-      f_equal.
-      apply swap_casts. }
+    { reflexivity. }
   Qed.
 
   Import Spec.Registers.
diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v
index a4b27c561..ec4848b0b 100644
--- a/src/Fancy/Montgomery256.v
+++ b/src/Fancy/Montgomery256.v
@@ -49,7 +49,7 @@ Module Montgomery256.
       0 <= lo < R ->
       0 <= hi < R ->
       0 <= lo + R * hi < R * N ->
-      expr.Interp (@ident.interp) montred256 lo hi = ((lo + R * hi) * R') mod N.
+      expr.Interp (@ident.gen_interp cast_oor) montred256 lo hi = ((lo + R * hi) * R') mod N.
   Proof.
     intros.
     rewrite <-montred'_correct_specialized by assumption.
@@ -62,7 +62,6 @@ Module Montgomery256.
       generalize MontgomeryReduction.montred'; vm_compute; reflexivity. }
   Qed.
 
-
   Definition montred256_fancy' (RegMod RegPInv RegZero lo hi error : positive) :=
     of_Expr 6%positive
             (make_consts [(RegMod, N); (RegZero, 0); (RegPInv, N')])
@@ -101,15 +100,6 @@ Module Montgomery256.
            | |- of_prefancy_scalar _ _ _ _ = _ => cbn; solve [eauto]
            end.
 
-  (* TODO(jgross): switch out casts *)
-  (* might need to use CheckCasts.interp_eqv_without_casts? *)
-  Lemma swap_casts lo hi :
-    expr.interp (@ident.gen_interp cast_oor)
-                (invert_expr.smart_App_curried (montred256 (type.interp base.interp)) (lo, (hi, tt))) =
-    expr.interp (@ident.interp)
-                (invert_expr.smart_App_curried (montred256 (type.interp base.interp)) (lo, (hi, tt))).
-  Admitted.
-
   Lemma montred256_fancy_correct :
     forall lo hi error,
       0 <= lo < R ->
@@ -156,9 +146,7 @@ Module Montgomery256.
     { cbn. cbv [N' N].
       repeat (econstructor; [ solve [valid_expr_subgoal] | intros ]).
       econstructor. valid_expr_subgoal. }
-    { cbn - [montred256]. cbv [id].
-      f_equal.
-      apply swap_casts. }
+    { reflexivity. }
   Qed.
 
   Import Spec.Registers.
-- 
cgit v1.2.3