val compute_hsk_msg_flags_is_increasing (ir : bool)
                                        (hskf0 : handshake_pattern_flags)
                                        (msg : list message_token) :
  Lemma
  (requires True)
  (ensures(
    let hskf1 = compute_hsk_msg_flags ir hskf0 msg in
    hskf0 `hskf_less_than` hskf1))
  (decreases msg)
val compute_hsk_msg_flags_is_increasing (ir : bool)
                                        (hskf0 : handshake_pattern_flags)
                                        (msg : list message_token) :
  Lemma
  (requires True)
  (ensures(
    let hskf1 = compute_hsk_msg_flags ir hskf0 msg in
    hskf0 `hskf_less_than` hskf1))
  (decreases msg)
let rec compute_hsk_msg_flags_is_increasing ir hskf0 msg =
  match msg with
  | [] -> ()
  | tk :: msg' ->
    let hskf1 = compute_hsk_token_flags ir hskf0 tk in
    // I don't know why we need to call this lemma
    compute_hsk_token_flags_is_increasing ir hskf0 tk;
    assert(hskf0 `hskf_less_than` hskf1);
    compute_hsk_msg_flags_is_increasing ir hskf1 msg'
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

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

(**** Monotonicity lemmas *)
let compute_hsk_token_flags_is_increasing ir hskf0 tk = ()
/
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 ->
    hskf0: Spec.Noise.HandshakeFlags.handshake_pattern_flags ->
    msg: Prims.list Spec.Noise.Base.Definitions.message_token
  -> FStar.Pervasives.Lemma
      (ensures
        (let hskf1 = Spec.Noise.HandshakeFlags.compute_hsk_msg_flags ir hskf0 msg in
          Spec.Noise.HandshakeFlags.hskf_less_than hskf0 hskf1)) (decreases msg)
Prims.bool Spec.Noise.HandshakeFlags.handshake_pattern_flags Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.HandshakeFlags.compute_hsk_msg_flags_is_increasing Prims.unit Prims._assert Prims.b2t Spec.Noise.HandshakeFlags.hskf_less_than Spec.Noise.HandshakeFlags.compute_hsk_token_flags_is_increasing Spec.Noise.HandshakeFlags.hsk_flags_same_pre_flags Spec.Noise.HandshakeFlags.compute_hsk_token_flags
let rec compute_hsk_msg_flags_is_increasing ir hskf0 msg =
  
match msg with
| [] -> ()
| tk :: msg' ->
  let hskf1 = compute_hsk_token_flags ir hskf0 tk in
  compute_hsk_token_flags_is_increasing ir hskf0 tk;
  assert (hskf0 `hskf_less_than` hskf1);
  compute_hsk_msg_flags_is_increasing ir hskf1 msg'