Derive EdDSA.verify from equational specification

Experiments/SpecEd25519 will come back soon

1 files changed, 29 insertions, 0 deletions

diff --git a/src/Util/Relations.v b/src/Util/Relations.v
new file mode 100644
index 000000000..aa280db26
--- /dev/null
+++ b/src/Util/Relations.v
@@ -0,0 +1,29 @@
+Require Import Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Logic.
+Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
+
+Lemma symmetry_iff {T} {R} {Rsym:@Symmetric T R} x y: R x y <-> R y x.
+  intuition eauto using symmetry.
+Qed.
+
+Lemma and_rewrite_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB}
+      (f:A->B) ref P {Proper_P: Proper (RA==>RB==>iff) P} a
+  : (RB (f a) ref /\ P a (f a)) <-> (RB (f a) ref /\ P a ref).
+Proof.
+  logic; match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end.
+Qed.
+
+Lemma and_rewriteleft_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB}
+      (f:A->B) ref P {Proper_P: Proper (RA==>RB==>iff) P} a
+  : (RB ref (f a) /\ P a (f a)) <-> (RB ref (f a) /\ P a ref).
+Proof.
+  logic; match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end.
+Qed.
+
+Lemma exists_and_equiv_r {A} {RA} {Equivalence_RA:Equivalence RA}
+      P {Proper_P: Proper (RA==>iff) P} (ref:A)
+  : (exists a, P a /\ RA a ref) <-> P ref.
+Proof.
+  logic; try match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end.
+  repeat (assumption||reflexivity||econstructor); assumption. (* WHY the last [assumption]?*)
+Qed.