val frodo_shake_r:
    a:FP.frodo_alg
  -> c:uint8
  -> seed_se:lbytes (crypto_bytes a)
  -> output_len:size_t
  -> r:lbytes output_len
  -> Stack unit
    (requires fun h ->
      live h seed_se /\ live h r /\ disjoint seed_se r)
    (ensures  fun h0 _ h1 -> modifies (loc r) h0 h1 /\
      as_seq h1 r == S.frodo_shake_r a c (as_seq h0 seed_se) (v output_len))
let frodo_shake_r a c seed_se output_len r =
  push_frame ();
  let h0 = ST.get () in
  let shake_input_seed_se = create (1ul +! crypto_bytes a) (u8 0) in
  shake_input_seed_se.(0ul) <- c;
  update_sub shake_input_seed_se 1ul (crypto_bytes a) seed_se;
  let h2 = ST.get () in
  LSeq.eq_intro (LSeq.sub (as_seq h2 shake_input_seed_se) 0 1) (LSeq.create 1 c);
  LSeq.eq_intro (LSeq.sub (as_seq h2 shake_input_seed_se) 1 (v (crypto_bytes a))) (as_seq h0 seed_se);
  LSeq.eq_intro (LSeq.concat (LSeq.create 1 c) (as_seq h0 seed_se)) (as_seq h2 shake_input_seed_se);
  frodo_shake a (1ul +! crypto_bytes a) shake_input_seed_se output_len r;
  clear_words_u8 shake_input_seed_se;
  pop_frame ()
val frodo_shake_r:
    a:FP.frodo_alg
  -> c:uint8
  -> seed_se:lbytes (crypto_bytes a)
  -> output_len:size_t
  -> r:lbytes output_len
  -> Stack unit
    (requires fun h ->
      live h seed_se /\ live h r /\ disjoint seed_se r)
    (ensures  fun h0 _ h1 -> modifies (loc r) h0 h1 /\
      as_seq h1 r == S.frodo_shake_r a c (as_seq h0 seed_se) (v output_len))
let frodo_shake_r a c seed_se output_len r =
push_frame ();
let h0 = ST.get () in
let shake_input_seed_se = create (1ul +! crypto_bytes a) (u8 0) in
shake_input_seed_se.(0ul) <- c;
update_sub shake_input_seed_se 1ul (crypto_bytes a) seed_se;
let h2 = ST.get () in
LSeq.eq_intro (LSeq.sub (as_seq h2 shake_input_seed_se) 0 1) (LSeq.create 1 c);
LSeq.eq_intro (LSeq.sub (as_seq h2 shake_input_seed_se) 1 (v (crypto_bytes a))) (as_seq h0 seed_se);
LSeq.eq_intro (LSeq.concat (LSeq.create 1 c) (as_seq h0 seed_se)) (as_seq h2 shake_input_seed_se);
frodo_shake a (1ul +! crypto_bytes a) shake_input_seed_se output_len r;
clear_words_u8 shake_input_seed_se;
pop_frame ()
Hacl.Impl.Frodo.KEM.KeyGen.fst.checked
Spec.Matrix.fst.checked Spec.Frodo.Params.fst.checked Spec.Frodo.KEM.KeyGen.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Matrix.fst.checked Hacl.Impl.Frodo.Sample.fst.checked Hacl.Impl.Frodo.Params.fst.checked Hacl.Impl.Frodo.Pack.fst.checked Hacl.Impl.Frodo.KEM.fst.checked Hacl.Frodo.Random.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.Frodo.KEM.KeyGen.fst
Spec.Frodo.Params.frodo_alg Lib.IntTypes.uint8 Hacl.Impl.Matrix.lbytes Hacl.Impl.Frodo.Params.crypto_bytes Lib.IntTypes.size_t FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.Frodo.KEM.clear_words_u8 Lib.IntTypes.op_Plus_Bang Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.UInt32.__uint_to_t Hacl.Impl.Frodo.Params.frodo_shake Lib.Sequence.eq_intro Prims.op_Addition Lib.IntTypes.v Lib.Sequence.concat Lib.Sequence.create Lib.Buffer.as_seq Lib.Buffer.MUT Lib.Sequence.sub FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.update_sub Lib.Buffer.op_Array_Assignment Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.add FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.create Lib.IntTypes.u8 Lib.Buffer.lbuffer FStar.HyperStack.ST.push_frame
module Hacl.Impl.Frodo.KEM.KeyGen

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

open LowStar.Buffer

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.Matrix
open Hacl.Impl.Frodo.Params
open Hacl.Impl.Frodo.KEM
open Hacl.Impl.Frodo.Pack
open Hacl.Impl.Frodo.Sample
open Hacl.Frodo.Random

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence
module M = Spec.Matrix

module FP = Spec.Frodo.Params
module S = Spec.Frodo.KEM.KeyGen

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

inline_for_extraction noextract
val frodo_shake_r:
    a:FP.frodo_alg
  -> c:uint8
  -> seed_se:lbytes (crypto_bytes a)
  -> output_len:size_t
  -> r:lbytes output_len
  -> Stack unit
    (requires fun h ->
      live h seed_se /\ live h r /\ disjoint seed_se r)
    (ensures  fun h0 _ h1 -> modifies (loc r) h0 h1 /\
      as_seq h1 r == S.frodo_shake_r a c (as_seq h0 seed_se) (v output_len))
val frodo_shake_r:
    a:FP.frodo_alg
  -> c:uint8
  -> seed_se:lbytes (crypto_bytes a)
  -> output_len:size_t
  -> r:lbytes output_len
  -> Stack unit
    (requires fun h ->
      live h seed_se /\ live h r /\ disjoint seed_se r)
    (ensures  fun h0 _ h1 -> modifies (loc r) h0 h1 /\
      as_seq h1 r == S.frodo_shake_r a c (as_seq h0 seed_se) (v output_len))

    a: Spec.Frodo.Params.frodo_alg ->
    c: Lib.IntTypes.uint8 ->
    seed_se: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.crypto_bytes a) ->
    output_len: Lib.IntTypes.size_t ->
    r: Hacl.Impl.Matrix.lbytes output_len
  -> FStar.HyperStack.ST.Stack Prims.unit