Require Export PBFTreceived_prepare_like1.
Require Export PBFTtactics5.


Section PBFTreceived_prepare_like5.

  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 prepare_like_of_send_view_change_are_in_log :
    forall (eo : EventOrdering) (e : Event) vc dst st i pi pl,
      loc e = PBFTreplica i
      -> In (send_view_change vc dst) (output_system_on_event_ldata PBFTsys e)
      -> state_sm_on_event (PBFTreplicaSM i) e = Some st
      -> In pi (view_change2prep vc)
      -> prepare_like_in_prepared_info pl pi
      -> prepare_like_in_log pl (log st).
  Proof.
    introv eqloce j eqst invc inpi.
    eapply in_output_system_on_event_ldata in j; eauto.

    unfold PBFTsys in j.
    try rewrite eqloce in j.

    rw @loutput_sm_on_event_unroll2 in j.
    fold (@DirectedMsgs _ _ _) in *.
    simpl in *.
    rewrite state_sm_on_event_unroll2 in eqst.

    match goal with
    | [ H : context[state_sm_before_event ?a ?b] |- _ ] =>
      remember (state_sm_before_event a b) as q; symmetry in Heqq; hide_hyp Heqq
    end.
    destruct q; simpl in *; ginv;[].

    op_st_some m eqtrig; rewrite eqtrig in *; simpl in *.

    unfold PBFTreplica_update in *.
    destruct m; simpl in *; ginv; subst; tcsp;
      smash_handlers; try conflicting_sends;
        try (complete (allrw in_app_iff; repndors; eauto 3 with pbft pbft_false)).

    {
      (* check-ready *)

      rename_hyp_with find_and_execute_requests fexec.
      eapply message_in_find_and_execute_requests_implies in fexec;[|eauto].
      repndors; exrepnd; conflicting_sends.
    }

    {
      (* check-bcast-new-view *)

      rename_hyp_with update_state_new_view upd.

      unfold broadcast2others in *; repndors; ginv.
      eapply message_in_update_state_new_view_implies in upd;[|eauto].
      exrepnd; ginv.
    }

    {
      (* expired-timer *)

      repndors; ginv; smash_pbft.
      unfold broadcast2others in *; exrepnd; ginv; simpl in *.
      unfold view_change2prep in *; simpl in *; eauto 3 with pbft.
    }

    {
      (* new_view *)

      rename_hyp_with update_state_new_view upd.
      rename_hyp_with add_prepares_to_log_from_new_view_pre_prepares add.

      allrw in_app_iff; repndors;
        [|eapply message_in_update_state_new_view_implies in upd;
          [|eauto];exrepnd;ginv];[].

      apply send_view_change_in_trim_outputs_with_low_water_mark in j.
      eapply in_add_prepares_to_log_from_new_view_pre_prepares_implies in add;[|eauto].
      repndors; exrepnd; ginv.
    }
  Qed.
  Hint Resolve prepare_like_of_send_view_change_are_in_log : pbft.

End PBFTreceived_prepare_like5.


Hint Resolve prepare_like_of_send_view_change_are_in_log : pbft.
