val create_point: unit -> StackInline point
  (requires fun h -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (LSeq.create (3 * v 5ul) (u64 0)))
let create_point () =
  create (3ul *! 5ul) (u64 0)
val create_point: unit -> StackInline point
  (requires fun h -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (LSeq.create (3 * v 5ul) (u64 0)))
let create_point () =
create (3ul *! 5ul) (u64 0)
Hacl.Impl.K256.Point.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.Field52.Lemmas.fsti.checked Hacl.Spec.K256.Field52.fst.checked Hacl.K256.Field.fsti.checked Hacl.Impl.K256.Finv.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Impl.K256.Point.fst
Prims.unit Lib.Buffer.create Lib.IntTypes.uint64 Lib.IntTypes.op_Star_Bang Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.UInt32.__uint_to_t Lib.IntTypes.u64 Lib.Buffer.lbuffer Hacl.Impl.K256.Point.point
module Hacl.Impl.K256.Point

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence

module S = Spec.K256
module SL = Spec.K256.Lemmas
module BI = Hacl.Spec.K256.Field52
module BL = Hacl.Spec.K256.Field52.Lemmas

open Hacl.K256.Field
open Hacl.Impl.K256.Finv

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

///  Create a point

let create_aff_point () =
  create 10ul (u64 0)
val create_point: unit -> StackInline point
  (requires fun h -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (LSeq.create (3 * v 5ul) (u64 0)))
_: Prims.unit -> FStar.HyperStack.ST.StackInline Hacl.Impl.K256.Point.point