val precomp_base_table_list_rec
      (#t: Type)
      (#a_t: BE.inttype_a)
      (#len: size_t{v len > 0})
      (#ctx_len: size_t)
      (k: mk_precomp_base_table t a_t len ctx_len)
      (g: t)
      (n: nat)
      (acc: g_i_acc_t t a_t len ctx_len 0)
    : Tot (g_i_acc_t t a_t len ctx_len n) (decreases n)
let rec precomp_base_table_list_rec
  (#t:Type) (#a_t:BE.inttype_a) (#len:size_t{v len > 0}) (#ctx_len:size_t)
  (k:mk_precomp_base_table t a_t len ctx_len) (g:t)
  (n:nat) (acc:g_i_acc_t t a_t len ctx_len 0) : Tot (g_i_acc_t t a_t len ctx_len n) (decreases n) =

  if n = 0 then acc
  else precomp_base_table_f k g (n - 1) (precomp_base_table_list_rec k g (n - 1) acc)
val precomp_base_table_list_rec
      (#t: Type)
      (#a_t: BE.inttype_a)
      (#len: size_t{v len > 0})
      (#ctx_len: size_t)
      (k: mk_precomp_base_table t a_t len ctx_len)
      (g: t)
      (n: nat)
      (acc: g_i_acc_t t a_t len ctx_len 0)
    : Tot (g_i_acc_t t a_t len ctx_len n) (decreases n)
let rec precomp_base_table_list_rec
      (#t: Type)
      (#a_t: BE.inttype_a)
      (#len: size_t{v len > 0})
      (#ctx_len: size_t)
      (k: mk_precomp_base_table t a_t len ctx_len)
      (g: t)
      (n: nat)
      (acc: g_i_acc_t t a_t len ctx_len 0)
    : Tot (g_i_acc_t t a_t len ctx_len n) (decreases n) =
if n = 0
then acc
else precomp_base_table_f k g (n - 1) (precomp_base_table_list_rec k g (n - 1) acc)
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 Hacl.Spec.PrecompBaseTable.mk_precomp_base_table Prims.nat Hacl.Spec.PrecompBaseTable.g_i_acc_t Prims.op_Equality Prims.int Prims.bool Hacl.Spec.PrecompBaseTable.precomp_base_table_f Prims.op_Subtraction Hacl.Spec.PrecompBaseTable.precomp_base_table_list_rec
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
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}

inline_for_extraction noextract
let precomp_base_table_f (#t:Type) (#a_t:BE.inttype_a) (#len:size_t{v len > 0}) (#ctx_len:size_t)
  (k:mk_precomp_base_table t a_t len ctx_len) (g:t)
  (i:nat) ((g_i,acc): g_i_acc_t t a_t len ctx_len i) : g_i_acc_t t a_t len ctx_len (i + 1) =
  let acc = FL.(acc @ k.to_list g_i) in
  let g_i = k.concr_ops.SE.mul g_i g in
  g_i, acc


let rec precomp_base_table_list_rec
  (#t:Type) (#a_t:BE.inttype_a) (#len:size_t{v len > 0}) (#ctx_len:size_t)
  (k:mk_precomp_base_table t a_t len ctx_len) (g:t)
  (n:nat) (acc:g_i_acc_t t a_t len ctx_len 0) : Tot (g_i_acc_t t a_t len ctx_len n) (decreases n) =
val precomp_base_table_list_rec
      (#t: Type)
      (#a_t: BE.inttype_a)
      (#len: size_t{v len > 0})
      (#ctx_len: size_t)
      (k: mk_precomp_base_table t a_t len ctx_len)
      (g: t)
      (n: nat)
      (acc: g_i_acc_t t a_t len ctx_len 0)
    : Tot (g_i_acc_t t a_t len ctx_len n) (decreases n)

    k: Hacl.Spec.PrecompBaseTable.mk_precomp_base_table t a_t len ctx_len ->
    g: t ->
    n: Prims.nat ->
    acc: Hacl.Spec.PrecompBaseTable.g_i_acc_t t a_t len ctx_len 0
  -> Prims.Tot (Hacl.Spec.PrecompBaseTable.g_i_acc_t t a_t len ctx_len n)