let montgomery_ladder =
  generic_montgomery_ladder_higher #M51 True point_double C.cswap2 point_add_and_double
let montgomery_ladder =
generic_montgomery_ladder_higher #M51 True point_double C.cswap2 point_add_and_double
Hacl.Curve25519_51.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Buffer.fsti.checked Hacl.Meta.Curve25519.fst.checked Hacl.Impl.Curve25519.Field51.fst.checked FStar.Pervasives.fsti.checked
Hacl.Curve25519_51.fst
Hacl.Meta.Curve25519.generic_montgomery_ladder_higher Hacl.Impl.Curve25519.Fields.Core.M51 Prims.l_True Hacl.Curve25519_51.point_double Hacl.Impl.Curve25519.Field51.cswap2 Hacl.Curve25519_51.point_add_and_double
module Hacl.Curve25519_51

friend Hacl.Meta.Curve25519
open Hacl.Meta.Curve25519

// The Hacl core.
module C = Hacl.Impl.Curve25519.Field51

let g25519: g25519_t =
  Lib.Buffer.createL_global Spec.Curve25519.basepoint_list

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 100"
let point_add_and_double =
  addanddouble_point_add_and_double_higher #M51 True C.fmul C.fsqr2 C.fmul1 C.fmul2 C.fsub C.fadd
let point_double =
  addanddouble_point_double_higher #M51 True C.fmul2 C.fmul1 C.fsqr2 C.fsub C.fadd
val montgomery_ladder : Hacl.Meta.Curve25519.generic_montgomery_ladder_higher_t Prims.l_True
Hacl.Meta.Curve25519.generic_montgomery_ladder_higher_t Prims.l_True