val qinv_x8_x128 (x6 x_11: S.qelem) : S.qelem
let qinv_x8_x128 (x6 x_11: S.qelem) : S.qelem =
  let x8 = S.qmul (qsquare_times x6 2) x_11 in
  let x16 = S.qmul (qsquare_times x8 8) x8 in
  let x32 = S.qmul (qsquare_times x16 16) x16 in
  let x96 = S.qmul (qsquare_times x32 64) x32 in
  let x128 = S.qmul (qsquare_times x96 32) x32 in
  x128
val qinv_x8_x128 (x6 x_11: S.qelem) : S.qelem
let qinv_x8_x128 (x6 x_11: S.qelem) : S.qelem =
let x8 = S.qmul (qsquare_times x6 2) x_11 in
let x16 = S.qmul (qsquare_times x8 8) x8 in
let x32 = S.qmul (qsquare_times x16 16) x16 in
let x96 = S.qmul (qsquare_times x32 64) x32 in
let x128 = S.qmul (qsquare_times x96 32) x32 in
x128
Hacl.Spec.P256.Qinv.fst.checked
Spec.P256.fst.checked Spec.Exponentiation.fsti.checked prims.fst.checked Lib.NatMod.fsti.checked Lib.Exponentiation.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.P256.Qinv.fst
Spec.P256.PointOps.qelem Spec.P256.PointOps.qmul Hacl.Spec.P256.Qinv.qsquare_times
module Hacl.Spec.P256.Qinv

open FStar.Mul

module SE = Spec.Exponentiation
module LE = Lib.Exponentiation
module M = Lib.NatMod
module S = Spec.P256

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

let nat_mod_comm_monoid = M.mk_nat_mod_comm_monoid S.order

let mk_to_nat_mod_comm_monoid : SE.to_comm_monoid S.qelem = {
  SE.a_spec = S.qelem;
  SE.comm_monoid = nat_mod_comm_monoid;
  SE.refl = (fun (x:S.qelem) -> x);
}

val one_mod : SE.one_st S.qelem mk_to_nat_mod_comm_monoid
let one_mod _ = 1

val mul_mod : SE.mul_st S.qelem mk_to_nat_mod_comm_monoid
let mul_mod x y = S.qmul x y

val sqr_mod : SE.sqr_st S.qelem mk_to_nat_mod_comm_monoid
let sqr_mod x = S.qmul x x

let mk_nat_mod_concrete_ops : SE.concrete_ops S.qelem = {
  SE.to = mk_to_nat_mod_comm_monoid;
  SE.one = one_mod;
  SE.mul = mul_mod;
  SE.sqr = sqr_mod;
}

let qsquare_times (a:S.qelem) (b:nat) : S.qelem =
  SE.exp_pow2 mk_nat_mod_concrete_ops a b

val qsquare_times_lemma: a:S.qelem -> b:nat ->
  Lemma (qsquare_times a b == M.pow a (pow2 b) % S.order)
let qsquare_times_lemma a b =
  SE.exp_pow2_lemma mk_nat_mod_concrete_ops a b;
  LE.exp_pow2_lemma nat_mod_comm_monoid a b;
  assert (qsquare_times a b == LE.pow nat_mod_comm_monoid a (pow2 b));
  M.lemma_pow_nat_mod_is_pow #S.order a (pow2 b)
val qinv_x8_x128 (x6 x_11: S.qelem) : S.qelem
x6: Spec.P256.PointOps.qelem -> x_11: Spec.P256.PointOps.qelem -> Spec.P256.PointOps.qelem