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
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
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.crypto_ciphertextbytes Hacl.Impl.Matrix.matrix_t Hacl.Impl.Frodo.Params.params_nbar Hacl.Impl.Frodo.Params.params_n Hacl.Impl.Frodo.Pack.frodo_unpack Hacl.Impl.Frodo.Params.params_logq Prims.unit Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Hacl.Impl.Frodo.Params.ct2bytes_len Lib.Buffer.sub Lib.IntTypes.uint8 Hacl.Impl.Frodo.Params.ct1bytes_len FStar.UInt32.__uint_to_t
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))
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))

    a: Spec.Frodo.Params.frodo_alg ->
    ct: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.crypto_ciphertextbytes 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
  -> FStar.HyperStack.ST.Stack Prims.unit