val bn_mod_inv_prime_n2:
    #t:limb_t
  -> len:BN.meta_len t
  -> n:lbignum t len
  -> res:lbignum t len ->
  Stack unit
  (requires fun h -> 1 < bn_v h n /\
    live h n /\ live h res /\ disjoint res n)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.bn_mod_inv_prime_n2 (as_seq h0 n))
let bn_mod_inv_prime_n2 #t len n res =
  let c = BN.bn_sub1 len n (uint #t #SEC 2) res in
  LowStar.Ignore.ignore c;
  ()
val bn_mod_inv_prime_n2:
    #t:limb_t
  -> len:BN.meta_len t
  -> n:lbignum t len
  -> res:lbignum t len ->
  Stack unit
  (requires fun h -> 1 < bn_v h n /\
    live h n /\ live h res /\ disjoint res n)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.bn_mod_inv_prime_n2 (as_seq h0 n))
let bn_mod_inv_prime_n2 #t len n res =
let c = BN.bn_sub1 len n (uint #t #SEC 2) res in
LowStar.Ignore.ignore c;
()
Hacl.Bignum.ModInv.fst.checked
prims.fst.checked LowStar.Ignore.fsti.checked Lib.NatMod.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.ModInv.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Bignum.Montgomery.fsti.checked Hacl.Bignum.Exponentiation.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Bignum.ModInv.fst
Hacl.Bignum.Definitions.limb_t Hacl.Bignum.meta_len Hacl.Bignum.Definitions.lbignum Prims.unit LowStar.Ignore.ignore Hacl.Spec.Bignum.Base.carry Hacl.Bignum.bn_sub1 Lib.IntTypes.uint Lib.IntTypes.SEC
module Hacl.Bignum.ModInv

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Definitions

module ST = FStar.HyperStack.ST
module S = Hacl.Spec.Bignum.ModInv

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

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

inline_for_extraction noextract
let bn_check_mod_inv_prime_st (t:limb_t) (len:BN.meta_len t) =
    n:lbignum t len
  -> a:lbignum t len ->
  Stack (limb t)
  (requires fun h -> live h n /\ live h a /\ disjoint n a)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    r == S.bn_check_mod_inv_prime (as_seq h0 n) (as_seq h0 a))


inline_for_extraction noextract
val bn_check_mod_inv_prime: #t:limb_t -> len:BN.meta_len t -> bn_check_mod_inv_prime_st t len
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 len a in
  let m2 = BN.bn_lt_mask len a n in
  m0 &. (lognot m1) &. m2


inline_for_extraction noextract
val bn_mod_inv_prime_n2:
    #t:limb_t
  -> len:BN.meta_len t
  -> n:lbignum t len
  -> res:lbignum t len ->
  Stack unit
  (requires fun h -> 1 < bn_v h n /\
    live h n /\ live h res /\ disjoint res n)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.bn_mod_inv_prime_n2 (as_seq h0 n))
val bn_mod_inv_prime_n2:
    #t:limb_t
  -> len:BN.meta_len t
  -> n:lbignum t len
  -> res:lbignum t len ->
  Stack unit
  (requires fun h -> 1 < bn_v h n /\
    live h n /\ live h res /\ disjoint res n)
  (ensures  fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_seq h1 res == S.bn_mod_inv_prime_n2 (as_seq h0 n))

    len: Hacl.Bignum.meta_len t ->
    n: Hacl.Bignum.Definitions.lbignum t len ->
    res: Hacl.Bignum.Definitions.lbignum t len
  -> FStar.HyperStack.ST.Stack Prims.unit