val scalarmult: scalarmult_st M64 p
let scalarmult = generic_scalarmult_higher #M64 C.p encode_point montgomery_ladder decode_point
val scalarmult: scalarmult_st M64 p
let scalarmult =
generic_scalarmult_higher #M64 C.p encode_point montgomery_ladder decode_point
Hacl.Curve25519_64.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Buffer.fsti.checked Hacl.Meta.Curve25519.fst.checked Hacl.Impl.Curve25519.Field64.Vale.fsti.checked FStar.Pervasives.fsti.checked
Hacl.Curve25519_64.fst
Hacl.Meta.Curve25519.generic_scalarmult_higher Hacl.Impl.Curve25519.Fields.Core.M64 Hacl.Impl.Curve25519.Field64.Vale.p Hacl.Curve25519_64.encode_point Hacl.Curve25519_64.montgomery_ladder Hacl.Impl.Curve25519.Generic.decode_point
module Hacl.Curve25519_64

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

// The Vale core.
module C = Hacl.Impl.Curve25519.Field64.Vale

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 #M64 C.p C.fmul C.fsqr2 C.fmul_scalar C.fmul2 C.fsub C.fadd
let point_double =
  addanddouble_point_double_higher #M64 C.p C.fmul2 C.fmul_scalar C.fsqr2 C.fsub C.fadd
let montgomery_ladder =
  generic_montgomery_ladder_higher #M64 C.p point_double C.cswap2 point_add_and_double
let fsquare_times = finv_fsquare_times_higher #M64 C.p C.fsqr
let finv = finv_finv_higher #M64 C.p C.fmul fsquare_times
// Note that here, for implementations of Curve64, we have a generic store_felem
// over an *implementation* of add1. (For Curve51, store_felem does not have
// that generic aspect.)
let store_felem = fields_store_felem_higher #M64 C.p C.add_scalar
val scalarmult: scalarmult_st M64 p
Hacl.Impl.Curve25519.Generic.scalarmult_st Hacl.Impl.Curve25519.Fields.Core.M64 Hacl.Curve25519_64.p