val 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}) :
  Lemma(
    let ssmi1, rsmi1 = handshake_messages_pre_smi is_psk ir ssmi rsmi messages i in
    let ssmi2, rsmi2 = handshake_messages_pre_smi is_psk ir ssmi rsmi messages (i+1) in
    let msg = List.Tot.index messages i in
    (ssmi2, rsmi2) == crawl_messages_update_smi is_psk msg ssmi1 rsmi1)
val 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}) :
  Lemma(
    let ssmi1, rsmi1 = handshake_messages_pre_smi is_psk ir ssmi rsmi messages i in
    let ssmi2, rsmi2 = handshake_messages_pre_smi is_psk ir ssmi rsmi messages (i+1) in
    let msg = List.Tot.index messages i in
    (ssmi2, rsmi2) == crawl_messages_update_smi is_psk msg ssmi1 rsmi1)
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
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
/
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

    is_psk: Prims.bool ->
    ir: Prims.bool ->
    ssmi: Spec.Noise.MetaInfo.meta_info ->
    rsmi: Spec.Noise.MetaInfo.meta_info ->
    messages: Prims.list (Prims.list Spec.Noise.Base.Definitions.message_token) ->
    i: Prims.nat{i < FStar.List.Tot.Base.length messages}
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = Spec.Noise.MetaInfo.handshake_messages_pre_smi is_psk ir ssmi rsmi messages i in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ ssmi1 rsmi1 = _ in
          let _ =
            Spec.Noise.MetaInfo.handshake_messages_pre_smi is_psk ir ssmi rsmi messages (i + 1)
          in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ ssmi2 rsmi2 = _ in
            let msg = FStar.List.Tot.Base.index messages i in
            (ssmi2, rsmi2) == Spec.Noise.MetaInfo.crawl_messages_update_smi is_psk msg ssmi1 rsmi1)
          <:
          Type0)
        <:
        Type0))
Prims.bool Spec.Noise.MetaInfo.meta_info Prims.list Spec.Noise.Base.Definitions.message_token Prims.nat Prims.b2t Prims.op_LessThan FStar.List.Tot.Base.length Spec.Noise.MetaInfo.crawl_handshake_messages_step_lem FStar.Pervasives.Native.Mktuple2 Spec.Noise.MetaInfo.handshake_messages_crawler Spec.Noise.MetaInfo.greater_smi FStar.Pervasives.Native.tuple2 Prims.unit
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