Require Export PBFTreceived_prepare_like1.


Section PBFTdelay_of_send_prepares.

  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 delay_of_send_prepares :
    forall (eo : EventOrdering) (e : Event) p dst delay,
      In (MkDMsg (PBFTprepare p) dst delay) (output_system_on_event_ldata PBFTsys e)
      -> delay = ('0).
  Proof.
    introv j.
    apply in_output_system_on_event_ldata_ex in j; destruct j as [n [eqloc j] ].
    unfold PBFTsys in j.

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

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

    remember (trigger_op e) as trig; symmetry in Heqtrig.
    destruct trig; simpl in *; tcsp.
    unfold PBFTreplica_update in *.
    destruct m; simpl in *; ginv; subst; tcsp;
      smash_handlers; try conflicting_sends;
        try (complete (repndors; tcsp; ginv));
        try (complete (unfold broadcast2others in *; ginv)).

    {
      (* pre-prepare *)
      allrw in_app_iff; repndors.
      - apply in_check_broadcast_prepare_implies in j; exrepnd; subst; unfold send_prepare in *; ginv.
      - apply in_check_broadcast_commit_implies in j; exrepnd; ginv.
      - eapply message_in_check_send_replies_implies in j;[|eauto]; ginv.
    }

    {
      (* prepare *)
      allrw in_app_iff; repndors.
      - apply in_check_broadcast_commit_implies in j; exrepnd; ginv.
      - eapply message_in_check_send_replies_implies in j;[|eauto]; ginv.
    }

    {
      (* commit *)
      eapply message_in_check_send_replies_implies in j;[|eauto]; ginv.
    }

    {
      (* check-ready *)
      eapply message_in_find_and_execute_requests_implies in j;[|eauto]; repndors; exrepnd; ginv.
    }

    {
      (* check-bcast-new-view *)
      repndors; ginv.
      eapply message_in_update_state_new_view_implies in j;[|eauto]; exrepnd; ginv.
    }

    {
      (* expired-timer *)
      allrw in_app_iff; repndors.
      - apply send_message_in_trim_outputs_with_low_water_mark in j.
        eapply in_add_prepares_to_log_from_new_view_pre_prepares_implies in j;[|eauto].
        repndors; exrepnd; unfold send_prepare in *; ginv.
      - eapply message_in_update_state_new_view_implies in j;[|eauto]; exrepnd; ginv.
    }
  Qed.

  Lemma send_prepare_no_delay :
    forall (eo : EventOrdering) (e : Event) p dst delay,
      In (MkDMsg (PBFTprepare p) dst delay) (output_system_on_event_ldata PBFTsys e)
      -> In (send_prepare p dst) (output_system_on_event_ldata PBFTsys e).
  Proof.
    introv i.
    applydup delay_of_send_prepares in i; subst; auto.
  Qed.

End PBFTdelay_of_send_prepares.
