diff options
Diffstat (limited to 'src/Spec/MxDH.v')
| -rw-r--r-- | src/Spec/MxDH.v | 9 |
1 files changed, 9 insertions, 0 deletions
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 |