let bn_v_n (#t:limb_t) (h:mem) (k:pbn_mont_ctx t) =
  let k1 = B.deref h k in
  let n : lbignum t k1.len = k1.n in
  bn_v h n
let bn_v_n (#t: limb_t) (h: mem) (k: pbn_mont_ctx t) =
let k1 = B.deref h k in
let n:lbignum t k1.len = k1.n in
bn_v h n
Hacl.Bignum.MontArithmetic.fsti.checked
prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.MontArithmetic.fsti.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.Math.Euclid.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Bignum.MontArithmetic.fsti
Hacl.Bignum.Definitions.limb_t FStar.Monotonic.HyperStack.mem Hacl.Bignum.MontArithmetic.pbn_mont_ctx Hacl.Bignum.Definitions.bn_v Hacl.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx'__item__len Hacl.Bignum.MontArithmetic.lb Hacl.Bignum.MontArithmetic.ll Hacl.Bignum.Definitions.lbignum Hacl.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx'__item__n Hacl.Bignum.MontArithmetic.bn_mont_ctx LowStar.Monotonic.Buffer.deref LowStar.Buffer.trivial_preorder Prims.nat
module Hacl.Bignum.MontArithmetic

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Definitions

module B = LowStar.Buffer
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST

module Euclid = FStar.Math.Euclid
module S = Hacl.Spec.Bignum.MontArithmetic
module BE = Hacl.Bignum.Exponentiation
module BN = Hacl.Bignum
module BM = Hacl.Bignum.Montgomery

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

val _align_fsti : unit

inline_for_extraction noextract
let lb (t:limb_t) =
  match t with
  | U32 -> buffer uint32
  | U64 -> buffer uint64

inline_for_extraction noextract
let ll (t:limb_t) =
  match t with
  | U32 -> uint32
  | U64 -> uint64

inline_for_extraction
noeq
type bn_mont_ctx' (t:limb_t) (a:Type0{a == lb t}) (b:Type0{b == ll t}) = {
  len: BN.meta_len t;
  n: x:a{length #MUT #(limb t) x == v len};
  mu: b;
  r2: x:a{length #MUT #(limb t) x == v len};
  }

inline_for_extraction noextract
let bn_mont_ctx (t:limb_t) = bn_mont_ctx' t (lb t) (ll t)

let bn_mont_ctx_u32 = bn_mont_ctx' U32 (lb U32) (ll U32)
let bn_mont_ctx_u64 = bn_mont_ctx' U64 (lb U64) (ll U64)

inline_for_extraction noextract
let pbn_mont_ctx (t:limb_t) = B.pointer (bn_mont_ctx t)

inline_for_extraction noextract
let pbn_mont_ctx_u32 = B.pointer bn_mont_ctx_u32
inline_for_extraction noextract
let pbn_mont_ctx_u64 = B.pointer bn_mont_ctx_u64

inline_for_extraction noextract
let as_ctx (#t:limb_t) (h:mem) (k:bn_mont_ctx t) : GTot (S.bn_mont_ctx t) = {
  S.len = v k.len;
  S.n = as_seq h (k.n <: lbignum t k.len);
  S.mu = k.mu;
  S.r2 = as_seq h (k.r2 <: lbignum t k.len);
  }

inline_for_extraction noextract
let bn_mont_ctx_inv (#t:limb_t) (h:mem) (k:bn_mont_ctx t) =
  let n : buffer (limb t) = k.n in
  let r2 : buffer (limb t) = k.r2 in
  live h n /\ live h r2 /\ disjoint n r2 /\
  S.bn_mont_ctx_inv (as_ctx h k)
val bn_v_n : h: FStar.Monotonic.HyperStack.mem -> k: Hacl.Bignum.MontArithmetic.pbn_mont_ctx t
  -> Prims.GTot Prims.nat
h: FStar.Monotonic.HyperStack.mem -> k: Hacl.Bignum.MontArithmetic.pbn_mont_ctx t
  -> Prims.GTot Prims.nat