val bn_mul_:
    #t:limb_t
  -> #aLen:size_nat
  -> #bLen:size_nat{aLen + bLen <= max_size_t}
  -> a:lbignum t aLen
  -> b:lbignum t bLen
  -> j:size_nat{j < bLen}
  -> res:lbignum t (aLen + bLen) ->
  lbignum t (aLen + bLen)
let bn_mul_ #t #aLen #bLen a b j res =
  let c, res = bn_mul1_lshift_add a b.[j] j res in
  res.[aLen + j] <- c
val bn_mul_:
    #t:limb_t
  -> #aLen:size_nat
  -> #bLen:size_nat{aLen + bLen <= max_size_t}
  -> a:lbignum t aLen
  -> b:lbignum t bLen
  -> j:size_nat{j < bLen}
  -> res:lbignum t (aLen + bLen) ->
  lbignum t (aLen + bLen)
let bn_mul_ #t #aLen #bLen a b j res =
let c, res = bn_mul1_lshift_add a b.[ j ] j res in
res.[ aLen + j ] <- c
Hacl.Spec.Bignum.Multiplication.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Lib.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Base.fst.checked FStar.Seq.fst.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.Multiplication.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.max_size_t Hacl.Spec.Bignum.Definitions.lbignum Prims.op_LessThan Hacl.Spec.Bignum.Definitions.limb Lib.Sequence.op_String_Assignment FStar.Pervasives.Native.tuple2 Hacl.Spec.Bignum.Multiplication.bn_mul1_lshift_add Lib.Sequence.op_String_Access
module Hacl.Spec.Bignum.Multiplication

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.Lib


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

val bn_mul1_f:
    #t:limb_t
  -> #aLen:size_nat
  -> a:lbignum t aLen
  -> l:limb t
  -> i:size_nat{i < aLen}
  -> c:limb t ->
  limb t & limb t // carry & out

let bn_mul1_f #t #aLen a l i c =
  mul_wide_add a.[i] l c


val bn_mul1:
    #t:limb_t
  -> #aLen:size_nat
  -> a:lbignum t aLen
  -> l:limb t ->
  limb t & lbignum t aLen

let bn_mul1 #t #aLen a l =
  generate_elems aLen aLen (bn_mul1_f a l) (uint #t 0)


val bn_mul1_add_in_place_f:
    #t:limb_t
  -> #aLen:size_nat
  -> a:lbignum t aLen
  -> l:limb t
  -> acc:lbignum t aLen
  -> i:size_nat{i < aLen}
  -> c:limb t ->
  limb t & limb t // carry & out

let bn_mul1_add_in_place_f #t #aLen a l acc i c =
  mul_wide_add2 a.[i] l c acc.[i]


val bn_mul1_add_in_place:
    #t:limb_t
  -> #aLen:size_nat
  -> a:lbignum t aLen
  -> l:limb t
  -> acc:lbignum t aLen ->
  limb t & lbignum t aLen

let bn_mul1_add_in_place #t #aLen a l acc =
  generate_elems aLen aLen (bn_mul1_add_in_place_f a l acc) (uint #t 0)


val bn_mul1_lshift_add:
    #t:limb_t
  -> #aLen:size_nat
  -> #resLen:size_nat
  -> a:lbignum t aLen
  -> b_j:limb t
  -> j:size_nat{j + aLen <= resLen}
  -> res:lbignum t resLen ->
  limb t & lbignum t resLen

let bn_mul1_lshift_add #t #aLen #resLen a b_j j res =
  let res' = sub res j aLen in
  let c, res' = bn_mul1_add_in_place a b_j res' in
  let res = update_sub res j aLen res' in
  c, res


val bn_mul_:
    #t:limb_t
  -> #aLen:size_nat
  -> #bLen:size_nat{aLen + bLen <= max_size_t}
  -> a:lbignum t aLen
  -> b:lbignum t bLen
  -> j:size_nat{j < bLen}
  -> res:lbignum t (aLen + bLen) ->
  lbignum t (aLen + bLen)
val bn_mul_:
    #t:limb_t
  -> #aLen:size_nat
  -> #bLen:size_nat{aLen + bLen <= max_size_t}
  -> a:lbignum t aLen
  -> b:lbignum t bLen
  -> j:size_nat{j < bLen}
  -> res:lbignum t (aLen + bLen) ->
  lbignum t (aLen + bLen)

    a: Hacl.Spec.Bignum.Definitions.lbignum t aLen ->
    b: Hacl.Spec.Bignum.Definitions.lbignum t bLen ->
    j: Lib.IntTypes.size_nat{j < bLen} ->
    res: Hacl.Spec.Bignum.Definitions.lbignum t (aLen + bLen)
  -> Hacl.Spec.Bignum.Definitions.lbignum t (aLen + bLen)