diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-07 21:32:36 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-07 21:32:36 -0500 |
commit | 46297225195b16a725348d8693a1a81197a8c2de (patch) | |
tree | e1d70ff01cb4bfcb9e214f753040dec246d877d4 /src | |
parent | 4d3d21d604243bc63774f4931f2313e20cdaf515 (diff) |
Add ladderstep_other_assoc
Diffstat (limited to 'src')
-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 |