EdDSA: prove things about spec

3 files changed, 96 insertions, 62 deletions

diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v
index e5b74085e..c0b6be25b 100644
--- a/src/Experiments/DerivationsOptionRectLetInEncoding.v
+++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v
@@ -150,63 +150,6 @@ Proof.
          end.
 Qed.
 
-Global Instance option_rect_Proper_nd {A T}
-  : Proper ((pointwise_relation _ eq) ==> eq  ==> eq ==> eq) (@option_rect A (fun _ => T)).
-Proof.
-  intros ?? H ??? [|]??; subst; simpl; congruence.
-Qed.
-
-Global Instance option_rect_Proper_nd' {A T}
-  : Proper ((pointwise_relation _ eq) ==> eq  ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)).
-Proof.
-  intros ?? H ??? [|]; subst; simpl; congruence.
-Qed.
-
-Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances.
-
-Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v,
-    option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v).
-Proof.
-  destruct v; reflexivity.
-Qed.
-
-Lemma option_rect_function {A B C S' N' v} f
-  : f (option_rect (fun _ : option A => option B) S' N' v)
-    = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v.
-Proof. destruct v; reflexivity. Qed.
-Local Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *)
-  idtac;
-  lazymatch goal with
-  | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ]
-    => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *)
-    cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta;
-    [ set_evars;
-      let H := fresh in
-      intro H;
-      rewrite H;
-      clear;
-      abstract (cbv [Let_In]; reflexivity)
-    | ]
-  end.
-
-(** TODO: possibly move me, remove local *)
-Local Ltac replace_option_match_with_option_rect :=
-  idtac;
-  lazymatch goal with
-  | [ |- _ = ?RHS :> ?T ]
-    => lazymatch RHS with
-       | match ?a with None => ?N | Some x => @?S x end
-         => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity)
-       end
-  end.
-Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *)
-  repeat match goal with
-         | [ |- context[option_rect ?P ?S ?N None] ]
-           => change (option_rect P S N None) with N
-         | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ]
-           => change (option_rect P S N (Some x)) with (S x); cbv beta
-         end.
-
 Definition COMPILETIME {T} (x:T) : T := x.
 
 Lemma N_to_nat_le_mono : forall a b, (a <= b)%N -> (N.to_nat a <= N.to_nat b)%nat.
@@ -348,4 +291,4 @@ End with_unqualified_modulo2.
 Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y.
 Proof.
   split; eauto using F_eqb_eq, F_eqb_complete.
-Qed.
+Qed.
\ No newline at end of file
diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
new file mode 100644
index 000000000..e3a1a6ad2
--- /dev/null
+++ b/src/Experiments/EdDSARefinement.v
@@ -0,0 +1,91 @@
+Require Import Crypto.Spec.EdDSA Bedrock.Word.
+Require Import Coq.Classes.Morphisms.
+Require Import Util.Decidable Util.Option Util.Tactics.
+
+Section EdDSA.
+  Context `{prm:EdDSA}.
+  Context {eq_dec:DecidableRel Eeq}.
+  Local Infix "==" := Eeq (at level 69, no associativity).
+  Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc).
+  Local Infix "*" := EscalarMult. Local Infix "+" := Eadd. Local Infix "++" := combine.
+  Local Notation "P - Q" := (P + Eopp Q).
+
+  Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}.
+  Context {Proper_Eopp : Proper (Eeq==>Eeq) Eopp}.
+  Context {Proper_Eadd : Proper (Eeq==>Eeq==>Eeq) Eadd}.
+  Context {Proper_EscalarMult : Proper (Logic.eq==>Eeq==>Eeq) EscalarMult}.
+
+  Context {decE:word b-> option E}.
+  Context {decS:word b-> option nat}.
+
+  Context {decE_canonical: forall x s, decE x = Some s -> x = Eenc s }.
+  Context {decS_canonical: forall x s, decS x = Some s -> x = Senc s }.
+
+  Context {decS_Senc: forall x, decS (Senc x) = Some x}.
+  Context {decE_Eenc: forall x, decE (Eenc x) = Some x}. (* FIXME: equivalence relation *)
+
+  Lemma solve_for_R : forall s B R n A, s * B == R + n * A <-> R == s*B - n*A.
+  Proof.
+    intros; split;
+      intro Heq; rewrite Heq; clear Heq.
+  Admitted.
+    
+  Definition verify {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool :=
+    option_rect (fun _ => bool) (fun S : nat =>
+    option_rect (fun _ => bool) (fun A : E =>
+       weqb
+         (split1 b b sig)
+         (Eenc (S * B - PeanoNat.Nat.modulo (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ pk ++ message))) l * A))
+    ) false (decE pk)
+    ) false (decS (split2 b b sig))
+  .
+  
+  Lemma verify_correct mlen (message:word mlen) (pk:word b) (sig:word (b+b)) :
+      verify message pk sig = true <-> valid message pk sig.
+  Proof.
+    cbv [verify option_rect option_map].
+    split.
+    {
+      repeat match goal with
+             | |- false = true -> _ => let H:=fresh "H" in intro H; discriminate H
+             | [H: _ |- _ ] => apply decS_canonical in H
+             | [H: _ |- _ ] => apply decE_canonical in H
+             | _ => rewrite weqb_true_iff
+             | _ => break_match
+             end.
+      intro.
+      subst.
+      rewrite <-combine_split.
+      rewrite Heqo.
+      rewrite H0.
+      constructor.
+      rewrite <-H0.
+      rewrite solve_for_R.
+      reflexivity.
+    }
+    {
+      intros [? ? ? ? Hvalid].
+      rewrite solve_for_R in Hvalid.
+      rewrite split1_combine.
+      rewrite split2_combine.
+      rewrite decS_Senc.
+      rewrite decE_Eenc.
+      rewrite weqb_true_iff.
+      f_equiv. exact Hvalid.
+    }
+  Qed.
+
+  Lemma scalarMult_mod_order : forall l x B, l * B == Ezero -> (Nat.modulo x l) * B == x * B. Admitted.
+
+  Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M).
+  Proof.
+    cbv [sign public].
+    intros. subst. constructor.
+    Local Arguments H {_} _.
+    Local Notation "'$' x" := (wordToNat x) (at level 1).
+    Local Infix "mod" := Nat.modulo (at level 50).
+    set (HRAM := H (Eenc ($ (H (prngKey sk ++ M)) * B) ++ Eenc (curveKey sk * B) ++ M)).
+    set (r := H (prngKey sk ++ M)).
+    repeat rewrite scalarMult_mod_order by eapply EdDSA_l_order_B.
+  Admitted.
+End EdDSA.
\ No newline at end of file
diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
index 4e30313d9..659a0ec66 100644
--- a/src/Experiments/SpecEd25519.v
+++ b/src/Experiments/SpecEd25519.v
@@ -149,11 +149,11 @@ Local Infix "*" := (E.mul(H0:=curve25519params)).
 Axiom H : forall n : nat, word n -> word (b + b).
 Axiom B : point. (* TODO: B = decodePoint (y=4/5, x="positive") *)
 Axiom B_nonzero : B <> zero.
-Axiom l_order_B : l * B = zero.
-Axiom point_encoding : canonical encoding of point as word b.
-Axiom scalar_encoding : canonical encoding of {n : nat | n < l} as word b.
+Axiom l_order_B : E.eq (l * B) zero.
+Axiom Eenc : point -> word b.
+Axiom Senc : nat -> word b.
 
-Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B point_encoding scalar_encoding :=
+Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B Eenc Senc :=
   {
     EdDSA_c_valid := c_valid;
     EdDSA_n_ge_c := n_ge_c;