almost fix Ed25519 for 8.4

1 files changed, 12 insertions, 7 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 8958aed4e..895c8bf15 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -1086,7 +1086,7 @@ Lemma shiftr_range : forall a n m,
   (0 <= Z.shiftr a n < 2 ^ m)%Z.
 Admitted.
 
-Lemma feDec_correct : forall w : Word.word (Init.Nat.pred b),
+Lemma feDec_correct : forall w : Word.word (pred b),
         option_eq GF25519BoundedCommon.eq
           (option_map GF25519BoundedCommon.encode
                       (PointEncoding.Fdecode w)) (feDec w).
@@ -1139,8 +1139,8 @@ Proof.
     destruct (lt_dec i 8).
     { cbv [Tuple.to_list Tuple.to_list' fst snd].
         assert (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4 \/ i = 5 \/ i = 6 \/ i = 7) by omega.
-        repeat match goal with H : _ \/ _ |- _ => destruct H; subst end;
-        cbv [nth_default nth_error]; try (apply pow2_mod_range; omega);
+        repeat match goal with H : (_ \/ _)%type |- _ => destruct H; subst end;
+        cbv [nth_default nth_error value]; try (apply pow2_mod_range; omega).
             repeat apply shiftr_range; apply WordNZ_range_mono; cbv;
             congruence. }
     { rewrite !nth_default_out_of_bounds
@@ -1168,7 +1168,7 @@ Proof.
       192 <= n < 224 \/
       224 <= n < 256 \/
       256 <= n)%Z by omega.
-  repeat match goal with H : _ \/ _ |- _ => destruct H; subst end;
+  repeat match goal with H : (_ \/ _)%type |- _ => destruct H; subst end;
   repeat match goal with
          | |- _ => rewrite Z.lor_spec
          | |- _ => rewrite Z.shiftl_spec by omega
@@ -1191,7 +1191,8 @@ Proof.
           replace m with n by omega; reflexivity
         | |- Z.testbit ?w ?n = (Z.testbit ?w ?m || _)%bool =>
           replace m with n by omega
-         end.
+         end;
+  admit. (* TODO(jadep): there are goal left here on 8.4 *)
   }
   match goal with
     |- option_eq _ (option_map _ (if Z_lt_dec ?a ?b then Some _ else None)) (if (?X =? 1)%Z then None else Some _) =>
@@ -1211,7 +1212,7 @@ Proof.
     intuition; try omega.
     apply Znat.N2Z.is_nonneg.
   }
-  
+ 
   do 2 VerdiTactics.break_if;
   [ 
   match goal with H: ?P, Hiff : ?P <-> ?x = 0%Z |- _ =>
@@ -1279,7 +1280,10 @@ Proof.
   rewrite GF25519Bounded.sqrt_correct.
   cbv [GF25519Bounded.GF25519sqrt].
   cbv [LetIn.Let_In].
-  rewrite !GF25519BoundedCommon.proj1_fe25519_encode.
+  repeat match goal with (* needed on Coq 8.4, should be the only default everywhere *)
+           |- context[GF25519BoundedCommon.proj1_fe25519 (GF25519BoundedCommon.encode ?x)] =>
+           rewrite (GF25519BoundedCommon.proj1_fe25519_encode x)
+         end.
   rewrite GF25519.sqrt_correct, ModularBaseSystemOpt.sqrt_5mod8_opt_correct by reflexivity.
   cbv [ModularBaseSystem.eq].
   rewrite ModularBaseSystemProofs.encode_rep.
@@ -1720,3 +1724,4 @@ erepAdd p q =
               let {y5 = mul3 g h0} in
               let {t3 = mul3 e h0} in let {z3 = mul3 f g} in (,) ((,) ((,) x3 y5) z3) t3}}}}}}
 *)
+