alternative signing derivation

cleanup

5 files changed, 128 insertions, 18 deletions

diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
index afdf24604..48845b08e 100644
--- a/src/Experiments/EdDSARefinement.v
+++ b/src/Experiments/EdDSARefinement.v
@@ -5,13 +5,10 @@ Require Import Crypto.Algebra. Import Group ScalarMult.
 Require Import Crypto.Util.Decidable Crypto.Util.Option Crypto.Util.Tactics.
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil.
+Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn.
 Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems.
 
-Module Import NotationsFor8485.
-  Import NPeano Nat.
-  Infix "mod" := modulo.
-End NotationsFor8485.
+Import Notations.
 
 Section EdDSA.
   Context `{prm:EdDSA}.
@@ -55,7 +52,7 @@ Section EdDSA.
   Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}.
 
   Local Infix "++" := combine.
-  Definition verify_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)),
+  Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)),
       verify mlen message pk sig = true <-> valid message pk sig }.
   Proof.
     eexists; intros; set_evars.
@@ -91,11 +88,11 @@ Section EdDSA.
          unify f term; reflexivity
     end.
   Defined.
-  Definition verify {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool :=
-    Eval cbv [proj1_sig verify_sig] in proj1_sig verify_sig mlen message pk sig.
-  Lemma verify_correct : forall {mlen} (message:word mlen) pk sig,
-    verify message pk sig = true <-> valid message pk sig.
-  Proof. exact (proj2_sig verify_sig). Qed.
+  Definition verify' {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool :=
+    Eval cbv [proj1_sig verify'_sig] in proj1_sig verify'_sig mlen message pk sig.
+  Lemma verify'_correct : forall {mlen} (message:word mlen) pk sig,
+    verify' message pk sig = true <-> valid message pk sig.
+  Proof. exact (proj2_sig verify'_sig). Qed.
 
   Section ChangeRep.
     Context {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@group Erep ErepEq ErepAdd ErepId ErepOpp}.
@@ -121,12 +118,12 @@ Section EdDSA.
 
     Definition verify_using_representation
                {mlen} (message:word mlen) (pk:word b) (sig:word (b+b))
-               : { answer | answer = verify message pk sig }.
+               : { answer | answer = verify' message pk sig }.
     Proof.
+      eexists.
       pose proof EdDSA_l_odd.
       assert (l_pos:(0 < l)%Z) by omega.
-      eexists.
-      cbv [verify].
+      cbv [verify'].
 
       etransitivity. Focus 2. {
         eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
@@ -184,5 +181,102 @@ Section EdDSA.
 
       reflexivity.
     Defined.
+    
+    Definition verify {mlen} (msg:word mlen) pk sig :=
+      Eval cbv beta iota delta [proj1_sig verify_using_representation] in
+      proj1_sig (verify_using_representation msg pk sig).
+    Lemma verify_correct {mlen} (msg:word mlen) pk sig : verify msg pk sig = true <-> valid msg pk sig.
+    Proof.
+      etransitivity; [|eapply (verify'_correct msg pk sig)].
+      eapply iff_R_R_same_r, (proj2_sig (verify_using_representation _ _ _)).
+    Qed.
+
+    Context {SRepEnc : SRep -> word b}
+            {SRepEnc_correct : forall x, Senc x = SRepEnc (S2Rep x)}
+            {Proper_SRepEnc:Proper (SRepEq==>Logic.eq) SRepEnc}.
+    Context {SRepAdd : SRep -> SRep -> SRep}
+            {SRepAdd_correct : forall x y, SRepEq (S2Rep (x+y)%F) (SRepAdd (S2Rep x) (S2Rep y)) }
+            {Proper_SRepAdd:Proper (SRepEq==>SRepEq==>SRepEq) SRepAdd}.
+    Context {SRepMul : SRep -> SRep -> SRep}
+            {SRepMul_correct : forall x y, SRepEq (S2Rep (x*y)%F) (SRepMul (S2Rep x) (S2Rep y)) }
+            {Proper_SRepMul:Proper (SRepEq==>SRepEq==>SRepEq) SRepMul}.
+    Context {ErepB:Erep} {ErepB_correct:ErepEq ErepB (EToRep B)}.
+
+    Context {wbRepKeepLow wbRepClearLow wbRepClearBit wbRepSetBit:nat->word b->word b}.
+    Context {wbRepSetBit_correct : forall n x, wordToNat (wbRepSetBit n x) = setbit (wordToNat x) n}.
+    Context {wbRepClearLow_correct : forall c x, wordToNat (wbRepClearLow c x) = wordToNat x - wordToNat x mod 2 ^ c}.
+    Context {wbRepKeepLow_correct : forall n x, wordToNat (wbRepKeepLow n x) = (wordToNat x) mod (2^n)}.
+    Context {SRepDecModLShort} {SRepDecModLShort_correct: forall (w:word b), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModLShort w)}.
+
+    (* We would ideally derive the optimized implementations from
+    specifications using `setoid_rewrite`, but doing this without
+    inlining let-bound subexpressions turned out to be quite messy in
+    the current state of Coq: <https://github.com/mit-plv/fiat-crypto/issues/64> *)
+
+    Definition splitSecretPrngCurve (sk:word b) : SRep * word b :=
+      dlet hsk := H _ sk in
+      dlet curveKey := SRepDecModLShort (wbRepSetBit n (wbRepClearLow c (wbRepKeepLow n (split1 b b hsk)))) in
+      dlet prngKey := split2 b b hsk in
+      (curveKey, prngKey).
+
+    (* TODO: prove these, somewhere *)
+    Axiom wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a).
+    Axiom wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a).
+    Axiom nat_mod_smaller_power_of_two : forall n b:nat,
+      (n <= b -> forall x:nat, (x mod 2 ^ b) mod 2 ^ n = (x mod 2^n))%nat.
+
+    Lemma splitSecretPrngCurve_correct sk :
+      let (s, r) := splitSecretPrngCurve sk in
+      SRepEq s (S2Rep (F.of_nat l (curveKey sk))) /\ r = prngKey (H:=H) sk.
+    Proof.
+      cbv [splitSecretPrngCurve EdDSA.curveKey EdDSA.prngKey Let_In]; split;
+        repeat (
+            reflexivity
+            || rewrite <-SRepDecModLShort_correct
+            || rewrite wbRepSetBit_correct
+            || rewrite wbRepClearLow_correct
+            || rewrite wbRepKeepLow_correct
+            || rewrite wordToNat_split1
+            || rewrite wordToNat_wfirstn
+            || rewrite nat_mod_smaller_power_of_two by (destruct prm; omega)
+          ).
+    Qed.
+
+    Definition sign (pk sk : word b) {mlen} (msg:word mlen) :=
+      dlet sp := splitSecretPrngCurve sk in
+      dlet s := fst sp in
+      dlet p := snd sp in
+      dlet r := SRepDecModL (H _ (p ++ msg)) in
+      dlet R := SRepERepMul r ErepB in
+      dlet S := SRepAdd r (SRepMul (SRepDecModL (H _ (ERepEnc R ++ pk ++ msg))) s) in
+      ERepEnc R ++ SRepEnc S.
+
+    Lemma sign_correct (pk sk : word b) {mlen} (msg:word mlen)
+               : sign pk sk msg = EdDSA.sign pk sk msg.
+    Proof.
+      cbv [sign EdDSA.sign Let_In].
+
+      let H := fresh "H" in 
+      pose proof (splitSecretPrngCurve_correct sk) as H;
+        destruct (splitSecretPrngCurve sk);
+        destruct H as [curveKey_correct prngKey_correct].
+
+      repeat (
+          reflexivity
+          || rewrite ERepEnc_correct
+          || rewrite SRepEnc_correct
+          || rewrite SRepDecModL_correct
+          || rewrite SRepERepMul_correct
+          || rewrite (F.of_nat_add (m:=l))
+          || rewrite (F.of_nat_mul (m:=l))
+          || rewrite SRepAdd_correct
+          || rewrite SRepMul_correct
+          || rewrite ErepB_correct
+          || rewrite <-prngKey_correct
+          || rewrite <-curveKey_correct
+          || eapply (f_equal2 (fun a b => a ++ b))
+          || f_equiv
+        ).
+    Qed.
   End ChangeRep.
 End EdDSA.
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 5984b4e6d..f1a2d15a4 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -173,6 +173,14 @@ Module F.
       rewrite Z2Nat.id by omega.
       rewrite <-F.of_Z_mod; reflexivity.
     Qed.
+
+    Lemma of_nat_add x y :
+      F.of_nat m (x + y) = (F.of_nat m x + F.of_nat m y)%F.
+    Proof. unfold F.of_nat; rewrite Nat2Z.inj_add, F.of_Z_add; reflexivity. Qed.
+
+    Lemma of_nat_mul x y :
+      F.of_nat m (x * y) = (F.of_nat m x * F.of_nat m y)%F.
+    Proof. unfold F.of_nat; rewrite Nat2Z.inj_mul, F.of_Z_mul; reflexivity. Qed.
   End FandNat.
 
   Section RingTacticGadgets.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 2971bfef8..f8581c4c9 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -21,6 +21,7 @@ Module Import Notations.
   Infix "^" := pow.
   Infix "mod" := modulo (at level 40, no associativity).
   Infix "++" := Word.combine.
+  Notation setbit := setbit.
 End Notations.
 
 Generalizable All Variables.
@@ -73,7 +74,7 @@ Section EdDSA.
   Program Definition curveKey (sk:secretkey) : nat :=
     let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret scalar *)
     let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *)
-             x + 2^n. (* and the high bit is always set *)
+             setbit x n. (* and the high bit is always set *)
 
   Local Infix "+" := Eadd.
   Local Infix "*" := EscalarMult.
diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v
index a472f4090..80310b833 100644
--- a/src/Util/LetIn.v
+++ b/src/Util/LetIn.v
@@ -14,9 +14,11 @@ Global Instance Proper_Let_In_nd_changevalue {A B} (RA:relation A) {RB:relation
   : Proper (RA ==> (RA ==> RB) ==> RB) (Let_In (P:=fun _=>B)).
 Proof. cbv; intuition. Qed.
 
-Lemma app_Let_In_nd {A B C} (f:B -> C) : forall (e:A) (C:A -> B),
-  f (Let_In e C) = Let_In e (fun v => f (C v)).
-Proof. cbv; intuition. Qed.
+Definition app_Let_In_nd {A B T} (f:B->T) (e:A) (C:A->B)
+  : f (Let_In e C) = Let_In e (fun v => f (C v)) := eq_refl.
+
+Definition Let_app_In_nd {A B T} (f:A->B) (e:A) (C:B->T)
+  : Let_In (f e) C = Let_In e (fun v => C (f v)) := eq_refl.
 
 Class _call_let_in_to_Let_In {T} (e:T) := _let_in_to_Let_In_return : T.
 (* : forall T, gallina T -> gallina T, structurally recursive in the argument *)
diff --git a/src/Util/Relations.v b/src/Util/Relations.v
index aa280db26..4612fa8a8 100644
--- a/src/Util/Relations.v
+++ b/src/Util/Relations.v
@@ -27,3 +27,8 @@ Proof.
   logic; try match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end.
   repeat (assumption||reflexivity||econstructor); assumption. (* WHY the last [assumption]?*)
 Qed.
+
+Lemma iff_R_R_same_r {T R} {Req:@Equivalence T R} x y ref : R x y -> (R x ref <-> R y ref).
+Proof.
+  intro Hx; rewrite Hx; clear Hx. reflexivity.
+Qed.
\ No newline at end of file