val compute_hsk_token_flags (ir: bool) (f: handshake_pattern_flags) (tk: message_token)
    : (f': handshake_pattern_flags{hsk_flags_same_pre_flags f f'})
val compute_hsk_token_flags (ir: bool) (f: handshake_pattern_flags) (tk: message_token)
    : (f': handshake_pattern_flags{hsk_flags_same_pre_flags f f'})
let compute_hsk_token_flags
  (ir : bool)
  (f : handshake_pattern_flags)
  (tk : message_token) :
  (f':handshake_pattern_flags{hsk_flags_same_pre_flags f f'}) =
  begin match tk with
  | S -> if ir then { f with hsk_is = true } else { f with hsk_rs = true }
  | E -> if ir then { f with hsk_ie = true } else { f with hsk_re = true }
  | SS -> { f with hsk_ss = true }
  | EE -> { f with hsk_ee = true }
  | SE -> { f with hsk_se = true }
  | ES -> { f with hsk_es = true }
  | PSK -> { f with hsk_psk = true }
  end
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))


(**** Compute over premessages *)
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

let compute_hsk_pretoken_flags (ir : bool) (f : handshake_pattern_flags)
                               (tk : premessage_token) :
  Tot (f':handshake_pattern_flags{hsk_flags_same_msg_flags f f'}) =
  match tk with
  | PS -> if ir then { f with hsk_pis = true } else { f with hsk_prs = true }
  | PE -> if ir then { f with hsk_pie = true } else { f with hsk_pre = true }

(* Rk.: initially defined with fold_left. Proved cumbersome later because of
 * the type refinement (see the remark for compute_hsk_msg_flags) *)
[@(strict_on_arguments [2])]
let rec compute_hsk_premessage_flags (ir : bool) (f : handshake_pattern_flags)
                                     (pattern : list premessage_token) :
  Tot (f':handshake_pattern_flags{hsk_flags_same_msg_flags f f'})
  (decreases pattern) =
  match pattern with
  | [] -> f
  | tk :: pattern' ->
    let f' = compute_hsk_pretoken_flags ir f tk in
    compute_hsk_premessage_flags ir f' pattern'
/
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

    ir: Prims.bool ->
    f: Spec.Noise.HandshakeFlags.handshake_pattern_flags ->
    tk: Spec.Noise.Base.Definitions.message_token
  -> f':
    Spec.Noise.HandshakeFlags.handshake_pattern_flags
      {Spec.Noise.HandshakeFlags.hsk_flags_same_pre_flags f f'}
Prims.bool Spec.Noise.HandshakeFlags.handshake_pattern_flags Spec.Noise.Base.Definitions.message_token Spec.Noise.HandshakeFlags.Mkhandshake_pattern_flags Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_pis Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_pie Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_prs Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_pre 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 Spec.Noise.HandshakeFlags.__proj__Mkhandshake_pattern_flags__item__hsk_is Prims.b2t Spec.Noise.HandshakeFlags.hsk_flags_same_pre_flags
let compute_hsk_token_flags (ir: bool) (f: handshake_pattern_flags) (tk: message_token)
    : (f': handshake_pattern_flags{hsk_flags_same_pre_flags f f'}) =
  
match tk with
| S -> if ir then { f with hsk_is = true } else { f with hsk_rs = true }
| E -> if ir then { f with hsk_ie = true } else { f with hsk_re = true }
| SS -> { f with hsk_ss = true }
| EE -> { f with hsk_ee = true }
| SE -> { f with hsk_se = true }
| ES -> { f with hsk_es = true }
| PSK -> { f with hsk_psk = true }