val frodo_mul_add_sb_plus_e:
    a:FP.frodo_alg
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> v_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h b /\ live h epp_matrix /\ live h v_matrix /\ live h sp_matrix /\
      disjoint v_matrix b /\ disjoint v_matrix epp_matrix /\ disjoint v_matrix sp_matrix)
    (ensures fun h0 _ h1 -> modifies (loc v_matrix) h0 h1 /\
      as_matrix h1 v_matrix ==
      S.frodo_mul_add_sb_plus_e a (as_seq h0 b) (as_matrix h0 sp_matrix) (as_matrix h0 epp_matrix))
let frodo_mul_add_sb_plus_e a b sp_matrix epp_matrix v_matrix =
  push_frame ();
  let b_matrix = matrix_create (params_n a) params_nbar in
  frodo_unpack (params_n a) params_nbar (params_logq a) b b_matrix;
  matrix_mul sp_matrix b_matrix v_matrix;
  matrix_add v_matrix epp_matrix;
  pop_frame ()
val frodo_mul_add_sb_plus_e:
    a:FP.frodo_alg
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> v_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h b /\ live h epp_matrix /\ live h v_matrix /\ live h sp_matrix /\
      disjoint v_matrix b /\ disjoint v_matrix epp_matrix /\ disjoint v_matrix sp_matrix)
    (ensures fun h0 _ h1 -> modifies (loc v_matrix) h0 h1 /\
      as_matrix h1 v_matrix ==
      S.frodo_mul_add_sb_plus_e a (as_seq h0 b) (as_matrix h0 sp_matrix) (as_matrix h0 epp_matrix))
let frodo_mul_add_sb_plus_e a b sp_matrix epp_matrix v_matrix =
push_frame ();
let b_matrix = matrix_create (params_n a) params_nbar in
frodo_unpack (params_n a) params_nbar (params_logq a) b b_matrix;
matrix_mul sp_matrix b_matrix v_matrix;
matrix_add v_matrix epp_matrix;
pop_frame ()
Hacl.Impl.Frodo.KEM.Encaps.fst.checked
Spec.Matrix.fst.checked Spec.Frodo.Params.fst.checked Spec.Frodo.KEM.Encaps.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.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.KeyGen.fst.checked Hacl.Impl.Frodo.KEM.fst.checked Hacl.Impl.Frodo.Encode.fst.checked Hacl.Frodo.Random.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.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.Encaps.fst
Spec.Frodo.Params.frodo_alg Hacl.Impl.Matrix.lbytes Hacl.Impl.Frodo.Params.publicmatrixbytes_len Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar Hacl.Impl.Frodo.Params.params_n FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.Matrix.matrix_add Hacl.Impl.Matrix.matrix_mul Hacl.Impl.Frodo.Pack.frodo_unpack Hacl.Impl.Frodo.Params.params_logq 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
module Hacl.Impl.Frodo.KEM.Encaps

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.Encode
open Hacl.Impl.Frodo.Pack
open Hacl.Impl.Frodo.Sample
open Hacl.Frodo.Random

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence
module LB = Lib.ByteSequence

module FP = Spec.Frodo.Params
module S = Spec.Frodo.KEM.Encaps
module M = Spec.Matrix
module KG = Hacl.Impl.Frodo.KEM.KeyGen

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

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

let frodo_mul_add_sa_plus_e a gen_a seed_a sp_matrix ep_matrix bp_matrix =
  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 sp_matrix a_matrix bp_matrix;
  matrix_add bp_matrix ep_matrix;
  pop_frame ()


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

let crypto_kem_enc_ct_pack_c1 a gen_a seed_a sp_matrix ep_matrix c1 =
  push_frame ();
  let bp_matrix = matrix_create params_nbar (params_n a) in
  frodo_mul_add_sa_plus_e a gen_a seed_a sp_matrix ep_matrix bp_matrix;
  frodo_pack (params_logq a) bp_matrix c1;
  pop_frame ()


inline_for_extraction noextract
val frodo_mul_add_sb_plus_e:
    a:FP.frodo_alg
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> v_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h b /\ live h epp_matrix /\ live h v_matrix /\ live h sp_matrix /\
      disjoint v_matrix b /\ disjoint v_matrix epp_matrix /\ disjoint v_matrix sp_matrix)
    (ensures fun h0 _ h1 -> modifies (loc v_matrix) h0 h1 /\
      as_matrix h1 v_matrix ==
      S.frodo_mul_add_sb_plus_e a (as_seq h0 b) (as_matrix h0 sp_matrix) (as_matrix h0 epp_matrix))
val frodo_mul_add_sb_plus_e:
    a:FP.frodo_alg
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> v_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h b /\ live h epp_matrix /\ live h v_matrix /\ live h sp_matrix /\
      disjoint v_matrix b /\ disjoint v_matrix epp_matrix /\ disjoint v_matrix sp_matrix)
    (ensures fun h0 _ h1 -> modifies (loc v_matrix) h0 h1 /\
      as_matrix h1 v_matrix ==
      S.frodo_mul_add_sb_plus_e a (as_seq h0 b) (as_matrix h0 sp_matrix) (as_matrix h0 epp_matrix))

    a: Spec.Frodo.Params.frodo_alg ->
    b: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.publicmatrixbytes_len a) ->
    sp_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        (Hacl.Impl.Frodo.Params.params_n a) ->
    epp_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        Hacl.Impl.Frodo.Params.params_nbar ->
    v_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        Hacl.Impl.Frodo.Params.params_nbar
  -> FStar.HyperStack.ST.Stack Prims.unit