val handshake_pattern_cleared_flags : Spec.Noise.HandshakeFlags.handshake_pattern_flags
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;
}
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;
}
/
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
Spec.Noise.HandshakeFlags.handshake_pattern_flags
Spec.Noise.HandshakeFlags.Mkhandshake_pattern_flags
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
}