val receive_message_return_type : smi: Spec.Noise.MetaInfo.meta_info ->
    is_psk: Prims.bool ->
    pattern: Prims.list Spec.Noise.Base.Definitions.message_token
  -> y:
    Impl.Noise.Types.return_type
      {y == Impl.Noise.SendReceive.message_return_type smi is_psk false pattern}
let receive_message_return_type smi is_psk pattern =
  with_norm(message_return_type smi is_psk false 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)

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; }

inline_for_extraction noextract
let receive_prim_error_code : Type0 =
  r:prim_error_code{
    r == CSuccess \/ r == CDH_error \/ r == CDecrypt_error}

inline_for_extraction noextract
let receive_return_type : return_type =
  { prim_error_code_return_type with
    rty = receive_prim_error_code; }

/// The following types and functions are used to statically compute information
/// about the operations performed in the pattern, in order to determine which
/// return type is relevant. For instance: hash, DH, encryption/decryption.
inline_for_extraction //noextract
type pattern_type_ops = {
  hash_op : bool;
  dh_op : bool;
  sk_op : bool;
  
  (* The following field is not directly used to compute the return type:
   * we need it to keep track whether there is a symmetric key in the cipher
   * state so as to compute correctly the [sk_op] field *)
  has_sk : bool;
}

let init_pto (has_sk : bool) : pattern_type_ops =
  { hash_op = false; dh_op = false; sk_op = false; has_sk = has_sk; }

/// [patter_type_ops] is monotonous over a pattern execution
noextract
let pto_less_than (pto0 pto1 : pattern_type_ops) : Tot bool =
  (pto1.hash_op || (not pto0.hash_op)) &&
  (pto1.dh_op || (not pto0.dh_op)) &&
  (pto1.sk_op || (not pto0.sk_op)) &&
  (pto1.has_sk || (not pto0.has_sk))

inline_for_extraction noextract
type greater_pto (pto0 : pattern_type_ops) =
  pto1:pattern_type_ops{pto_less_than pto0 pto1}

let pto_do_hash (pto : pattern_type_ops) : greater_pto pto =
  { pto with hash_op = true }

let pto_do_dh_hash (pto : pattern_type_ops) : greater_pto pto =
  { pto with hash_op = true; dh_op = true; has_sk = true; }

let pto_do_cipher_hash (pto : pattern_type_ops) : greater_pto pto =
  { pto with hash_op = true; sk_op = pto.sk_op || pto.has_sk }

let pto_do_mix_key_hash (pto : pattern_type_ops) : greater_pto pto =
  { pto with hash_op = true; has_sk = true }

/// Functions to compute a pto over a pattern
#push-options "--ifuel 1"
inline_for_extraction noextract
let token_update_pto (is_psk : bool) (tk : message_token)
                     (pto : pattern_type_ops) : greater_pto pto =
  match tk with
  | S -> pto_do_cipher_hash pto
  | E -> if is_psk then pto_do_mix_key_hash pto else pto_do_hash pto
  | SS | EE | SE | ES -> pto_do_dh_hash pto
  | PSK -> pto_do_mix_key_hash pto
#pop-options

inline_for_extraction noextract
let compute_token_pto (smi : meta_info) (is_psk : bool)
                      (tk : message_token) :
  Tot pattern_type_ops =
  with_norm (token_update_pto is_psk tk (init_pto smi.hsf.sk))

#push-options "--ifuel 1"
[@(strict_on_arguments [1])]
inline_for_extraction noextract
let rec tokens_update_pto (is_psk : bool) (pattern : list message_token)
                          (pto : pattern_type_ops) :
  Tot (greater_pto pto)
  (decreases pattern) =
  match pattern with
  | [] -> pto
  | tk :: pattern' ->
    tokens_update_pto is_psk pattern' (token_update_pto is_psk tk pto)
#pop-options

inline_for_extraction noextract
let compute_tokens_pto (smi : meta_info) (is_psk : bool)
                       (pattern : list message_token) :
  Tot pattern_type_ops =
  with_norm (tokens_update_pto is_psk pattern (init_pto smi.hsf.sk))

[@(strict_on_arguments [1])]
inline_for_extraction noextract
let message_update_pto (is_psk : bool) (pattern : list message_token)
                       (pto : pattern_type_ops) :
  Tot (greater_pto pto) =
  let pto1 = tokens_update_pto is_psk pattern pto in
  pto_do_cipher_hash pto1

// Don't put strict_on_arguments here: makes [send_message_tokens_with_payload_m] loop
inline_for_extraction noextract
let compute_message_pto (smi : meta_info) (is_psk : bool)
                        (pattern : list message_token) :
  Tot pattern_type_ops =
  with_norm (message_update_pto is_psk pattern (init_pto smi.hsf.sk))

/// Useful lemma, especially for type conversions
#push-options "--fuel 1 --ifuel 1"
let rec tokens_update_pto_monotonous (is_psk : bool)
                                     (pattern : list message_token)
                                     (pto0 pto1 : pattern_type_ops) :
  Lemma
  (requires (pto0 `pto_less_than` pto1))
  (ensures (
    tokens_update_pto is_psk pattern pto0 `pto_less_than`
      tokens_update_pto is_psk pattern pto1))
  (decreases pattern) =
  match pattern with
  | [] -> ()
  | tk :: pattern' ->
    let pto0' = token_update_pto is_psk tk pto0 in
    let pto1' = token_update_pto is_psk tk pto1 in
    tokens_update_pto_monotonous is_psk pattern' pto0' pto1'
#pop-options

/// Consistency of the computation of the has_sk field:
let token_update_pto_has_sk_consistent (is_psk : bool) (tk : message_token)
                                       (pto : pattern_type_ops) :
  Lemma((token_update_pto is_psk tk pto).has_sk ==
        token_update_sym_key_flag pto.has_sk is_psk tk) = ()

#push-options "--fuel 1 --ifuel 1"
let rec tokens_update_pto_has_sk_consistent (is_psk : bool) (pattern : list message_token)
                                            (pto : pattern_type_ops) :
  Lemma
  (requires True)
  (ensures (
    (tokens_update_pto is_psk pattern pto).has_sk ==
    tokens_update_sym_key_flag pto.has_sk is_psk pattern))
  (decreases pattern) =
  match pattern with
  | [] -> ()
  | tk :: pattern' ->
    let pto' = token_update_pto is_psk tk pto in
    tokens_update_pto_has_sk_consistent is_psk pattern' pto'
#pop-options

/// Below, we define the general return types used by the send/receive message
/// functions.

/// This return type is only used in [return_type_from_pto] (see the explanations below)
let dh_use_sk_rtype (sender : bool) : Type0 =
  r:prim_error_code{
    if sender then
      r <> CDecrypt_error
    else True
  }

let dh_use_sk_return_type (sender : bool) : return_type =
  { prim_error_code_return_type with
    rty = dh_use_sk_rtype sender; }

/// Conversion from a [pattern_type_ops]. Note that some of the branches won't
/// actually be used (they are not legit operation combinations for a token/pattern),
/// but we define them in a way which is consistent with the rest because it eases/
/// makes possible some proofs later on (in particular the proofs about return type
/// conversions).
[@(strict_on_arguments [0;1])]
inline_for_extraction noextract
let return_type_from_pto (sender : bool) (pto : pattern_type_ops) :
  return_type =
  match pto.hash_op, pto.dh_op, pto.sk_op with
  | false, false, false -> unit_return_type
  | false, false, true -> (* won't happen *)
    if sender then encrypt_return_type else decrypt_return_type
  | false, true, false -> (* won't happen *)
    dh_return_type
  | false, true, true -> (* won't happen *)
    dh_use_sk_return_type sender
  | true, false, false -> hash_return_type
  | true, true, false -> dh_hash_return_type
  | true, false, true -> if sender then encrypt_hash_return_type
                                   else decrypt_hash_return_type true //pto.sk_op
  | true, true, true -> if sender then send_return_type else receive_return_type

/// token message error code

inline_for_extraction noextract
let token_message_return_type (smi : meta_info) (is_psk sender : bool)
                              (tk : message_token) : return_type =
  with_norm(
    let pto = compute_token_pto smi is_psk tk in
    return_type_from_pto sender pto)

inline_for_extraction noextract
let send_token_return_type smi is_psk tk =
  with_norm(token_message_return_type smi is_psk true tk)

inline_for_extraction noextract
let receive_token_return_type smi is_psk tk =
  with_norm(token_message_return_type smi is_psk false tk)

inline_for_extraction noextract
let tokens_message_return_type (smi : meta_info) (is_psk sender : bool)
                               (pattern : list message_token) : return_type =
  with_norm(
    let pto = compute_tokens_pto smi is_psk pattern in
    return_type_from_pto sender pto)

inline_for_extraction noextract
let send_tokens_return_type smi is_psk pattern =
  with_norm(tokens_message_return_type smi is_psk true pattern)

inline_for_extraction noextract
let receive_tokens_return_type smi is_psk pattern =
  with_norm(tokens_message_return_type smi is_psk false pattern)

inline_for_extraction noextract
let message_return_type (smi : meta_info) (is_psk sender : bool)
                        (pattern : list message_token) : return_type =
  with_norm(
    let pto = compute_message_pto smi is_psk pattern in
    return_type_from_pto sender pto)

// Don't put strict_on_arguments here: it causes type inference to loop
// in [Impl.Noise.RecursiveMessages.send_message_tokens_with_payload_m]
inline_for_extraction noextract
let send_message_return_type smi is_psk pattern =
  with_norm(message_return_type smi is_psk true pattern)

// Don't put strict_on_arguments here: it causes type inference to loop in
// [Impl.Noise.PatternMessages.Definitions.to_creceive_message_rtype]
/
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

    smi: Spec.Noise.MetaInfo.meta_info ->
    is_psk: Prims.bool ->
    pattern: Prims.list Spec.Noise.Base.Definitions.message_token
  -> y:
    Impl.Noise.Types.return_type
      {y == Impl.Noise.SendReceive.message_return_type smi is_psk false pattern}
Spec.Noise.MetaInfo.meta_info Prims.bool Prims.list Spec.Noise.Base.Definitions.message_token Meta.Noise.with_norm Impl.Noise.Types.return_type Impl.Noise.SendReceive.message_return_type Prims.eq2
let receive_message_return_type smi is_psk pattern =
  
with_norm (message_return_type smi is_psk false pattern)