Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to

comparing points).

1 files changed, 9 insertions, 0 deletions

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index d655d046d..6a8831b14 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -46,6 +46,15 @@ Proof.
   rewrite pow2_id; assumption.
 Qed.
 
+Lemma weqb_false_iff : forall sz (x y : word sz), weqb x y = false <-> x <> y.
+Proof.
+  split; intros.
+  + intro eq_xy; apply weqb_true_iff in eq_xy; congruence.
+  + case_eq (weqb x y); intros weqb_xy; auto.
+    apply weqb_true_iff in weqb_xy.
+    congruence.
+Qed.
+
 Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
   refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
                             | eq_refl => w