val create_felem:
    s:field_spec
  -> StackInline (felem s)
    (requires fun h -> True)
    (ensures  fun h0 f h1 ->
      stack_allocated f h0 h1 (LSeq.create (v (nlimb s)) (limb_zero s)) /\
      as_nat h1 f == 0)
let create_felem s =
  match s with
  | M51 -> (F51.create_felem ()) <: felem s
  | M64 -> (F64.create_felem ()) <: felem s
val create_felem:
    s:field_spec
  -> StackInline (felem s)
    (requires fun h -> True)
    (ensures  fun h0 f h1 ->
      stack_allocated f h0 h1 (LSeq.create (v (nlimb s)) (limb_zero s)) /\
      as_nat h1 f == 0)
let create_felem s =
match s with
| M51 -> (F51.create_felem ()) <: felem s
| M64 -> (F64.create_felem ()) <: felem s
Hacl.Impl.Curve25519.Fields.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Curve25519.Fields.Core.fsti.checked Hacl.Impl.Curve25519.Field64.fst.checked Hacl.Impl.Curve25519.Field51.fst.checked FStar.UInt32.fsti.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.Fields.fst
Hacl.Impl.Curve25519.Fields.Core.field_spec Hacl.Impl.Curve25519.Field51.create_felem Hacl.Impl.Curve25519.Field51.felem Hacl.Impl.Curve25519.Fields.Core.felem Hacl.Impl.Curve25519.Field64.create_felem Hacl.Impl.Curve25519.Field64.felem
module Hacl.Impl.Curve25519.Fields

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

open Lib.IntTypes
open Lib.Buffer

include Hacl.Impl.Curve25519.Fields.Core

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

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


#set-options "--z3rlimit 50 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1 --record_options"

inline_for_extraction noextract
val create_felem:
    s:field_spec
  -> StackInline (felem s)
    (requires fun h -> True)
    (ensures  fun h0 f h1 ->
      stack_allocated f h0 h1 (LSeq.create (v (nlimb s)) (limb_zero s)) /\
      as_nat h1 f == 0)
val create_felem:
    s:field_spec
  -> StackInline (felem s)
    (requires fun h -> True)
    (ensures  fun h0 f h1 ->
      stack_allocated f h0 h1 (LSeq.create (v (nlimb s)) (limb_zero s)) /\
      as_nat h1 f == 0)
s: Hacl.Impl.Curve25519.Fields.Core.field_spec
  -> FStar.HyperStack.ST.StackInline (Hacl.Impl.Curve25519.Fields.Core.felem s)