val bn_almost_mont_reduction_u32 (len: BN.meta_len U32) : bn_almost_mont_reduction_st U32 len
let bn_almost_mont_reduction_u32 (len:BN.meta_len U32) : bn_almost_mont_reduction_st U32 len =
  bn_almost_mont_reduction (BN.mk_runtime_bn U32 len)
val bn_almost_mont_reduction_u32 (len: BN.meta_len U32) : bn_almost_mont_reduction_st U32 len
let bn_almost_mont_reduction_u32 (len: BN.meta_len U32) : bn_almost_mont_reduction_st U32 len =
bn_almost_mont_reduction (BN.mk_runtime_bn U32 len)
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.meta_len Lib.IntTypes.U32 Hacl.Bignum.AlmostMontgomery.bn_almost_mont_reduction Hacl.Bignum.mk_runtime_bn Hacl.Bignum.AlmostMontgomery.bn_almost_mont_reduction_st
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 ()


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 ()


let bn_almost_mont_sqr #t k almost_mont_reduction n nInv_u64 aM resM =
  [@inline_let] let len = k.BN.len in
  push_frame ();
  let c = create (len +! len) (uint #t 0) in
  k.BN.sqr aM c;
  almost_mont_reduction n nInv_u64 c resM;
  pop_frame ()
val bn_almost_mont_reduction_u32 (len: BN.meta_len U32) : bn_almost_mont_reduction_st U32 len
len: Hacl.Bignum.meta_len Lib.IntTypes.U32
  -> Hacl.Bignum.AlmostMontgomery.bn_almost_mont_reduction_st Lib.IntTypes.U32 len