let point_double =
  addanddouble_point_double_higher #M64 True C.fmul2_ C.fmul1_ C.fsqr2_ C.fsub_ C.fadd_
let point_double =
addanddouble_point_double_higher #M64 True C.fmul2_ C.fmul1_ C.fsqr2_ C.fsub_ C.fadd_
Hacl.Curve25519_64_Slow.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Buffer.fsti.checked Hacl.Meta.Curve25519.fst.checked Hacl.Impl.Curve25519.Field64.Hacl.fsti.checked FStar.Pervasives.fsti.checked
Hacl.Curve25519_64_Slow.fst
Hacl.Meta.Curve25519.addanddouble_point_double_higher Hacl.Impl.Curve25519.Fields.Core.M64 Prims.l_True Hacl.Impl.Curve25519.Field64.Hacl.fmul2_ Hacl.Impl.Curve25519.Field64.Hacl.fmul1_ Hacl.Impl.Curve25519.Field64.Hacl.fsqr2_ Hacl.Impl.Curve25519.Field64.Hacl.fsub_ Hacl.Impl.Curve25519.Field64.Hacl.fadd_
module Hacl.Curve25519_64_Slow

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

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

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 True C.fmul_ C.fsqr2_ C.fmul1_ C.fmul2_ C.fsub_ C.fadd_
val point_double : Hacl.Meta.Curve25519.addanddouble_point_double_higher_t Prims.l_True
Hacl.Meta.Curve25519.addanddouble_point_double_higher_t Prims.l_True