val as_nat (h: mem) (f: felem) : GTot nat
let as_nat (h:mem) (f:felem) : GTot nat = P.as_nat h f
val as_nat (h: mem) (f: felem) : GTot nat
let as_nat (h: mem) (f: felem) : GTot nat =
P.as_nat h f
Hacl.Impl.Ed25519.Field51.fst.checked
Spec.Ed25519.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Spec.Curve25519.Field51.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.fst.checked
Hacl.Impl.Ed25519.Field51.fst
FStar.Monotonic.HyperStack.mem Hacl.Impl.Ed25519.Field51.felem Hacl.Impl.Curve25519.Field51.as_nat Prims.nat
module Hacl.Impl.Ed25519.Field51

open FStar.HyperStack

open Lib.IntTypes
open Lib.Buffer

open FStar.Mul

module LSeq = Lib.Sequence
module P = Hacl.Impl.Curve25519.Field51
module S = Spec.Curve25519

let felem = lbuffer uint64 5ul
let point = lbuffer uint64 20ul
val as_nat (h: mem) (f: felem) : GTot nat
h: FStar.Monotonic.HyperStack.mem -> f: Hacl.Impl.Ed25519.Field51.felem -> Prims.GTot Prims.nat