val qsquare_times (out a:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ live h a /\ disjoint out a /\
    as_nat h a < S.order)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    as_nat h1 out < S.order /\
    qmont_as_nat h1 out == SI.qsquare_times (qmont_as_nat h0 a) (v b))
let qsquare_times out a b =
  let h0 = ST.get () in
  SE.exp_pow2_lemma SI.mk_nat_mod_concrete_ops (qmont_as_nat h0 a) (v b);
  BE.lexp_pow2 4ul 0ul mk_p256_order_concrete_ops (null uint64) a b out
val qsquare_times (out a:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ live h a /\ disjoint out a /\
    as_nat h a < S.order)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    as_nat h1 out < S.order /\
    qmont_as_nat h1 out == SI.qsquare_times (qmont_as_nat h0 a) (v b))
let qsquare_times out a b =
let h0 = ST.get () in
SE.exp_pow2_lemma SI.mk_nat_mod_concrete_ops (qmont_as_nat h0 a) (v b);
BE.lexp_pow2 4ul 0ul mk_p256_order_concrete_ops (null uint64) a b out
Hacl.Impl.P256.Qinv.fst.checked
Spec.P256.fst.checked Spec.Exponentiation.fsti.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.P256.Qinv.fst.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Impl.P256.Scalar.fsti.checked Hacl.Impl.P256.Bignum.fsti.checked Hacl.Impl.Exponentiation.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.P256.Qinv.fst
Hacl.Impl.P256.Bignum.felem Lib.IntTypes.size_t Hacl.Impl.Exponentiation.lexp_pow2 Lib.IntTypes.U64 FStar.UInt32.__uint_to_t Hacl.Impl.P256.Qinv.mk_p256_order_concrete_ops Lib.Buffer.null Lib.Buffer.MUT Lib.IntTypes.uint64 Prims.unit Spec.Exponentiation.exp_pow2_lemma Spec.P256.PointOps.qelem Hacl.Spec.P256.Qinv.mk_nat_mod_concrete_ops Hacl.Impl.P256.Scalar.qmont_as_nat Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module Hacl.Impl.P256.Qinv

open FStar.Mul
open FStar.HyperStack.All
open FStar.HyperStack
module ST = FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.P256.Bignum
open Hacl.Impl.P256.Scalar

module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation
module BD = Hacl.Spec.Bignum.Definitions
module LSeq = Lib.Sequence

module S = Spec.P256
module SI = Hacl.Spec.P256.Qinv
module SM = Hacl.Spec.P256.Montgomery

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

unfold
let linv_ctx (a:LSeq.lseq uint64 0) : Type0 = True

unfold
let linv (a:LSeq.lseq uint64 4) : Type0 =
  BD.bn_v a < S.order

unfold
let refl (a:LSeq.lseq uint64 4{linv a}) : GTot S.qelem =
  SM.from_qmont (BD.bn_v a)


inline_for_extraction noextract
let mk_to_p256_order_comm_monoid : BE.to_comm_monoid U64 4ul 0ul = {
  BE.a_spec = S.qelem;
  BE.comm_monoid = SI.nat_mod_comm_monoid;
  BE.linv_ctx = linv_ctx;
  BE.linv = linv;
  BE.refl = refl;
}

inline_for_extraction noextract
val one_mod : BE.lone_st U64 4ul 0ul mk_to_p256_order_comm_monoid
let one_mod ctx one = make_qone one


inline_for_extraction noextract
val mul_mod : BE.lmul_st U64 4ul 0ul mk_to_p256_order_comm_monoid
let mul_mod ctx x y xy = qmul xy x y


inline_for_extraction noextract
val sqr_mod : BE.lsqr_st U64 4ul 0ul mk_to_p256_order_comm_monoid
let sqr_mod ctx x xx = qsqr xx x


inline_for_extraction noextract
let mk_p256_order_concrete_ops : BE.concrete_ops U64 4ul 0ul = {
  BE.to = mk_to_p256_order_comm_monoid;
  BE.lone = one_mod;
  BE.lmul = mul_mod;
  BE.lsqr = sqr_mod;
}


inline_for_extraction noextract
val qsquare_times_in_place (out:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ as_nat h out < S.order)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    as_nat h1 out < S.order /\
    qmont_as_nat h1 out == SI.qsquare_times (qmont_as_nat h0 out) (v b))

let qsquare_times_in_place out b =
  let h0 = ST.get () in
  SE.exp_pow2_lemma SI.mk_nat_mod_concrete_ops (qmont_as_nat h0 out) (v b);
  BE.lexp_pow2_in_place 4ul 0ul mk_p256_order_concrete_ops (null uint64) out b


inline_for_extraction noextract
val qsquare_times (out a:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ live h a /\ disjoint out a /\
    as_nat h a < S.order)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    as_nat h1 out < S.order /\
    qmont_as_nat h1 out == SI.qsquare_times (qmont_as_nat h0 a) (v b))
val qsquare_times (out a:felem) (b:size_t) : Stack unit
  (requires fun h ->
    live h out /\ live h a /\ disjoint out a /\
    as_nat h a < S.order)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    as_nat h1 out < S.order /\
    qmont_as_nat h1 out == SI.qsquare_times (qmont_as_nat h0 a) (v b))
out: Hacl.Impl.P256.Bignum.felem -> a: Hacl.Impl.P256.Bignum.felem -> b: Lib.IntTypes.size_t
  -> FStar.HyperStack.ST.Stack Prims.unit