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
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
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
Lib.Buffer.lbuffer Lib.IntTypes.uint_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.UInt32.__uint_to_t Hacl.Impl.P256.Scalar.qmul Prims.unit
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
Hacl.Impl.Exponentiation.Definitions.lmul_st Lib.IntTypes.U64
  4ul
  0ul
  Hacl.Impl.P256.Qinv.mk_to_p256_order_comm_monoid