val encrypt_with_ad : nc:config -> aad:bytes -> plain:bytes -> cipher_state ->
                      Tot (eresult (bytes & cipher_state))
val encrypt_with_ad : nc:config -> aad:bytes -> plain:bytes -> cipher_state ->
                      Tot (eresult (bytes & cipher_state))
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})
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; })
/
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

    nc: Spec.Noise.CryptoPrimitives.config ->
    aad: Lib.ByteSequence.bytes ->
    plain: Lib.ByteSequence.bytes ->
    st: Spec.Noise.Base.Definitions.cipher_state
  -> Spec.Noise.Base.Definitions.eresult (Lib.ByteSequence.bytes *
        Spec.Noise.Base.Definitions.cipher_state)
Spec.Noise.CryptoPrimitives.config Lib.ByteSequence.bytes Spec.Noise.Base.Definitions.cipher_state Spec.Noise.Base.Definitions.__proj__Mkcipher_state__item__k Spec.Noise.Base.Definitions.Res FStar.Pervasives.Native.tuple2 Spec.Noise.Base.Definitions.error FStar.Pervasives.Native.Mktuple2 Spec.Noise.CryptoPrimitives.aead_key Prims.op_GreaterThanOrEqual Spec.Noise.Base.Definitions.__proj__Mkcipher_state__item__n Spec.Noise.Base.Definitions.saturated_nonce_value Spec.Noise.Base.Definitions.Fail Spec.Noise.Base.Definitions.Saturated_nonce Prims.bool Prims.op_GreaterThan Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Noise.CryptoPrimitives.aead_max_input Spec.Noise.Base.Definitions.Input_size Spec.Noise.Base.Definitions.Mkcipher_state Prims.op_Addition Lib.Sequence.seq Lib.IntTypes.int_t Prims.eq2 Prims.int Spec.Noise.CryptoPrimitives.aead_tag_size Spec.Noise.CryptoPrimitives.aead_encrypt Spec.Noise.Base.Definitions.eresult
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 })