val table_select_consttime_f:
    #t:BD.limb_t
  -> len:size_t{v len > 0}
  -> table_len:size_t{1 < v table_len /\ v table_len * v len <= max_size_t}
  -> table:clbuffer (uint_t t SEC) (table_len *! len)
  -> i:uint_t t SEC{v i < v table_len}
  -> j:size_t{v j < v table_len - 1}
  -> acc:lbuffer (uint_t t SEC) len ->
  Stack unit
  (requires fun h ->
    live h table /\ live h acc /\ disjoint table acc)
  (ensures  fun h0 _ h1 -> modifies (loc acc) h0 h1 /\
    as_seq h1 acc ==
    PT.table_select_f (v len) (v table_len) (as_seq h0 table) i (v j) (as_seq h0 acc))
let table_select_consttime_f #t len table_len table i j acc =
  let c = eq_mask i (BB.size_to_limb (j +! 1ul)) in
  let res_j = table_sub_len len table_len table (j +! 1ul) in
  map2T len acc (BB.mask_select c) res_j acc
val table_select_consttime_f:
    #t:BD.limb_t
  -> len:size_t{v len > 0}
  -> table_len:size_t{1 < v table_len /\ v table_len * v len <= max_size_t}
  -> table:clbuffer (uint_t t SEC) (table_len *! len)
  -> i:uint_t t SEC{v i < v table_len}
  -> j:size_t{v j < v table_len - 1}
  -> acc:lbuffer (uint_t t SEC) len ->
  Stack unit
  (requires fun h ->
    live h table /\ live h acc /\ disjoint table acc)
  (ensures  fun h0 _ h1 -> modifies (loc acc) h0 h1 /\
    as_seq h1 acc ==
    PT.table_select_f (v len) (v table_len) (as_seq h0 table) i (v j) (as_seq h0 acc))
let table_select_consttime_f #t len table_len table i j acc =
let c = eq_mask i (BB.size_to_limb (j +! 1ul)) in
let res_j = table_sub_len len table_len table (j +! 1ul) in
map2T len acc (BB.mask_select c) res_j acc
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 Lib.IntTypes.size_t Prims.b2t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.l_and Prims.op_LessThan Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.max_size_t Lib.Buffer.clbuffer Lib.IntTypes.uint_t Lib.IntTypes.SEC Lib.IntTypes.op_Star_Bang Prims.op_Subtraction Lib.Buffer.lbuffer Lib.Buffer.map2T Lib.Buffer.CONST Lib.Buffer.MUT Hacl.Spec.Bignum.Base.mask_select Prims.unit Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Hacl.Impl.PrecompTable.table_sub_len Lib.IntTypes.op_Plus_Bang FStar.UInt32.__uint_to_t Lib.IntTypes.eq_mask Hacl.Spec.Bignum.Base.size_to_limb
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) =

  lemma_table_sub_len len table_len i;
  LSeq.update_sub table (i * len) len b


inline_for_extraction noextract
val table_update_sub_len:
    #t:BD.limb_t
  -> len:size_t{v len > 0}
  -> table_len:size_t{v table_len * v len <= max_size_t}
  -> table:lbuffer (uint_t t SEC) (table_len *! len)
  -> i:size_t{v i < v table_len}
  -> b:lbuffer (uint_t t SEC) len ->
  Stack unit
  (requires fun h ->
    live h table /\ live h b /\ disjoint table b)
  (ensures  fun h0 r h1 -> modifies (loc table) h0 h1 /\
    as_seq h1 table ==
    spec_table_update_sub_len (v len) (v table_len) (as_seq h0 table) (v i) (as_seq h0 b))

let table_update_sub_len #t len table_len table i b =
  lemma_table_sub_len (v len) (v table_len) (v i);
  update_sub table (i *! len) len b

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

inline_for_extraction noextract
val table_select_consttime_f:
    #t:BD.limb_t
  -> len:size_t{v len > 0}
  -> table_len:size_t{1 < v table_len /\ v table_len * v len <= max_size_t}
  -> table:clbuffer (uint_t t SEC) (table_len *! len)
  -> i:uint_t t SEC{v i < v table_len}
  -> j:size_t{v j < v table_len - 1}
  -> acc:lbuffer (uint_t t SEC) len ->
  Stack unit
  (requires fun h ->
    live h table /\ live h acc /\ disjoint table acc)
  (ensures  fun h0 _ h1 -> modifies (loc acc) h0 h1 /\
    as_seq h1 acc ==
    PT.table_select_f (v len) (v table_len) (as_seq h0 table) i (v j) (as_seq h0 acc))
val table_select_consttime_f:
    #t:BD.limb_t
  -> len:size_t{v len > 0}
  -> table_len:size_t{1 < v table_len /\ v table_len * v len <= max_size_t}
  -> table:clbuffer (uint_t t SEC) (table_len *! len)
  -> i:uint_t t SEC{v i < v table_len}
  -> j:size_t{v j < v table_len - 1}
  -> acc:lbuffer (uint_t t SEC) len ->
  Stack unit
  (requires fun h ->
    live h table /\ live h acc /\ disjoint table acc)
  (ensures  fun h0 _ h1 -> modifies (loc acc) h0 h1 /\
    as_seq h1 acc ==
    PT.table_select_f (v len) (v table_len) (as_seq h0 table) i (v j) (as_seq h0 acc))

    len: Lib.IntTypes.size_t{Lib.IntTypes.v len > 0} ->
    table_len:
      Lib.IntTypes.size_t
        { 1 < Lib.IntTypes.v table_len /\
          Lib.IntTypes.v table_len * Lib.IntTypes.v len <= Lib.IntTypes.max_size_t } ->
    table: Lib.Buffer.clbuffer (Lib.IntTypes.uint_t t Lib.IntTypes.SEC) (table_len *! len) ->
    i: Lib.IntTypes.uint_t t Lib.IntTypes.SEC {Lib.IntTypes.v i < Lib.IntTypes.v table_len} ->
    j: Lib.IntTypes.size_t{Lib.IntTypes.v j < Lib.IntTypes.v table_len - 1} ->
    acc: Lib.Buffer.lbuffer (Lib.IntTypes.uint_t t Lib.IntTypes.SEC) len
  -> FStar.HyperStack.ST.Stack Prims.unit