val check_send_message_smi (smi: meta_info) (initiator is_psk: bool) (message: list message_token)
    : Tot bool (decreases message)
val check_send_message_smi (smi: meta_info) (initiator is_psk: bool) (message: list message_token)
    : Tot bool (decreases message)
let rec check_send_message_smi (smi : meta_info)
                               (initiator is_psk : bool)
                               (message : list message_token) :
  Tot bool (decreases message) =
  match message with
  | [] ->
    (* For the payload encryption *)
    smi.nonce < saturated_nonce_value
  | tk :: message' ->
    if check_send_token_smi smi initiator tk then
      let smi' = send_token_update_smi is_psk tk smi in
      check_send_message_smi smi' initiator is_psk message'
    else false
module Spec.Noise.WellFormedness
/// This file defines two notions of well-formedness:
/// - one of them is the well-formedness defined by Trevor Perrin in the Noise
///   technical paper (section 7.3)
/// - the other one is an internal requirement for a pattern to be implementable:
///   it just checks that the pattern can be executed, or rather than it doesn't
///   provably always fail (because some keys are exchanged twice for example).

open FStar.Mul

open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base
open Spec.Noise.HandshakeFlags
open Spec.Noise.Lengths
open Spec.Noise.NonceCounter
open Spec.Noise.MetaInfo

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

(*** Premessages *)
noextract
let has_pretoken (smi : meta_info) (tk : premessage_token) : Tot bool =
  match tk with
  | PS -> smi.hsf.s
  | PE -> smi.hsf.e

[@(strict_on_arguments [1])]
let has_pretokens (smi : meta_info) (pattern : list premessage_token) :
  Tot bool =
  List.Tot.for_all (has_pretoken smi) pattern

noextract
let no_remote_pretoken (smi : meta_info) (tk : premessage_token) :
  Tot bool =
  match tk with
  | PS -> smi.hsf.rs = false
  | PE -> smi.hsf.re = false

[@(strict_on_arguments [1])]
let rec no_remote_pretokens (smi : meta_info)
                            (pattern : list premessage_token) :
  Tot bool
  (decreases pattern) =
  match pattern with
  | [] -> true
  | tk :: pattern' ->
    if no_remote_pretoken smi tk then
      let smi' = receive_pretoken_update_smi tk smi in
      no_remote_pretokens smi' pattern'
    else false

(*** Send/receive conditions *)
(**** Predicates *)
(** We begin by checking that a pattern is executable (which actually gives
    us rule 1 and 2, together with non-saturation of nonces) *)
let check_token_nonce (smi : meta_info) (token : message_token) : Tot bool =
  if token = S then smi.nonce < saturated_nonce_value else true

let check_send_token_hsf (hsf : handshake_state_flags) (initiator : bool)
                         (tk : message_token) : Tot bool =
  match tk with
  | S -> hsf.s
  | E -> hsf.e
  | SS -> hsf.s && hsf.rs
  | EE -> hsf.e && hsf.re
  | SE -> if initiator then hsf.s && hsf.re
                       else hsf.e && hsf.rs
  | ES -> if initiator then hsf.e && hsf.rs
                       else hsf.s && hsf.re
  | PSK -> hsf.psk

let check_send_token_smi (smi : meta_info) (initiator : bool)
                         (tk : message_token) : Tot bool =
  check_send_token_hsf smi.hsf initiator tk &&
  check_token_nonce smi tk
/
Spec.Noise.NonceCounter.fsti.checked Spec.Noise.MetaInfo.fsti.checked Spec.Noise.Lengths.fsti.checked Spec.Noise.HandshakeFlags.fsti.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.fst.checked prims.fst.checked LowStar.Literal.fsti.checked Lib.IntTypes.fsti.checked FStar.String.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
Spec.Noise.WellFormedness.fsti

    smi: Spec.Noise.MetaInfo.meta_info ->
    initiator: Prims.bool ->
    is_psk: Prims.bool ->
    message: Prims.list Spec.Noise.Base.Definitions.message_token
  -> Prims.Tot Prims.bool
Spec.Noise.MetaInfo.meta_info Prims.bool Prims.list Spec.Noise.Base.Definitions.message_token Prims.op_LessThan Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__nonce Spec.Noise.Base.Definitions.saturated_nonce_value Spec.Noise.WellFormedness.check_send_token_smi Spec.Noise.WellFormedness.check_send_message_smi Spec.Noise.MetaInfo.greater_smi Spec.Noise.MetaInfo.send_token_update_smi
let rec check_send_message_smi
      (smi: meta_info)
      (initiator is_psk: bool)
      (message: list message_token)
    : Tot bool (decreases message) =
  
match message with
| [] -> smi.nonce < saturated_nonce_value
| tk :: message' ->
  if check_send_token_smi smi initiator tk
  then
    let smi' = send_token_update_smi is_psk tk smi in
    check_send_message_smi smi' initiator is_psk message'
  else false