val compute_hsk_flags_consistent_with_check_hsk_is_psk_lem
  (hsk : handshake_pattern) :
  Lemma((compute_hsk_flags hsk).hsk_psk == Spec.Noise.Base.check_hsk_is_psk hsk)
val compute_hsk_flags_consistent_with_check_hsk_is_psk_lem
  (hsk : handshake_pattern) :
  Lemma((compute_hsk_flags hsk).hsk_psk == Spec.Noise.Base.check_hsk_is_psk hsk)
let compute_hsk_flags_consistent_with_check_hsk_is_psk_lem
  (hsk : handshake_pattern) =
  let hskf = compute_hsk_pre_msgs_flags hsk in
  assert(hskf.hsk_psk == false);
  compute_hsk_msg_flags_aux_psk_exists_lem true hskf hsk.messages
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

#push-options "--fuel 1 --ifuel 1"
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
#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
hsk: Spec.Noise.Base.Definitions.handshake_pattern
  -> FStar.Pervasives.Lemma
    (ensures
      Mkhandshake_pattern_flags?.hsk_psk (Spec.Noise.HandshakeFlags.compute_hsk_flags hsk) ==
      Spec.Noise.Base.Definitions.check_hsk_is_psk hsk)
Spec.Noise.Base.Definitions.handshake_pattern Spec.Noise.HandshakeFlags.compute_hsk_msg_flags_aux_psk_exists_lem Spec.Noise.Base.Definitions.__proj__Mkhandshake_pattern__item__messages Prims.unit Prims._assert Prims.eq2 Prims.bool Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_psk Spec.Noise.HandshakeFlags.handshake_pattern_flags Prims.b2t Spec.Noise.HandshakeFlags.hsk_flags_same_msg_flags Spec.Noise.HandshakeFlags.handshake_pattern_cleared_flags Spec.Noise.HandshakeFlags.compute_hsk_pre_msgs_flags
let compute_hsk_flags_consistent_with_check_hsk_is_psk_lem (hsk: handshake_pattern) =
  
let hskf = compute_hsk_pre_msgs_flags hsk in
assert (hskf.hsk_psk == false);
compute_hsk_msg_flags_aux_psk_exists_lem true hskf hsk.messages