let max_table_len_t (len:size_t) = n:nat{(n + 1) * v len <= max_size_t}
let max_table_len_t (len: size_t) =
n: nat{(n + 1) * v len <= max_size_t}
Hacl.Spec.PrecompBaseTable.fst.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.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.PrecompBaseTable.fst
Lib.IntTypes.size_t Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.max_size_t
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"

#push-options "--fuel 2"
val list_append_index1: #a:Type -> x:list a -> y:list a -> i:nat{i < FL.length x} ->
  Lemma (ensures (FL.(index (x @ y)) i == FL.index x i)) (decreases (FL.length x))

let rec list_append_index1 #a x y i =
  match x with
  | [] -> ()
  | hd::tl -> if i = 0 then () else list_append_index1 tl y (i - 1)


val list_append_index2: #a:Type -> x:list a -> y:list a -> i:nat{FL.length x <= i /\ i < FL.length x + FL.length y} ->
  Lemma (ensures (FL.(index (x @ y)) i == FL.index y (i - FL.length x))) (decreases (FL.length x))

let rec list_append_index2 #a x y i =
  match x with
  | [] -> ()
  | hd::tl -> list_append_index2 tl y (i - 1)
#pop-options


val list_append_index: #a:Type -> x:list a -> y:list a -> i:nat{i < FL.length x + FL.length y} ->
  Lemma (FL.(index (x @ y)) i ==
    (if i < FL.length x then FL.index x i else FL.index y (i - FL.length x)))

let list_append_index #a x y i =
  if i < FL.length x then list_append_index1 x y i else list_append_index2 x y i


let seq_of_list_append_lemma #a x y =
  let xy = FL.(x @ y) in
  let x_lseq = Seq.seq_of_list x in
  let y_lseq = Seq.seq_of_list y in
  let xy_lseq = Seq.seq_of_list xy in
  let x_len = FL.length x in
  let y_len = FL.length y in

  let lemma_x_lseq (i:nat{i < x_len}) : Lemma (Seq.index xy_lseq i == Seq.index x_lseq i) =
    list_append_index x y i in

  FStar.Classical.forall_intro lemma_x_lseq;
  Seq.lemma_eq_intro (Seq.slice xy_lseq 0 x_len) x_lseq;
  assert (Seq.slice xy_lseq 0 x_len == x_lseq);

  let lemma_y_lseq (i:nat{i < y_len}) :
    Lemma (Seq.index xy_lseq (x_len + i) == Seq.index y_lseq i) =
    list_append_index x y (x_len + i) in

  FStar.Classical.forall_intro lemma_y_lseq;
  Seq.lemma_eq_intro (Seq.slice xy_lseq x_len (x_len + y_len)) y_lseq;
  assert (Seq.slice xy_lseq x_len (x_len + y_len) == y_lseq)

//-----------------------------------

#push-options "--fuel 1"
val eq_precomp_base_table_list_rec0
  (#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) :
  Lemma (precomp_base_table_list_rec k g 0 acc == acc)

let eq_precomp_base_table_list_rec0 #t #a_t #len #ctx_len k g n acc = ()

val unroll_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:pos) (acc:g_i_acc_t t a_t len ctx_len 0) :
  Lemma (precomp_base_table_list_rec k g n acc ==
    precomp_base_table_f k g (n - 1) (precomp_base_table_list_rec k g (n - 1) acc))

let unroll_precomp_base_table_list_rec #t #a_t #len #ctx_len k g n acc = ()
#pop-options

//--------------------------------------------

val precomp_base_table_acc_inv0
  (#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) :
  Lemma (precomp_base_table_acc_inv k g 1 (Seq.seq_of_list (k.to_list (k.concr_ops.SE.one ()))) 0)

let precomp_base_table_acc_inv0 #t #a_t #len #ctx_len k g =
  let table = Seq.seq_of_list (k.to_list (k.concr_ops.SE.one ())) <:
    LSeq.lseq (uint_t a_t SEC) (v len) in
  let bj = LSeq.sub table 0 (v len) in
  assert (bj == table);

  assert (k.to_cm.BE.linv bj);
  k.lemma_refl (k.concr_ops.SE.one ());
  assert (k.to_cm.BE.refl (Seq.seq_of_list (k.to_list (k.concr_ops.SE.one ()))) ==
    k.concr_ops.SE.to.SE.refl (k.concr_ops.SE.one ()));
  assert (k.concr_ops.SE.to.SE.refl (k.concr_ops.SE.one ()) ==
    k.concr_ops.SE.to.SE.comm_monoid.LE.one);

  LE.lemma_pow0 k.concr_ops.SE.to.comm_monoid (k.concr_ops.SE.to.refl g)
val max_table_len_t : len: Lib.IntTypes.size_t -> Type0
len: Lib.IntTypes.size_t -> Type0