val bn_check_mod_inv_prime:
    #t:limb_t
  -> #len:BN.bn_len t
  -> n:lbignum t len
  -> a:lbignum t len ->
  res:limb t{
    let b =
      bn_v n % 2 = 1 && 1 < bn_v n &&
      0 < bn_v a && bn_v a < bn_v n in
    v res == (if b then v (ones t SEC) else v (zeros t SEC))}
let bn_check_mod_inv_prime #t #len n a =
  let m0 = BM.bn_check_modulus n in
  let m1 = BN.bn_is_zero_mask a in
  BN.bn_is_zero_mask_lemma a;
  let m1' = lognot m1 in
  lognot_lemma m1;
  let m2 = BN.bn_lt_mask a n in
  BN.bn_lt_mask_lemma a n;
  logand_ones (m0 &. m1');
  logand_zeros (m0 &. m1');
  logand_ones m0;
  logand_zeros m0;
  m0 &. m1' &. m2
val bn_check_mod_inv_prime:
    #t:limb_t
  -> #len:BN.bn_len t
  -> n:lbignum t len
  -> a:lbignum t len ->
  res:limb t{
    let b =
      bn_v n % 2 = 1 && 1 < bn_v n &&
      0 < bn_v a && bn_v a < bn_v n in
    v res == (if b then v (ones t SEC) else v (zeros t SEC))}
let bn_check_mod_inv_prime #t #len n a =
let m0 = BM.bn_check_modulus n in
let m1 = BN.bn_is_zero_mask a in
BN.bn_is_zero_mask_lemma a;
let m1' = lognot m1 in
lognot_lemma m1;
let m2 = BN.bn_lt_mask a n in
BN.bn_lt_mask_lemma a n;
logand_ones (m0 &. m1');
logand_zeros (m0 &. m1');
logand_ones m0;
logand_zeros m0;
m0 &. m1' &. m2
Hacl.Spec.Bignum.ModInv.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.NatMod.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Bignum.Montgomery.fsti.checked Hacl.Spec.Bignum.Exponentiation.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Math.Fermat.fsti.checked FStar.Math.Euclid.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.Bignum.ModInv.fst
Hacl.Spec.Bignum.Definitions.limb_t Hacl.Spec.Bignum.bn_len Hacl.Spec.Bignum.Definitions.lbignum Lib.IntTypes.op_Amp_Dot Lib.IntTypes.SEC Prims.unit Lib.IntTypes.logand_zeros Lib.IntTypes.logand_ones Hacl.Spec.Bignum.bn_lt_mask_lemma Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.bn_lt_mask Lib.IntTypes.lognot_lemma Lib.IntTypes.int_t Lib.IntTypes.lognot Hacl.Spec.Bignum.bn_is_zero_mask_lemma Hacl.Spec.Bignum.bn_is_zero_mask Prims.eq2 Prims.int Lib.IntTypes.range Lib.IntTypes.v Prims.op_AmpAmp Prims.op_Equality Prims.op_Modulus Hacl.Spec.Bignum.Definitions.bn_v Prims.op_LessThan Lib.IntTypes.ones Prims.bool Lib.IntTypes.zeros Hacl.Spec.Bignum.Montgomery.bn_check_modulus Lib.IntTypes.range_t
module Hacl.Spec.Bignum.ModInv

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.LoopCombinators

open Hacl.Spec.Bignum.Definitions
open Hacl.Spec.Bignum

module Fermat = FStar.Math.Fermat
module Euclid = FStar.Math.Euclid

module BE = Hacl.Spec.Bignum.Exponentiation
module BM = Hacl.Spec.Bignum.Montgomery
module BN = Hacl.Spec.Bignum

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

#push-options "--fuel 1"
val pow_eq: a:nat -> n:nat -> Lemma (Fermat.pow a n == Lib.NatMod.pow a n)
let rec pow_eq a n =
  if n = 0 then ()
  else pow_eq a (n - 1)
#pop-options

val mod_inv_prime_lemma: n:nat{1 < n /\ Euclid.is_prime n} -> a:pos{a < n} ->
  Lemma (Lib.NatMod.pow_mod #n a (n - 2) * a % n = 1)

let mod_inv_prime_lemma n a =
  Math.Lemmas.small_mod a n;
  assert (a == a % n);
  assert (a <> 0 /\ a % n <> 0);

  calc (==) {
    Lib.NatMod.pow_mod #n a (n - 2) * a % n;
    (==) { Lib.NatMod.lemma_pow_mod #n a (n - 2) }
    Lib.NatMod.pow a (n - 2) % n * a % n;
    (==) { Math.Lemmas.lemma_mod_mul_distr_l (Lib.NatMod.pow a (n - 2)) a n }
    Lib.NatMod.pow a (n - 2) * a % n;
    (==) { Lib.NatMod.lemma_pow1 a; Lib.NatMod.lemma_pow_add a (n - 2) 1 }
    Lib.NatMod.pow a (n - 1) % n;
    (==) { pow_eq a (n - 1) }
    Fermat.pow a (n - 1) % n;
    (==) { Fermat.fermat_alt n a }
    1;
    }

//pow2 nBits < bn_v n /\ Euclid.is_prime (bn_v n) are still needed to be checked
val bn_check_mod_inv_prime:
    #t:limb_t
  -> #len:BN.bn_len t
  -> n:lbignum t len
  -> a:lbignum t len ->
  res:limb t{
    let b =
      bn_v n % 2 = 1 && 1 < bn_v n &&
      0 < bn_v a && bn_v a < bn_v n in
    v res == (if b then v (ones t SEC) else v (zeros t SEC))}
val bn_check_mod_inv_prime:
    #t:limb_t
  -> #len:BN.bn_len t
  -> n:lbignum t len
  -> a:lbignum t len ->
  res:limb t{
    let b =
      bn_v n % 2 = 1 && 1 < bn_v n &&
      0 < bn_v a && bn_v a < bn_v n in
    v res == (if b then v (ones t SEC) else v (zeros t SEC))}
n: Hacl.Spec.Bignum.Definitions.lbignum t len -> a: Hacl.Spec.Bignum.Definitions.lbignum t len
  -> res:
    Hacl.Spec.Bignum.Definitions.limb t
      { let b =
          Hacl.Spec.Bignum.Definitions.bn_v n % 2 = 1 && 1 < Hacl.Spec.Bignum.Definitions.bn_v n &&
          0 < Hacl.Spec.Bignum.Definitions.bn_v a &&
          Hacl.Spec.Bignum.Definitions.bn_v a < Hacl.Spec.Bignum.Definitions.bn_v n
        in
        Lib.IntTypes.v res ==
        (match b with
          | true -> Lib.IntTypes.v (Lib.IntTypes.ones t Lib.IntTypes.SEC)
          | _ -> Lib.IntTypes.v (Lib.IntTypes.zeros t Lib.IntTypes.SEC)) }