val string_of_dh_length (nc: config) : n: nat{n = String.length (string_of_dh nc)}
val string_of_dh_length (nc: config) : n: nat{n = String.length (string_of_dh nc)}
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
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 *)
/
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
  -> n: Prims.nat{n = FStar.String.length (Spec.Noise.Base.Definitions.string_of_dh nc)}
Spec.Noise.CryptoPrimitives.config Spec.Noise.CryptoPrimitives.get_dh_alg Prims.nat Prims.b2t Prims.op_Equality FStar.String.length Spec.Noise.Base.Definitions.string_of_dh Prims.unit FStar.Pervasives.normalize_term_spec
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