first pass of scalarmult

1 files changed, 27 insertions, 11 deletions

diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
index 7f2f3f8f3..44e251b3b 100644
--- a/src/Experiments/EdDSARefinement.v
+++ b/src/Experiments/EdDSARefinement.v
@@ -1,10 +1,11 @@
 Require Import Crypto.Spec.EdDSA Bedrock.Word.
 Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Algebra. Import Group.
 Require Import Util.Decidable Util.Option Util.Tactics.
 
 Module Import NotationsFor8485.
   Import NPeano Nat.
-  Notation modulo := modulo.
+  Infix "mod" := modulo (at level 40).
 End NotationsFor8485.
 
 Section EdDSA.
@@ -33,14 +34,16 @@ Section EdDSA.
   Proof.
     intros; split;
       intro Heq; rewrite Heq; clear Heq.
-  Admitted.
+    { rewrite <-associative, right_inverse, right_identity; reflexivity. }
+    { rewrite <-associative, left_inverse, right_identity; reflexivity. }
+  Qed.
 
   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 - modulo (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ pk ++ message))) l * A))
+         (Eenc (S * B - (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ pk ++ message))) mod l * A))
     ) false (decE pk)
     ) false (decS (split2 b b sig))
   .
@@ -80,17 +83,30 @@ Section EdDSA.
     }
   Qed.
 
-  Lemma scalarMult_mod_order : forall l x B, l * B == Ezero -> (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" := 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.
+    rewrite (@mul_mod_order E Eeq Eadd Ezero Eopp _ EscalarMult _).
+    rewrite (@mul_add_l E Eeq Eadd Ezero Eopp _ EscalarMult).
+    eapply cancel_left.
+    rewrite (@mul_mod_order E Eeq Eadd Ezero Eopp _ EscalarMult _).
+    symmetry.
+    rewrite NPeano.Nat.mul_comm.
+    eapply (@mul_assoc E Eeq Eadd Ezero Eopp _ EscalarMult _ _ (wordToNat _) (curveKey sk) B).
+
+    admit.
+    admit.
+    admit.
+
+    admit.
+    
+    admit.
+    admit.
+    admit.
+    admit.
+    admit.
+
+    admit.
   Admitted.
 End EdDSA.