val fsquare_times_lemma: a:S.felem -> b:nat ->
  Lemma (fsquare_times a b == M.pow a (pow2 b) % S.prime)
let fsquare_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 (fsquare_times a b == LE.pow nat_mod_comm_monoid a (pow2 b));
  M.lemma_pow_nat_mod_is_pow #S.prime a (pow2 b)
val fsquare_times_lemma: a:S.felem -> b:nat ->
  Lemma (fsquare_times a b == M.pow a (pow2 b) % S.prime)
let fsquare_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 (fsquare_times a b == LE.pow nat_mod_comm_monoid a (pow2 b));
M.lemma_pow_nat_mod_is_pow #S.prime a (pow2 b)
Hacl.Spec.P256.Finv.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.Finv.fst
Spec.P256.PointOps.felem Prims.nat Lib.NatMod.lemma_pow_nat_mod_is_pow Spec.P256.PointOps.prime Prims.pow2 Prims.unit Prims._assert Prims.eq2 Prims.l_or Prims.b2t Prims.op_LessThan Hacl.Spec.P256.Finv.fsquare_times Lib.Exponentiation.Definition.pow Lib.NatMod.nat_mod Hacl.Spec.P256.Finv.nat_mod_comm_monoid Lib.Exponentiation.exp_pow2_lemma Spec.Exponentiation.exp_pow2_lemma Hacl.Spec.P256.Finv.mk_nat_mod_concrete_ops
module Hacl.Spec.P256.Finv

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.prime

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

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

val mul_mod : SE.mul_st S.felem mk_to_nat_mod_comm_monoid
let mul_mod x y = S.fmul x y

val sqr_mod : SE.sqr_st S.felem mk_to_nat_mod_comm_monoid
let sqr_mod x = S.fmul x x

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

let fsquare_times (a:S.felem) (b:nat) : S.felem =
  SE.exp_pow2 mk_nat_mod_concrete_ops a b

val fsquare_times_lemma: a:S.felem -> b:nat ->
  Lemma (fsquare_times a b == M.pow a (pow2 b) % S.prime)
val fsquare_times_lemma: a:S.felem -> b:nat ->
  Lemma (fsquare_times a b == M.pow a (pow2 b) % S.prime)
a: Spec.P256.PointOps.felem -> b: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      Hacl.Spec.P256.Finv.fsquare_times a b ==
      Lib.NatMod.pow a (Prims.pow2 b) % Spec.P256.PointOps.prime)