val spec_table_update_sub_len
      (#t: BD.limb_t)
      (len: pos)
      (table_len: size_nat{table_len * len <= max_size_t})
      (table: LSeq.lseq (uint_t t SEC) (table_len * len))
      (i: nat{i < table_len})
      (b: LSeq.lseq (uint_t t SEC) len)
    : LSeq.lseq (uint_t t SEC) (table_len * len)
let spec_table_update_sub_len
  (#t:BD.limb_t)
  (len:pos)
  (table_len:size_nat{table_len * len <= max_size_t})
  (table:LSeq.lseq (uint_t t SEC) (table_len * len))
  (i:nat{i < table_len})
  (b:LSeq.lseq (uint_t t SEC) len) : LSeq.lseq (uint_t t SEC) (table_len * len) =

  lemma_table_sub_len len table_len i;
  LSeq.update_sub table (i * len) len b
val spec_table_update_sub_len
      (#t: BD.limb_t)
      (len: pos)
      (table_len: size_nat{table_len * len <= max_size_t})
      (table: LSeq.lseq (uint_t t SEC) (table_len * len))
      (i: nat{i < table_len})
      (b: LSeq.lseq (uint_t t SEC) len)
    : LSeq.lseq (uint_t t SEC) (table_len * len)
let spec_table_update_sub_len
      (#t: BD.limb_t)
      (len: pos)
      (table_len: size_nat{table_len * len <= max_size_t})
      (table: LSeq.lseq (uint_t t SEC) (table_len * len))
      (i: nat{i < table_len})
      (b: LSeq.lseq (uint_t t SEC) len)
    : LSeq.lseq (uint_t t SEC) (table_len * len) =
lemma_table_sub_len len table_len i;
LSeq.update_sub table (i * len) len b
Hacl.Impl.PrecompTable.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.Definition.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.PrecompTable.fst.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.Base.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked
Hacl.Impl.PrecompTable.fst
Hacl.Bignum.Definitions.limb_t Prims.pos Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.max_size_t Lib.Sequence.lseq Lib.IntTypes.uint_t Lib.IntTypes.SEC Prims.nat Prims.op_LessThan Lib.Sequence.update_sub Prims.unit Hacl.Impl.PrecompTable.lemma_table_sub_len
module Hacl.Impl.PrecompTable

open FStar.Mul

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

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module B = LowStar.Buffer

module LSeq = Lib.Sequence
module Loops = Lib.LoopCombinators

module BB = Hacl.Bignum.Base
module BD = Hacl.Bignum.Definitions
module PT = Hacl.Spec.PrecompTable
module S = Lib.Exponentiation.Definition

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

// val lemma_table_sub_len: len:nat -> table_len:nat -> i:nat{i < table_len} ->
//   Lemma (i * len + len <= table_len * len)
let lemma_table_sub_len len table_len i =
  Math.Lemmas.distributivity_add_left i 1 len;
  Math.Lemmas.lemma_mult_le_right len (i + 1) table_len

inline_for_extraction noextract
let table_gsub_len
  (#bt:buftype)
  (#t:BD.limb_t)
  (len:size_t{v len > 0})
  (table_len:size_t{v table_len * v len <= max_size_t})
  (table:lbuffer_t bt (uint_t t SEC) (table_len *! len))
  (i:size_t{v i < v table_len}) : GTot (lbuffer_t bt (uint_t t SEC) len) =

  lemma_table_sub_len (v len) (v table_len) (v i);
  gsub table (i *! len) len


inline_for_extraction noextract
val table_sub_len:
    #bt:buftype
  -> #t:BD.limb_t
  -> len:size_t{v len > 0}
  -> table_len:size_t{v table_len * v len <= max_size_t}
  -> table:lbuffer_t bt (uint_t t SEC) (table_len *! len)
  -> i:size_t{v i < v table_len} ->
  Stack (lbuffer_t bt (uint_t t SEC) len)
  (requires fun h -> live h table)
  (ensures  fun h0 r h1 -> h0 == h1 /\ live h1 r /\
    r == table_gsub_len len table_len table i /\
    as_seq h1 r == spec_table_sub_len (v len) (v table_len) (as_seq h0 table) (v i) /\
    B.loc_includes (loc table) (loc r))

let table_sub_len #t len table_len table i =
  lemma_table_sub_len (v len) (v table_len) (v i);
  sub table (i *! len) len

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

inline_for_extraction noextract
let spec_table_update_sub_len
  (#t:BD.limb_t)
  (len:pos)
  (table_len:size_nat{table_len * len <= max_size_t})
  (table:LSeq.lseq (uint_t t SEC) (table_len * len))
  (i:nat{i < table_len})
  (b:LSeq.lseq (uint_t t SEC) len) : LSeq.lseq (uint_t t SEC) (table_len * len) =
val spec_table_update_sub_len
      (#t: BD.limb_t)
      (len: pos)
      (table_len: size_nat{table_len * len <= max_size_t})
      (table: LSeq.lseq (uint_t t SEC) (table_len * len))
      (i: nat{i < table_len})
      (b: LSeq.lseq (uint_t t SEC) len)
    : LSeq.lseq (uint_t t SEC) (table_len * len)

    len: Prims.pos ->
    table_len: Lib.IntTypes.size_nat{table_len * len <= Lib.IntTypes.max_size_t} ->
    table: Lib.Sequence.lseq (Lib.IntTypes.uint_t t Lib.IntTypes.SEC) (table_len * len) ->
    i: Prims.nat{i < table_len} ->
    b: Lib.Sequence.lseq (Lib.IntTypes.uint_t t Lib.IntTypes.SEC) len
  -> Lib.Sequence.lseq (Lib.IntTypes.uint_t t Lib.IntTypes.SEC) (table_len * len)