val check_handshake_pattern_well_formed_forall_psk_true_lem :
     hsk : wf_handshake_pattern
  -> i : nat{ i < List.length hsk.messages} ->
  Lemma(
    let msg = List.Tot.index hsk.messages i in
    let is_psk = chskf_check_is_psk hsk in
    let ir = is_even i in
    let has_psk = true in (**)
    let ssmi0 = csend_message_pre_smi hsk has_psk i in
    let rsmi0 = creceive_message_pre_smi hsk has_psk i in
    check_send_message_smi ssmi0 ir is_psk msg /\
    check_receive_message_smi rsmi0 (not ir) is_psk msg)
val check_handshake_pattern_well_formed_forall_psk_true_lem :
     hsk : wf_handshake_pattern
  -> i : nat{ i < List.length hsk.messages} ->
  Lemma(
    let msg = List.Tot.index hsk.messages i in
    let is_psk = chskf_check_is_psk hsk in
    let ir = is_even i in
    let has_psk = true in (**)
    let ssmi0 = csend_message_pre_smi hsk has_psk i in
    let rsmi0 = creceive_message_pre_smi hsk has_psk i in
    check_send_message_smi ssmi0 ir is_psk msg /\
    check_receive_message_smi rsmi0 (not ir) is_psk msg)
let check_handshake_pattern_well_formed_forall_psk_true_lem hsk i =
  let has_psk = true in
  forallb_handshake_pattern_messages_lem hsk has_psk
                                         check_message_executable
module Spec.Noise.WellFormedness
open FStar.Mul

open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base
open Spec.Noise.HandshakeFlags
open Spec.Noise.Lengths
open Spec.Noise.NonceCounter
open Spec.Noise.MetaInfo

friend Spec.Noise.Base.Definitions

#set-options "--z3rlimit 25 --fuel 0 --ifuel 1"

(*** Properties *)

#push-options "--fuel 1"
let rec check_send_message_smi_psk_no_diff_lem smi initiator is_psk message =
  match message with
  | [] -> ()
  | tk :: message' ->
    let smi' = send_token_update_smi is_psk tk smi in
    check_send_message_smi_psk_no_diff_lem smi' initiator is_psk message'
#pop-options

#push-options "--fuel 1"
let rec check_receive_message_smi_psk_no_diff_lem smi initiator is_psk message =
  match message with
  | [] -> ()
  | tk :: message' ->
    let smi' = receive_token_update_smi is_psk tk smi in
    check_receive_message_smi_psk_no_diff_lem smi' initiator is_psk message'
#pop-options
/
Spec.Noise.NonceCounter.fsti.checked Spec.Noise.MetaInfo.fsti.checked Spec.Noise.Lengths.fsti.checked Spec.Noise.HandshakeFlags.fsti.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.Definitions.fst.checked Spec.Noise.Base.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.WellFormedness.fst

    hsk: Spec.Noise.WellFormedness.wf_handshake_pattern ->
    i: Prims.nat{i < FStar.List.Tot.Base.length (Mkhandshake_pattern?.messages hsk)}
  -> FStar.Pervasives.Lemma
    (ensures
      (let msg = FStar.List.Tot.Base.index (Mkhandshake_pattern?.messages hsk) i in
        let is_psk = Spec.Noise.HandshakeFlags.chskf_check_is_psk hsk in
        let ir = Spec.Noise.Base.Definitions.is_even i in
        let has_psk = true in
        let ssmi0 = Spec.Noise.MetaInfo.csend_message_pre_smi hsk has_psk i in
        let rsmi0 = Spec.Noise.MetaInfo.creceive_message_pre_smi hsk has_psk i in
        Spec.Noise.WellFormedness.check_send_message_smi ssmi0 ir is_psk msg /\
        Spec.Noise.WellFormedness.check_receive_message_smi rsmi0 (Prims.op_Negation ir) is_psk msg)
    )
Spec.Noise.WellFormedness.wf_handshake_pattern 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.forallb_handshake_pattern_messages_lem Spec.Noise.WellFormedness.check_message_executable Prims.bool Prims.unit
let check_handshake_pattern_well_formed_forall_psk_true_lem hsk i =
  
let has_psk = true in
forallb_handshake_pattern_messages_lem hsk has_psk check_message_executable