val mix_key : #nc:config -> hashable_key nc -> symmetric_state nc -> Tot (symmetric_state nc)
val mix_key : #nc:config -> hashable_key nc -> symmetric_state nc -> Tot (symmetric_state nc)
let mix_key #nc key st =
  let ck, temp_k = kdf2 st.ck key in
  let temp_k' = key_from_hash temp_k in
  let c_st = initialize_key (Some temp_k') in
  { st with ck = ck; c_state = c_st }
module Spec.Noise.Base.Definitions

open FStar.Mul

open Lib.IntTypes
open Lib.RawIntTypes
open Lib.ByteSequence
open Lib.Sequence

open Spec.Noise.CryptoPrimitives

#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"

/// Small helper for the proofs


(*** Cipher state *)

let initialize_key k = { k = k; n = 0; }

let has_key st =
  match st.k with
  | None -> false
  | Some _ -> true

let set_nonce n st = ({ st with n = n; })

let encrypt_with_ad nc aad plain st =
  match st.k with
  | None -> Res (plain, st)
  | Some k' ->
    if st.n >= saturated_nonce_value then Fail Saturated_nonce else
    if length aad > aead_max_input nc then Fail Input_size else
    if length plain > aead_max_input nc then Fail Input_size else
    let cipher = aead_encrypt nc k' st.n aad plain in
    Res (cipher, {st with n = st.n + 1})

let decrypt_with_ad nc aad c st =
  match st.k with
  | None -> Res (c, st)
  | Some k' ->
    if st.n >= saturated_nonce_value then Fail Saturated_nonce else
    if length aad > aead_max_input nc then Fail Input_size else
    if length c < aead_tag_size then Fail Input_size else
    if length c > aead_max_input nc + aead_tag_size  then Fail Input_size else
    let r = aead_decrypt nc k' st.n aad c in
    match r with
    | None -> Fail Decryption
    | Some decrypted ->
      Res (decrypted, {st with n = st.n + 1})

(*** Symmetric state *)

let initialize_symmetric #nc pname =
  let pname_len : size_nat = length pname in
  let h : hash nc =
  begin
    if pname_len <= hash_size nc
    then
      begin
      let pad_size = (hash_size nc - pname_len) in
      let zeros = create pad_size (u8 0) in
      concat #uint8 #pname_len #pad_size pname zeros
      end
    else do_hash nc pname
  end in
  { c_state = initialize_key None; ck = h; h = h }


(** Facility function not in the Noise technical paper: if the hash size is 64,
  * truncates a hash to so that it can be used as a key *)
val key_from_hash : #nc:config -> hash nc -> aead_key
let key_from_hash #nc h = if hash_size nc = 64 then Seq.slice h 0 32 else h
/
Spec.Noise.CryptoPrimitives.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.Base.Definitions.fst

    key: Spec.Noise.CryptoPrimitives.hashable_key nc ->
    st: Spec.Noise.Base.Definitions.symmetric_state nc
  -> Spec.Noise.Base.Definitions.symmetric_state nc
Spec.Noise.CryptoPrimitives.config Spec.Noise.CryptoPrimitives.hashable_key Spec.Noise.Base.Definitions.symmetric_state Spec.Noise.CryptoPrimitives.hash Spec.Noise.Base.Definitions.Mksymmetric_state Spec.Noise.Base.Definitions.__proj__Mksymmetric_state__item__h Spec.Noise.Base.Definitions.cipher_state Spec.Noise.Base.Definitions.initialize_key FStar.Pervasives.Native.Some Spec.Noise.CryptoPrimitives.aead_key Spec.Noise.Base.Definitions.key_from_hash FStar.Pervasives.Native.tuple2 Spec.Noise.CryptoPrimitives.kdf2 Spec.Noise.Base.Definitions.__proj__Mksymmetric_state__item__ck
let mix_key #nc key st =
  
let ck, temp_k = kdf2 st.ck key in
let temp_k' = key_from_hash temp_k in
let c_st = initialize_key (Some temp_k') in
{ st with ck = ck; c_state = c_st }