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))
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');
  ()
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))
/
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
n: Prims.nat -> p: (x: Prims.nat{x < n} -> Prims.prop)
  -> FStar.Pervasives.Lemma
    (ensures
      (forall (i: Prims.nat{i < n - 1}). p (i + 1)) <==>
      (forall (j: Prims.nat{0 < j /\ j < n}). p j))
Prims.nat Prims.b2t Prims.op_LessThan Prims.prop Prims.unit Prims._assert Prims.l_imp Prims.logical Prims.l_Forall Prims.l_and Prims.op_Addition Prims.op_Subtraction
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
assert (pj ==> pi);
let pj' = forall (j: nat{0 < j /\ j < n}). p ((j - 1) + 1) in
assert (pi ==> pj');
()