val crypto_kem_enc_ss:
    a:FP.frodo_alg
  -> k:lbytes (crypto_bytes a)
  -> ct:lbytes (crypto_ciphertextbytes a)
  -> ss:lbytes (crypto_bytes a)
  -> Stack unit
    (requires fun h ->
      live h k /\ live h ct /\ live h ss /\
      disjoint ct ss /\ disjoint k ct /\ disjoint k ss)
    (ensures  fun h0 _ h1 -> modifies (loc ss) h0 h1 /\
      as_seq h1 ss == S.crypto_kem_enc_ss a (as_seq h0 k) (as_seq h0 ct))
let crypto_kem_enc_ss a k ct ss =
  push_frame ();
  let ss_init_len = crypto_ciphertextbytes a +! crypto_bytes a in
  let shake_input_ss = create ss_init_len (u8 0) in
  concat2 (crypto_ciphertextbytes a) ct (crypto_bytes a) k shake_input_ss;
  frodo_shake a ss_init_len shake_input_ss (crypto_bytes a) ss;
  clear_words_u8 shake_input_ss;
  pop_frame ()
val crypto_kem_enc_ss:
    a:FP.frodo_alg
  -> k:lbytes (crypto_bytes a)
  -> ct:lbytes (crypto_ciphertextbytes a)
  -> ss:lbytes (crypto_bytes a)
  -> Stack unit
    (requires fun h ->
      live h k /\ live h ct /\ live h ss /\
      disjoint ct ss /\ disjoint k ct /\ disjoint k ss)
    (ensures  fun h0 _ h1 -> modifies (loc ss) h0 h1 /\
      as_seq h1 ss == S.crypto_kem_enc_ss a (as_seq h0 k) (as_seq h0 ct))
let crypto_kem_enc_ss a k ct ss =
push_frame ();
let ss_init_len = crypto_ciphertextbytes a +! crypto_bytes a in
let shake_input_ss = create ss_init_len (u8 0) in
concat2 (crypto_ciphertextbytes a) ct (crypto_bytes a) k shake_input_ss;
frodo_shake a ss_init_len shake_input_ss (crypto_bytes a) ss;
clear_words_u8 shake_input_ss;
pop_frame ()
Hacl.Impl.Frodo.KEM.Encaps.fst.checked
Spec.Matrix.fst.checked Spec.Frodo.Params.fst.checked Spec.Frodo.KEM.Encaps.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.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.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.Encaps.fst
Spec.Frodo.Params.frodo_alg Hacl.Impl.Matrix.lbytes Hacl.Impl.Frodo.Params.crypto_bytes Hacl.Impl.Frodo.Params.crypto_ciphertextbytes FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.Frodo.KEM.clear_words_u8 Hacl.Impl.Frodo.Params.frodo_shake Lib.Buffer.concat2 Lib.Buffer.MUT Lib.IntTypes.uint8 Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Buffer.create Lib.IntTypes.u8 Lib.Buffer.lbuffer Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.op_Plus_Bang FStar.HyperStack.ST.push_frame
module Hacl.Impl.Frodo.KEM.Encaps

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.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 LB = Lib.ByteSequence

module FP = Spec.Frodo.Params
module S = Spec.Frodo.KEM.Encaps
module M = Spec.Matrix
module KG = Hacl.Impl.Frodo.KEM.KeyGen

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

inline_for_extraction noextract
val frodo_mul_add_sa_plus_e:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> seed_a:lbytes bytes_seed_a
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> ep_matrix:matrix_t params_nbar (params_n a)
  -> bp_matrix:matrix_t params_nbar (params_n a)
  -> Stack unit
    (requires fun h ->
      live h seed_a /\ live h ep_matrix /\ live h sp_matrix /\ live h bp_matrix /\
      disjoint bp_matrix seed_a /\ disjoint bp_matrix ep_matrix /\ disjoint bp_matrix sp_matrix)
    (ensures  fun h0 _ h1 -> modifies (loc bp_matrix) h0 h1 /\
      as_matrix h1 bp_matrix ==
      S.frodo_mul_add_sa_plus_e a gen_a (as_seq h0 seed_a) (as_matrix h0 sp_matrix) (as_matrix h0 ep_matrix))

let frodo_mul_add_sa_plus_e a gen_a seed_a sp_matrix ep_matrix bp_matrix =
  push_frame ();
  let a_matrix  = matrix_create (params_n a) (params_n a) in
  frodo_gen_matrix gen_a (params_n a) seed_a a_matrix;
  matrix_mul sp_matrix a_matrix bp_matrix;
  matrix_add bp_matrix ep_matrix;
  pop_frame ()


inline_for_extraction noextract
val crypto_kem_enc_ct_pack_c1:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> seed_a:lbytes bytes_seed_a
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> ep_matrix:matrix_t params_nbar (params_n a)
  -> c1:lbytes (ct1bytes_len a)
  -> Stack unit
    (requires fun h ->
      live h seed_a /\ live h ep_matrix /\ live h sp_matrix /\ live h c1 /\
      disjoint seed_a c1 /\ disjoint ep_matrix c1 /\ disjoint sp_matrix c1)
    (ensures fun h0 _ h1 -> modifies (loc c1) h0 h1 /\
      as_seq h1 c1 ==
      S.crypto_kem_enc_ct_pack_c1 a gen_a (as_seq h0 seed_a) (as_matrix h0 sp_matrix) (as_matrix h0 ep_matrix))

let crypto_kem_enc_ct_pack_c1 a gen_a seed_a sp_matrix ep_matrix c1 =
  push_frame ();
  let bp_matrix = matrix_create params_nbar (params_n a) in
  frodo_mul_add_sa_plus_e a gen_a seed_a sp_matrix ep_matrix bp_matrix;
  frodo_pack (params_logq a) bp_matrix c1;
  pop_frame ()


inline_for_extraction noextract
val frodo_mul_add_sb_plus_e:
    a:FP.frodo_alg
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> v_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h b /\ live h epp_matrix /\ live h v_matrix /\ live h sp_matrix /\
      disjoint v_matrix b /\ disjoint v_matrix epp_matrix /\ disjoint v_matrix sp_matrix)
    (ensures fun h0 _ h1 -> modifies (loc v_matrix) h0 h1 /\
      as_matrix h1 v_matrix ==
      S.frodo_mul_add_sb_plus_e a (as_seq h0 b) (as_matrix h0 sp_matrix) (as_matrix h0 epp_matrix))

let frodo_mul_add_sb_plus_e a b sp_matrix epp_matrix v_matrix =
  push_frame ();
  let b_matrix = matrix_create (params_n a) params_nbar in
  frodo_unpack (params_n a) params_nbar (params_logq a) b b_matrix;
  matrix_mul sp_matrix b_matrix v_matrix;
  matrix_add v_matrix epp_matrix;
  pop_frame ()


inline_for_extraction noextract
val frodo_mul_add_sb_plus_e_plus_mu:
    a:FP.frodo_alg
  -> mu:lbytes (bytes_mu a)
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> v_matrix:matrix_t params_nbar params_nbar
  -> Stack unit
    (requires fun h ->
      live h b /\ live h mu /\ live h v_matrix /\
      live h sp_matrix /\ live h epp_matrix /\
      disjoint v_matrix b /\ disjoint v_matrix sp_matrix /\
      disjoint v_matrix mu /\ disjoint v_matrix epp_matrix)
    (ensures fun h0 _ h1 -> modifies (loc v_matrix) h0 h1 /\
      as_matrix h1 v_matrix ==
      S.frodo_mul_add_sb_plus_e_plus_mu a (as_seq h0 mu) (as_seq h0 b) (as_matrix h0 sp_matrix) (as_matrix h0 epp_matrix))

let frodo_mul_add_sb_plus_e_plus_mu a mu b sp_matrix epp_matrix v_matrix =
  push_frame ();
  frodo_mul_add_sb_plus_e a b sp_matrix epp_matrix v_matrix;
  let mu_encode = matrix_create params_nbar params_nbar in
  frodo_key_encode (params_logq a) (params_extracted_bits a) params_nbar mu mu_encode;
  matrix_add v_matrix mu_encode;
  clear_matrix mu_encode;
  pop_frame ()


inline_for_extraction noextract
val crypto_kem_enc_ct_pack_c2:
    a:FP.frodo_alg
  -> mu:lbytes (bytes_mu a)
  -> b:lbytes (publicmatrixbytes_len a)
  -> sp_matrix:matrix_t params_nbar (params_n a)
  -> epp_matrix:matrix_t params_nbar params_nbar
  -> c2:lbytes (ct2bytes_len a)
  -> Stack unit
    (requires fun h ->
      live h mu /\ live h b /\ live h sp_matrix /\
      live h epp_matrix /\ live h c2 /\
      disjoint mu c2 /\ disjoint b c2 /\
      disjoint sp_matrix c2 /\ disjoint epp_matrix c2)
    (ensures fun h0 _ h1 -> modifies (loc c2) h0 h1 /\
      as_seq h1 c2 ==
      S.crypto_kem_enc_ct_pack_c2 a (as_seq h0 mu) (as_seq h0 b) (as_matrix h0 sp_matrix) (as_matrix h0 epp_matrix))

#push-options "--z3rlimit 200"
let crypto_kem_enc_ct_pack_c2 a mu b sp_matrix epp_matrix c2 =
  push_frame ();
  let v_matrix = matrix_create params_nbar params_nbar in
  frodo_mul_add_sb_plus_e_plus_mu a mu b sp_matrix epp_matrix v_matrix;
  frodo_pack (params_logq a) v_matrix c2;
  clear_matrix v_matrix;
  pop_frame ()
#pop-options

inline_for_extraction noextract
val get_sp_ep_epp_matrices:
    a:FP.frodo_alg
  -> seed_se:lbytes (crypto_bytes a)
  -> 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 seed_se /\ live h sp_matrix /\
      live h ep_matrix /\ live h epp_matrix /\
      disjoint seed_se sp_matrix /\ disjoint seed_se ep_matrix /\
      disjoint seed_se epp_matrix /\ disjoint sp_matrix ep_matrix /\
      disjoint sp_matrix epp_matrix /\ disjoint ep_matrix epp_matrix)
    (ensures  fun h0 _ h1 -> modifies (loc sp_matrix |+| loc ep_matrix |+| loc epp_matrix) h0 h1 /\
      (as_matrix h1 sp_matrix, as_matrix h1 ep_matrix, as_matrix h1 epp_matrix) ==
      S.get_sp_ep_epp_matrices a (as_seq h0 seed_se))

let get_sp_ep_epp_matrices a seed_se sp_matrix ep_matrix epp_matrix =
  push_frame ();
  [@inline_let] let s_bytes_len = secretmatrixbytes_len a in
  let r = create (2ul *! s_bytes_len +! 2ul *! params_nbar *! params_nbar) (u8 0) in
  KG.frodo_shake_r a (u8 0x96) seed_se (2ul *! s_bytes_len +! 2ul *! params_nbar *! params_nbar) r;
  frodo_sample_matrix a params_nbar (params_n a) (sub r 0ul s_bytes_len) sp_matrix;
  frodo_sample_matrix a params_nbar (params_n a) (sub r s_bytes_len s_bytes_len) ep_matrix;
  frodo_sample_matrix a params_nbar params_nbar (sub r (2ul *! s_bytes_len) (2ul *! params_nbar *! params_nbar)) epp_matrix;
  pop_frame ()


inline_for_extraction noextract
val crypto_kem_enc_ct0:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> seed_a:lbytes bytes_seed_a
  -> b:lbytes (publicmatrixbytes_len a)
  -> mu:lbytes (bytes_mu a)
  -> 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
  -> ct:lbytes (crypto_ciphertextbytes a)
  -> Stack unit
    (requires fun h ->
      live h seed_a /\ live h b /\ live h mu /\ live h ct /\
      live h sp_matrix /\ live h ep_matrix /\ live h epp_matrix /\
      disjoint ct seed_a /\ disjoint ct b /\ disjoint ct mu /\
      disjoint ct sp_matrix /\ disjoint ct ep_matrix /\ disjoint ct epp_matrix)
    (ensures fun h0 _ h1 -> modifies (loc ct) h0 h1 /\
      (let c1:LB.lbytes (FP.ct1bytes_len a) = S.crypto_kem_enc_ct_pack_c1 a gen_a (as_seq h0 seed_a) (as_seq h0 sp_matrix) (as_seq h0 ep_matrix) in
      let c2:LB.lbytes (FP.ct2bytes_len a) = S.crypto_kem_enc_ct_pack_c2 a (as_seq h0 mu) (as_seq h0 b) (as_seq h0 sp_matrix) (as_seq h0 epp_matrix) in
      v (crypto_ciphertextbytes a) == FP.ct1bytes_len a + FP.ct2bytes_len a /\
      as_seq h1 ct `Seq.equal` LSeq.concat #_ #(FP.ct1bytes_len a) #(FP.ct2bytes_len a) c1 c2))

let crypto_kem_enc_ct0 a gen_a seed_a b mu sp_matrix ep_matrix epp_matrix ct =
  let c1 = sub ct 0ul (ct1bytes_len a) in
  let c2 = sub ct (ct1bytes_len a) (ct2bytes_len a) in
  let h0 = ST.get () in
  crypto_kem_enc_ct_pack_c1 a gen_a seed_a sp_matrix ep_matrix c1;
  let h1 = ST.get () in
  crypto_kem_enc_ct_pack_c2 a mu b sp_matrix epp_matrix c2;
  let h2 = ST.get () in
  LSeq.eq_intro
    (LSeq.sub (as_seq h2 ct) 0 (v (ct1bytes_len a)))
    (LSeq.sub (as_seq h1 ct) 0 (v (ct1bytes_len a)));
  LSeq.lemma_concat2
    (v (ct1bytes_len a)) (LSeq.sub (as_seq h1 ct) 0 (v (ct1bytes_len a)))
    (v (ct2bytes_len a)) (LSeq.sub (as_seq h2 ct) (v (ct1bytes_len a)) (v (ct2bytes_len a))) (as_seq h2 ct)


inline_for_extraction noextract
val clear_matrix3:
    a:FP.frodo_alg
  -> 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 sp_matrix /\ live h ep_matrix /\ live h epp_matrix /\
      disjoint sp_matrix ep_matrix /\ disjoint sp_matrix epp_matrix /\
      disjoint ep_matrix epp_matrix)
    (ensures  fun h0 _ h1 ->
      modifies (loc sp_matrix |+| loc ep_matrix |+| loc epp_matrix) h0 h1)

let clear_matrix3 a sp_matrix ep_matrix epp_matrix =
  clear_matrix sp_matrix;
  clear_matrix ep_matrix;
  clear_matrix epp_matrix

inline_for_extraction noextract
val crypto_kem_enc_ct:
    a:FP.frodo_alg
  -> gen_a:FP.frodo_gen_a{is_supported gen_a}
  -> mu:lbytes (bytes_mu a)
  -> pk:lbytes (crypto_publickeybytes a)
  -> seed_se:lbytes (crypto_bytes a)
  -> ct:lbytes (crypto_ciphertextbytes a)
  -> Stack unit
    (requires fun h ->
      live h mu /\ live h pk /\ live h seed_se /\ live h ct /\
      disjoint ct mu /\ disjoint ct pk /\ disjoint ct seed_se)
    (ensures fun h0 _ h1 -> modifies (loc ct) h0 h1 /\
      as_seq h1 ct == S.crypto_kem_enc_ct a gen_a (as_seq h0 mu) (as_seq h0 pk) (as_seq h0 seed_se))

#push-options "--z3rlimit 200"
let crypto_kem_enc_ct a gen_a mu pk seed_se ct =
  push_frame ();
  let h0 = ST.get () in
  FP.expand_crypto_publickeybytes a;
  let seed_a = sub pk 0ul bytes_seed_a in
  let b = sub pk bytes_seed_a (publicmatrixbytes_len a) in

  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;
  crypto_kem_enc_ct0 a gen_a seed_a b mu sp_matrix ep_matrix epp_matrix ct;

  clear_matrix3 a sp_matrix ep_matrix epp_matrix;
  let h1 = ST.get () in
  LSeq.eq_intro
    (as_seq h1 ct)
    (S.crypto_kem_enc_ct a gen_a (as_seq h0 mu) (as_seq h0 pk) (as_seq h0 seed_se));
  pop_frame ()
#pop-options

inline_for_extraction noextract
val crypto_kem_enc_ss:
    a:FP.frodo_alg
  -> k:lbytes (crypto_bytes a)
  -> ct:lbytes (crypto_ciphertextbytes a)
  -> ss:lbytes (crypto_bytes a)
  -> Stack unit
    (requires fun h ->
      live h k /\ live h ct /\ live h ss /\
      disjoint ct ss /\ disjoint k ct /\ disjoint k ss)
    (ensures  fun h0 _ h1 -> modifies (loc ss) h0 h1 /\
      as_seq h1 ss == S.crypto_kem_enc_ss a (as_seq h0 k) (as_seq h0 ct))
val crypto_kem_enc_ss:
    a:FP.frodo_alg
  -> k:lbytes (crypto_bytes a)
  -> ct:lbytes (crypto_ciphertextbytes a)
  -> ss:lbytes (crypto_bytes a)
  -> Stack unit
    (requires fun h ->
      live h k /\ live h ct /\ live h ss /\
      disjoint ct ss /\ disjoint k ct /\ disjoint k ss)
    (ensures  fun h0 _ h1 -> modifies (loc ss) h0 h1 /\
      as_seq h1 ss == S.crypto_kem_enc_ss a (as_seq h0 k) (as_seq h0 ct))

    a: Spec.Frodo.Params.frodo_alg ->
    k: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.crypto_bytes a) ->
    ct: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.crypto_ciphertextbytes a) ->
    ss: Hacl.Impl.Matrix.lbytes (Hacl.Impl.Frodo.Params.crypto_bytes a)
  -> FStar.HyperStack.ST.Stack Prims.unit