let g_i_acc_t (t:Type) (a_t:BE.inttype_a) (len:size_t{v len > 0}) (ctx_len:size_t) (i:nat) =
  t & acc:list (uint_t a_t SEC){FL.length acc == (i + 1) * v len}
let g_i_acc_t (t: Type) (a_t: BE.inttype_a) (len: size_t{v len > 0}) (ctx_len: size_t) (i: nat) =
t & acc: list (uint_t a_t SEC) {FL.length acc == (i + 1) * v len}
Hacl.Spec.PrecompBaseTable.fsti.checked
Spec.Exponentiation.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.Definition.fsti.checked Hacl.Impl.Exponentiation.Definitions.fst.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked
Hacl.Spec.PrecompBaseTable.fsti
Hacl.Impl.Exponentiation.Definitions.inttype_a Lib.IntTypes.size_t Prims.b2t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.nat FStar.Pervasives.Native.tuple2 Prims.list Lib.IntTypes.uint_t Lib.IntTypes.SEC Prims.eq2 Prims.int FStar.List.Tot.Base.length FStar.Mul.op_Star Prims.op_Addition
module Hacl.Spec.PrecompBaseTable

open FStar.Mul
open Lib.IntTypes

module FL = FStar.List.Tot
module LSeq = Lib.Sequence

module LE = Lib.Exponentiation.Definition
module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation.Definitions

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

inline_for_extraction noextract
class mk_precomp_base_table (t:Type) (a_t:BE.inttype_a) (len:size_t{v len > 0}) (ctx_len:size_t) = {
  concr_ops: SE.concrete_ops t;
  to_cm: x:BE.to_comm_monoid a_t len ctx_len{x.BE.a_spec == concr_ops.SE.to.SE.a_spec};
  to_list: t -> x:list (uint_t a_t SEC){FL.length x = v len /\ to_cm.BE.linv (Seq.seq_of_list x)};
  lemma_refl: x:t ->
    Lemma (concr_ops.SE.to.SE.refl x == to_cm.BE.refl (Seq.seq_of_list (to_list x)));
}


inline_for_extraction noextract
val g_i_acc_t : t: Type ->
    a_t: Hacl.Impl.Exponentiation.Definitions.inttype_a ->
    len: Lib.IntTypes.size_t{Lib.IntTypes.v len > 0} ->
    ctx_len: Lib.IntTypes.size_t ->
    i: Prims.nat
  -> Type

    t: Type ->
    a_t: Hacl.Impl.Exponentiation.Definitions.inttype_a ->
    len: Lib.IntTypes.size_t{Lib.IntTypes.v len > 0} ->
    ctx_len: Lib.IntTypes.size_t ->
    i: Prims.nat
  -> Type