val lemma_pow_mod_mul: f:S.qelem -> a:nat -> b:nat ->
  Lemma (S.qmul (M.pow f a % S.q) (M.pow f b % S.q) == M.pow f (a + b) % S.q)
let lemma_pow_mod_mul f a b =
  calc (==) {
    S.qmul (M.pow f a % S.q) (M.pow f b % S.q);
    (==) {
      Math.Lemmas.lemma_mod_mul_distr_l (M.pow f a) (M.pow f b % S.q) S.q;
      Math.Lemmas.lemma_mod_mul_distr_r (M.pow f a) (M.pow f b) S.q }
    M.pow f a * M.pow f b % S.q;
    (==) { M.lemma_pow_add f a b }
    M.pow f (a + b) % S.q;
  }
val lemma_pow_mod_mul: f:S.qelem -> a:nat -> b:nat ->
  Lemma (S.qmul (M.pow f a % S.q) (M.pow f b % S.q) == M.pow f (a + b) % S.q)
let lemma_pow_mod_mul f a b =
calc ( == ) {
  S.qmul (M.pow f a % S.q) (M.pow f b % S.q);
  ( == ) { (Math.Lemmas.lemma_mod_mul_distr_l (M.pow f a) (M.pow f b % S.q) S.q;
    Math.Lemmas.lemma_mod_mul_distr_r (M.pow f a) (M.pow f b) S.q) }
  M.pow f a * M.pow f b % S.q;
  ( == ) { M.lemma_pow_add f a b }
  M.pow f (a + b) % S.q;
}
Hacl.Spec.K256.Qinv.fst.checked
Spec.K256.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.K256.Qinv.fst
Spec.K256.PointOps.qelem Prims.nat FStar.Calc.calc_finish Prims.eq2 Spec.K256.PointOps.qmul Prims.op_Modulus Lib.NatMod.pow Spec.K256.PointOps.q Prims.op_Addition Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Mul.op_Star FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.lemma_mod_mul_distr_r FStar.Math.Lemmas.lemma_mod_mul_distr_l Prims.squash Lib.NatMod.lemma_pow_add
module Hacl.Spec.K256.Qinv

open FStar.Mul

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

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

let nat_mod_comm_monoid = M.mk_nat_mod_comm_monoid S.q

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.q)
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.q a (pow2 b)


(**
The algorithm is taken from
https://briansmith.org/ecc-inversion-addition-chains-01
*)

val qinv_r0_r1 (x14: S.qelem) : S.qelem
let qinv_r0_r1 x14 =
  let x28 = S.qmul (qsquare_times x14 14) x14 in
  let x56 = S.qmul (qsquare_times x28 28) x28 in
  let r0 = S.qmul (qsquare_times x56 56) x56 in
  let r1 = S.qmul (qsquare_times r0 14) x14 in
  r1


val qinv_r2_r8 (r1 x_101 x_111 x_1011: S.qelem) : S.qelem
let qinv_r2_r8 r1 x_101 x_111 x_1011 =
  let r2 = S.qmul (qsquare_times r1 3) x_101 in
  let r3 = S.qmul (qsquare_times r2 4) x_111 in
  let r4 = S.qmul (qsquare_times r3 4) x_101 in
  let r5 = S.qmul (qsquare_times r4 5) x_1011 in
  let r6 = S.qmul (qsquare_times r5 4) x_1011 in
  let r7 = S.qmul (qsquare_times r6 4) x_111 in
  let r8 = S.qmul (qsquare_times r7 5) x_111 in
  r8


val qinv_r9_r15 (r8 x_101 x_111 x_1001 x_1101: S.qelem) : S.qelem
let qinv_r9_r15 r8 x_101 x_111 x_1001 x_1101 =
  let r9 = S.qmul (qsquare_times r8 6) x_1101 in
  let r10 = S.qmul (qsquare_times r9 4) x_101 in
  let r11 = S.qmul (qsquare_times r10 3) x_111 in
  let r12 = S.qmul (qsquare_times r11 5) x_1001 in
  let r13 = S.qmul (qsquare_times r12 6) x_101 in
  let r14 = S.qmul (qsquare_times r13 10) x_111 in
  let r15 = S.qmul (qsquare_times r14 4) x_111 in
  r15


val qinv_r16_r23 (r15 x8 x_11 x_1001 x_1011 x_1101: S.qelem) : S.qelem
let qinv_r16_r23 r15 x8 x_11 x_1001 x_1011 x_1101 =
  let r16 = S.qmul (qsquare_times r15 9) x8 in
  let r17 = S.qmul (qsquare_times r16 5) x_1001 in
  let r18 = S.qmul (qsquare_times r17 6) x_1011 in
  let r19 = S.qmul (qsquare_times r18 4) x_1101 in
  let r20 = S.qmul (qsquare_times r19 5) x_11 in
  let r21 = S.qmul (qsquare_times r20 6) x_1101 in
  let r22 = S.qmul (qsquare_times r21 10) x_1101 in
  let r23 = S.qmul (qsquare_times r22 4) x_1001 in
  r23


val qinv_r24_r25 (r23 x_1 x6: S.qelem) : S.qelem
let qinv_r24_r25 r23 x_1 x6 =
  let r24 = S.qmul (qsquare_times r23 6) x_1 in
  let r25 = S.qmul (qsquare_times r24 8) x6 in
  r25


val qinv_r0_r25 (x_1 x_11 x_101 x_111 x_1001 x_1011 x_1101: S.qelem) : S.qelem
let qinv_r0_r25 x_1 x_11 x_101 x_111 x_1001 x_1011 x_1101 =
  let x6 = S.qmul (qsquare_times x_1101 2) x_1011 in
  let x8 = S.qmul (qsquare_times x6 2) x_11 in
  let x14 = S.qmul (qsquare_times x8 6) x6 in

  let r1 = qinv_r0_r1 x14 in
  let r8 = qinv_r2_r8 r1 x_101 x_111 x_1011 in
  let r15 = qinv_r9_r15 r8 x_101 x_111 x_1001 x_1101 in
  let r23 = qinv_r16_r23 r15 x8 x_11 x_1001 x_1011 x_1101 in
  qinv_r24_r25 r23 x_1 x6


val qinv: f:S.qelem -> S.qelem
let qinv f =
  let x_1 = f in
  let x_10 = qsquare_times f 1 in
  let x_11 = S.qmul x_10 x_1 in
  let x_101 = S.qmul x_10 x_11 in
  let x_111 = S.qmul x_10 x_101 in
  let x_1001 = S.qmul x_10 x_111 in
  let x_1011 = S.qmul x_10 x_1001 in
  let x_1101 = S.qmul x_10 x_1011 in

  qinv_r0_r25 x_1 x_11 x_101 x_111 x_1001 x_1011 x_1101


val lemma_pow_mod_1: f:S.qelem -> Lemma (f == M.pow f 1 % S.q)
let lemma_pow_mod_1 f =
  M.lemma_pow1 f;
  Math.Lemmas.small_mod f S.q;
  assert_norm (pow2 0 = 1);
  assert (f == M.pow f 1 % S.q)


val lemma_pow_mod_mul: f:S.qelem -> a:nat -> b:nat ->
  Lemma (S.qmul (M.pow f a % S.q) (M.pow f b % S.q) == M.pow f (a + b) % S.q)
val lemma_pow_mod_mul: f:S.qelem -> a:nat -> b:nat ->
  Lemma (S.qmul (M.pow f a % S.q) (M.pow f b % S.q) == M.pow f (a + b) % S.q)
f: Spec.K256.PointOps.qelem -> a: Prims.nat -> b: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.K256.PointOps.qmul (Lib.NatMod.pow f a % Spec.K256.PointOps.q)
        (Lib.NatMod.pow f b % Spec.K256.PointOps.q) ==
      Lib.NatMod.pow f (a + b) % Spec.K256.PointOps.q)