let qelem4 = uint64 & uint64 & uint64 & uint64
let qelem4 =
uint64 & uint64 & uint64 & uint64
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
FStar.Pervasives.Native.tuple4 Lib.IntTypes.uint64
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
val qelem4 : Type0
Type0