val check_send_message_smi_psk_no_diff_lem :
     smi : meta_info
  -> initiator : bool
  -> is_psk : bool
  -> message : list message_token ->
  Lemma
  (requires (not (List.mem PSK message)))
  (ensures (
    check_send_message_smi (smi_set_psk true smi) initiator is_psk message =
    check_send_message_smi (smi_set_psk false smi) initiator is_psk message))
  (decreases message)
val check_send_message_smi_psk_no_diff_lem :
     smi : meta_info
  -> initiator : bool
  -> is_psk : bool
  -> message : list message_token ->
  Lemma
  (requires (not (List.mem PSK message)))
  (ensures (
    check_send_message_smi (smi_set_psk true smi) initiator is_psk message =
    check_send_message_smi (smi_set_psk false smi) initiator is_psk message))
  (decreases message)
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'
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 *)
/
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

    smi: Spec.Noise.MetaInfo.meta_info ->
    initiator: Prims.bool ->
    is_psk: Prims.bool ->
    message: Prims.list Spec.Noise.Base.Definitions.message_token
  -> FStar.Pervasives.Lemma
      (requires Prims.op_Negation (FStar.List.Tot.Base.mem Spec.Noise.Base.Definitions.PSK message))
      (ensures
        Spec.Noise.WellFormedness.check_send_message_smi (Spec.Noise.MetaInfo.smi_set_psk true smi)
          initiator
          is_psk
          message =
        Spec.Noise.WellFormedness.check_send_message_smi (Spec.Noise.MetaInfo.smi_set_psk false smi)
          initiator
          is_psk
          message)
      (decreases message)
Spec.Noise.MetaInfo.meta_info Prims.bool Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.WellFormedness.check_send_message_smi_psk_no_diff_lem Spec.Noise.MetaInfo.greater_smi Spec.Noise.MetaInfo.send_token_update_smi Prims.unit
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'