val protocol_name_length (patlength: nat) (nc: config) : nat
val protocol_name_length (patlength: nat) (nc: config) : nat
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
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
/
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
patlength: Prims.nat -> nc: Spec.Noise.CryptoPrimitives.config -> Prims.nat
Prims.nat Spec.Noise.CryptoPrimitives.config Prims.op_Addition Spec.Noise.Lengths.string_of_dh_length Spec.Noise.Lengths.string_of_aead_length Spec.Noise.Lengths.string_of_hash_length
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