From b3d0b26ee3f97b1afade0880540d6d87e0cef03f Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Mon, 27 Jun 2016 18:22:37 -0400
Subject: eddsa refinement setup

---
 src/Experiments/EdDSARefinement.v | 38 +++++++++++++++++++++++++++++++++++++-
 1 file changed, 37 insertions(+), 1 deletion(-)

(limited to 'src/Experiments')

diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
index cf9083061..c8de64895 100644
--- a/src/Experiments/EdDSARefinement.v
+++ b/src/Experiments/EdDSARefinement.v
@@ -16,6 +16,7 @@ Section EdDSA.
   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).
+  Local Arguments H {_} _.
 
   Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}.
   Context {Proper_Eopp : Proper (Eeq==>Eeq) Eopp}.
@@ -43,7 +44,7 @@ Section EdDSA.
     option_rect (fun _ => bool) (fun A : E =>
        weqb
          (split1 b b sig)
-         (Eenc (S * B - (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ pk ++ message))) mod l * A))
+         (Eenc (S * B - (wordToNat (H (split1 b b sig ++ pk ++ message))) mod l * A))
     ) false (decE pk)
     ) false (decS (split2 b b sig))
   .
@@ -93,4 +94,39 @@ Section EdDSA.
                 | rewrite scalarmult_assoc, mult_comm, <-scalarmult_assoc,
                              EdDSA_l_order_B, scalarmult_zero_r; reflexivity ].
   Qed.
+
+  Section ChangeRep.
+    Context {A Aeq Aadd Aid Aopp} {Agroup:@group A Aeq Aadd Aid Aopp}.
+    Context {EtoA} {Ahomom:@is_homomorphism E Eeq Eadd A Aeq Aadd EtoA}.
+
+    Context {Aenc : A -> word b} {Proper_Aenc:Proper (Aeq==>Logic.eq) Aenc}
+            {Aenc_correct : forall P:E, Eenc P = Aenc (EtoA P)}.
+
+    Context {S Seq} `{@Equivalence S Seq} {natToS:nat->S}
+            {SAmul:S->A->A} {Proper_SAmul: Proper (Seq==>Aeq==>Aeq) SAmul}
+            {SAmul_correct: forall n P, Aeq (EtoA (n*P)) (SAmul (natToS n) (EtoA P))}
+            {SdecS} {SdecS_correct : forall w, (decS w) = (SdecS w)} (* FIXME: equivalence relation *)
+            {natToS_modl : forall n,  Seq (natToS (n mod l)) (natToS n)}.
+
+    Create HintDb hintsEtoA discriminated.
+    Hint Rewrite 
+      Aenc_correct
+      homomorphism
+      homomorphism_id
+      homomorphism_inv
+      SAmul_correct
+      SdecS_correct
+      natToS_modl
+      : hintsEtoA.
+
+    Definition verify_using_representation
+               {mlen} (message:word mlen) (pk:word b) (sig:word (b+b))
+               : { answer | answer = verify message pk sig }.
+    Proof.
+      eexists.
+      cbv [verify].
+      (rewrite_strat topdown hints hintsEtoA).
+      reflexivity.
+    Defined.
+  End ChangeRep.
 End EdDSA.
-- 
cgit v1.2.3