val receive_prim_error_code:Type0
val receive_prim_error_code:Type0
let receive_prim_error_code : Type0 =
  r:prim_error_code{
    r == CSuccess \/ r == CDH_error \/ r == CDecrypt_error}
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)

inline_for_extraction noextract
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)

inline_for_extraction noextract
let tokens_message_vs (nc : iconfig) (smi : meta_info) (is_psk : bool)
                      (pattern : list message_token) :
  Pure size_t
  (requires (tokens_message_vsv nc smi is_psk pattern <= max_size_t))
  (ensures (fun _ -> True)) =
  size (tokens_message_vsv nc smi is_psk pattern)

inline_for_extraction noextract
let message_vsv
  (nc : iconfig) (smi : meta_info) (is_psk : bool)
  (pattern : list message_token)
  (payload_len : size_nat{payload_len + aead_tag_size + hash_size (get_config nc) <= max_size_t}) :
  Tot (n:nat{n == message_size (get_config nc) smi.hsf.sk is_psk pattern payload_len}) =
  [@inline_let] let c = with_norm(get_config nc) in
  with_norm(message_size c smi.hsf.sk is_psk pattern payload_len)

/// In the following we define the return types for the send message functions.
/// Note that we try to be as precise as possible so as to remove as many tests
/// as we can, and use unit as the return type for our functions whenever possible.

/// Most general message return types (handle hash, dh and encryption/decryption
/// errors). Those types will be used in more precise types (which adapt the error
/// code precision to the pattern) defined below.
inline_for_extraction noextract
let send_prim_error_code : Type0 =
  r:prim_error_code{
    r == CSuccess \/ r == CDH_error}

inline_for_extraction noextract
let send_return_type : return_type =
  { prim_error_code_return_type with
    rty = send_prim_error_code; }
/
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
Type0
Impl.Noise.Types.prim_error_code Prims.l_or Prims.eq2 Impl.Noise.Types.error_code Impl.Noise.Types.CSuccess Impl.Noise.Types.CDH_error Impl.Noise.Types.CDecrypt_error
let receive_prim_error_code:Type0 =
  
r: prim_error_code{r == CSuccess \/ r == CDH_error \/ r == CDecrypt_error}