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)
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)
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
Lib.IntTypes.size_t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.max_size_t Prims.op_LessThan Hacl.Impl.Matrix.lbytes Lib.IntTypes.op_Star_Bang Lib.IntTypes.size Hacl.Impl.Matrix.matrix_t Hacl.Impl.Matrix.mset Prims.unit Lib.IntTypes.int_t Lib.IntTypes.U16 Lib.IntTypes.SEC Lib.ByteBuffer.uint_from_bytes_le Lib.IntTypes.uint_t Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.U8 Lib.IntTypes.mk_int Lib.Buffer.sub Lib.IntTypes.uint8
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))
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))

    n:
      Lib.IntTypes.size_t
        { Lib.IntTypes.v n * Lib.IntTypes.v n <= Lib.IntTypes.max_size_t /\
          2 * Lib.IntTypes.v n <= Lib.IntTypes.max_size_t } ->
    i: Lib.IntTypes.size_t{Lib.IntTypes.v i < Lib.IntTypes.v n} ->
    r: Hacl.Impl.Matrix.lbytes (Lib.IntTypes.size 2 *! n) ->
    j: Lib.IntTypes.size_t{Lib.IntTypes.v j < Lib.IntTypes.v n} ->
    res: Hacl.Impl.Matrix.matrix_t n n
  -> FStar.HyperStack.ST.Stack Prims.unit