val point_post_sub_t:#s:field_spec -> h:mem -> f:felem s -> Type0
let point_post_sub_t #s h f =
  match s with
  | M51 -> F51.felem_fits h f (9, 10, 9, 9, 9)
  | M64 -> True
val point_post_sub_t:#s:field_spec -> h:mem -> f:felem s -> Type0
let point_post_sub_t #s h f =
match s with
| M51 -> F51.felem_fits h f (9, 10, 9, 9, 9)
| M64 -> True
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.Fields.Core.felem Hacl.Impl.Curve25519.Field51.felem_fits FStar.Pervasives.Native.Mktuple5 Prims.nat Prims.l_True
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)

let fget_x (#s:field_spec) (h:mem) (p:point s) = feval h (gsub p 0ul (nlimb s))
let fget_z (#s:field_spec) (h:mem) (p:point s) = feval h (gsub p (nlimb s) (nlimb s))
let fget_xz (#s:field_spec) (h:mem) (p:point s) = fget_x h p, fget_z h p

val point_post_sub_t:#s:field_spec -> h:mem -> f:felem s -> Type0
val point_post_sub_t:#s:field_spec -> h:mem -> f:felem s -> Type0
h: FStar.Monotonic.HyperStack.mem -> f: Hacl.Impl.Curve25519.Fields.Core.felem s -> Type0