val crypto_kem_dec_kp_s_cond:
    a:FP.frodo_alg
  -> bp_matrix:matrix_t params_nbar (params_n a)
  -> bpp_matrix:matrix_t params_nbar (params_n a)
  -> c_matrix:matrix_t params_nbar params_nbar
  -> cp_matrix:matrix_t params_nbar params_nbar
  -> Stack uint16
    (requires fun h ->
      live h bp_matrix /\ live h bpp_matrix /\
      live h c_matrix /\ live h cp_matrix)
    (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
      r == S.crypto_kem_dec_kp_s_cond a (as_matrix h0 bp_matrix) (as_matrix h0 bpp_matrix)
        (as_matrix h0 c_matrix) (as_matrix h0 cp_matrix))
let crypto_kem_dec_kp_s_cond a bp_matrix bpp_matrix c_matrix cp_matrix =
  let b1 = matrix_eq bp_matrix bpp_matrix in
  let b2 = matrix_eq c_matrix cp_matrix in
  b1 &. b2
val crypto_kem_dec_kp_s_cond:
    a:FP.frodo_alg
  -> bp_matrix:matrix_t params_nbar (params_n a)
  -> bpp_matrix:matrix_t params_nbar (params_n a)
  -> c_matrix:matrix_t params_nbar params_nbar
  -> cp_matrix:matrix_t params_nbar params_nbar
  -> Stack uint16
    (requires fun h ->
      live h bp_matrix /\ live h bpp_matrix /\
      live h c_matrix /\ live h cp_matrix)
    (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
      r == S.crypto_kem_dec_kp_s_cond a (as_matrix h0 bp_matrix) (as_matrix h0 bpp_matrix)
        (as_matrix h0 c_matrix) (as_matrix h0 cp_matrix))
let crypto_kem_dec_kp_s_cond a bp_matrix bpp_matrix c_matrix cp_matrix =
let b1 = matrix_eq bp_matrix bpp_matrix in
let b2 = matrix_eq c_matrix cp_matrix in
b1 &. b2
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 Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar Hacl.Impl.Frodo.Params.params_n Lib.IntTypes.op_Amp_Dot Lib.IntTypes.U16 Lib.IntTypes.SEC Lib.IntTypes.uint16 Lib.IntTypes.int_t Hacl.Impl.Matrix.matrix_eq
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))

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


#push-options "--z3rlimit 150"
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)
  -> seed_se:lbytes (crypto_bytes a)
  -> sk:lbytes (crypto_secretkeybytes a)
  -> bpp_matrix:matrix_t params_nbar (params_n a)
  -> cp_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h seed_se /\ live h mu_decode /\ live h sk /\
      live h bpp_matrix /\ live h cp_matrix /\
      loc_pairwise_disjoint [loc mu_decode; loc seed_se; loc sk; loc bpp_matrix; loc cp_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 seed_se) (as_seq h0 sk))

let get_bpp_cp_matrices a gen_a mu_decode seed_se sk bpp_matrix cp_matrix =
  push_frame ();
  let sp_matrix  = matrix_create params_nbar (params_n a) in
  let ep_matrix  = matrix_create params_nbar (params_n a) in
  let epp_matrix = matrix_create params_nbar params_nbar in
  get_sp_ep_epp_matrices a seed_se sp_matrix ep_matrix epp_matrix;
  get_bpp_cp_matrices_ a gen_a mu_decode sk bpp_matrix cp_matrix sp_matrix ep_matrix epp_matrix;
  clear_matrix3 a sp_matrix ep_matrix epp_matrix;
  pop_frame ()
#pop-options


inline_for_extraction noextract
val crypto_kem_dec_kp_s_cond:
    a:FP.frodo_alg
  -> bp_matrix:matrix_t params_nbar (params_n a)
  -> bpp_matrix:matrix_t params_nbar (params_n a)
  -> c_matrix:matrix_t params_nbar params_nbar
  -> cp_matrix:matrix_t params_nbar params_nbar
  -> Stack uint16
    (requires fun h ->
      live h bp_matrix /\ live h bpp_matrix /\
      live h c_matrix /\ live h cp_matrix)
    (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
      r == S.crypto_kem_dec_kp_s_cond a (as_matrix h0 bp_matrix) (as_matrix h0 bpp_matrix)
        (as_matrix h0 c_matrix) (as_matrix h0 cp_matrix))
val crypto_kem_dec_kp_s_cond:
    a:FP.frodo_alg
  -> bp_matrix:matrix_t params_nbar (params_n a)
  -> bpp_matrix:matrix_t params_nbar (params_n a)
  -> c_matrix:matrix_t params_nbar params_nbar
  -> cp_matrix:matrix_t params_nbar params_nbar
  -> Stack uint16
    (requires fun h ->
      live h bp_matrix /\ live h bpp_matrix /\
      live h c_matrix /\ live h cp_matrix)
    (ensures  fun h0 r h1 -> modifies0 h0 h1 /\
      r == S.crypto_kem_dec_kp_s_cond a (as_matrix h0 bp_matrix) (as_matrix h0 bpp_matrix)
        (as_matrix h0 c_matrix) (as_matrix h0 cp_matrix))

    a: Spec.Frodo.Params.frodo_alg ->
    bp_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        (Hacl.Impl.Frodo.Params.params_n a) ->
    bpp_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        (Hacl.Impl.Frodo.Params.params_n a) ->
    c_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        Hacl.Impl.Frodo.Params.params_nbar ->
    cp_matrix:
      Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar
        Hacl.Impl.Frodo.Params.params_nbar
  -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint16