val receive_token_update_smi_frame_lem (is_psk : bool) (tk : message_token)
                                       (smi : meta_info) :
  Lemma(
    forall s e psk.
    let hsf1 = { smi.hsf with s = s; e = e; psk = psk } in
    let smi1 = { smi with hsf = hsf1 } in
    let smi2 = receive_token_update_smi is_psk tk smi in
    receive_token_update_smi is_psk tk smi1 ==
      { smi2 with hsf = { smi2.hsf with s = s; e = e; psk = psk }})
val receive_token_update_smi_frame_lem (is_psk : bool) (tk : message_token)
                                       (smi : meta_info) :
  Lemma(
    forall s e psk.
    let hsf1 = { smi.hsf with s = s; e = e; psk = psk } in
    let smi1 = { smi with hsf = hsf1 } in
    let smi2 = receive_token_update_smi is_psk tk smi in
    receive_token_update_smi is_psk tk smi1 ==
      { smi2 with hsf = { smi2.hsf with s = s; e = e; psk = psk }})
let receive_token_update_smi_frame_lem (is_psk : bool) (tk : message_token)
                                       (smi : meta_info) =
  receive_token_update_hsf_frame_lem is_psk tk smi.hsf
module Spec.Noise.MetaInfo
open FStar.Mul

open Spec.Noise.Base
open Spec.Noise.HandshakeFlags
open Spec.Noise.NonceCounter

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

(*** Crawlers *)
(**** Compute over whole pattern *)
#push-options "--fuel 2 --ifuel 2"
let rec crawl_handshake_messages_step_lem (a : Type)
                                          (crawler : handshake_messages_crawler a)
                                          (acc0 : a)
                                          (is_psk ir : bool)
                                          (ssmi rsmi : meta_info)
                                          (messages : list (list message_token))
                                          (i : nat{i < List.length messages}) =
  match messages with
  | [] -> ()
  | msg1 :: messages' ->
    if i = 0 then () else
    let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg1 ssmi rsmi in
    let acc1 = crawler is_psk ir ssmi rsmi ssmi1 rsmi1 msg1 acc0 in
    let ir' = not ir in
    crawl_handshake_messages_step_lem a crawler acc1 is_psk ir' ssmi1 rsmi1 messages' (i-1)
#pop-options

let handshake_messages_pre_smi_step_lem (is_psk ir : bool)
                                        (ssmi rsmi : meta_info)
                                        (messages : list (list message_token))
                                        (i : nat{i < List.length messages}) =
  let a = meta_info & meta_info in
  let crawler : handshake_messages_crawler a =
    (fun is_psk ir ssmi0 rsmi0 ssmi1 rsmi1 msg acc ->
      ((ssmi1 <: meta_info), (rsmi1 <: meta_info))) in
  let acc0 : a = ssmi, rsmi in
  crawl_handshake_messages_step_lem a crawler acc0 is_psk ir ssmi rsmi messages i

let handshake_pattern_smi_step_lem (hsk : handshake_pattern) (set_psk : bool)
                                   (i : nat{i < List.length hsk.messages}) =
  let ismi, rsmi, is_psk = compute_premessages_post_smi hsk set_psk in
  handshake_messages_pre_smi_step_lem is_psk true ismi rsmi hsk.messages i

#push-options "--fuel 1"
let rec crawl_handshake_messages_pred_lem (a : Type)
                                          (crawler : handshake_messages_crawler a)
                                          (p : a -> prop)
                                          (acc : a)
                                          (is_psk ir : bool)
                                          (send_smi recv_smi : meta_info)
                                          (messages : list (list message_token)) =
  match messages with
  | [] -> ()
  | msg :: messages' ->
    let send_smi1, recv_smi1 = crawl_messages_update_smi is_psk msg send_smi recv_smi in
    let acc1 = crawler is_psk ir send_smi recv_smi send_smi1 recv_smi1 msg acc in
    crawl_handshake_messages_pred_lem a crawler p acc1 is_psk (not ir)
                                      send_smi1 recv_smi1 messages'
#pop-options

#push-options "--fuel 3 --ifuel 3"
let rec forallb_handshake_messages_and_lem (checker : handshake_messages_crawl_checker)
                                           (b0 : bool)
                                           (is_psk ir : bool)
                                           (ssmi rsmi : meta_info)
                                           (msg : list message_token)
                                           (messages : list (list message_token)) =
  match messages with
  | [] -> ()
  | [msg1] -> ()
  | msg1 :: messages1 ->
    let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg ssmi rsmi in
    let ir1 = not ir in
    let b1 = b0 && (checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg) in
    forallb_handshake_messages_and_lem checker b1 is_psk ir1 ssmi1 rsmi1 msg1 messages1
#pop-options

#push-options "--z3rlimit 25 --fuel 3 --ifuel 3"
let rec existsb_handshake_messages_or_lem (checker : handshake_messages_crawl_checker)
                                          (b0 : bool)
                                          (is_psk ir : bool)
                                          (ssmi rsmi : meta_info)
                                          (msg : list message_token)
                                          (messages : list (list message_token)) =
  match messages with
  | [] -> ()
  | [msg1] -> ()
  | msg1 :: messages1 ->
    let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg ssmi rsmi in
    let ir1 = not ir in
    let b1 = b0 || (checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg) in
    existsb_handshake_messages_or_lem checker b1 is_psk ir1 ssmi1 rsmi1 msg1 messages1
#pop-options

val forall_shift_nat_boundaries_lem (n : nat) (p : (x:nat{x < n}) -> prop) :
  Lemma ((forall (i : nat{i < n - 1}). p (i+1)) <==> (forall (j : nat{0 < j /\ j < n}). p j))

let forall_shift_nat_boundaries_lem (n : nat) (p : (x:nat{x < n}) -> prop) =
  let pi = forall (i : nat{i < n - 1}). p (i+1) in
  let pj = forall (j : nat{0 < j /\ j < n}). p j in
  (* The prove can easily prove the first implication *)
  assert(pj ==> pi);
  (* For the other, we use some trick to help Z3 instantiate the hypotheses *)
  let pj' = forall (j : nat{0 < j /\ j < n}). p ((j-1)+1) in
  assert(pi ==> pj');
  ()

val exists_shift_nat_boundaries_lem (n : nat) (p : (x:nat{x < n}) -> prop) :
  Lemma ((exists (i : nat{i < n - 1}). p (i+1)) <==> (exists (j : nat{0 < j /\ j < n}). p j))

let exists_shift_nat_boundaries_lem (n : nat) (p : (x:nat{x < n}) -> prop) =
  let pi = exists (i : nat{i < n - 1}). p (i+1) in
  let pj = exists (j : nat{0 < j /\ j < n}). p j in
  assert(pi ==> pj);
  (* Same as above *)
  let pj' = exists (j : nat{0 < j /\ j < n}). p ((j-1)+1) in
  assert(pi ==> pj');
  assert(pj' <==> pj);
  assert(pj' ==> pi);
  ()

let exists_join_nat_boundaries_lem (n : nat{n > 0}) (p : (x:nat{x < n}) -> prop) :
  Lemma (((p 0) \/ (exists (j : nat{0 < j /\ j < n}). p j)) <==>
        ((exists (j : nat{j < n}). p j))) = ()

#push-options "--z3rlimit 100 --fuel 2 --ifuel 2"
let rec forallb_handshake_messages_lem (checker : handshake_messages_crawl_checker)
                                       (is_psk ir : bool)
                                       (ssmi rsmi : meta_info)
                                       (messages : list (list message_token)) =
  match messages with
  | [] -> ()
  | msg1 :: messages1 ->
    let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg1 ssmi rsmi in
    let ir1 = not ir in
    forallb_handshake_messages_and_lem checker true is_psk ir ssmi rsmi msg1 messages1;
    forallb_handshake_messages_lem checker is_psk ir1 ssmi1 rsmi1 messages1;
    (* We still need to do a bit of work *)
    let b0 = forallb_handshake_messages checker is_psk ir ssmi rsmi (msg1 :: messages1) in
    let b1 = true && (checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg1) in
    let b2 = forallb_handshake_messages checker is_psk ir1 ssmi1 rsmi1 messages1 in
    (* Check that we get what we were supposed to *)
    assert(b0 = (b1 && b2));
    (* Some asserts to check some equalities *)
    assert(forall (i : nat{i < List.length messages1}).
           List.Tot.index messages1 i == List.Tot.index messages (i+1));
    assert(forall (i : nat{i < List.length messages1}).
      handshake_messages_pre_smi is_psk ir ssmi1 rsmi1 messages1 i ==
      handshake_messages_pre_smi is_psk ir1 ssmi rsmi messages (i+1));
    assert(b2 <==>
      (forall (i : nat{i < List.length messages1}).
      checkerb_handshake_messages_one checker is_psk ir1 ssmi1 rsmi1 messages1 i));
    assert(
      (forall (i : nat{i < List.length messages1}).
      checkerb_handshake_messages_one checker is_psk ir1 ssmi1 rsmi1 messages1 i =
      checkerb_handshake_messages_one checker is_psk ir ssmi rsmi messages (i + 1)));
    assert(b1 <==>
      checkerb_handshake_messages_one checker is_psk ir ssmi rsmi messages 0);
    (* Here is the trick: we can prove that:
       [> b <==> forall i < (length messages)-1. P (i+1)
       But F* and Z3 don't manage to deduce from it:
       [> b <==> forall 0 < i < length messages. P i
       So we need to call a lemma *)
    let n = List.length messages in
    let p i : prop =
      checkerb_handshake_messages_one checker is_psk ir ssmi rsmi messages i == true in
    forall_shift_nat_boundaries_lem n p
#pop-options

#push-options "--z3rlimit 100 --fuel 2 --ifuel 2"
let rec existsb_handshake_messages_lem (checker : handshake_messages_crawl_checker)
                                       (is_psk ir : bool)
                                       (ssmi rsmi : meta_info)
                                       (messages : list (list message_token)) =
  match messages with
  | [] -> ()
  | msg1 :: messages1 ->
    let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg1 ssmi rsmi in
    let ir1 = not ir in
    existsb_handshake_messages_or_lem checker false is_psk ir ssmi rsmi msg1 messages1;
    existsb_handshake_messages_lem checker is_psk ir1 ssmi1 rsmi1 messages1;
    (* We still need to do a bit of work *)
    let b0 = existsb_handshake_messages checker is_psk ir ssmi rsmi (msg1 :: messages1) in
    let b1 = false || (checker is_psk ir ssmi rsmi ssmi1 rsmi1 msg1) in
    let b2 = existsb_handshake_messages checker is_psk ir1 ssmi1 rsmi1 messages1 in
    (* Check that we get what we were supposed to *)
    assert(b0 = (b1 || b2));
    (* Some asserts to check some equalities *)
    assert(forall (i : nat{i < List.length messages1}).
           List.Tot.index messages1 i == List.Tot.index messages (i+1));
    assert(forall (i : nat{i < List.length messages1}).
      handshake_messages_pre_smi is_psk ir ssmi1 rsmi1 messages1 i ==
      handshake_messages_pre_smi is_psk ir1 ssmi rsmi messages (i+1));
    assert(b2 <==>
      (exists (i : nat{i < List.length messages1}).
      checkerb_handshake_messages_one checker is_psk ir1 ssmi1 rsmi1 messages1 i));
    assert(
      (forall (i : nat{i < List.length messages1}).
      checkerb_handshake_messages_one checker is_psk ir1 ssmi1 rsmi1 messages1 i =
      checkerb_handshake_messages_one checker is_psk ir ssmi rsmi messages (i + 1)));
    (* Same thing as for the previous lemma: the prover doesn't manage to shift
     * the boundaries. *)
    let n = List.length messages in
    let p i : prop =
      checkerb_handshake_messages_one checker is_psk ir ssmi rsmi messages i == true in
    let pi = (exists (i : nat{i < List.length messages1}). p (i+1)) in
    let pj = (exists (j : nat{0 < j /\ j < List.length messages}). p j) in    
    exists_shift_nat_boundaries_lem n p;
    assert(pi <==> pj);
    (* Even now, we still need a bit of work *)
    exists_join_nat_boundaries_lem n p    
#pop-options

let forallb_handshake_pattern_messages_lem (hsk : handshake_pattern)
                                           (set_psk : bool)
                                           (checker : handshake_messages_crawl_checker) =
  let ismi, rsmi, is_psk = compute_premessages_post_smi hsk set_psk in
  forallb_handshake_messages_lem checker is_psk true ismi rsmi hsk.messages

(** Monotonicity *)
#push-options "--fuel 1"
let rec handshake_messages_pre_smi_is_greater_than_input is_psk ir ssmi0 rsmi0 messages i =
  if i = 0 then ()
  else
    match messages with
    | [] -> ()
    | msg :: messages' ->
      let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg ssmi0 rsmi0 in
      handshake_messages_pre_smi_is_greater_than_input is_psk (not ir) ssmi1 rsmi1 messages' (i-1)
#pop-options

#push-options "--fuel 1"
let rec handshake_messages_pre_smi_is_increasing is_psk ir ssmi0 rsmi0 messages i j =
  if i = j then ()
  else if i = 0 then handshake_messages_pre_smi_is_greater_than_input is_psk ir ssmi0 rsmi0 messages j
  else
    match messages with
    | [] -> ()
    | msg :: messages' ->
      let ssmi1, rsmi1 = crawl_messages_update_smi is_psk msg ssmi0 rsmi0 in
      handshake_messages_pre_smi_is_increasing is_psk (not ir) ssmi1 rsmi1 messages' (i-1) (j-1)
#pop-options    

let handshake_pattern_smi_is_increasing hsk set_psk i j =
  let ismi, rsmi, is_psk = compute_premessages_post_smi hsk set_psk in
  handshake_messages_pre_smi_is_increasing is_psk true ismi rsmi hsk.messages i j


(*** Handshake functions flags *)
(**** Messages *)
(***** Consistency lemmas *)

let csend_receive_message_pre_post_smi_consistent_lem
  (hsk : handshake_pattern)
  (set_psk : bool)
  (i : nat{0 < i /\ i < List.length hsk.messages}) = ()

#push-options "--z3rlimit 400 --fuel 4 --ifuel 4"
let csend_creceive_cexchange_smi_consistent_lem
  (hsk : handshake_pattern{
    (match hsk.premessage_ir with | Some pre -> List.length pre <= 2| None -> True) /\
    (match hsk.premessage_ri with | Some pre -> List.length pre <= 2 | None -> True)})
  (has_psk : bool) = ()
#pop-options

(**** Decomposition lemma *)
let receive_tokens_update_smi_decompose_lem is_psk tokens1 tokens2 smi =
  receive_tokens_update_hsf_decompose_lem is_psk tokens1 tokens2 smi.hsf;
  tokens_update_nonce_decompose_lem smi.hsf.sk is_psk tokens1 tokens2 smi.nonce;
  updt_sk_consistent_with_receive_tokens_update_smi is_psk tokens1 smi

(**** Frame lemmas *)

let receive_pretoken_update_smi_frame_lem (tk : premessage_token)
                                          (smi : meta_info) =
  receive_pretoken_update_hsf_frame_lem tk smi.hsf

let receive_premessage_update_smi_frame_lem (pattern : list premessage_token)
                                            (smi : meta_info) =
  receive_premessage_update_hsf_frame_lem pattern smi.hsf
/
Spec.Noise.NonceCounter.fsti.checked Spec.Noise.HandshakeFlags.fsti.checked Spec.Noise.Base.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
Spec.Noise.MetaInfo.fst

    is_psk: Prims.bool ->
    tk: Spec.Noise.Base.Definitions.message_token ->
    smi: Spec.Noise.MetaInfo.meta_info
  -> FStar.Pervasives.Lemma
    (ensures
      forall (s: Prims.bool) (e: Prims.bool) (psk: Prims.bool).
        let hsf1 =
          let _ = Mkmeta_info?.hsf smi in
          Spec.Noise.HandshakeFlags.Mkhandshake_state_flags (Mkhandshake_state_flags?.sk _)
            s
            e
            (Mkhandshake_state_flags?.rs _)
            (Mkhandshake_state_flags?.re _)
            psk
        in
        let smi1 = Spec.Noise.MetaInfo.Mkmeta_info hsf1 (Mkmeta_info?.nonce smi) in
        let smi2 = Spec.Noise.MetaInfo.receive_token_update_smi is_psk tk smi in
        Spec.Noise.MetaInfo.receive_token_update_smi is_psk tk smi1 ==
        Spec.Noise.MetaInfo.Mkmeta_info
          (let _ = Mkmeta_info?.hsf smi2 in
            Spec.Noise.HandshakeFlags.Mkhandshake_state_flags (Mkhandshake_state_flags?.sk _)
              s
              e
              (Mkhandshake_state_flags?.rs _)
              (Mkhandshake_state_flags?.re _)
              psk) (Mkmeta_info?.nonce smi2))
Prims.bool Spec.Noise.Base.Definitions.message_token Spec.Noise.MetaInfo.meta_info Spec.Noise.HandshakeFlags.receive_token_update_hsf_frame_lem Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf Prims.unit
let receive_token_update_smi_frame_lem (is_psk: bool) (tk: message_token) (smi: meta_info) =
  
receive_token_update_hsf_frame_lem is_psk tk smi.hsf