val send_token_update_smi (is_psk: bool) (tk: message_token) (smi: meta_info)
    : Tot (greater_smi smi)
val send_token_update_smi (is_psk: bool) (tk: message_token) (smi: meta_info)
    : Tot (greater_smi smi)
let send_token_update_smi (is_psk : bool) (tk : message_token)
                          (smi : meta_info) :
  Tot (greater_smi smi) =
  {
    hsf = send_token_update_hsf is_psk tk smi.hsf;
    nonce = token_update_nonce smi.hsf.sk is_psk tk smi.nonce;
  }
module Spec.Noise.MetaInfo
open FStar.Mul

open Spec.Noise.Base
open Spec.Noise.HandshakeFlags
open Spec.Noise.NonceCounter

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

/// Defines the information about the handshake state that we will carry around
/// in the implementation functions. We qualify this information as meta because:
/// - it is statically known
/// - it has an influence on computation (for example: encryption/decryption is
///   conditionned at several positions on the presence of a symmetric key - still:
///   note that part of the information is actually ghost)
/// - the structures carrying this information will be erased by post-processing and
///   inlining and thus won't appear in the generated code, and the branches testing
///   meta booleans will be simplified thus leading to correctly specialized code

// TODO: we could put the [is_psk] and [initiator] field inside the [meta_info].
// Or at leat initiator

(** state meta info *)
inline_for_extraction //noextract
type meta_info = {
  hsf : handshake_state_flags;
  nonce : nat;
}

/// [meta_info] is monotonous over a handshake execution

noextract
let less_than (smi1 smi2 : meta_info) : Tot bool =
  Spec.Noise.HandshakeFlags.less_than smi1.hsf smi2.hsf

inline_for_extraction noextract
type greater_smi (smi0 : meta_info) =
  smi1:meta_info{less_than smi0 smi1}

let smi_set_psk (psk : bool) (smi : meta_info) : Tot meta_info =
  { smi with hsf = { smi.hsf with psk = psk } }

let smi_set_sk (sk : bool) (smi : meta_info) : Tot meta_info =
  { smi with hsf = { smi.hsf with sk = sk; } }

let smi_or_set_psk (psk : bool) (smi : meta_info) : Tot meta_info =
  { smi with hsf = { smi.hsf with psk = psk || smi.hsf.psk } }

(*** Update functions *)
noextract
let receive_pretoken_update_smi (tk : premessage_token) (smi : meta_info) :
  Tot meta_info =
  { smi with hsf = receive_pretoken_update_hsf tk smi.hsf }

noextract
let receive_premessage_update_smi (pattern : list premessage_token)
                                  (smi : meta_info) :
  smi':greater_smi smi {
    let hsf, hsf' = smi.hsf, smi'.hsf in
    hsf'.sk == hsf.sk /\ hsf'.s == hsf.s /\ hsf'.e == hsf.e /\ hsf'.psk == hsf.psk} =
  { smi with hsf = receive_premessage_update_hsf pattern smi.hsf }
/
Spec.Noise.NonceCounter.fsti.checked Spec.Noise.HandshakeFlags.fsti.checked Spec.Noise.Base.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
Spec.Noise.MetaInfo.fsti

    is_psk: Prims.bool ->
    tk: Spec.Noise.Base.Definitions.message_token ->
    smi: Spec.Noise.MetaInfo.meta_info
  -> Spec.Noise.MetaInfo.greater_smi smi
Prims.bool Spec.Noise.Base.Definitions.message_token Spec.Noise.MetaInfo.meta_info Spec.Noise.MetaInfo.Mkmeta_info Spec.Noise.HandshakeFlags.send_token_update_hsf Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf Spec.Noise.NonceCounter.token_update_nonce Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__sk Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__nonce Spec.Noise.MetaInfo.greater_smi
let send_token_update_smi (is_psk: bool) (tk: message_token) (smi: meta_info)
    : Tot (greater_smi smi) =
  
{
  hsf = send_token_update_hsf is_psk tk smi.hsf;
  nonce = token_update_nonce smi.hsf.sk is_psk tk smi.nonce
}