val point_eval:h:mem -> p:point -> GTot Spec.Ed25519.ext_point
let point_eval h p =
  let x = gsub p 0ul 5ul in
  let y = gsub p 5ul 5ul in
  let z = gsub p 10ul 5ul in
  let t = gsub p 15ul 5ul in
  (fevalh h x, fevalh h y, fevalh h z, fevalh h t)
val point_eval:h:mem -> p:point -> GTot Spec.Ed25519.ext_point
let point_eval h p =
let x = gsub p 0ul 5ul in
let y = gsub p 5ul 5ul in
let z = gsub p 10ul 5ul in
let t = gsub p 15ul 5ul in
(fevalh h x, fevalh h y, fevalh h z, fevalh h t)
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
FStar.Monotonic.HyperStack.mem Hacl.Impl.Ed25519.Field51.point FStar.Pervasives.Native.Mktuple4 Spec.Curve25519.elem Hacl.Impl.Ed25519.Field51.fevalh Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.gsub Lib.IntTypes.uint64 FStar.UInt32.__uint_to_t Spec.Ed25519.PointOps.ext_point
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

let felem = lbuffer uint64 5ul
let point = lbuffer uint64 20ul

let as_nat (h:mem) (f:felem) : GTot nat = P.as_nat h f

let fevalh (h:mem) (f:felem) : GTot S.elem = P.fevalh h f

noextract
val point_eval:h:mem -> p:point -> GTot Spec.Ed25519.ext_point
h: FStar.Monotonic.HyperStack.mem -> p: Hacl.Impl.Ed25519.Field51.point
  -> Prims.GTot Spec.Ed25519.PointOps.ext_point