val check_hsk_wf_csend_creceive_message_smi_precond_psk_no_diff_lem :
     hsk : wf_handshake_pattern
  -> has_psk : bool
  -> i : nat{i < List.length hsk.messages} ->
  Lemma
  (requires (List.mem PSK (List.Tot.index hsk.messages i) ==> has_psk))
  (ensures (
    csend_message_smi_precond hsk has_psk i /\
    creceive_message_smi_precond hsk has_psk i))
val check_hsk_wf_csend_creceive_message_smi_precond_psk_no_diff_lem :
     hsk : wf_handshake_pattern
  -> has_psk : bool
  -> i : nat{i < List.length hsk.messages} ->
  Lemma
  (requires (List.mem PSK (List.Tot.index hsk.messages i) ==> has_psk))
  (ensures (
    csend_message_smi_precond hsk has_psk i /\
    creceive_message_smi_precond hsk has_psk i))
let check_hsk_wf_csend_creceive_message_smi_precond_psk_no_diff_lem hsk has_psk i =
  check_handshake_pattern_well_formed_forall_psk_true_lem hsk i;
  let msg = List.Tot.index hsk.messages i in
  let is_psk = chskf_check_is_psk hsk in
  let ir = is_even i in
  (* send *)
  let ssmi0 = csend_message_pre_smi hsk true i in
  let ssmi1 = csend_message_pre_smi hsk false i in
  assert(csend_message_smi_precond hsk true i);
  (* receive *)
  let rsmi0 = creceive_message_pre_smi hsk true i in
  let rsmi1 = creceive_message_pre_smi hsk false i in
  assert(creceive_message_smi_precond hsk true i);
  (* frame lemma *)
  csend_creceive_message_pre_smi_psk_frame_lem hsk i;
  assert(ssmi0 == smi_set_psk true ssmi1);
  assert(rsmi0 == smi_set_psk true rsmi1);
  (* Prove that csend/creceive_message_pre_smi are true for has_psk = false  *)
  if not (has_psk) then
    begin
    check_send_message_smi_psk_no_diff_lem ssmi0 ir is_psk msg;
    check_receive_message_smi_psk_no_diff_lem rsmi0 (not ir) is_psk msg
    end
  else ()
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

#push-options "--fuel 1"
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
#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 ->
    has_psk: Prims.bool ->
    i: Prims.nat{i < FStar.List.Tot.Base.length (Mkhandshake_pattern?.messages hsk)}
  -> FStar.Pervasives.Lemma
      (requires
        FStar.List.Tot.Base.mem Spec.Noise.Base.Definitions.PSK
          (FStar.List.Tot.Base.index (Mkhandshake_pattern?.messages hsk) i) ==>
        has_psk)
      (ensures
        Spec.Noise.WellFormedness.csend_message_smi_precond hsk has_psk i /\
        Spec.Noise.WellFormedness.creceive_message_smi_precond hsk has_psk i)
Spec.Noise.WellFormedness.wf_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 Prims.op_Negation Spec.Noise.WellFormedness.check_receive_message_smi_psk_no_diff_lem Prims.unit Spec.Noise.WellFormedness.check_send_message_smi_psk_no_diff_lem Prims._assert Prims.eq2 Spec.Noise.MetaInfo.meta_info Spec.Noise.MetaInfo.smi_set_psk Spec.Noise.MetaInfo.csend_creceive_message_pre_smi_psk_frame_lem Spec.Noise.WellFormedness.creceive_message_smi_precond Spec.Noise.MetaInfo.creceive_message_pre_smi Spec.Noise.WellFormedness.csend_message_smi_precond Spec.Noise.MetaInfo.csend_message_pre_smi Spec.Noise.Base.Definitions.is_even Prims.op_Equality Spec.Noise.Base.Definitions.check_hsk_is_psk Spec.Noise.HandshakeFlags.chskf_check_is_psk FStar.List.Tot.Base.index Spec.Noise.WellFormedness.check_handshake_pattern_well_formed_forall_psk_true_lem
let check_hsk_wf_csend_creceive_message_smi_precond_psk_no_diff_lem hsk has_psk i =
  
check_handshake_pattern_well_formed_forall_psk_true_lem hsk i;
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 ssmi0 = csend_message_pre_smi hsk true i in
let ssmi1 = csend_message_pre_smi hsk false i in
assert (csend_message_smi_precond hsk true i);
let rsmi0 = creceive_message_pre_smi hsk true i in
let rsmi1 = creceive_message_pre_smi hsk false i in
assert (creceive_message_smi_precond hsk true i);
csend_creceive_message_pre_smi_psk_frame_lem hsk i;
assert (ssmi0 == smi_set_psk true ssmi1);
assert (rsmi0 == smi_set_psk true rsmi1);
if not (has_psk)
then
  (check_send_message_smi_psk_no_diff_lem ssmi0 ir is_psk msg;
    check_receive_message_smi_psk_no_diff_lem rsmi0 (not ir) is_psk msg)