val hsk_flags_same_msg_flags (f1 f2: handshake_pattern_flags) : bool
val hsk_flags_same_msg_flags (f1 f2: handshake_pattern_flags) : bool
let hsk_flags_same_msg_flags (f1 f2 : handshake_pattern_flags) : bool =
  f2.hsk_is = f1.hsk_is && f2.hsk_ie = f1.hsk_ie &&
  f2.hsk_rs = f1.hsk_rs && f2.hsk_re = f1.hsk_re &&
  f2.hsk_ss = f1.hsk_ss && f2.hsk_ee = f1.hsk_ee &&
  f2.hsk_se = f1.hsk_se && f2.hsk_es = f1.hsk_es &&
  f2.hsk_psk = f1.hsk_psk
module Spec.Noise.HandshakeFlags
open FStar.Mul

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

/// The following file implements functions, predicates and lemmas to reason about
/// the availability of the different keys in the handshake (and cipher) state at
/// every step of the handshake. On top of that it also builds pattern
/// well-formedness analysis.

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

let opt_list_to_list_or_empty (#a : Type) (ols : option (list a)) : list a =
  match ols with
  | Some ls -> ls
  | None -> []

(*** Handshake pattern flags *)
(**** Definition, initialization *)
// TODO: remove handshake_pattern_flags and replace its use by handshake_state_flags
inline_for_extraction //noextract
type handshake_pattern_flags = {
  hsk_pis : bool;
  hsk_pie : bool;
  hsk_prs : bool;
  hsk_pre : bool;
  hsk_is : bool;
  hsk_ie : bool;
  hsk_rs : bool;
  hsk_re : bool;
  hsk_ss : bool;
  hsk_ee : bool;
  hsk_se : bool;
  hsk_es : bool;
  hsk_psk : bool;
}

inline_for_extraction noextract
let handshake_pattern_cleared_flags = {
  hsk_pis = false; hsk_pie = false; hsk_prs = false; hsk_pre = false;
  hsk_is = false; hsk_ie = false; hsk_rs = false; hsk_re = false;
  hsk_ss = false; hsk_ee = false; hsk_se = false; hsk_es = false; hsk_psk = false;
}

let hsk_flags_same_pre_flags (f1 f2 : handshake_pattern_flags) : bool =
  f2.hsk_pis = f1.hsk_pis && f2.hsk_pie = f1.hsk_pie &&
  f2.hsk_prs = f1.hsk_prs && f2.hsk_pre = f1.hsk_pre

/// Hskf is monotonous
let hskf_less_than (hskf0 hskf1 : handshake_pattern_flags) : Tot bool =  
  (hskf1.hsk_pis || (not hskf0.hsk_pis)) &&
  (hskf1.hsk_pie || (not hskf0.hsk_pie)) &&
  (hskf1.hsk_prs || (not hskf0.hsk_prs)) &&
  (hskf1.hsk_pre || (not hskf0.hsk_pre)) &&
  (hskf1.hsk_is || (not hskf0.hsk_is)) &&
  (hskf1.hsk_ie || (not hskf0.hsk_ie)) &&
  (hskf1.hsk_rs || (not hskf0.hsk_rs)) &&
  (hskf1.hsk_re || (not hskf0.hsk_re)) &&
  (hskf1.hsk_ss || (not hskf0.hsk_ss)) &&
  (hskf1.hsk_ee || (not hskf0.hsk_ee)) &&
  (hskf1.hsk_se || (not hskf0.hsk_se)) &&
  (hskf1.hsk_es || (not hskf0.hsk_es)) &&
  (hskf1.hsk_psk || (not hskf0.hsk_psk))
/
Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
Spec.Noise.HandshakeFlags.fsti

    f1: Spec.Noise.HandshakeFlags.handshake_pattern_flags ->
    f2: Spec.Noise.HandshakeFlags.handshake_pattern_flags
  -> Prims.bool
Spec.Noise.HandshakeFlags.handshake_pattern_flags Prims.op_AmpAmp Prims.op_Equality Prims.bool Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_is Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_ie Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_rs Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_re Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_ss Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_ee Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_se Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_es Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_psk
let hsk_flags_same_msg_flags (f1 f2: handshake_pattern_flags) : bool =
  
f2.hsk_is = f1.hsk_is && f2.hsk_ie = f1.hsk_ie && f2.hsk_rs = f1.hsk_rs && f2.hsk_re = f1.hsk_re &&
f2.hsk_ss = f1.hsk_ss &&
f2.hsk_ee = f1.hsk_ee &&
f2.hsk_se = f1.hsk_se &&
f2.hsk_es = f1.hsk_es &&
f2.hsk_psk = f1.hsk_psk