val bn_reduce_once:
    #t:limb_t
  -> #len:size_nat
  -> n:lbignum t len
  -> c:carry t
  -> a:lbignum t len ->
  lbignum t len
let bn_reduce_once #t #len n c0 a =
  let c1, res = bn_sub a n in
  let c = c0 -. c1 in
  map2 (mask_select c) a res
val bn_reduce_once:
    #t:limb_t
  -> #len:size_nat
  -> n:lbignum t len
  -> c:carry t
  -> a:lbignum t len ->
  lbignum t len
let bn_reduce_once #t #len n c0 a =
let c1, res = bn_sub a n in
let c = c0 -. c1 in
map2 (mask_select c) a res
Hacl.Spec.Bignum.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Squaring.fst.checked Hacl.Spec.Bignum.Multiplication.fst.checked Hacl.Spec.Bignum.Lib.fst.checked Hacl.Spec.Bignum.Karatsuba.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Spec.Bignum.Comparison.fst.checked Hacl.Spec.Bignum.Addition.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Hacl.Spec.Bignum.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_nat Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Base.carry Lib.Sequence.map2 Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.Base.mask_select Lib.IntTypes.int_t Lib.IntTypes.SEC Lib.IntTypes.op_Subtraction_Dot FStar.Pervasives.Native.tuple2 Hacl.Spec.Bignum.bn_sub
module Hacl.Spec.Bignum

module Loops = Lib.LoopCombinators


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

let bn_add1 #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_add1 a b1

let bn_add1_lemma #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_add1_lemma a b1

let bn_sub1 #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_sub1 a b1

let bn_sub1_lemma #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_sub1_lemma a b1

let bn_add #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_add a b

let bn_add_lemma #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_add_lemma a b

let bn_sub #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_sub a b

let bn_sub_lemma #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_sub_lemma a b
val bn_reduce_once:
    #t:limb_t
  -> #len:size_nat
  -> n:lbignum t len
  -> c:carry t
  -> a:lbignum t len ->
  lbignum t len

    n: Hacl.Spec.Bignum.Definitions.lbignum t len ->
    c: Hacl.Spec.Bignum.Base.carry t ->
    a: Hacl.Spec.Bignum.Definitions.lbignum t len
  -> Hacl.Spec.Bignum.Definitions.lbignum t len