val bn_almost_mont_mul:
    #t:limb_t
  -> k:BN.bn t
  -> mr:bn_almost_mont_reduction_st t k.BN.len ->
  bn_almost_mont_mul_st t k.BN.len
let bn_almost_mont_mul #t k almost_mont_reduction n nInv_u64 aM bM resM =
  [@inline_let] let len = k.BN.len in
  push_frame ();
  let c = create (len +! len) (uint #t 0) in
  k.BN.mul aM bM c;
  almost_mont_reduction n nInv_u64 c resM;
  pop_frame ()
val bn_almost_mont_mul:
    #t:limb_t
  -> k:BN.bn t
  -> mr:bn_almost_mont_reduction_st t k.BN.len ->
  bn_almost_mont_mul_st t k.BN.len
let bn_almost_mont_mul #t k almost_mont_reduction n nInv_u64 aM bM resM =
[@@ inline_let ]let len = k.BN.len in
push_frame ();
let c = create (len +! len) (uint #t 0) in
k.BN.mul aM bM c;
almost_mont_reduction n nInv_u64 c resM;
pop_frame ()
Hacl.Bignum.AlmostMontgomery.fst.checked
prims.fst.checked LowStar.Ignore.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.AlmostMontgomery.fst.checked Hacl.Spec.Bignum.AlmostMontgomery.fst.checked Hacl.Bignum.Montgomery.fst.checked Hacl.Bignum.Montgomery.fst.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.Base.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.AlmostMontgomery.fst
Hacl.Bignum.Definitions.limb_t Hacl.Bignum.bn Hacl.Bignum.AlmostMontgomery.bn_almost_mont_reduction_st Hacl.Bignum.__proj__Mkbn__item__len Hacl.Bignum.Definitions.lbignum Hacl.Bignum.Definitions.limb FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Bignum.__proj__Mkbn__item__mul Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.add Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.create Lib.IntTypes.op_Plus_Bang Lib.IntTypes.uint Lib.IntTypes.SEC Lib.Buffer.lbuffer FStar.HyperStack.ST.push_frame Hacl.Bignum.meta_len
module Hacl.Bignum.AlmostMontgomery

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Definitions
open Hacl.Bignum.Base

module ST = FStar.HyperStack.ST
module S = Hacl.Spec.Bignum.AlmostMontgomery
module BN = Hacl.Bignum
module BM = Hacl.Bignum.Montgomery

friend Hacl.Spec.Bignum.AlmostMontgomery
friend Hacl.Bignum.Montgomery

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

let bn_almost_mont_reduction #t k n nInv c res =
  [@inline_let] let len = k.BN.len in
  push_frame ();
  let c0 = BM.bn_mont_reduction_loop_div_r #t k n nInv c res in
  let tmp = create len (uint #t #SEC 0) in
  let c1 = k.BN.sub res n tmp in
  LowStar.Ignore.ignore c1;
  let m = uint #t 0 -. c0 in
  map2T len res (mask_select m) tmp res;
  pop_frame ()
val bn_almost_mont_mul:
    #t:limb_t
  -> k:BN.bn t
  -> mr:bn_almost_mont_reduction_st t k.BN.len ->
  bn_almost_mont_mul_st t k.BN.len
k: Hacl.Bignum.bn t -> mr: Hacl.Bignum.AlmostMontgomery.bn_almost_mont_reduction_st t (Mkbn?.len k)
  -> Hacl.Bignum.AlmostMontgomery.bn_almost_mont_mul_st t (Mkbn?.len k)