let bn_field_init_st (t:limb_t) (len:BN.meta_len t) =
    r:HS.rid
  -> n:lbignum t len ->
  ST (pbn_mont_ctx t)
  (requires fun h ->
    S.bn_mont_ctx_pre (as_seq h n) /\

    live h n /\ ST.is_eternal_region r)
  (ensures  fun h0 res h1 ->
    B.(modifies loc_none h0 h1) /\
    B.(fresh_loc (footprint h1 res) h0 h1) /\
    B.(loc_includes (loc_region_only true r) (footprint h1 res)) /\
    freeable h1 res /\
    (B.deref h1 res).len == len /\ bn_v_n h1 res == bn_v h0 n /\
    S.bn_mont_ctx_inv (as_pctx h1 res) /\
    as_pctx h1 res == S.bn_field_init (as_seq h0 n))
let bn_field_init_st (t: limb_t) (len: BN.meta_len t) =
r: HS.rid -> n: lbignum t len
  -> ST (pbn_mont_ctx t)
      (requires fun h -> S.bn_mont_ctx_pre (as_seq h n) /\ live h n /\ ST.is_eternal_region r)
      (ensures
        fun h0 res h1 ->
          B.(modifies loc_none h0 h1) /\ B.(fresh_loc (footprint h1 res) h0 h1) /\
          B.(loc_includes (loc_region_only true r) (footprint h1 res)) /\ freeable h1 res /\
          (B.deref h1 res).len == len /\ bn_v_n h1 res == bn_v h0 n /\
          S.bn_mont_ctx_inv (as_pctx h1 res) /\ as_pctx h1 res == S.bn_field_init (as_seq h0 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 Hacl.Bignum.meta_len FStar.Monotonic.HyperHeap.rid Hacl.Bignum.Definitions.lbignum Hacl.Bignum.MontArithmetic.pbn_mont_ctx FStar.Monotonic.HyperStack.mem Prims.l_and Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_pre Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.as_seq Lib.Buffer.MUT Hacl.Bignum.Definitions.limb Lib.Buffer.live FStar.HyperStack.ST.is_eternal_region LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none LowStar.Monotonic.Buffer.fresh_loc Hacl.Bignum.MontArithmetic.footprint LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.loc_region_only Hacl.Bignum.MontArithmetic.freeable Prims.eq2 Hacl.Bignum.MontArithmetic.__proj__Mkbn_mont_ctx'__item__len Hacl.Bignum.MontArithmetic.lb Hacl.Bignum.MontArithmetic.ll LowStar.Monotonic.Buffer.deref Hacl.Bignum.MontArithmetic.bn_mont_ctx LowStar.Buffer.trivial_preorder Prims.nat Hacl.Bignum.MontArithmetic.bn_v_n Hacl.Bignum.Definitions.bn_v Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx_inv Hacl.Bignum.MontArithmetic.as_pctx Hacl.Spec.Bignum.MontArithmetic.bn_mont_ctx Hacl.Spec.Bignum.MontArithmetic.bn_field_init
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)


inline_for_extraction noextract
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

inline_for_extraction noextract
let freeable_s (#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
  B.freeable n /\ B.freeable r2

inline_for_extraction noextract
let freeable (#t:limb_t) (h:mem) (k:pbn_mont_ctx t) =
  B.freeable k /\ freeable_s h (B.deref h k)

inline_for_extraction noextract
let footprint_s (#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
  B.(loc_union (loc_addr_of_buffer n) (loc_addr_of_buffer r2))

inline_for_extraction noextract
let footprint (#t:limb_t) (h:mem) (k:pbn_mont_ctx t) =
  B.(loc_union (loc_addr_of_buffer k) (footprint_s h (B.deref h k)))

inline_for_extraction noextract
let as_pctx (#t:limb_t) (h:mem) (k:pbn_mont_ctx t) : GTot (S.bn_mont_ctx t) =
  as_ctx h (B.deref h k)

inline_for_extraction noextract
let pbn_mont_ctx_inv (#t:limb_t) (h:mem) (k:pbn_mont_ctx t) =
  B.live h k /\
  B.(loc_disjoint (loc_addr_of_buffer k) (footprint_s h (B.deref h k))) /\
  bn_mont_ctx_inv h (B.deref h k)


inline_for_extraction noextract
let bn_field_get_len_st (t:limb_t) = k:pbn_mont_ctx t ->
  Stack (BN.meta_len t)
  (requires fun h -> pbn_mont_ctx_inv h k)
  (ensures  fun h0 r h1 -> h0 == h1 /\
    r == (B.deref h0 k).len /\
    v r == S.bn_field_get_len (as_pctx h0 k))


inline_for_extraction noextract
val bn_field_get_len: #t:limb_t -> bn_field_get_len_st t


inline_for_extraction noextract
let bn_field_check_modulus_st (t:limb_t) (len:BN.meta_len t) = n:lbignum t len ->
  Stack bool
  (requires fun h -> live h n)
  (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
    r == S.bn_field_check_modulus (as_seq h0 n))


inline_for_extraction noextract
val bn_field_check_modulus: #t:limb_t -> km:BM.mont t -> bn_field_check_modulus_st t km.BM.bn.BN.len


inline_for_extraction noextract
val bn_field_init_st : t: Hacl.Bignum.Definitions.limb_t -> len: Hacl.Bignum.meta_len t -> Type0
t: Hacl.Bignum.Definitions.limb_t -> len: Hacl.Bignum.meta_len t -> Type0