let get_z #s (p:point s) = gsub p (nlimb s) (nlimb s)
let get_z #s (p: point s) =
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 Hacl.Impl.Curve25519.AddAndDouble.point 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 Lib.Buffer.lbuffer_t
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 *)
val get_z : p: Hacl.Impl.Curve25519.AddAndDouble.point s
  -> Prims.GTot
    (Lib.Buffer.lbuffer_t Lib.Buffer.MUT
        (Hacl.Impl.Curve25519.Fields.Core.limb s)
        (Hacl.Impl.Curve25519.Fields.Core.nlimb s))
p: Hacl.Impl.Curve25519.AddAndDouble.point s
  -> Prims.GTot
    (Lib.Buffer.lbuffer_t Lib.Buffer.MUT
        (Hacl.Impl.Curve25519.Fields.Core.limb s)
        (Hacl.Impl.Curve25519.Fields.Core.nlimb s))