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()
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 ()
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.lbytes Hacl.Impl.Frodo.Params.secretmatrixbytes_len Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar Hacl.Impl.Frodo.Params.params_n Hacl.Impl.Frodo.Params.bytes_mu FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.Frodo.KEM.clear_matrix Hacl.Impl.Frodo.Encode.frodo_key_decode Hacl.Impl.Frodo.Params.params_logq Hacl.Impl.Frodo.Params.params_extracted_bits Hacl.Impl.Matrix.matrix_sub Hacl.Impl.Matrix.matrix_mul_s Hacl.Impl.Matrix.matrix_from_lbytes 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.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))
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))

    a: Spec.Frodo.Params.frodo_alg ->
    s_bytes: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.secretmatrixbytes_len a) ->
    bp_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 ->
    mu_decode: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.bytes_mu a)
  -> FStar.HyperStack.ST.Stack Prims.unit