val handshake_pattern_smi_step_lem (hsk : handshake_pattern) (set_psk : bool)
                                   (i : nat{i < List.length hsk.messages}) :
  Lemma(
    let is_psk = (compute_hsk_flags hsk).hsk_psk in
    let ssmi1, rsmi1 = handshake_pattern_smi hsk set_psk i in
    let ssmi2, rsmi2 = handshake_pattern_smi hsk set_psk (i+1) in
    let msg = List.Tot.index hsk.messages i in
    (ssmi2, rsmi2) == crawl_messages_update_smi is_psk msg ssmi1 rsmi1)
val handshake_pattern_smi_step_lem (hsk : handshake_pattern) (set_psk : bool)
                                   (i : nat{i < List.length hsk.messages}) :
  Lemma(
    let is_psk = (compute_hsk_flags hsk).hsk_psk in
    let ssmi1, rsmi1 = handshake_pattern_smi hsk set_psk i in
    let ssmi2, rsmi2 = handshake_pattern_smi hsk set_psk (i+1) in
    let msg = List.Tot.index hsk.messages i in
    (ssmi2, rsmi2) == crawl_messages_update_smi is_psk msg ssmi1 rsmi1)
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
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
/
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

    hsk: Spec.Noise.Base.Definitions.handshake_pattern ->
    set_psk: Prims.bool ->
    i: Prims.nat{i < FStar.List.Tot.Base.length (Mkhandshake_pattern?.messages hsk)}
  -> FStar.Pervasives.Lemma
    (ensures
      (let is_psk =
          Mkhandshake_pattern_flags?.hsk_psk (Spec.Noise.HandshakeFlags.compute_hsk_flags hsk)
        in
        let _ = Spec.Noise.MetaInfo.handshake_pattern_smi hsk set_psk i in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ ssmi1 rsmi1 = _ in
          let _ = Spec.Noise.MetaInfo.handshake_pattern_smi hsk set_psk (i + 1) in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ ssmi2 rsmi2 = _ in
            let msg = FStar.List.Tot.Base.index (Mkhandshake_pattern?.messages hsk) i in
            (ssmi2, rsmi2) == Spec.Noise.MetaInfo.crawl_messages_update_smi is_psk msg ssmi1 rsmi1)
          <:
          Type0)
        <:
        Type0))
Spec.Noise.Base.Definitions.handshake_pattern Prims.bool Prims.nat Prims.b2t Prims.op_LessThan FStar.List.Tot.Base.length Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.Base.Definitions.__proj__Mkhandshake_pattern__item__messages Spec.Noise.MetaInfo.meta_info Spec.Noise.MetaInfo.handshake_messages_pre_smi_step_lem Prims.unit FStar.Pervasives.Native.tuple3 Spec.Noise.MetaInfo.compute_premessages_post_smi
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