diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-12 16:45:04 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-12 16:45:27 -0400 |
| commit | bef674408e406a0bf537fff69d8890abaa3693f0 (patch) | |
| tree | 41edf14d058a4353ec4ff9b7040f92a95ee992fe /src/Spec | |
| parent | a88e4ec64cf96a23d4cf23ce3f62c57f7f3ca0ba (diff) | |
Add commented out proof of equivalence in MxDH
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/MxDH.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Spec/MxDH.v b/src/Spec/MxDH.v index d70521581..bee9c784d 100644 --- a/src/Spec/MxDH.v +++ b/src/Spec/MxDH.v @@ -1,5 +1,6 @@ Require Crypto.Algebra.Hierarchy. Require Import Crypto.Util.Notations. +(*Require Crypto.Curves.Montgomery.XZ.*) Module MxDH. (* from RFC7748 *) Section MontgomeryLadderKeyExchange. @@ -67,6 +68,13 @@ Module MxDH. (* from RFC7748 *) (fun x f => let y := x in f y) X1 P1 P2. + (*Import Curves.Montgomery.XZ. + Goal forall X1 P1 P2, Logic.eq (ladderstep X1 P1 P2) (@M.xzladderstep F Fadd Fsub Fmul a24 X1 P1 P2). + Proof. + intros ? [? ?] [? ?]. + reflexivity. + Qed.*) + Context {cswap:bool->F*F->F*F->(F*F)*(F*F)}. Fixpoint downto_iter (i:nat) : list nat := |