let qas_nat4 (f:qelem4) =
  let (f0, f1, f2, f3) = f in
  v f0 + v f1 * pow2 64 + v f2 * pow2 128 + v f3 * pow2 192
let qas_nat4 (f: qelem4) =
let f0, f1, f2, f3 = f in
v f0 + v f1 * pow2 64 + v f2 * pow2 128 + v f3 * pow2 192
Hacl.K256.Scalar.fsti.checked
Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.GLV.fst.checked Hacl.Bignum.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.K256.Scalar.fsti
Hacl.K256.Scalar.qelem4 Lib.IntTypes.uint64 Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.Mul.op_Star Prims.pow2 Prims.int
module Hacl.K256.Scalar

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

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

module S = Spec.K256
module SG = Hacl.Spec.K256.GLV

module BD = Hacl.Bignum.Definitions

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


inline_for_extraction noextract
let qnlimb = 4ul

inline_for_extraction noextract
let qelem = lbuffer uint64 qnlimb

noextract
let qas_nat (h:mem) (e:qelem) : GTot nat = BD.bn_v #U64 #qnlimb h e

noextract
let qeval (h:mem) (e:qelem) : GTot S.qelem = qas_nat h e % S.q

noextract
let qe_lt_q (h:mem) (e:qelem) = qas_nat h e < S.q


inline_for_extraction noextract
let qelem4 = uint64 & uint64 & uint64 & uint64
val qas_nat4 : f: Hacl.K256.Scalar.qelem4 -> Prims.int
f: Hacl.K256.Scalar.qelem4 -> Prims.int