val initialize_symmetric :
     #nc : config
  -> protocol_name : hashable nc
  -> Tot (symmetric_state nc)
val initialize_symmetric :
     #nc : config
  -> protocol_name : hashable nc
  -> Tot (symmetric_state nc)
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 }
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 *)
/
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
protocol_name: Spec.Noise.CryptoPrimitives.hashable nc
  -> Spec.Noise.Base.Definitions.symmetric_state nc
Spec.Noise.CryptoPrimitives.config Spec.Noise.CryptoPrimitives.hashable Spec.Noise.Base.Definitions.Mksymmetric_state Spec.Noise.Base.Definitions.initialize_key FStar.Pervasives.Native.None Spec.Noise.CryptoPrimitives.aead_key Spec.Noise.CryptoPrimitives.hash Prims.op_LessThanOrEqual Spec.Noise.CryptoPrimitives.hash_size Lib.Sequence.concat Lib.IntTypes.uint8 Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.l_and Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.create Lib.IntTypes.mk_int Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan Lib.Sequence.index Lib.Sequence.create Lib.IntTypes.u8 Prims.int Prims.op_Subtraction Prims.bool Spec.Noise.CryptoPrimitives.do_hash Prims.pow2 Lib.Sequence.length Lib.IntTypes.uint_t Spec.Noise.Base.Definitions.symmetric_state
let initialize_symmetric #nc pname =
  
let pname_len:size_nat = length pname in
let h:hash nc =
  if pname_len <= hash_size nc
  then
    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
  else do_hash nc pname
in
{ c_state = initialize_key None; ck = h; h = h }