val as_nat (h: mem) (e: felem) : GTot nat
let as_nat (h:mem) (e:felem) : GTot nat =
  let s = as_seq h e in
  let s0 = s.[0] in
  let s1 = s.[1] in
  let s2 = s.[2] in
  let s3 = s.[3] in
  S.as_nat4 (s0, s1, s2, s3)
val as_nat (h: mem) (e: felem) : GTot nat
let as_nat (h: mem) (e: felem) : GTot nat =
let s = as_seq h e in
let s0 = s.[ 0 ] in
let s1 = s.[ 1 ] in
let s2 = s.[ 2 ] in
let s3 = s.[ 3 ] in
S.as_nat4 (s0, s1, s2, s3)
Hacl.Impl.Curve25519.Field64.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.Spec.Curve25519.Field64.Definition.fst.checked Hacl.Spec.Curve25519.Field64.Core.fst.checked Hacl.Spec.Curve25519.Field64.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Impl.Curve25519.Lemmas.fst.checked Hacl.Impl.Curve25519.Fields.Core.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.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 FStar.Ghost.fsti.checked
Hacl.Impl.Curve25519.Field64.fst
FStar.Monotonic.HyperStack.mem Hacl.Impl.Curve25519.Field64.felem Hacl.Spec.Curve25519.Field64.Definition.as_nat4 FStar.Pervasives.Native.Mktuple4 Lib.IntTypes.uint64 Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.eq2 FStar.Seq.Base.index Lib.Sequence.to_seq Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Sequence.op_String_Access FStar.UInt32.__uint_to_t Lib.Sequence.lseq Lib.Buffer.as_seq Lib.Buffer.MUT Prims.nat
module Hacl.Impl.Curve25519.Field64

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

open Lib.Sequence
open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.Curve25519.Fields.Core

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

module P = Spec.Curve25519
module S = Hacl.Spec.Curve25519.Field64.Definition
module SC = Hacl.Spec.Curve25519.Field64
module SD = Hacl.Spec.Bignum.Definitions

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

let u256 = lbuffer uint64 4ul
let u512 = lbuffer uint64 8ul
let u1024 = lbuffer uint64 16ul

let felem = lbuffer uint64 4ul
let felem2 = lbuffer uint64 8ul
val as_nat (h: mem) (e: felem) : GTot nat
h: FStar.Monotonic.HyperStack.mem -> e: Hacl.Impl.Curve25519.Field64.felem -> Prims.GTot Prims.nat