val frodo_mul_add_as_plus_e:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> seed_a:lbytes bytes_seed_a
  -> s_matrix:matrix_t (params_n a) params_nbar
  -> e_matrix:matrix_t (params_n a) params_nbar
  -> b_matrix:matrix_t (params_n a) params_nbar
  -> Stack unit
    (requires fun h ->
      live h seed_a /\ live h s_matrix /\ live h e_matrix /\ live h b_matrix /\
      disjoint b_matrix seed_a /\ disjoint b_matrix e_matrix /\
      disjoint b_matrix s_matrix /\ disjoint s_matrix e_matrix)
    (ensures  fun h0 _ h1 -> modifies (loc b_matrix) h0 h1 /\
      as_matrix h1 b_matrix == S.frodo_mul_add_as_plus_e a gen_a (as_seq h0 seed_a)
        (as_matrix h0 s_matrix) (as_matrix h0 e_matrix))
let frodo_mul_add_as_plus_e a gen_a seed_a s_matrix e_matrix b_matrix =
  FP.params_n_sqr a;
  push_frame();
  let a_matrix = matrix_create (params_n a) (params_n a) in
  frodo_gen_matrix gen_a (params_n a) seed_a a_matrix;
  matrix_mul_s a_matrix s_matrix b_matrix;
  matrix_add b_matrix e_matrix;
  pop_frame()
val frodo_mul_add_as_plus_e:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> seed_a:lbytes bytes_seed_a
  -> s_matrix:matrix_t (params_n a) params_nbar
  -> e_matrix:matrix_t (params_n a) params_nbar
  -> b_matrix:matrix_t (params_n a) params_nbar
  -> Stack unit
    (requires fun h ->
      live h seed_a /\ live h s_matrix /\ live h e_matrix /\ live h b_matrix /\
      disjoint b_matrix seed_a /\ disjoint b_matrix e_matrix /\
      disjoint b_matrix s_matrix /\ disjoint s_matrix e_matrix)
    (ensures  fun h0 _ h1 -> modifies (loc b_matrix) h0 h1 /\
      as_matrix h1 b_matrix == S.frodo_mul_add_as_plus_e a gen_a (as_seq h0 seed_a)
        (as_matrix h0 s_matrix) (as_matrix h0 e_matrix))
let frodo_mul_add_as_plus_e a gen_a seed_a s_matrix e_matrix b_matrix =
FP.params_n_sqr a;
push_frame ();
let a_matrix = matrix_create (params_n a) (params_n a) in
frodo_gen_matrix gen_a (params_n a) seed_a a_matrix;
matrix_mul_s a_matrix s_matrix b_matrix;
matrix_add b_matrix e_matrix;
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 Spec.Frodo.Params.frodo_gen_a Prims.b2t Hacl.Impl.Frodo.Params.is_supported Hacl.Impl.Matrix.lbytes Hacl.Impl.Frodo.Params.bytes_seed_a Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_n Hacl.Impl.Frodo.Params.params_nbar FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.Matrix.matrix_add Hacl.Impl.Matrix.matrix_mul_s Hacl.Impl.Frodo.Params.frodo_gen_matrix Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U16 Lib.IntTypes.SEC Lib.IntTypes.mul Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Impl.Matrix.matrix_create FStar.HyperStack.ST.push_frame Spec.Frodo.Params.params_n_sqr
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))

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 ()


inline_for_extraction noextract
val frodo_mul_add_as_plus_e:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> seed_a:lbytes bytes_seed_a
  -> s_matrix:matrix_t (params_n a) params_nbar
  -> e_matrix:matrix_t (params_n a) params_nbar
  -> b_matrix:matrix_t (params_n a) params_nbar
  -> Stack unit
    (requires fun h ->
      live h seed_a /\ live h s_matrix /\ live h e_matrix /\ live h b_matrix /\
      disjoint b_matrix seed_a /\ disjoint b_matrix e_matrix /\
      disjoint b_matrix s_matrix /\ disjoint s_matrix e_matrix)
    (ensures  fun h0 _ h1 -> modifies (loc b_matrix) h0 h1 /\
      as_matrix h1 b_matrix == S.frodo_mul_add_as_plus_e a gen_a (as_seq h0 seed_a)
        (as_matrix h0 s_matrix) (as_matrix h0 e_matrix))
val frodo_mul_add_as_plus_e:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> seed_a:lbytes bytes_seed_a
  -> s_matrix:matrix_t (params_n a) params_nbar
  -> e_matrix:matrix_t (params_n a) params_nbar
  -> b_matrix:matrix_t (params_n a) params_nbar
  -> Stack unit
    (requires fun h ->
      live h seed_a /\ live h s_matrix /\ live h e_matrix /\ live h b_matrix /\
      disjoint b_matrix seed_a /\ disjoint b_matrix e_matrix /\
      disjoint b_matrix s_matrix /\ disjoint s_matrix e_matrix)
    (ensures  fun h0 _ h1 -> modifies (loc b_matrix) h0 h1 /\
      as_matrix h1 b_matrix == S.frodo_mul_add_as_plus_e a gen_a (as_seq h0 seed_a)
        (as_matrix h0 s_matrix) (as_matrix h0 e_matrix))

    a: Spec.Frodo.Params.frodo_alg ->
    gen_a: Spec.Frodo.Params.frodo_gen_a{Hacl.Impl.Frodo.Params.is_supported gen_a} ->
    seed_a: Hacl.Impl.Matrix.lbytes Hacl.Impl.Frodo.Params.bytes_seed_a ->
    s_matrix:
      Hacl.Impl.Matrix.matrix_t (Hacl.Impl.Frodo.Params.params_n a)
        Hacl.Impl.Frodo.Params.params_nbar ->
    e_matrix:
      Hacl.Impl.Matrix.matrix_t (Hacl.Impl.Frodo.Params.params_n a)
        Hacl.Impl.Frodo.Params.params_nbar ->
    b_matrix:
      Hacl.Impl.Matrix.matrix_t (Hacl.Impl.Frodo.Params.params_n a)
        Hacl.Impl.Frodo.Params.params_nbar
  -> FStar.HyperStack.ST.Stack Prims.unit