val existsb_handshake_messages
      (checker: handshake_messages_crawl_checker)
      (is_psk ir: bool)
      (send_smi recv_smi: meta_info)
      (messages: list (list message_token))
    : Tot bool
val existsb_handshake_messages
      (checker: handshake_messages_crawl_checker)
      (is_psk ir: bool)
      (send_smi recv_smi: meta_info)
      (messages: list (list message_token))
    : Tot bool
let existsb_handshake_messages (checker : handshake_messages_crawl_checker)
                               (is_psk ir : bool)
                               (send_smi recv_smi : meta_info)
                               (messages : list (list message_token)) :
  Tot bool =
  crawl_handshake_messages bool (or_crawler checker) false is_psk ir send_smi recv_smi messages
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 }

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

inline_for_extraction noextract
let receive_token_update_smi (is_psk : bool) (tk : message_token)
                             (smi : meta_info) :
  Tot (greater_smi smi) =
  {
    hsf = receive_token_update_hsf is_psk tk smi.hsf;
    nonce = token_update_nonce smi.hsf.sk is_psk tk smi.nonce;
  }

inline_for_extraction noextract
let token_update_smi (is_psk sender : bool) (tk : message_token)
                     (smi : meta_info) :
  Tot (greater_smi smi) =
  if sender then send_token_update_smi is_psk tk smi
            else receive_token_update_smi is_psk tk smi

inline_for_extraction noextract
let send_tokens_update_smi (is_psk : bool) (pattern : list message_token)
                            (smi : meta_info) :
  greater_smi smi =
  let hsf1 = send_tokens_update_hsf is_psk pattern smi.hsf in
  let nonce1 = tokens_update_nonce smi.hsf.sk is_psk pattern smi.nonce in
  { hsf = hsf1; nonce = nonce1; }

inline_for_extraction noextract
let receive_tokens_update_smi (is_psk : bool) (pattern : list message_token)
                               (smi : meta_info) :
  greater_smi smi =
  let hsf1 = receive_tokens_update_hsf is_psk pattern smi.hsf in
  let nonce1 = tokens_update_nonce smi.hsf.sk is_psk pattern smi.nonce in
  { hsf = hsf1; nonce = nonce1; }

inline_for_extraction noextract
let send_message_update_smi (is_psk : bool) (pattern : list message_token)
                            (smi : meta_info) :
  greater_smi smi =
  let smi1 = send_tokens_update_smi is_psk pattern smi in
  { smi1 with nonce = if smi1.hsf.sk then smi1.nonce + 1 else smi1.nonce }

inline_for_extraction noextract
let receive_message_update_smi (is_psk : bool) (pattern : list message_token)
                               (smi : meta_info) :
  greater_smi smi =
  let smi1 = receive_tokens_update_smi is_psk pattern smi in
  { smi1 with nonce = if smi1.hsf.sk then smi1.nonce + 1 else smi1.nonce }

(*** Crawlers *)
(**** Compute over lisf of tokens *)
// TODO: those crawlers are more annoying than anything: get rid of them
(* TODO: for now, those are not used *)
type message_tokens_crawler (a : Type) : Type =
  (send_smi : meta_info) -> (recv_smi : meta_info) ->
  (tk : message_token) -> (acc : a) -> a

[@(strict_on_arguments [6])]
inline_for_extraction noextract
let rec crawl_message_tokens (a : Type)
                             (crawler : message_tokens_crawler a)
                             (acc : a)
                             (is_psk : bool)
                             (send_smi recv_smi : meta_info)
                             (message : list message_token) :
  Tot a (decreases message) =
  match message with
  | [] -> acc
  | tk :: message' ->
    (* Update the accumulator *)
    let acc1 = crawler send_smi recv_smi tk acc in
    (* Update the flags *)
    let send_smi1 = send_token_update_smi is_psk tk send_smi in
    let recv_smi1 = receive_token_update_smi is_psk tk recv_smi in
    (* Recursive call *)
    crawl_message_tokens a crawler acc1 is_psk send_smi recv_smi message'

(**** Compute over list of messages *)
(* Handshake pattern crawler: allows to traverse the messages of a
 * handshake_pattern with the proper meta_info for the sender
 * and the receiver *)
type handshake_messages_crawler (a : Type) : Type =
  (is_psk : bool) -> (ir : bool) ->
  (send_smi0 : meta_info) -> (recv_smi0 : meta_info) ->
  (send_smi1 : greater_smi recv_smi0) -> (recv_smi1 : greater_smi send_smi0) ->
  (msg : list message_token) -> (acc : a) -> a

(* A boolean crawler with no accumulator *)
type handshake_messages_crawl_checker =
  (is_psk : bool) -> (ir : bool) ->
  (send_smi0 : meta_info) -> (recv_smi0 : meta_info) ->
  (send_smi1 : greater_smi recv_smi0) -> (recv_smi1 : greater_smi send_smi0) ->
  (msg : list message_token) -> bool

let crawl_messages_update_smi (is_psk : bool)
                              (msg : list message_token)
                              (send_smi recv_smi : meta_info) :
  (fp:(meta_info & meta_info){
    less_than send_smi (snd fp) /\ less_than recv_smi (fst fp)})=
  let recv_smi1 = send_message_update_smi is_psk msg send_smi in
  let send_smi1 = receive_message_update_smi is_psk msg recv_smi in
  send_smi1, recv_smi1

[@(strict_on_arguments [7])]
let rec crawl_handshake_messages (a : Type)
                                 (crawler : handshake_messages_crawler a)
                                 (acc : a)
                                 (is_psk ir : bool)
                                 (send_smi recv_smi : meta_info)
                                 (messages : list (list message_token)) :
  Tot a (decreases messages) =
  match messages with
  | [] -> acc
  | msg :: messages' ->
    (* Update the flags over the pattern, invert the sender and receiver *)
    let send_smi1, recv_smi1 = crawl_messages_update_smi is_psk msg send_smi recv_smi in
    (* Update the accumulator *)
    let acc1 = crawler is_psk ir send_smi recv_smi send_smi1 recv_smi1 msg acc in
    (* Recursive call: negate the direction and reverse the sender and receiver flags *)
    crawl_handshake_messages a crawler acc1 is_psk (not ir) send_smi1 recv_smi1 messages'

let crawl_forallb_handshake_messages (checker : handshake_messages_crawl_checker)
                                     (is_psk ir : bool)
                                     (send_smi recv_smi : meta_info)
                                     (messages : list (list message_token)) :
  Tot bool =
  let acc_checker is_psk ir sf0 rf0 sf1 rf1 msg acc =
    acc && checker is_psk ir sf0 rf0 sf1 rf1 msg
  in
  crawl_handshake_messages bool acc_checker true is_psk ir send_smi recv_smi messages

let and_crawler (checker : handshake_messages_crawl_checker)
                (is_psk ir : bool)
                (ssmi0 rsmi0 : meta_info)
                (ssmi1 : greater_smi rsmi0) (rsmi1 : greater_smi ssmi0)
                (msg : list message_token) (acc : bool) : Tot bool =
  acc && checker is_psk ir ssmi0 rsmi0 ssmi1 rsmi1 msg

let or_crawler (checker : handshake_messages_crawl_checker)
               (is_psk ir : bool)
               (ssmi0 rsmi0 : meta_info)
               (ssmi1 : greater_smi rsmi0) (rsmi1 : greater_smi ssmi0)
               (msg : list message_token) (acc : bool) : Tot bool =
  acc || checker is_psk ir ssmi0 rsmi0 ssmi1 rsmi1 msg

let forallb_handshake_messages (checker : handshake_messages_crawl_checker)
                               (is_psk ir : bool)
                               (send_smi recv_smi : meta_info)
                               (messages : list (list message_token)) :
  Tot bool =
  crawl_handshake_messages bool (and_crawler checker) true is_psk ir send_smi recv_smi messages
/
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

    checker: Spec.Noise.MetaInfo.handshake_messages_crawl_checker ->
    is_psk: Prims.bool ->
    ir: Prims.bool ->
    send_smi: Spec.Noise.MetaInfo.meta_info ->
    recv_smi: Spec.Noise.MetaInfo.meta_info ->
    messages: Prims.list (Prims.list Spec.Noise.Base.Definitions.message_token)
  -> Prims.bool
Spec.Noise.MetaInfo.handshake_messages_crawl_checker Prims.bool Spec.Noise.MetaInfo.meta_info Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.MetaInfo.crawl_handshake_messages Spec.Noise.MetaInfo.or_crawler
let existsb_handshake_messages
      (checker: handshake_messages_crawl_checker)
      (is_psk ir: bool)
      (send_smi recv_smi: meta_info)
      (messages: list (list message_token))
    : Tot bool =
  
crawl_handshake_messages bool (or_crawler checker) false is_psk ir send_smi recv_smi messages