val get_bpp_cp_matrices_:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> mu_decode:lbytes (bytes_mu a)
  -> sk:lbytes (crypto_secretkeybytes a)
  -> bpp_matrix:matrix_t params_nbar (params_n a)
  -> cp_matrix:matrix_t params_nbar params_nbar
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> ep_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h mu_decode /\ live h sk /\
      live h bpp_matrix /\ live h cp_matrix /\
      live h sp_matrix /\ live h ep_matrix /\ live h epp_matrix /\
      loc_pairwise_disjoint [loc mu_decode; loc sk; loc bpp_matrix;
        loc cp_matrix; loc sp_matrix; loc ep_matrix; loc epp_matrix])
    (ensures fun h0 _ h1 -> modifies (loc bpp_matrix |+| loc cp_matrix) h0 h1 /\
      (as_matrix h1 bpp_matrix, as_matrix h1 cp_matrix) ==
      S.get_bpp_cp_matrices_ a gen_a (as_seq h0 mu_decode) (as_seq h0 sk)
        (as_matrix h0 sp_matrix) (as_matrix h0 ep_matrix) (as_matrix h0 epp_matrix))
let get_bpp_cp_matrices_ a gen_a mu_decode sk bpp_matrix cp_matrix sp_matrix ep_matrix epp_matrix =
  FP.expand_crypto_secretkeybytes a;
  FP.expand_crypto_publickeybytes a;
  let pk = sub sk (crypto_bytes a) (crypto_publickeybytes a) in
  let seed_a = sub pk 0ul bytes_seed_a in
  let b = sub pk bytes_seed_a (crypto_publickeybytes a -! bytes_seed_a) in

  frodo_mul_add_sa_plus_e a gen_a seed_a sp_matrix ep_matrix bpp_matrix;
  frodo_mul_add_sb_plus_e_plus_mu a mu_decode b sp_matrix epp_matrix cp_matrix;
  mod_pow2 (params_logq a) bpp_matrix;
  mod_pow2 (params_logq a) cp_matrix
val get_bpp_cp_matrices_:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> mu_decode:lbytes (bytes_mu a)
  -> sk:lbytes (crypto_secretkeybytes a)
  -> bpp_matrix:matrix_t params_nbar (params_n a)
  -> cp_matrix:matrix_t params_nbar params_nbar
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> ep_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h mu_decode /\ live h sk /\
      live h bpp_matrix /\ live h cp_matrix /\
      live h sp_matrix /\ live h ep_matrix /\ live h epp_matrix /\
      loc_pairwise_disjoint [loc mu_decode; loc sk; loc bpp_matrix;
        loc cp_matrix; loc sp_matrix; loc ep_matrix; loc epp_matrix])
    (ensures fun h0 _ h1 -> modifies (loc bpp_matrix |+| loc cp_matrix) h0 h1 /\
      (as_matrix h1 bpp_matrix, as_matrix h1 cp_matrix) ==
      S.get_bpp_cp_matrices_ a gen_a (as_seq h0 mu_decode) (as_seq h0 sk)
        (as_matrix h0 sp_matrix) (as_matrix h0 ep_matrix) (as_matrix h0 epp_matrix))
let get_bpp_cp_matrices_ a gen_a mu_decode sk bpp_matrix cp_matrix sp_matrix ep_matrix epp_matrix =
FP.expand_crypto_secretkeybytes a;
FP.expand_crypto_publickeybytes a;
let pk = sub sk (crypto_bytes a) (crypto_publickeybytes a) in
let seed_a = sub pk 0ul bytes_seed_a in
let b = sub pk bytes_seed_a (crypto_publickeybytes a -! bytes_seed_a) in
frodo_mul_add_sa_plus_e a gen_a seed_a sp_matrix ep_matrix bpp_matrix;
frodo_mul_add_sb_plus_e_plus_mu a mu_decode b sp_matrix epp_matrix cp_matrix;
mod_pow2 (params_logq a) bpp_matrix;
mod_pow2 (params_logq a) cp_matrix
Hacl.Impl.Frodo.KEM.Decaps.fst.checked
Spec.Matrix.fst.checked Spec.Frodo.Params.fst.checked Spec.Frodo.KEM.Decaps.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.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.Encaps.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.Decaps.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_mu Hacl.Impl.Frodo.Params.crypto_secretkeybytes Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar Hacl.Impl.Frodo.Params.params_n Hacl.Impl.Matrix.mod_pow2 Hacl.Impl.Frodo.Params.params_logq Prims.unit Hacl.Impl.Frodo.KEM.Encaps.frodo_mul_add_sb_plus_e_plus_mu Hacl.Impl.Frodo.KEM.Encaps.frodo_mul_add_sa_plus_e Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.sub Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Impl.Frodo.Params.crypto_publickeybytes Hacl.Impl.Frodo.Params.bytes_seed_a Lib.Buffer.sub Lib.IntTypes.uint8 Lib.IntTypes.op_Subtraction_Bang FStar.UInt32.__uint_to_t Hacl.Impl.Frodo.Params.crypto_bytes Spec.Frodo.Params.expand_crypto_publickeybytes Spec.Frodo.Params.expand_crypto_secretkeybytes
module Hacl.Impl.Frodo.KEM.Decaps

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.KEM.Encaps
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 FP = Spec.Frodo.Params
module KG = Hacl.Impl.Frodo.KEM.KeyGen
module S = Spec.Frodo.KEM.Decaps
module M = Spec.Matrix

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

inline_for_extraction noextract
val get_bp_c_matrices:
     a:FP.frodo_alg
  -> ct:lbytes (crypto_ciphertextbytes a)
  -> bp_matrix:matrix_t params_nbar (params_n a)
  -> c_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h ct /\ live h bp_matrix /\ live h c_matrix /\
      disjoint bp_matrix ct /\ disjoint c_matrix ct /\ disjoint bp_matrix c_matrix)
    (ensures  fun h0 _ h1 -> modifies (loc bp_matrix |+| loc c_matrix) h0 h1 /\
      (as_matrix h1 bp_matrix, as_matrix h1 c_matrix) == S.get_bp_c_matrices a (as_seq h0 ct))

let get_bp_c_matrices a ct bp_matrix c_matrix =
  let c1 = sub ct 0ul (ct1bytes_len a) in
  let c2 = sub ct (ct1bytes_len a) (ct2bytes_len a) in
  frodo_unpack params_nbar (params_n a) (params_logq a) c1 bp_matrix;
  frodo_unpack params_nbar params_nbar (params_logq a) c2 c_matrix


inline_for_extraction noextract
val frodo_mu_decode:
    a:FP.frodo_alg
  -> s_bytes:lbytes (secretmatrixbytes_len a)
  -> bp_matrix:matrix_t params_nbar (params_n a)
  -> c_matrix:matrix_t params_nbar params_nbar
  -> mu_decode:lbytes (bytes_mu a)
  -> Stack unit
    (requires fun h ->
      live h s_bytes /\ live h bp_matrix /\
      live h c_matrix /\ live h mu_decode /\
      disjoint mu_decode s_bytes /\
      as_seq h (mu_decode) == Seq.create (v (bytes_mu a)) (u8 0))
    (ensures fun h0 _ h1 -> modifies (loc mu_decode) h0 h1 /\
      as_seq h1 mu_decode ==
      S.frodo_mu_decode a (as_seq h0 s_bytes) (as_matrix h0 bp_matrix) (as_matrix h0 c_matrix))

let frodo_mu_decode a s_bytes bp_matrix c_matrix mu_decode =
  push_frame();
  let s_matrix = matrix_create (params_n a) params_nbar in
  let m_matrix = matrix_create params_nbar params_nbar in
  matrix_from_lbytes s_bytes s_matrix;
  matrix_mul_s bp_matrix s_matrix m_matrix;
  matrix_sub c_matrix m_matrix;
  frodo_key_decode (params_logq a) (params_extracted_bits a) params_nbar m_matrix mu_decode;
  clear_matrix s_matrix;
  clear_matrix m_matrix;
  pop_frame()


inline_for_extraction noextract
val get_bpp_cp_matrices_:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> mu_decode:lbytes (bytes_mu a)
  -> sk:lbytes (crypto_secretkeybytes a)
  -> bpp_matrix:matrix_t params_nbar (params_n a)
  -> cp_matrix:matrix_t params_nbar params_nbar
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> ep_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h mu_decode /\ live h sk /\
      live h bpp_matrix /\ live h cp_matrix /\
      live h sp_matrix /\ live h ep_matrix /\ live h epp_matrix /\
      loc_pairwise_disjoint [loc mu_decode; loc sk; loc bpp_matrix;
        loc cp_matrix; loc sp_matrix; loc ep_matrix; loc epp_matrix])
    (ensures fun h0 _ h1 -> modifies (loc bpp_matrix |+| loc cp_matrix) h0 h1 /\
      (as_matrix h1 bpp_matrix, as_matrix h1 cp_matrix) ==
      S.get_bpp_cp_matrices_ a gen_a (as_seq h0 mu_decode) (as_seq h0 sk)
        (as_matrix h0 sp_matrix) (as_matrix h0 ep_matrix) (as_matrix h0 epp_matrix))
val get_bpp_cp_matrices_:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> mu_decode:lbytes (bytes_mu a)
  -> sk:lbytes (crypto_secretkeybytes a)
  -> bpp_matrix:matrix_t params_nbar (params_n a)
  -> cp_matrix:matrix_t params_nbar params_nbar
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> ep_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h mu_decode /\ live h sk /\
      live h bpp_matrix /\ live h cp_matrix /\
      live h sp_matrix /\ live h ep_matrix /\ live h epp_matrix /\
      loc_pairwise_disjoint [loc mu_decode; loc sk; loc bpp_matrix;
        loc cp_matrix; loc sp_matrix; loc ep_matrix; loc epp_matrix])
    (ensures fun h0 _ h1 -> modifies (loc bpp_matrix |+| loc cp_matrix) h0 h1 /\
      (as_matrix h1 bpp_matrix, as_matrix h1 cp_matrix) ==
      S.get_bpp_cp_matrices_ a gen_a (as_seq h0 mu_decode) (as_seq h0 sk)
        (as_matrix h0 sp_matrix) (as_matrix h0 ep_matrix) (as_matrix h0 epp_matrix))

    a: Spec.Frodo.Params.frodo_alg ->
    gen_a: Spec.Frodo.Params.frodo_gen_a{Hacl.Impl.Frodo.Params.is_supported gen_a} ->
    mu_decode: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.bytes_mu a) ->
    sk: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.crypto_secretkeybytes a) ->
    bpp_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        (Hacl.Impl.Frodo.Params.params_n a) ->
    cp_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        Hacl.Impl.Frodo.Params.params_nbar ->
    sp_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        (Hacl.Impl.Frodo.Params.params_n a) ->
    ep_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
  -> FStar.HyperStack.ST.Stack Prims.unit