let fget_z (#s:field_spec) (h:mem) (p:point s) = feval h (gsub p (nlimb s) (nlimb s))
let fget_z (#s: field_spec) (h: mem) (p: point s) =
feval h (gsub p (nlimb s) (nlimb s))
Hacl.Impl.Curve25519.AddAndDouble.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Curve25519.AddAndDouble.fst.checked Hacl.Impl.Curve25519.Fields.fst.checked Hacl.Impl.Curve25519.Field64.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.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Curve25519.AddAndDouble.fst
Hacl.Impl.Curve25519.Fields.Core.field_spec FStar.Monotonic.HyperStack.mem Hacl.Impl.Curve25519.AddAndDouble.point Hacl.Impl.Curve25519.Fields.Core.feval Lib.Buffer.gsub Lib.Buffer.MUT Hacl.Impl.Curve25519.Fields.Core.limb Lib.IntTypes.op_Plus_Bang Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Impl.Curve25519.Fields.Core.nlimb Spec.Curve25519.elem
module Hacl.Impl.Curve25519.AddAndDouble

open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Hacl.Impl.Curve25519.Fields

module ST = FStar.HyperStack.ST

module F51 = Hacl.Impl.Curve25519.Field51
module F64 = Hacl.Impl.Curve25519.Field64

module P = Spec.Curve25519
module S = Hacl.Spec.Curve25519.AddAndDouble

#reset-options "--z3rlimit 300 --fuel 0 --ifuel 1 --using_facts_from '* -FStar.Seq' --record_options"

inline_for_extraction noextract
let point (s:field_spec) = lbuffer (limb s) (nlimb s +! nlimb s)

(* NEEDED ONLY FOR WRAPPERS *)
inline_for_extraction noextract
let point51 = lbuffer uint64 10ul
inline_for_extraction noextract
let point64 = lbuffer uint64 8ul
(* NEEDED ONLY FOR WRAPPERS *)

let get_x #s (p:point s) = gsub p 0ul (nlimb s)
let get_z #s (p:point s) = gsub p (nlimb s) (nlimb s)
val fget_z : h: FStar.Monotonic.HyperStack.mem -> p: Hacl.Impl.Curve25519.AddAndDouble.point s
  -> Prims.GTot Spec.Curve25519.elem
h: FStar.Monotonic.HyperStack.mem -> p: Hacl.Impl.Curve25519.AddAndDouble.point s
  -> Prims.GTot Spec.Curve25519.elem