diff options
Diffstat (limited to 'src')
-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 := |