val g25519:g25519_t
let g25519: g25519_t =
  Lib.Buffer.createL_global Spec.Curve25519.basepoint_list
val g25519:g25519_t
let g25519:g25519_t =
Lib.Buffer.createL_global Spec.Curve25519.basepoint_list
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
Lib.Buffer.createL_global Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB Spec.Curve25519.basepoint_list Lib.Buffer.glbuffer Lib.IntTypes.size FStar.Pervasives.normalize_term Lib.IntTypes.size_nat FStar.List.Tot.Base.length
module Hacl.Curve25519_64_Slow

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

// The Vale core.
module C = Hacl.Impl.Curve25519.Field64.Hacl
val g25519:g25519_t
Hacl.Impl.Curve25519.Generic.g25519_t