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_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
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 Spec.K256.PointOps.qmul Hacl.Spec.K256.Qinv.qsquare_times
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
r23: Spec.K256.PointOps.qelem -> x_1: Spec.K256.PointOps.qelem -> x6: Spec.K256.PointOps.qelem
  -> Spec.K256.PointOps.qelem