val tokens_message_vsv (nc: iconfig) (smi: meta_info) (is_psk: bool) (pattern: list message_token)
    : Tot (n: nat{n == tokens_message_size (get_config nc) smi.hsf.sk is_psk pattern})
val tokens_message_vsv (nc: iconfig) (smi: meta_info) (is_psk: bool) (pattern: list message_token)
    : Tot (n: nat{n == tokens_message_size (get_config nc) smi.hsf.sk is_psk pattern})
let tokens_message_vsv (nc : iconfig) (smi : meta_info) (is_psk : bool)
                       (pattern : list message_token) :
  Tot (n:nat{n == tokens_message_size (get_config nc) smi.hsf.sk is_psk pattern}) =
  (* We need to perform the normalization in 2 steps, otherwise it doesn't
   * work properly *)
  [@inline_let] let c = with_norm(get_config nc) in
  with_norm(tokens_message_size c smi.hsf.sk is_psk pattern)
module Impl.Noise.SendReceive

open FStar.Mul
module HS = FStar.HyperStack
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.RawIntTypes
open Lib.IntTypes

module HST = FStar.HyperStack.ST
open Lib.Sequence
module S = Lib.Sequence
module SB = FStar.Seq.Base
module L = FStar.List
module Seq = FStar.Seq

module B = LowStar.Buffer
module BS = Lib.ByteSequence
module LB = Lib.Buffer
open Lib.Buffer
module BB = Lib.ByteBuffer
open Lib.ByteBuffer

open LowStar.BufferOps

module Spec = Spec.Noise
open Spec.Noise
open Meta.Noise
open Impl.Noise.Types
open Impl.Noise.CipherState
open Impl.Noise.HKDF
open Impl.Noise.SymmetricState
open Impl.Noise.HandshakeState

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

(* TODO: move those functions? *)
inline_for_extraction noextract
let token_message_vsv (nc : iconfig) (smi : meta_info) (tk : message_token) :
  Tot size_nat =
  token_message_size (get_config nc) smi.hsf.sk tk

inline_for_extraction noextract
let token_message_vs (nc : iconfig) (smi : meta_info) (tk : message_token) :
  Tot size_t =
  size (token_message_vsv nc smi tk)

inline_for_extraction noextract
type token_message_t (nc : iconfig) (smi : meta_info) (tk : message_token) =
  lbuffer uint8 (token_message_vs nc smi tk)
/
Spec.Noise.fst.checked prims.fst.checked Meta.Noise.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.Types.fst.checked Impl.Noise.SymmetricState.fsti.checked Impl.Noise.HKDF.fsti.checked Impl.Noise.HandshakeState.fsti.checked Impl.Noise.CipherState.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.SendReceive.fsti

    nc: Impl.Noise.Types.iconfig ->
    smi: Spec.Noise.MetaInfo.meta_info ->
    is_psk: Prims.bool ->
    pattern: Prims.list Spec.Noise.Base.Definitions.message_token
  -> n:
    Prims.nat
      { n ==
        Spec.Noise.Lengths.tokens_message_size (Impl.Noise.Types.get_config nc)
          (Mkhandshake_state_flags?.sk (Mkmeta_info?.hsf smi))
          is_psk
          pattern }
Impl.Noise.Types.iconfig Spec.Noise.MetaInfo.meta_info Prims.bool Prims.list Spec.Noise.Base.Definitions.message_token Meta.Noise.with_norm Prims.nat Spec.Noise.Lengths.tokens_message_size Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__sk Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf Spec.Noise.CryptoPrimitives.config Prims.eq2 Impl.Noise.Types.get_config
let tokens_message_vsv (nc: iconfig) (smi: meta_info) (is_psk: bool) (pattern: list message_token)
    : Tot (n: nat{n == tokens_message_size (get_config nc) smi.hsf.sk is_psk pattern}) =
  
[@@ inline_let ]let c = with_norm (get_config nc) in
with_norm (tokens_message_size c smi.hsf.sk is_psk pattern)