val forallb_handshake_messages_lem (checker : handshake_messages_crawl_checker)
                                   (is_psk ir : bool)
                                   (ssmi rsmi : meta_info)
                                   (messages : list (list message_token)) :
  Lemma
  (ensures (
    forallb_handshake_messages checker is_psk ir ssmi rsmi messages <==>
    (forall (i : nat{i < List.length messages}).
    checkerb_handshake_messages_one checker is_psk ir ssmi rsmi messages i)))
  (decreases messages)
val forallb_handshake_messages_lem (checker : handshake_messages_crawl_checker)
                                   (is_psk ir : bool)
                                   (ssmi rsmi : meta_info)
                                   (messages : list (list message_token)) :
  Lemma
  (ensures (
    forallb_handshake_messages checker is_psk ir ssmi rsmi messages <==>
    (forall (i : nat{i < List.length messages}).
    checkerb_handshake_messages_one checker is_psk ir ssmi rsmi messages i)))
  (decreases messages)
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
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))) = ()
/
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

    checker: Spec.Noise.MetaInfo.handshake_messages_crawl_checker ->
    is_psk: Prims.bool ->
    ir: Prims.bool ->
    ssmi: Spec.Noise.MetaInfo.meta_info ->
    rsmi: Spec.Noise.MetaInfo.meta_info ->
    messages: Prims.list (Prims.list Spec.Noise.Base.Definitions.message_token)
  -> FStar.Pervasives.Lemma
      (ensures
        Spec.Noise.MetaInfo.forallb_handshake_messages checker is_psk ir ssmi rsmi messages <==>
        (forall (i: Prims.nat{i < FStar.List.Tot.Base.length messages}).
            Spec.Noise.MetaInfo.checkerb_handshake_messages_one checker
              is_psk
              ir
              ssmi
              rsmi
              messages
              i)) (decreases messages)
Spec.Noise.MetaInfo.handshake_messages_crawl_checker Prims.bool Spec.Noise.MetaInfo.meta_info Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.MetaInfo.forall_shift_nat_boundaries_lem Prims.nat Prims.b2t Prims.op_LessThan FStar.List.Tot.Base.length Prims.prop Prims.eq2 Spec.Noise.MetaInfo.checkerb_handshake_messages_one Prims.unit Prims._assert Prims.l_iff Prims.l_Forall Prims.op_Equality Prims.op_Addition FStar.Pervasives.Native.tuple2 Spec.Noise.MetaInfo.handshake_messages_pre_smi FStar.List.Tot.Base.index Prims.op_AmpAmp Spec.Noise.MetaInfo.forallb_handshake_messages Prims.Cons Spec.Noise.MetaInfo.forallb_handshake_messages_lem Spec.Noise.MetaInfo.forallb_handshake_messages_and_lem Prims.op_Negation Prims.l_and Spec.Noise.MetaInfo.less_than FStar.Pervasives.Native.snd FStar.Pervasives.Native.fst Spec.Noise.MetaInfo.crawl_messages_update_smi
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;
  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
  assert (b0 = (b1 && b2));
  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);
  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