Require Export PBFTview_changes_from_good1.


Section PBFTview_changes_from_good4.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { pbft_context : PBFTcontext      }.
  Context { pbft_auth    : PBFTauth         }.
  Context { pbft_keys    : PBFTinitial_keys }.
  Context { pbft_hash    : PBFThash         }.

  Lemma own_view_changes_are_own :
    forall (eo : EventOrdering) (e : Event) i st vc,
      state_sm_on_event (PBFTreplicaSM i) e = Some st
      -> own_view_change_in_log vc (view_change_state st)
      -> view_change2sender vc = i.
  Proof.
    prove_by_ind ind h eqst sop p m eqtrig trig smash_handlers3 smash_pbft_ind3.

    {
      (* check-bcast_new_view *)

      rename_hyp_with update_state_new_view upd.
      rename_hyp_with CheckBCastNewView2entry cb.
      rename_hyp_with check_broadcast_new_view check.
      rename_hyp_with own_view_change_in_log vcinlog.

      apply CheckBCastNewView2entry_some_implies in cb.

      apply update_state_new_view_preserves_view_change_state in upd; simpl in *.
      rewrite upd in vcinlog; clear upd.

      apply own_view_change_log_new_view_and_entry_implies in vcinlog;
        repndors;[try (smash_pbft_ind ind)|];[].

      applydup check_broadcast_new_view_implies in check.
      exrepnd; subst; simpl in *; autorewrite with pbft in *; ginv.
      autorewrite with pbft in *.

      dup cb as j.
      eapply in_implies_own_view_change_in_log in j;[| |eauto]; eauto 2 with pbft;[].
      try (smash_pbft_ind ind).
    }

    {
      (* expired-timer *)

      rename_hyp_with start_view_change start.
      rename_hyp_with own_view_change_in_log vcinlog.

      eapply start_view_change_preserves_own_view_change_in_log in vcinlog;[|eauto].
      simpl in *; repndors; subst; tcsp.
      try (smash_pbft_ind ind).
    }

    {
      (* new-view *)

      rename_hyp_with add_prepares_to_log_from_new_view_pre_prepares add.
      rename_hyp_with update_state_new_view upd.
      rename_hyp_with own_view_change_in_log vcinlog.

      apply update_state_new_view_preserves_view_change_state in upd; simpl in *.
      rewrite upd in vcinlog; clear upd.
      apply add_prepares_to_log_from_new_view_pre_prepares_preserves_view_change_state in add; simpl in *.
      rewrite add in vcinlog; clear add.

      apply own_view_change_log_new_view_implies in vcinlog.
      try (smash_pbft_ind ind).
    }
  Qed.
  Hint Resolve own_view_changes_are_own : pbft.

  Lemma own_view_changes_are_own_before :
    forall (eo : EventOrdering) (e : Event) i st vc,
      state_sm_before_event (PBFTreplicaSM i) e = Some st
      -> own_view_change_in_log vc (view_change_state st)
      -> view_change2sender vc = i.
  Proof.
    introv eqst own.
    rewrite <- ite_first_state_sm_on_event_as_before in eqst.
    unfold ite_first in *.
    destruct (dec_isFirst e) as [d1|d1]; ginv; subst; simpl in *; tcsp.
    eauto 3 with pbft.
  Qed.
  Hint Resolve own_view_changes_are_own_before : pbft.

End PBFTview_changes_from_good4.


Hint Resolve own_view_changes_are_own : pbft.
Hint Resolve own_view_changes_are_own_before : pbft.
