val existsb_handshake_messages_or_lem (checker : handshake_messages_crawl_checker)
                                      (b0 : bool)
                                      (is_psk ir : bool)
                                      (ssmi rsmi : meta_info)
                                      (msg : list message_token)
                                      (messages : list (list message_token)) :
  Lemma
  (ensures (
    crawl_handshake_messages bool (or_crawler checker) b0 is_psk
                             ir ssmi rsmi (msg :: messages) =
    (let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg ssmi rsmi in
     let ir1 = not ir in
     let b1 = b0 || (checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg) in
     let b2 = existsb_handshake_messages checker is_psk ir1 ssmi1 rsmi1 messages in
     b1 || b2)))
  (decreases messages)
val existsb_handshake_messages_or_lem (checker : handshake_messages_crawl_checker)
                                      (b0 : bool)
                                      (is_psk ir : bool)
                                      (ssmi rsmi : meta_info)
                                      (msg : list message_token)
                                      (messages : list (list message_token)) :
  Lemma
  (ensures (
    crawl_handshake_messages bool (or_crawler checker) b0 is_psk
                             ir ssmi rsmi (msg :: messages) =
    (let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg ssmi rsmi in
     let ir1 = not ir in
     let b1 = b0 || (checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg) in
     let b2 = existsb_handshake_messages checker is_psk ir1 ssmi1 rsmi1 messages in
     b1 || b2)))
  (decreases messages)
let rec existsb_handshake_messages_or_lem (checker : handshake_messages_crawl_checker)
                                          (b0 : bool)
                                          (is_psk ir : bool)
                                          (ssmi rsmi : meta_info)
                                          (msg : list message_token)
                                          (messages : list (list message_token)) =
  match messages with
  | [] -> ()
  | [msg1] -> ()
  | msg1 :: messages1 ->
    let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg ssmi rsmi in
    let ir1 = not ir in
    let b1 = b0 || (checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg) in
    existsb_handshake_messages_or_lem checker b1 is_psk ir1 ssmi1 rsmi1 msg1 messages1
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"

(*** Crawlers *)
(**** Compute over whole pattern *)
#push-options "--fuel 2 --ifuel 2"
let rec crawl_handshake_messages_step_lem (a : Type)
                                          (crawler : handshake_messages_crawler a)
                                          (acc0 : a)
                                          (is_psk ir : bool)
                                          (ssmi rsmi : meta_info)
                                          (messages : list (list message_token))
                                          (i : nat{i < List.length messages}) =
  match messages with
  | [] -> ()
  | msg1 :: messages' ->
    if i = 0 then () else
    let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg1 ssmi rsmi in
    let acc1 = crawler is_psk ir ssmi rsmi ssmi1 rsmi1 msg1 acc0 in
    let ir' = not ir in
    crawl_handshake_messages_step_lem a crawler acc1 is_psk ir' ssmi1 rsmi1 messages' (i-1)
#pop-options

let handshake_messages_pre_smi_step_lem (is_psk ir : bool)
                                        (ssmi rsmi : meta_info)
                                        (messages : list (list message_token))
                                        (i : nat{i < List.length messages}) =
  let a = meta_info & meta_info in
  let crawler : handshake_messages_crawler a =
    (fun is_psk ir ssmi0 rsmi0 ssmi1 rsmi1 msg acc ->
      ((ssmi1 <: meta_info), (rsmi1 <: meta_info))) in
  let acc0 : a = ssmi, rsmi in
  crawl_handshake_messages_step_lem a crawler acc0 is_psk ir ssmi rsmi messages i

let handshake_pattern_smi_step_lem (hsk : handshake_pattern) (set_psk : bool)
                                   (i : nat{i < List.length hsk.messages}) =
  let ismi, rsmi, is_psk = compute_premessages_post_smi hsk set_psk in
  handshake_messages_pre_smi_step_lem is_psk true ismi rsmi hsk.messages i

#push-options "--fuel 1"
let rec crawl_handshake_messages_pred_lem (a : Type)
                                          (crawler : handshake_messages_crawler a)
                                          (p : a -> prop)
                                          (acc : a)
                                          (is_psk ir : bool)
                                          (send_smi recv_smi : meta_info)
                                          (messages : list (list message_token)) =
  match messages with
  | [] -> ()
  | msg :: messages' ->
    let send_smi1, recv_smi1 = crawl_messages_update_smi is_psk msg send_smi recv_smi in
    let acc1 = crawler is_psk ir send_smi recv_smi send_smi1 recv_smi1 msg acc in
    crawl_handshake_messages_pred_lem a crawler p acc1 is_psk (not ir)
                                      send_smi1 recv_smi1 messages'
#pop-options

#push-options "--fuel 3 --ifuel 3"
let rec forallb_handshake_messages_and_lem (checker : handshake_messages_crawl_checker)
                                           (b0 : bool)
                                           (is_psk ir : bool)
                                           (ssmi rsmi : meta_info)
                                           (msg : list message_token)
                                           (messages : list (list message_token)) =
  match messages with
  | [] -> ()
  | [msg1] -> ()
  | msg1 :: messages1 ->
    let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg ssmi rsmi in
    let ir1 = not ir in
    let b1 = b0 && (checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg) in
    forallb_handshake_messages_and_lem checker b1 is_psk ir1 ssmi1 rsmi1 msg1 messages1
#pop-options
/
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.fst

    checker: Spec.Noise.MetaInfo.handshake_messages_crawl_checker ->
    b0: Prims.bool ->
    is_psk: Prims.bool ->
    ir: Prims.bool ->
    ssmi: Spec.Noise.MetaInfo.meta_info ->
    rsmi: Spec.Noise.MetaInfo.meta_info ->
    msg: Prims.list Spec.Noise.Base.Definitions.message_token ->
    messages: Prims.list (Prims.list Spec.Noise.Base.Definitions.message_token)
  -> FStar.Pervasives.Lemma
      (ensures
        Spec.Noise.MetaInfo.crawl_handshake_messages Prims.bool
          (Spec.Noise.MetaInfo.or_crawler checker)
          b0
          is_psk
          ir
          ssmi
          rsmi
          (msg :: messages) =
        (let _ = Spec.Noise.MetaInfo.crawl_messages_update_smi is_psk msg ssmi rsmi in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ ssmi1 rsmi1 = _ in
            let ir1 = Prims.op_Negation ir in
            let b1 = b0 || checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg in
            let b2 =
              Spec.Noise.MetaInfo.existsb_handshake_messages checker is_psk ir1 ssmi1 rsmi1 messages
            in
            b1 || b2)
          <:
          Prims.bool)) (decreases messages)
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.existsb_handshake_messages_or_lem Prims.op_BarBar Prims.op_Negation Prims.unit FStar.Pervasives.Native.tuple2 Prims.l_and Prims.b2t Spec.Noise.MetaInfo.less_than FStar.Pervasives.Native.snd FStar.Pervasives.Native.fst Spec.Noise.MetaInfo.crawl_messages_update_smi
let rec existsb_handshake_messages_or_lem
      (checker: handshake_messages_crawl_checker)
      (b0 is_psk ir: bool)
      (ssmi rsmi: meta_info)
      (msg: list message_token)
      (messages: list (list message_token))
     =
  
match messages with
| [] -> ()
| [msg1] -> ()
| msg1 :: messages1 ->
  let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg ssmi rsmi in
  let ir1 = not ir in
  let b1 = b0 || (checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg) in
  existsb_handshake_messages_or_lem checker b1 is_psk ir1 ssmi1 rsmi1 msg1 messages1