val no_remote_pretokens (smi: meta_info) (pattern: list premessage_token)
    : Tot bool (decreases pattern)
val no_remote_pretokens (smi: meta_info) (pattern: list premessage_token)
    : Tot bool (decreases pattern)
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
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
/
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 ->
    pattern: Prims.list Spec.Noise.Base.Definitions.premessage_token
  -> Prims.Tot Prims.bool
Spec.Noise.MetaInfo.meta_info Prims.list Spec.Noise.Base.Definitions.premessage_token Spec.Noise.WellFormedness.no_remote_pretoken Spec.Noise.WellFormedness.no_remote_pretokens Spec.Noise.MetaInfo.receive_pretoken_update_smi Prims.bool
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