val as_nat4: f:felem4 -> GTot nat
let as_nat4 f =
  let (s0, s1, s2, s3) = f in
  v s0 + v s1 * pow2 64 + v s2 * pow2 64 * pow2 64 +
  v s3 * pow2 64 * pow2 64 * pow2 64
val as_nat4: f:felem4 -> GTot nat
let as_nat4 f =
let s0, s1, s2, s3 = f in
v s0 + v s1 * pow2 64 + (v s2 * pow2 64) * pow2 64 + ((v s3 * pow2 64) * pow2 64) * pow2 64
Hacl.Spec.Curve25519.Field64.Definition.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Impl.Curve25519.Lemmas.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.Curve25519.Field64.Definition.fst
Hacl.Spec.Curve25519.Field64.Definition.felem4 Lib.IntTypes.uint64 Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Mul.op_Star Prims.pow2 Prims.nat
module Hacl.Spec.Curve25519.Field64.Definition

open Lib.Sequence
open Lib.IntTypes

module P = Spec.Curve25519

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

let felem4 = (uint64 * uint64 * uint64 * uint64)

open FStar.Mul

noextract
val as_nat4: f:felem4 -> GTot nat
f: Hacl.Spec.Curve25519.Field64.Definition.felem4 -> Prims.GTot Prims.nat