val concat_ind_seed:
    tmp_seed:lbytes 18ul
  -> i:size_t{v i < maxint U16}
  -> Stack unit
    (requires fun h -> live h tmp_seed)
    (ensures  fun h0 _ h1 -> modifies (loc tmp_seed) h0 h1 /\
      as_seq h1 tmp_seed == LSeq.concat (BSeq.uint_to_bytes_le (u16 (v i))) (LSeq.sub (as_seq h0 tmp_seed) 2 16) /\
      LSeq.sub (as_seq h0 tmp_seed) 2 16 == LSeq.sub (as_seq h1 tmp_seed) 2 16)
let concat_ind_seed tmp_seed i =
  let h0 = ST.get () in
  update_sub_f h0 tmp_seed 0ul 2ul
    (fun h -> BSeq.uint_to_bytes_le (to_u16 i))
    (fun _ -> uint_to_bytes_le (sub tmp_seed 0ul 2ul) (to_u16 i));
  let h1 = ST.get () in
  LSeq.eq_intro
    (as_seq h1 tmp_seed)
    (LSeq.concat (BSeq.uint_to_bytes_le (to_u16 i)) (LSeq.sub (as_seq h0 tmp_seed) 2 16));
  LSeq.eq_intro (LSeq.sub (as_seq h0 tmp_seed) 2 16) (LSeq.sub (as_seq h1 tmp_seed) 2 16)
val concat_ind_seed:
    tmp_seed:lbytes 18ul
  -> i:size_t{v i < maxint U16}
  -> Stack unit
    (requires fun h -> live h tmp_seed)
    (ensures  fun h0 _ h1 -> modifies (loc tmp_seed) h0 h1 /\
      as_seq h1 tmp_seed == LSeq.concat (BSeq.uint_to_bytes_le (u16 (v i))) (LSeq.sub (as_seq h0 tmp_seed) 2 16) /\
      LSeq.sub (as_seq h0 tmp_seed) 2 16 == LSeq.sub (as_seq h1 tmp_seed) 2 16)
let concat_ind_seed tmp_seed i =
let h0 = ST.get () in
update_sub_f h0
  tmp_seed
  0ul
  2ul
  (fun h -> BSeq.uint_to_bytes_le (to_u16 i))
  (fun _ -> uint_to_bytes_le (sub tmp_seed 0ul 2ul) (to_u16 i));
let h1 = ST.get () in
LSeq.eq_intro (as_seq h1 tmp_seed)
  (LSeq.concat (BSeq.uint_to_bytes_le (to_u16 i)) (LSeq.sub (as_seq h0 tmp_seed) 2 16));
LSeq.eq_intro (LSeq.sub (as_seq h0 tmp_seed) 2 16) (LSeq.sub (as_seq h1 tmp_seed) 2 16)
Hacl.Impl.Frodo.Gen.fst.checked
Spec.Frodo.Lemmas.fst.checked Spec.Frodo.Gen.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.SHA3.fst.checked Hacl.Keccak.fsti.checked Hacl.Impl.Matrix.fst.checked Hacl.AES128.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.Frodo.Gen.fst
Hacl.Impl.Matrix.lbytes FStar.UInt32.__uint_to_t Lib.IntTypes.size_t Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.maxint Lib.IntTypes.U16 Lib.Sequence.eq_intro Lib.IntTypes.uint8 Lib.Sequence.sub Lib.Buffer.as_seq Lib.Buffer.MUT Prims.unit Lib.Sequence.concat Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.numbytes Lib.ByteSequence.uint_to_bytes_le Lib.IntTypes.to_u16 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.update_sub_f Lib.Sequence.lseq Lib.ByteBuffer.uint_to_bytes_le Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.mk_int Lib.Buffer.sub
module Hacl.Impl.Frodo.Gen

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

open LowStar.Buffer

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Hacl.Impl.Matrix

module ST = FStar.HyperStack.ST
module B = LowStar.Buffer
module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence
module Loops = Lib.LoopCombinators

module S = Spec.Frodo.Gen
module Lemmas = Spec.Frodo.Lemmas
module SHA3 = Hacl.SHA3

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

inline_for_extraction noextract private
val frodo_gen_matrix_shake0:
    n:size_t{v n * v n <= max_size_t /\ 2 * v n <= max_size_t}
  -> i:size_t{v i < v n}
  -> r:lbytes (size 2 *! n)
  -> j:size_t{v j < v n}
  -> res:matrix_t n n
  -> Stack unit
    (requires fun h -> live h r /\ live h res)
    (ensures  fun h0 _ h1 -> modifies1 res h0 h1 /\
      as_matrix h1 res == S.frodo_gen_matrix_shake0 (v n) (v i) (as_seq h0 r) (v j) (as_matrix h0 res))

let frodo_gen_matrix_shake0 n i r j res =
  let resij = sub r (size 2 *! j) (size 2) in
  mset res i j (uint_from_bytes_le resij)


inline_for_extraction noextract private
val concat_ind_seed:
    tmp_seed:lbytes 18ul
  -> i:size_t{v i < maxint U16}
  -> Stack unit
    (requires fun h -> live h tmp_seed)
    (ensures  fun h0 _ h1 -> modifies (loc tmp_seed) h0 h1 /\
      as_seq h1 tmp_seed == LSeq.concat (BSeq.uint_to_bytes_le (u16 (v i))) (LSeq.sub (as_seq h0 tmp_seed) 2 16) /\
      LSeq.sub (as_seq h0 tmp_seed) 2 16 == LSeq.sub (as_seq h1 tmp_seed) 2 16)
val concat_ind_seed:
    tmp_seed:lbytes 18ul
  -> i:size_t{v i < maxint U16}
  -> Stack unit
    (requires fun h -> live h tmp_seed)
    (ensures  fun h0 _ h1 -> modifies (loc tmp_seed) h0 h1 /\
      as_seq h1 tmp_seed == LSeq.concat (BSeq.uint_to_bytes_le (u16 (v i))) (LSeq.sub (as_seq h0 tmp_seed) 2 16) /\
      LSeq.sub (as_seq h0 tmp_seed) 2 16 == LSeq.sub (as_seq h1 tmp_seed) 2 16)

    tmp_seed: Hacl.Impl.Matrix.lbytes 18ul ->
    i: Lib.IntTypes.size_t{Lib.IntTypes.v i < Lib.IntTypes.maxint Lib.IntTypes.U16}
  -> FStar.HyperStack.ST.Stack Prims.unit