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
let bn_mul1_f #t #aLen a l i c =
  mul_wide_add a.[i] l c
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
let bn_mul1_f #t #aLen a l i c =
mul_wide_add a.[ i ] l 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 Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Definitions.limb Prims.b2t Prims.op_LessThan Hacl.Spec.Bignum.Base.mul_wide_add Lib.Sequence.op_String_Access FStar.Pervasives.Native.tuple2
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
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

    a: Hacl.Spec.Bignum.Definitions.lbignum t aLen ->
    l: Hacl.Spec.Bignum.Definitions.limb t ->
    i: Lib.IntTypes.size_nat{i < aLen} ->
    c: Hacl.Spec.Bignum.Definitions.limb t
  -> Hacl.Spec.Bignum.Definitions.limb t * Hacl.Spec.Bignum.Definitions.limb t