let lexp_double_fw_loop_st
  (a_t:inttype_a)
  (len:size_t{v len > 0})
  (ctx_len:size_t)
  (k:concrete_ops a_t len ctx_len)
  (l:size_window_t a_t len)
  (table_len:table_len_t len)
  (table_inv1:table_inv_t a_t len table_len)
  (table_inv2:table_inv_t a_t len table_len) =
    ctx:lbuffer (uint_t a_t SEC) ctx_len
  -> a1:lbuffer (uint_t a_t SEC) len
  -> bLen:size_t
  -> bBits:size_t{(v bBits - 1) / bits a_t < v bLen}
  -> b1:lbuffer (uint_t a_t SEC) bLen
  -> a2:lbuffer (uint_t a_t SEC) len
  -> b2:lbuffer (uint_t a_t SEC) bLen
  -> table1:clbuffer (uint_t a_t SEC) (table_len *! len)
  -> table2:clbuffer (uint_t a_t SEC) (table_len *! len)
  -> acc:lbuffer (uint_t a_t SEC) len ->
  Stack unit
  (requires fun h ->
    live h a1 /\ live h b1 /\ live h a2 /\ live h b2 /\
    live h acc /\ live h ctx /\ live h table1 /\ live h table2 /\

    eq_or_disjoint a1 a2 /\ disjoint a1 acc /\ disjoint a1 ctx /\
    disjoint b1 acc /\ disjoint a2 acc /\ disjoint a2 ctx /\
    disjoint b2 acc /\ disjoint acc ctx /\ disjoint acc table1 /\ disjoint acc table2 /\

    BD.bn_v h b1 < pow2 (v bBits) /\
    BD.bn_v h b2 < pow2 (v bBits) /\
    k.to.linv_ctx (as_seq h ctx) /\
    k.to.linv (as_seq h a1) /\ k.to.linv (as_seq h a2) /\
    k.to.linv (as_seq h acc) /\
    table_inv1 (as_seq h a1) (as_seq h table1) /\
    table_inv2 (as_seq h a2) (as_seq h table2))
  (ensures  fun h0 _ h1 -> modifies (loc acc) h0 h1 /\ k.to.linv (as_seq h1 acc) /\
    k.to.refl (as_seq h1 acc) ==
    Loops.repeati (v bBits / v l) (S.exp_double_fw_f k.to.comm_monoid (k.to.refl (as_seq h0 a1))
      (v bBits) (BD.bn_v h0 b1) (k.to.refl (as_seq h0 a2)) (BD.bn_v h0 b2) (v l)) (k.to.refl (as_seq h0 acc)))
let lexp_double_fw_loop_st
      (a_t: inttype_a)
      (len: size_t{v len > 0})
      (ctx_len: size_t)
      (k: concrete_ops a_t len ctx_len)
      (l: size_window_t a_t len)
      (table_len: table_len_t len)
      (table_inv1 table_inv2: table_inv_t a_t len table_len)
     =

    ctx: lbuffer (uint_t a_t SEC) ctx_len ->
    a1: lbuffer (uint_t a_t SEC) len ->
    bLen: size_t ->
    bBits: size_t{(v bBits - 1) / bits a_t < v bLen} ->
    b1: lbuffer (uint_t a_t SEC) bLen ->
    a2: lbuffer (uint_t a_t SEC) len ->
    b2: lbuffer (uint_t a_t SEC) bLen ->
    table1: clbuffer (uint_t a_t SEC) (table_len *! len) ->
    table2: clbuffer (uint_t a_t SEC) (table_len *! len) ->
    acc: lbuffer (uint_t a_t SEC) len
  -> Stack unit
      (requires
        fun h ->
          live h a1 /\ live h b1 /\ live h a2 /\ live h b2 /\ live h acc /\ live h ctx /\
          live h table1 /\ live h table2 /\ eq_or_disjoint a1 a2 /\ disjoint a1 acc /\
          disjoint a1 ctx /\ disjoint b1 acc /\ disjoint a2 acc /\ disjoint a2 ctx /\
          disjoint b2 acc /\ disjoint acc ctx /\ disjoint acc table1 /\ disjoint acc table2 /\
          BD.bn_v h b1 < pow2 (v bBits) /\ BD.bn_v h b2 < pow2 (v bBits) /\
          k.to.linv_ctx (as_seq h ctx) /\ k.to.linv (as_seq h a1) /\ k.to.linv (as_seq h a2) /\
          k.to.linv (as_seq h acc) /\ table_inv1 (as_seq h a1) (as_seq h table1) /\
          table_inv2 (as_seq h a2) (as_seq h table2))
      (ensures
        fun h0 _ h1 ->
          modifies (loc acc) h0 h1 /\ k.to.linv (as_seq h1 acc) /\
          k.to.refl (as_seq h1 acc) ==
          Loops.repeati (v bBits / v l)
            (S.exp_double_fw_f k.to.comm_monoid
                (k.to.refl (as_seq h0 a1))
                (v bBits)
                (BD.bn_v h0 b1)
                (k.to.refl (as_seq h0 a2))
                (BD.bn_v h0 b2)
                (v l))
            (k.to.refl (as_seq h0 acc)))
Hacl.Impl.MultiExponentiation.fst.checked
prims.fst.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.PrecompTable.fsti.checked Hacl.Impl.Exponentiation.fst.checked Hacl.Bignum.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.MultiExponentiation.fst
Hacl.Impl.Exponentiation.Definitions.inttype_a Lib.IntTypes.size_t Prims.b2t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Impl.Exponentiation.Definitions.concrete_ops Hacl.Impl.Exponentiation.size_window_t Hacl.Impl.Exponentiation.table_len_t Hacl.Impl.Exponentiation.table_inv_t Lib.Buffer.lbuffer Lib.IntTypes.uint_t Lib.IntTypes.SEC Prims.op_LessThan Prims.op_Division Prims.op_Subtraction Lib.IntTypes.bits Lib.Buffer.clbuffer Lib.IntTypes.op_Star_Bang Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Lib.Buffer.CONST Lib.Buffer.eq_or_disjoint Lib.Buffer.disjoint Hacl.Bignum.Definitions.bn_v Prims.pow2 Hacl.Impl.Exponentiation.Definitions.__proj__Mkto_comm_monoid__item__linv_ctx FStar.Ghost.reveal Hacl.Impl.Exponentiation.Definitions.to_comm_monoid Hacl.Impl.Exponentiation.Definitions.__proj__Mkconcrete_ops__item__to Lib.Buffer.as_seq Hacl.Impl.Exponentiation.Definitions.__proj__Mkto_comm_monoid__item__linv Lib.Buffer.modifies Lib.Buffer.loc Prims.eq2 Hacl.Impl.Exponentiation.Definitions.__proj__Mkto_comm_monoid__item__a_spec Hacl.Impl.Exponentiation.Definitions.__proj__Mkto_comm_monoid__item__refl Lib.LoopCombinators.repeati Lib.Exponentiation.exp_double_fw_f Hacl.Impl.Exponentiation.Definitions.__proj__Mkto_comm_monoid__item__comm_monoid
module Hacl.Impl.MultiExponentiation

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module Loops = Lib.LoopCombinators

module S = Lib.Exponentiation
module BD = Hacl.Bignum.Definitions
module PT = Hacl.Impl.PrecompTable

friend Hacl.Impl.Exponentiation

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

inline_for_extraction noextract
let lexp_double_fw_f_st
  (a_t:inttype_a)
  (len:size_t{v len > 0})
  (ctx_len:size_t)
  (k:concrete_ops a_t len ctx_len)
  (l:size_window_t a_t len)
  (table_len:table_len_t len)
  (table_inv1:table_inv_t a_t len table_len)
  (table_inv2:table_inv_t a_t len table_len) =
    ctx:lbuffer (uint_t a_t SEC) ctx_len
  -> a1:lbuffer (uint_t a_t SEC) len
  -> bLen:size_t
  -> bBits:size_t{(v bBits - 1) / bits a_t < v bLen}
  -> b1:lbuffer (uint_t a_t SEC) bLen
  -> a2:lbuffer (uint_t a_t SEC) len
  -> b2:lbuffer (uint_t a_t SEC) bLen
  -> table1:clbuffer (uint_t a_t SEC) (table_len *! len)
  -> table2:clbuffer (uint_t a_t SEC) (table_len *! len)
  -> i:size_t{v i < v bBits / v l}
  -> acc:lbuffer (uint_t a_t SEC) len
  -> tmp:lbuffer (uint_t a_t SEC) len ->
  Stack unit
  (requires fun h ->
    live h a1 /\ live h b1 /\ live h a2 /\ live h b2 /\
    live h acc /\ live h ctx /\ live h table1 /\ live h table2 /\

    live h tmp /\ disjoint tmp a1 /\ disjoint tmp a2 /\
    disjoint tmp b1 /\ disjoint tmp b2 /\ disjoint tmp acc /\
    disjoint tmp ctx /\ disjoint tmp table1 /\ disjoint tmp table2 /\

    eq_or_disjoint a1 a2 /\ disjoint a1 acc /\ disjoint a1 ctx /\
    disjoint b1 acc /\ disjoint a2 acc /\ disjoint a2 ctx /\
    disjoint b2 acc /\ disjoint acc ctx /\ disjoint acc table1 /\ disjoint acc table2 /\

    BD.bn_v h b1 < pow2 (v bBits) /\
    BD.bn_v h b2 < pow2 (v bBits) /\
    k.to.linv_ctx (as_seq h ctx) /\
    k.to.linv (as_seq h a1) /\ k.to.linv (as_seq h a2) /\
    k.to.linv (as_seq h acc) /\
    table_inv1 (as_seq h a1) (as_seq h table1) /\
    table_inv2 (as_seq h a2) (as_seq h table2))
  (ensures  fun h0 _ h1 -> modifies (loc acc |+| loc tmp) h0 h1 /\
    k.to.linv (as_seq h1 acc) /\
    k.to.refl (as_seq h1 acc) ==
    S.exp_double_fw_f #k.to.a_spec k.to.comm_monoid
      (k.to.refl (as_seq h0 a1)) (v bBits) (BD.bn_v h0 b1)
      (k.to.refl (as_seq h0 a2)) (BD.bn_v h0 b2) (v l) (v i) (k.to.refl (as_seq h0 acc)))


inline_for_extraction noextract
val lexp_double_fw_f:
    #a_t:inttype_a
  -> len:size_t{v len > 0}
  -> ctx_len:size_t
  -> k:concrete_ops a_t len ctx_len
  -> l:size_window_t a_t len
  -> table_len:table_len_t len
  -> table_inv1:table_inv_t a_t len table_len
  -> table_inv2:table_inv_t a_t len table_len
  -> pow_a_to_small_b1:pow_a_to_small_b_st a_t len ctx_len k l table_len table_inv1
  -> pow_a_to_small_b2:pow_a_to_small_b_st a_t len ctx_len k l table_len table_inv2 ->
  lexp_double_fw_f_st a_t len ctx_len k l table_len table_inv1 table_inv2

let lexp_double_fw_f #a_t len ctx_len k l table_len table_inv1 table_inv2
  pow_a_to_small_b1 pow_a_to_small_b2 ctx a1 bLen bBits b1 a2 b2 table1 table2 i acc tmp =
  lexp_fw_f len ctx_len k l table_len table_inv2 pow_a_to_small_b2 ctx a2 bLen bBits b2 table2 i acc tmp;
  lmul_acc_pow_a_bits_l len ctx_len k l table_len table_inv1 pow_a_to_small_b1 ctx a1 bLen bBits b1 table1 i acc tmp


inline_for_extraction noextract
let lexp_double_fw_acc0_st
  (a_t:inttype_a)
  (len:size_t{v len > 0})
  (ctx_len:size_t)
  (k:concrete_ops a_t len ctx_len)
  (l:size_window_t a_t len)
  (table_len:table_len_t len)
  (table_inv1:table_inv_t a_t len table_len)
  (table_inv2:table_inv_t a_t len table_len) =
    ctx:lbuffer (uint_t a_t SEC) ctx_len
  -> a1:lbuffer (uint_t a_t SEC) len
  -> bLen:size_t
  -> bBits:size_t{0 < v bBits /\ (v bBits - 1) / bits a_t < v bLen}
  -> b1:lbuffer (uint_t a_t SEC) bLen
  -> a2:lbuffer (uint_t a_t SEC) len
  -> b2:lbuffer (uint_t a_t SEC) bLen
  -> table1:clbuffer (uint_t a_t SEC) (table_len *! len)
  -> table2:clbuffer (uint_t a_t SEC) (table_len *! len)
  -> acc:lbuffer (uint_t a_t SEC) len ->
  Stack unit
  (requires fun h -> v bBits % v l <> 0 /\
    live h a1 /\ live h b1 /\ live h a2 /\ live h b2 /\
    live h acc /\ live h ctx /\ live h table1 /\ live h table2 /\

    eq_or_disjoint a1 a2 /\ disjoint a1 acc /\ disjoint a1 ctx /\
    disjoint b1 acc /\ disjoint a2 acc /\ disjoint a2 ctx /\
    disjoint b2 acc /\ disjoint acc ctx /\ disjoint acc table1 /\ disjoint acc table2 /\

    BD.bn_v h b1 < pow2 (v bBits) /\
    BD.bn_v h b2 < pow2 (v bBits) /\
    k.to.linv_ctx (as_seq h ctx) /\
    k.to.linv (as_seq h a1) /\ k.to.linv (as_seq h a2) /\
    table_inv1 (as_seq h a1) (as_seq h table1) /\
    table_inv2 (as_seq h a2) (as_seq h table2))
  (ensures  fun h0 _ h1 -> modifies (loc acc) h0 h1 /\
    k.to.linv (as_seq h1 acc) /\
    k.to.refl (as_seq h1 acc) ==
    S.exp_double_fw_acc0 #k.to.a_spec k.to.comm_monoid
      (k.to.refl (as_seq h0 a1)) (v bBits) (BD.bn_v h0 b1)
      (k.to.refl (as_seq h0 a2)) (BD.bn_v h0 b2) (v l))


inline_for_extraction noextract
val lexp_double_fw_acc0:
    #a_t:inttype_a
  -> len:size_t{v len > 0}
  -> ctx_len:size_t
  -> k:concrete_ops a_t len ctx_len
  -> l:size_window_t a_t len
  -> table_len:table_len_t len
  -> table_inv1:table_inv_t a_t len table_len
  -> table_inv2:table_inv_t a_t len table_len
  -> pow_a_to_small_b1:pow_a_to_small_b_st a_t len ctx_len k l table_len table_inv1
  -> pow_a_to_small_b2:pow_a_to_small_b_st a_t len ctx_len k l table_len table_inv2 ->
  lexp_double_fw_acc0_st a_t len ctx_len k l table_len table_inv1 table_inv2

let lexp_double_fw_acc0 #a_t len ctx_len k l table_len table_inv1 table_inv2 pow_a_to_small_b1 pow_a_to_small_b2 ctx a1 bLen bBits b1 a2 b2 table1 table2 acc =
  push_frame ();
  let tmp = create len (uint #a_t #SEC 0) in
  lexp_fw_acc0 len ctx_len k l table_len table_inv1 pow_a_to_small_b1 ctx a1 bLen bBits b1 table1 acc;
  lexp_fw_acc0 len ctx_len k l table_len table_inv2 pow_a_to_small_b2 ctx a2 bLen bBits b2 table2 tmp;
  k.lmul ctx acc tmp acc;
  pop_frame ()


inline_for_extraction noextract
let lexp_double_fw_loop_st
  (a_t:inttype_a)
  (len:size_t{v len > 0})
  (ctx_len:size_t)
  (k:concrete_ops a_t len ctx_len)
  (l:size_window_t a_t len)
  (table_len:table_len_t len)
  (table_inv1:table_inv_t a_t len table_len)
val lexp_double_fw_loop_st : a_t: Hacl.Impl.Exponentiation.Definitions.inttype_a ->
    len: Lib.IntTypes.size_t{Lib.IntTypes.v len > 0} ->
    ctx_len: Lib.IntTypes.size_t ->
    k: Hacl.Impl.Exponentiation.Definitions.concrete_ops a_t len ctx_len ->
    l: Hacl.Impl.Exponentiation.size_window_t a_t len ->
    table_len: Hacl.Impl.Exponentiation.table_len_t len ->
    table_inv1: Hacl.Impl.Exponentiation.table_inv_t a_t len table_len ->
    table_inv2: Hacl.Impl.Exponentiation.table_inv_t a_t len table_len
  -> Type0

    a_t: Hacl.Impl.Exponentiation.Definitions.inttype_a ->
    len: Lib.IntTypes.size_t{Lib.IntTypes.v len > 0} ->
    ctx_len: Lib.IntTypes.size_t ->
    k: Hacl.Impl.Exponentiation.Definitions.concrete_ops a_t len ctx_len ->
    l: Hacl.Impl.Exponentiation.size_window_t a_t len ->
    table_len: Hacl.Impl.Exponentiation.table_len_t len ->
    table_inv1: Hacl.Impl.Exponentiation.table_inv_t a_t len table_len ->
    table_inv2: Hacl.Impl.Exponentiation.table_inv_t a_t len table_len
  -> Type0