val bn_almost_mont_mul:
    #t:limb_t
  -> #nLen:size_pos{nLen + nLen <= max_size_t}
  -> n:lbignum t nLen
  -> mu:limb t
  -> aM:lbignum t nLen
  -> bM:lbignum t nLen ->
  lbignum t nLen
let bn_almost_mont_mul #t #nLen n mu aM bM =
  let c = BN.bn_mul aM bM in // c = aM * bM
  bn_almost_mont_reduction n mu c
val bn_almost_mont_mul:
    #t:limb_t
  -> #nLen:size_pos{nLen + nLen <= max_size_t}
  -> n:lbignum t nLen
  -> mu:limb t
  -> aM:lbignum t nLen
  -> bM:lbignum t nLen ->
  lbignum t nLen
let bn_almost_mont_mul #t #nLen n mu aM bM =
let c = BN.bn_mul aM bM in
bn_almost_mont_reduction n mu c
Hacl.Spec.Bignum.AlmostMontgomery.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Montgomery.Lemmas.fst.checked Hacl.Spec.Bignum.Montgomery.fst.checked Hacl.Spec.Bignum.Montgomery.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Base.fst.checked Hacl.Spec.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Hacl.Spec.Bignum.AlmostMontgomery.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_pos Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.max_size_t Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.AlmostMontgomery.bn_almost_mont_reduction Hacl.Spec.Bignum.bn_mul
module Hacl.Spec.Bignum.AlmostMontgomery

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence

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

module M = Hacl.Spec.Montgomery.Lemmas
module BN = Hacl.Spec.Bignum
module BM = Hacl.Spec.Bignum.Montgomery

friend Hacl.Spec.Bignum.Montgomery

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

///  Low-level specification of Almost Montgomery Multiplication

let bn_almost_mont_reduction #t #nLen n mu c =
  let c0, res = BM.bn_mont_reduction_loop_div_r #t #nLen n mu c in
  let mask = uint #t 0 -. c0 in
  let c1, tmp = BN.bn_sub res n in
  map2 (mask_select mask) tmp res
val bn_almost_mont_mul:
    #t:limb_t
  -> #nLen:size_pos{nLen + nLen <= max_size_t}
  -> n:lbignum t nLen
  -> mu:limb t
  -> aM:lbignum t nLen
  -> bM:lbignum t nLen ->
  lbignum t nLen

    n: Hacl.Spec.Bignum.Definitions.lbignum t nLen ->
    mu: Hacl.Spec.Bignum.Definitions.limb t ->
    aM: Hacl.Spec.Bignum.Definitions.lbignum t nLen ->
    bM: Hacl.Spec.Bignum.Definitions.lbignum t nLen
  -> Hacl.Spec.Bignum.Definitions.lbignum t nLen