val create_aff_point: unit -> StackInline aff_point
  (requires fun h -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (LSeq.create 10 (u64 0)))
let create_aff_point () =
  create 10ul (u64 0)
val create_aff_point: unit -> StackInline aff_point
  (requires fun h -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (LSeq.create 10 (u64 0)))
let create_aff_point () =
create 10ul (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 FStar.UInt32.__uint_to_t Lib.IntTypes.u64 Lib.Buffer.lbuffer Hacl.Impl.K256.Point.aff_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
val create_aff_point: unit -> StackInline aff_point
  (requires fun h -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (LSeq.create 10 (u64 0)))
_: Prims.unit -> FStar.HyperStack.ST.StackInline Hacl.Impl.K256.Point.aff_point