val compute_hsk_msg_flags_aux_psk_exists_lem
  (ir : bool) (f : handshake_pattern_flags)
  (msgs : list(list message_token)) :
  Lemma
  (ensures (compute_hsk_msgs_flags_aux ir f msgs).hsk_psk <==>
      (f.hsk_psk \/ List.existsb (List.Tot.mem PSK) msgs))
  (decreases msgs)
val compute_hsk_msg_flags_aux_psk_exists_lem
  (ir : bool) (f : handshake_pattern_flags)
  (msgs : list(list message_token)) :
  Lemma
  (ensures (compute_hsk_msgs_flags_aux ir f msgs).hsk_psk <==>
      (f.hsk_psk \/ List.existsb (List.Tot.mem PSK) msgs))
  (decreases msgs)
let rec compute_hsk_msg_flags_aux_psk_exists_lem
  (ir : bool) (f : handshake_pattern_flags)
  (msgs : list(list message_token)) =
  match msgs with
  | [] -> ()
  | msg :: msgs1 ->
    let f' = compute_hsk_msg_flags ir f msg in
    compute_hsk_msg_flags_psk_exists_lem ir f msg;
    compute_hsk_msg_flags_aux_psk_exists_lem (not ir) f' msgs1
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 *)
#push-options "--fuel 1 --ifuel 1"
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
#pop-options
/
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 ->
    msgs: Prims.list (Prims.list Spec.Noise.Base.Definitions.message_token)
  -> FStar.Pervasives.Lemma
      (ensures
        Mkhandshake_pattern_flags?.hsk_psk (Spec.Noise.HandshakeFlags.compute_hsk_msgs_flags_aux ir
              f
              msgs) <==>
        Mkhandshake_pattern_flags?.hsk_psk f \/
        FStar.List.Tot.Base.existsb (FStar.List.Tot.Base.mem Spec.Noise.Base.Definitions.PSK) msgs)
      (decreases msgs)
Prims.bool Spec.Noise.HandshakeFlags.handshake_pattern_flags Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.HandshakeFlags.compute_hsk_msg_flags_aux_psk_exists_lem Prims.op_Negation Prims.unit Spec.Noise.HandshakeFlags.compute_hsk_msg_flags_psk_exists_lem Prims.b2t Spec.Noise.HandshakeFlags.hsk_flags_same_pre_flags Spec.Noise.HandshakeFlags.compute_hsk_msg_flags
let rec compute_hsk_msg_flags_aux_psk_exists_lem
      (ir: bool)
      (f: handshake_pattern_flags)
      (msgs: list (list message_token))
     =
  
match msgs with
| [] -> ()
| msg :: msgs1 ->
  let f' = compute_hsk_msg_flags ir f msg in
  compute_hsk_msg_flags_psk_exists_lem ir f msg;
  compute_hsk_msg_flags_aux_psk_exists_lem (not ir) f' msgs1