let bn_mul_threshold = 32
let bn_mul_threshold =
32
Hacl.Spec.Bignum.Karatsuba.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Lib.fst.checked Hacl.Spec.Karatsuba.Lemmas.fst.checked Hacl.Spec.Bignum.Squaring.fst.checked Hacl.Spec.Bignum.Multiplication.fst.checked Hacl.Spec.Bignum.Lib.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Base.fst.checked Hacl.Spec.Bignum.Addition.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.Bignum.Karatsuba.fst
module Hacl.Spec.Bignum.Karatsuba

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.LoopCombinators

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

open Hacl.Spec.Bignum.Addition
open Hacl.Spec.Bignum.Multiplication
open Hacl.Spec.Bignum.Squaring

module K = Hacl.Spec.Karatsuba.Lemmas

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val bn_mul_threshold : Prims.int
Prims.int