val 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}) :
  Lemma
  (ensures (
    let ssmi1, rsmi1 = handshake_messages_pre_smi is_psk ir ssmi rsmi
                                                  messages i in
    let msg = List.Tot.index messages i in
    let messages1 = fst (List.Tot.splitAt i messages) in
    let messages2 = fst (List.Tot.splitAt (i+1) messages) in
    let ssmi2, rsmi2 = crawl_messages_update_smi is_psk msg ssmi1 rsmi1 in
    let crawl_fun = crawl_handshake_messages a crawler acc0 is_psk ir ssmi rsmi in
    let acc1 = crawl_fun messages1 in
    let acc2 = crawl_fun messages2 in
    let ir' = if is_even i then ir else not ir in
    acc2 == crawler is_psk ir' ssmi1 rsmi1 ssmi2 rsmi2 msg acc1))
  (decreases messages)
val 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}) :
  Lemma
  (ensures (
    let ssmi1, rsmi1 = handshake_messages_pre_smi is_psk ir ssmi rsmi
                                                  messages i in
    let msg = List.Tot.index messages i in
    let messages1 = fst (List.Tot.splitAt i messages) in
    let messages2 = fst (List.Tot.splitAt (i+1) messages) in
    let ssmi2, rsmi2 = crawl_messages_update_smi is_psk msg ssmi1 rsmi1 in
    let crawl_fun = crawl_handshake_messages a crawler acc0 is_psk ir ssmi rsmi in
    let acc1 = crawl_fun messages1 in
    let acc2 = crawl_fun messages2 in
    let ir' = if is_even i then ir else not ir in
    acc2 == crawler is_psk ir' ssmi1 rsmi1 ssmi2 rsmi2 msg acc1))
  (decreases messages)
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)
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 *)
/
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

    a: Type ->
    crawler: Spec.Noise.MetaInfo.handshake_messages_crawler a ->
    acc0: a ->
    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 msg = FStar.List.Tot.Base.index messages i in
            let messages1 = FStar.Pervasives.Native.fst (FStar.List.Tot.Base.splitAt i messages) in
            let messages2 =
              FStar.Pervasives.Native.fst (FStar.List.Tot.Base.splitAt (i + 1) messages)
            in
            let _ = Spec.Noise.MetaInfo.crawl_messages_update_smi is_psk msg ssmi1 rsmi1 in
            (let FStar.Pervasives.Native.Mktuple2 #_ #_ ssmi2 rsmi2 = _ in
              let crawl_fun =
                Spec.Noise.MetaInfo.crawl_handshake_messages a crawler acc0 is_psk ir ssmi rsmi
              in
              let acc1 = crawl_fun messages1 in
              let acc2 = crawl_fun messages2 in
              let ir' =
                (match Spec.Noise.Base.Definitions.is_even i with
                  | true -> ir
                  | _ -> Prims.op_Negation ir)
                <:
                Prims.bool
              in
              acc2 == crawler is_psk ir' ssmi1 rsmi1 ssmi2 rsmi2 msg acc1)
            <:
            Type0)
          <:
          Type0)) (decreases messages)
Spec.Noise.MetaInfo.handshake_messages_crawler 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 Prims.op_Equality Prims.int Spec.Noise.MetaInfo.crawl_handshake_messages_step_lem Prims.op_Subtraction Prims.op_Negation Prims.unit FStar.Pervasives.Native.tuple2 Prims.l_and Spec.Noise.MetaInfo.less_than FStar.Pervasives.Native.snd FStar.Pervasives.Native.fst Spec.Noise.MetaInfo.crawl_messages_update_smi
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)