val less_than (smi1 smi2: meta_info) : Tot bool
val less_than (smi1 smi2: meta_info) : Tot bool
let less_than (smi1 smi2 : meta_info) : Tot bool =
  Spec.Noise.HandshakeFlags.less_than smi1.hsf smi2.hsf
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
/
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
smi1: Spec.Noise.MetaInfo.meta_info -> smi2: Spec.Noise.MetaInfo.meta_info -> Prims.bool
Spec.Noise.MetaInfo.meta_info Spec.Noise.HandshakeFlags.less_than Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf Prims.bool
let less_than (smi1 smi2: meta_info) : Tot bool =
  
Spec.Noise.HandshakeFlags.less_than smi1.hsf smi2.hsf