Require Export MinBFTcount.
Require Export MinBFTacc_exec.
Require Export MinBFTacc_new.
Require Export MinBFTvreq_mon.


Section MinBFTprops1.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { dtc                 : DTimeContext        }.
  Context { minbft_context      : MinBFT_context      }.
  Context { m_initial_keys      : MinBFT_initial_keys }.
  Context { u_initial_keys      : USIG_initial_keys   }.
  Context { usig_hash           : USIG_hash           }.
  Context { minbft_auth         : MinBFT_auth         }.


  Lemma accepted_counter_if_know_UI_primary :
    forall {eo    : EventOrdering}
           (e     : Event)
           (R     : Rep)
           (r     : Request)
           (i     : nat)
           (l     : list name),
      In (send_accept (accept r i) l) (M_output_ls_on_event (MinBFTlocalSys R) e)
      ->
      exists (s  : MAIN_state)
             (s1 : USIG_state)
             (s2 : LOG_state)
             (ui : UI),
        M_run_ls_on_event (MinBFTlocalSys R) e = Some (MinBFTlocalSys_new R s s1 s2)
        /\ kc_knows (minbft_data_rdata (request_data (current_view s) r ui)) s2
        /\ kc_Tknows ui s2
        /\ kc_trust2owner ui = MinBFTprimary (current_view s)
        /\ kc_trust_has_id ui i.
  Proof.
    introv h.
    apply accepted_counter_if_received_UI_primary in h.
    exrepnd.
    exists s s1 s2 ui.
    simpl.
    dands; auto; unfold MinBFT_data_knows; simpl; subst; eauto 3 with minbft;[].
    unfold request_data_in_log; simpl.
    allrw <-; autorewrite with minbft; allrw; auto.
  Qed.

  Lemma kc_Tknows_implies :
    forall  (ui : UI) (l : LOG_state),
      kc_Tknows ui l
      -> exists en,
        In en l
        /\ ui_in_log ui l = true
        /\
        (
          (exists rd, request_data2ui rd = ui )
          \/
          (In ui (log_entry_commits en))
        ).
  Proof.
    introv H.
    unfold kc_Tknows in *.
    unfold kc_knows in *. simpl in *.
    unfold MinBFT_data_knows in *.
    unfold MinBFT_data_in_log in *.

    unfold ui_in_log in *.
    eapply existsb_exists in H.
    exrepnd.
    rename x into en.

    unfold ui_in_log_entry in *.
    dest_cases w;[|].
    {
      exists en; dands; eauto.
      eapply existsb_exists.
      exists en. dands; eauto.
      dest_cases x.
    }
    {
      dest_cases x;[].
      exists en; dands; eauto.
      eapply existsb_exists.
      exists en; dands; eauto.
      dest_cases x;[].
      dest_cases y.
    }
  Qed.

  Lemma request_data_was_verified :
    forall {eo : EventOrdering} (e : Event) (l : LOG_state) (u : USIG_state) v r ui,
      is_replica e
      -> M_state_sys_on_event MinBFTsys e LOGname = Some l
      -> M_state_sys_on_event MinBFTsys e USIGname = Some u
      -> kc_knows (minbft_data_rdata (request_data v r ui)) l
      -> verify_hash_usig (Build_HashData v r (ui_pre ui)) (ui2digest ui) (usig_local_keys u) = true.
  Proof.
    introv isr eqst1 eqst2 unl.

    unfold kc_Tknows in unl; simpl in unl.
    unfold MinBFT_data_knows in unl; simpl in unl.

    rewrite M_state_sys_on_event_unfold in eqst1.
    rewrite M_state_sys_on_event_unfold in eqst2.

    apply map_option_Some in eqst1.
    apply map_option_Some in eqst2.
    exrepnd; try rev_Some.

    rewrite eqst1 in eqst2; ginv.

    unfold is_replica in *; exrepnd.

    revert dependent u.
    revert dependent l.
    revert dependent a.
    rewrite isr0; simpl.

    (* WARNING *)
    clear isr0.

    induction e as [e ind] using predHappenedBeforeInd;[]; introv run stl inlog stu.

    rewrite M_run_ls_on_event_unroll2 in run.

    {
      apply map_option_Some in run; exrepnd; rev_Some.
      applydup M_run_ls_before_event_ls_is_minbft in run1; exrepnd; subst.

      unfold M_run_ls_on_this_one_event in run0; simpl in *.
      apply map_option_Some in run0; exrepnd; rev_Some.
      autorewrite with minbft in *.

      Time minbft_dest_msg Case;
        repeat (simpl in *; autorewrite with minbft in *; smash_minbft2);
        try (simpl in *; unfold state_of_subcomponents in *; simpl in *; ginv);
        try (complete (rewrite M_run_ls_before_event_unroll_on in run1;
                         destruct (dec_isFirst e); smash_minbft2;
                           eapply ind in run1; eauto; eauto 3 with eo));
        try (complete (ginv; smash_minbft2;
                         unfold verify_UI in *; simpl in *; autorewrite with minbft in *;
                           first [destruct p as [b pui], b
                                 |destruct c as [b pui], b]; simpl in *; ginv;
                             unfold prepare2hash_data, RequestData2HashData, prepare2request in *; simpl in *; auto;
                               unfold invalid_prepare, valid_prepare in *; simpl in *; smash_minbft;
                                 unfold prepare2view in *; simpl in *; subst; tcsp; ginv; auto;
                                   try (complete (rewrite M_run_ls_before_event_unroll_on in run1;
                                                    destruct (dec_isFirst e); smash_minbft2;
                                                      eapply ind in run1; eauto; eauto 3 with eo)))).
    }
  Qed.

  Lemma M_run_ls_on_event_MinBFT_to_components :
    forall i {eo : EventOrdering} (e : Event) j s l u,
      loc e = MinBFT_replica i
      -> M_run_ls_on_event (MinBFTlocalSys i) e = Some (MinBFTlocalSys_new j s u l)
      -> M_state_sys_on_event MinBFTsys e MAINname = Some s
         /\ M_state_sys_on_event MinBFTsys e USIGname = Some u
         /\ M_state_sys_on_event MinBFTsys e LOGname = Some l.
  Proof.
    introv eqrep h.
    unfold M_state_sys_on_event; allrw; simpl.
    unfold M_state_ls_on_event.
    allrw; simpl.
    unfold state_of_subcomponents; simpl; tcsp.
  Qed.

End MinBFTprops1.
