val frodo_mul_add_sb_plus_e_plus_mu:
    a:frodo_alg
  -> mu:lbytes (bytes_mu a)
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix params_nbar (params_n a)
  -> epp_matrix:matrix params_nbar params_nbar
  -> matrix params_nbar params_nbar
let frodo_mul_add_sb_plus_e_plus_mu a mu b sp_matrix epp_matrix =
  let v_matrix  = frodo_mul_add_sb_plus_e a b sp_matrix epp_matrix in
  let mu_encode = frodo_key_encode (params_logq a) (params_extracted_bits a) params_nbar mu in
  let v_matrix  = Matrix.add v_matrix mu_encode in
  v_matrix
val frodo_mul_add_sb_plus_e_plus_mu:
    a:frodo_alg
  -> mu:lbytes (bytes_mu a)
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix params_nbar (params_n a)
  -> epp_matrix:matrix params_nbar params_nbar
  -> matrix params_nbar params_nbar
let frodo_mul_add_sb_plus_e_plus_mu a mu b sp_matrix epp_matrix =
let v_matrix = frodo_mul_add_sb_plus_e a b sp_matrix epp_matrix in
let mu_encode = frodo_key_encode (params_logq a) (params_extracted_bits a) params_nbar mu in
let v_matrix = Matrix.add v_matrix mu_encode in
v_matrix
Spec.Frodo.KEM.Encaps.fst.checked
Spec.Matrix.fst.checked Spec.Frodo.Sample.fst.checked Spec.Frodo.Random.fst.checked Spec.Frodo.Params.fst.checked Spec.Frodo.Pack.fst.checked Spec.Frodo.Lemmas.fst.checked Spec.Frodo.KEM.KeyGen.fst.checked Spec.Frodo.Encode.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Frodo.KEM.Encaps.fst
Spec.Frodo.Params.frodo_alg Lib.ByteSequence.lbytes Spec.Frodo.Params.bytes_mu Spec.Frodo.Params.publicmatrixbytes_len Spec.Matrix.matrix Spec.Frodo.Params.params_nbar Spec.Frodo.Params.params_n Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U16 Lib.IntTypes.SEC Prims.op_Multiply Prims.l_Forall Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.l_and Prims.op_LessThan Prims.eq2 Spec.Matrix.mget Lib.IntTypes.add_mod Spec.Matrix.add Spec.Frodo.Encode.frodo_key_encode Spec.Frodo.Params.params_logq Spec.Frodo.Params.params_extracted_bits Spec.Frodo.KEM.Encaps.frodo_mul_add_sb_plus_e
module Spec.Frodo.KEM.Encaps

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.Matrix
open Spec.Frodo.Lemmas
open Spec.Frodo.Params
open Spec.Frodo.Encode
open Spec.Frodo.Pack
open Spec.Frodo.Sample

module LSeq = Lib.Sequence
module Matrix = Spec.Matrix
module KG = Spec.Frodo.KEM.KeyGen

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

val frodo_mul_add_sa_plus_e:
    a:frodo_alg
  -> gen_a:frodo_gen_a
  -> seed_a:lbytes bytes_seed_a
  -> sp_matrix:matrix params_nbar (params_n a)
  -> ep_matrix:matrix params_nbar (params_n a)
  -> matrix params_nbar (params_n a)

let frodo_mul_add_sa_plus_e a gen_a seed_a sp_matrix ep_matrix =
  let a_matrix  = frodo_gen_matrix gen_a (params_n a) seed_a in
  let b_matrix  = Matrix.add (Matrix.mul sp_matrix a_matrix) ep_matrix in
  b_matrix


val crypto_kem_enc_ct_pack_c1:
    a:frodo_alg
  -> gen_a:frodo_gen_a
  -> seed_a:lbytes bytes_seed_a
  -> sp_matrix:matrix params_nbar (params_n a)
  -> ep_matrix:matrix params_nbar (params_n a)
  -> lbytes (ct1bytes_len a)

let crypto_kem_enc_ct_pack_c1 a gen_a seed_a sp_matrix ep_matrix =
  let bp_matrix = frodo_mul_add_sa_plus_e a gen_a seed_a sp_matrix ep_matrix in
  let ct1 = frodo_pack (params_logq a) bp_matrix in
  ct1


val frodo_mul_add_sb_plus_e:
    a:frodo_alg
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix params_nbar (params_n a)
  -> epp_matrix:matrix params_nbar params_nbar
  -> matrix params_nbar params_nbar

let frodo_mul_add_sb_plus_e a b sp_matrix epp_matrix =
  let b_matrix = frodo_unpack #(params_n a) #params_nbar (params_logq a) b in
  let v_matrix = Matrix.add (Matrix.mul sp_matrix b_matrix) epp_matrix in
  v_matrix


val frodo_mul_add_sb_plus_e_plus_mu:
    a:frodo_alg
  -> mu:lbytes (bytes_mu a)
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix params_nbar (params_n a)
  -> epp_matrix:matrix params_nbar params_nbar
  -> matrix params_nbar params_nbar
val frodo_mul_add_sb_plus_e_plus_mu:
    a:frodo_alg
  -> mu:lbytes (bytes_mu a)
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix params_nbar (params_n a)
  -> epp_matrix:matrix params_nbar params_nbar
  -> matrix params_nbar params_nbar

    a: Spec.Frodo.Params.frodo_alg ->
    mu: Lib.ByteSequence.lbytes (Spec.Frodo.Params.bytes_mu a) ->
    b: Lib.ByteSequence.lbytes (Spec.Frodo.Params.publicmatrixbytes_len a) ->
    sp_matrix: Spec.Matrix.matrix Spec.Frodo.Params.params_nbar (Spec.Frodo.Params.params_n a) ->
    epp_matrix: Spec.Matrix.matrix Spec.Frodo.Params.params_nbar Spec.Frodo.Params.params_nbar
  -> Spec.Matrix.matrix Spec.Frodo.Params.params_nbar Spec.Frodo.Params.params_nbar