val finv: f:S.felem -> S.felem
let finv f =
  let x2 = S.fmul (fsquare_times f 1) f in
  let x3 = S.fmul (fsquare_times x2 1) f in
  let x6 = S.fmul (fsquare_times x3 3) x3 in
  let x12 = S.fmul (fsquare_times x6 6) x6 in
  let x15 = S.fmul (fsquare_times x12 3) x3 in
  let x30 = S.fmul (fsquare_times x15 15) x15 in
  let x32 = S.fmul (fsquare_times x30 2) x2 in
  let x64 = S.fmul (fsquare_times x32 32) f in
  let x192 = S.fmul (fsquare_times x64 128) x32 in
  let x224 = S.fmul (fsquare_times x192 32) x32 in
  let x254 = S.fmul (fsquare_times x224 30) x30 in
  let x256 = S.fmul (fsquare_times x254 2) f in
  x256
val finv: f:S.felem -> S.felem
let finv f =
let x2 = S.fmul (fsquare_times f 1) f in
let x3 = S.fmul (fsquare_times x2 1) f in
let x6 = S.fmul (fsquare_times x3 3) x3 in
let x12 = S.fmul (fsquare_times x6 6) x6 in
let x15 = S.fmul (fsquare_times x12 3) x3 in
let x30 = S.fmul (fsquare_times x15 15) x15 in
let x32 = S.fmul (fsquare_times x30 2) x2 in
let x64 = S.fmul (fsquare_times x32 32) f in
let x192 = S.fmul (fsquare_times x64 128) x32 in
let x224 = S.fmul (fsquare_times x192 32) x32 in
let x254 = S.fmul (fsquare_times x224 30) x30 in
let x256 = S.fmul (fsquare_times x254 2) f in
x256
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 Spec.P256.PointOps.fmul Hacl.Spec.P256.Finv.fsquare_times
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)
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)


(**
The algorithm is taken from
https://briansmith.org/ecc-inversion-addition-chains-01
*)
val finv: f:S.felem -> S.felem
f: Spec.P256.PointOps.felem -> Spec.P256.PointOps.felem