From 46297225195b16a725348d8693a1a81197a8c2de Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 7 Jan 2017 21:32:36 -0500 Subject: Add ladderstep_other_assoc --- src/Spec/MxDH.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/Spec') diff --git a/src/Spec/MxDH.v b/src/Spec/MxDH.v index 890605b70..27f5f9a7f 100644 --- a/src/Spec/MxDH.v +++ b/src/Spec/MxDH.v @@ -50,6 +50,15 @@ Module MxDH. (* from RFC7748 *) pair4 X4 Z4 X5 Z5. End generic. + (** TODO: Make this the only ladderstep? *) + Definition ladderstep_other_assoc (X1:F) (P1 P2:F*F) : F*F*F*F := + Eval cbv beta delta [ladderstep_gen] in + @ladderstep_gen + (F*F*F*F) + (fun X3 Y3 Z3 T3 => (X3, Y3, Z3, T3)) + (fun x f => let y := x in f y) + X1 P1 P2. + Definition ladderstep (X1:F) (P1 P2:F*F) : (F*F)*(F*F) := Eval cbv beta delta [ladderstep_gen] in @ladderstep_gen -- cgit v1.2.3