let point = lbuffer uint64 20ul
let point =
lbuffer uint64 20ul
Hacl.Impl.Ed25519.Field51.fst.checked
Spec.Ed25519.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Spec.Curve25519.Field51.fst.checked Hacl.Impl.Curve25519.Field51.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Ed25519.Field51.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint64 FStar.UInt32.__uint_to_t
module Hacl.Impl.Ed25519.Field51

open FStar.HyperStack

open Lib.IntTypes
open Lib.Buffer

open FStar.Mul

module LSeq = Lib.Sequence
module P = Hacl.Impl.Curve25519.Field51
module S = Spec.Curve25519
val point : Type0
Type0