val feval4 (f: felem4) : GTot P.elem
let feval4 (f:felem4) : GTot P.elem = as_nat4 f % P.prime
val feval4 (f: felem4) : GTot P.elem
let feval4 (f: felem4) : GTot P.elem =
as_nat4 f % P.prime
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 Prims.op_Modulus Hacl.Spec.Curve25519.Field64.Definition.as_nat4 Spec.Curve25519.prime Spec.Curve25519.elem
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
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 feval4 (f: felem4) : GTot P.elem
f: Hacl.Spec.Curve25519.Field64.Definition.felem4 -> Prims.GTot Spec.Curve25519.elem