From bef674408e406a0bf537fff69d8890abaa3693f0 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 12 Apr 2017 16:45:04 -0400
Subject: Add commented out proof of equivalence in MxDH

---
 src/Spec/MxDH.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/Spec')

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 :=
-- 
cgit v1.2.3