let qe_lt_q (h:mem) (e:qelem) = qas_nat h e < S.q
let qe_lt_q (h: mem) (e: qelem) =
qas_nat h e < S.q
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.Monotonic.HyperStack.mem Hacl.K256.Scalar.qelem Prims.op_LessThan Hacl.K256.Scalar.qas_nat Spec.K256.PointOps.q Prims.bool
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
val qe_lt_q : h: FStar.Monotonic.HyperStack.mem -> e: Hacl.K256.Scalar.qelem -> Prims.GTot Prims.bool
h: FStar.Monotonic.HyperStack.mem -> e: Hacl.K256.Scalar.qelem -> Prims.GTot Prims.bool