val token_message_size (nc: config) (has_sym_key: bool) (tk: message_token) : size_nat
val token_message_size (nc: config) (has_sym_key: bool) (tk: message_token) : size_nat
let token_message_size (nc : config) (has_sym_key : bool) (tk : message_token) :
  size_nat =
  match tk with
  | S -> opt_encrypt_size has_sym_key (public_key_size nc)
  | E -> public_key_size nc
  | _ -> 0
module Spec.Noise.Lengths

open FStar.Mul

open Lib.IntTypes
open Lib.ByteSequence
open Lib.Sequence
module L = LowStar.Literal

open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base
open Spec.Noise.HandshakeFlags

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

(*** Protocol name *)

let string_of_dh_length (nc : config) : n:nat{n = String.length (string_of_dh nc)} =
  (**) normalize_term_spec (String.length "25519");
  match get_dh_alg nc with
  | Spec.Agile.DH.DH_Curve25519 -> 5

let string_of_aead_length (nc: config) : n:nat{n = String.length (string_of_aead nc)} =
  (**) normalize_term_spec (String.length "AESGCM");
  (**) normalize_term_spec (String.length "ChaChaPoly");
  match get_aead_alg nc with
  | Spec.Agile.AEAD.AES256_GCM -> 6
  | Spec.Agile.AEAD.CHACHA20_POLY1305 -> 10

let string_of_hash_length (nc: config) : n:nat{n = String.length (string_of_hash nc)} =
  (**) normalize_term_spec (String.length "SHA256");
  (**) normalize_term_spec (String.length "SHA512");
  (**) normalize_term_spec (String.length "BLAKE2s");
  (**) normalize_term_spec (String.length "BLAKE2b");
  match get_hash_alg nc with
  | Spec.Agile.Hash.SHA2_256 -> 6
  | Spec.Agile.Hash.SHA2_512 -> 6
  | Spec.Agile.Hash.Blake2S -> 7
  | Spec.Agile.Hash.Blake2B -> 7

let protocol_name_length (patlength : nat) (nc: config) : nat =
  patlength + 9 + string_of_dh_length nc + string_of_aead_length nc + string_of_hash_length nc

val protocol_name_length_eq (pat: string) (nc: config) :
  Lemma (String.length (compute_protocol_name pat nc) = protocol_name_length (String.length pat) nc)

val protocol_name_length_lem (patlength : nat) (nc: config) :
  Lemma (protocol_name_length patlength nc <= patlength + 31)

val protocol_name_ascii_lem (pat: string) (c: config): Lemma
  (requires (L.is_ascii_string pat))
  (ensures (L.is_ascii_string (compute_protocol_name pat c)))
  [ SMTPat (L.is_ascii_string (compute_protocol_name pat c)) ]

(*** Length functions *)
inline_for_extraction noextract
let encrypt_size (n : nat) : Tot nat =
  n + aead_tag_size

inline_for_extraction noextract
let opt_encrypt_size (encrypt : bool) (n : nat) :
  Tot nat =
  if encrypt then encrypt_size n else n

inline_for_extraction noextract
let decrypt_size (n : size_nat{n >= encrypt_size 0}) : Tot size_nat =
  n - aead_tag_size

inline_for_extraction noextract
let opt_decrypt_size (has_sym_key : bool)
  (l : size_nat{l >= opt_encrypt_size has_sym_key 0}) =
  if has_sym_key then decrypt_size l else l
/
Spec.Noise.HandshakeFlags.fsti.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.fst.checked Spec.Agile.DH.fst.checked prims.fst.checked LowStar.Literal.fsti.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.String.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.Lengths.fsti

    nc: Spec.Noise.CryptoPrimitives.config ->
    has_sym_key: Prims.bool ->
    tk: Spec.Noise.Base.Definitions.message_token
  -> Lib.IntTypes.size_nat
Spec.Noise.CryptoPrimitives.config Prims.bool Spec.Noise.Base.Definitions.message_token Spec.Noise.Lengths.opt_encrypt_size Spec.Noise.CryptoPrimitives.public_key_size Lib.IntTypes.size_nat
let token_message_size (nc: config) (has_sym_key: bool) (tk: message_token) : size_nat =
  
match tk with
| S -> opt_encrypt_size has_sym_key (public_key_size nc)
| E -> public_key_size nc
| _ -> 0