val bn_karatsuba_mul:
    #t:limb_t
  -> len:size_t{0 < v len /\ 4 * v len <= max_size_t}
  -> a:lbignum t len ->
  bn_karatsuba_mul_st t len a
let bn_karatsuba_mul #t len a b res =
  let h0 = ST.get () in
  Hacl.Spec.Bignum.bn_karatsuba_mul_lemma (as_seq h0 a) (as_seq h0 b);
  Hacl.Bignum.Karatsuba.bn_karatsuba_mul len a b res
val bn_karatsuba_mul:
    #t:limb_t
  -> len:size_t{0 < v len /\ 4 * v len <= max_size_t}
  -> a:lbignum t len ->
  bn_karatsuba_mul_st t len a
let bn_karatsuba_mul #t len a b res =
let h0 = ST.get () in
Hacl.Spec.Bignum.bn_karatsuba_mul_lemma (as_seq h0 a) (as_seq h0 b);
Hacl.Bignum.Karatsuba.bn_karatsuba_mul len a b res
Hacl.Bignum.fst.checked
prims.fst.checked LowStar.Ignore.fsti.checked Lib.ByteBuffer.fsti.checked Hacl.Spec.Bignum.fst.checked Hacl.Bignum.Multiplication.fst.checked Hacl.Bignum.Lib.fst.checked Hacl.Bignum.Karatsuba.fst.checked Hacl.Bignum.Convert.fst.checked Hacl.Bignum.Comparison.fst.checked Hacl.Bignum.Addition.fst.checked FStar.UInt32.fsti.checked FStar.ST.fst.checked FStar.Pervasives.fsti.checked
Hacl.Bignum.fst
Hacl.Bignum.Definitions.limb_t Lib.IntTypes.size_t Prims.l_and Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.max_size_t Hacl.Bignum.Definitions.lbignum Lib.IntTypes.op_Plus_Bang Hacl.Bignum.Karatsuba.bn_karatsuba_mul Prims.unit Hacl.Spec.Bignum.bn_karatsuba_mul_lemma Lib.Buffer.as_seq Lib.Buffer.MUT Hacl.Bignum.Definitions.limb FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module Hacl.Bignum

friend Hacl.Spec.Bignum

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

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

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

let bn_add_eq_len #t aLen a b res =
  Hacl.Bignum.Addition.bn_add_eq_len aLen a b res

let bn_sub_eq_len #t aLen a b res =
  Hacl.Bignum.Addition.bn_sub_eq_len aLen a b res

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

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

let bn_reduce_once #t len n c0 res =
  push_frame ();
  let tmp = create len (uint #t 0) in
  let c1 = bn_sub_eq_len len res n tmp in
  let c = c0 -. c1 in
  map2T len res (mask_select c) res tmp;
  pop_frame()

let bn_add_mod_n #t len n a b res =
  let c0 = bn_add_eq_len len a b res in
  bn_reduce_once len n c0 res

let bn_sub_mod_n #t len n a b res =
  push_frame ();
  let c0 = bn_sub_eq_len len a b res in
  let tmp = create len (uint #t 0) in
  let c1 = bn_add_eq_len len res n tmp in
  LowStar.Ignore.ignore c1;
  let c = uint #t 0 -. c0 in
  map2T len res (mask_select c) tmp res;
  pop_frame ()

let bn_mul1 #t aLen a l res =
  Hacl.Bignum.Multiplication.bn_mul1 #t aLen a l res
val bn_karatsuba_mul:
    #t:limb_t
  -> len:size_t{0 < v len /\ 4 * v len <= max_size_t}
  -> a:lbignum t len ->
  bn_karatsuba_mul_st t len a

    len:
      Lib.IntTypes.size_t
        {0 < Lib.IntTypes.v len /\ 4 * Lib.IntTypes.v len <= Lib.IntTypes.max_size_t} ->
    a: Hacl.Bignum.Definitions.lbignum t len
  -> Hacl.Bignum.bn_karatsuba_mul_st t len a