val compute_hsk_msg_flags_psk_exists_lem
  (ir : bool) (f : handshake_pattern_flags)
  (msg : list message_token) :
  Lemma
  (ensures (
    compute_hsk_msg_flags ir f msg).hsk_psk <==>
      (f.hsk_psk \/ List.Tot.mem PSK msg))
  (decreases msg)
val compute_hsk_msg_flags_psk_exists_lem
  (ir : bool) (f : handshake_pattern_flags)
  (msg : list message_token) :
  Lemma
  (ensures (
    compute_hsk_msg_flags ir f msg).hsk_psk <==>
      (f.hsk_psk \/ List.Tot.mem PSK msg))
  (decreases msg)
let rec compute_hsk_msg_flags_psk_exists_lem
  (ir : bool) (f : handshake_pattern_flags)
  (msg : list message_token) =
  match msg with
  | [] -> ()
  | tk :: msg1 ->
    let f' = compute_hsk_token_flags ir f tk in
    (* TODO: doesn't work without this assert_norm and whatever the amount of
     * fuel. This is very weird... *)
    assert_norm(f'.hsk_psk <==> (f.hsk_psk \/ tk == PSK));
    compute_hsk_msg_flags_psk_exists_lem ir f' msg1
module Spec.Noise.HandshakeFlags
open FStar.Mul

open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base

friend Spec.Noise.Base.Definitions

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

(*** Handshake pattern flags *)
(**** Consistency lemmas *)
/
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
Spec.Noise.HandshakeFlags.fst

    ir: Prims.bool ->
    f: Spec.Noise.HandshakeFlags.handshake_pattern_flags ->
    msg: Prims.list Spec.Noise.Base.Definitions.message_token
  -> FStar.Pervasives.Lemma
      (ensures
        Mkhandshake_pattern_flags?.hsk_psk (Spec.Noise.HandshakeFlags.compute_hsk_msg_flags ir f msg
          ) <==>
        Mkhandshake_pattern_flags?.hsk_psk f \/
        FStar.List.Tot.Base.mem Spec.Noise.Base.Definitions.PSK msg) (decreases msg)
Prims.bool Spec.Noise.HandshakeFlags.handshake_pattern_flags Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.HandshakeFlags.compute_hsk_msg_flags_psk_exists_lem Prims.unit FStar.Pervasives.assert_norm Prims.l_iff Prims.b2t Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_psk Prims.l_or Prims.eq2 Spec.Noise.Base.Definitions.PSK Spec.Noise.HandshakeFlags.hsk_flags_same_pre_flags Spec.Noise.HandshakeFlags.compute_hsk_token_flags
let rec compute_hsk_msg_flags_psk_exists_lem
      (ir: bool)
      (f: handshake_pattern_flags)
      (msg: list message_token)
     =
  
match msg with
| [] -> ()
| tk :: msg1 ->
  let f' = compute_hsk_token_flags ir f tk in
  assert_norm (f'.hsk_psk <==> (f.hsk_psk \/ tk == PSK));
  compute_hsk_msg_flags_psk_exists_lem ir f' msg1