Require Export PBFTexecute4.
Require Export PBFTsame_states.


Section PBFTagreement.

  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         }.
  Context { pbft_hash_axioms : PBFThash_axioms  }.


  Lemma agreement :
    forall (eo : EventOrdering) (e1 e2 : Event) v1 v2 ts c j1 j2 r1 r2 a1 a2 i1 i2,
      AXIOM_authenticated_messages_were_sent_or_byz_usys eo PBFTsys
      -> AXIOM_PBFTcorrect_keys eo
      -> AXIOM_exists_at_most_f_faulty [e1,e2] F
      -> loc e1 = PBFTreplica i1
      -> loc e2 = PBFTreplica i2
      -> In (send_reply (mk_reply v1 ts c j1 r1 a1)) (output_system_on_event_ldata PBFTsys e1)
      -> In (send_reply (mk_reply v2 ts c j2 r2 a2)) (output_system_on_event_ldata PBFTsys e2)
      -> r1 = r2.
  Proof.
    introv sendbyz ckeys atmost eqloc1 eqloc2 out1 out2.

    dup out1 as h.
    eapply output_system_on_event_ldata_implies_state_sm_on_event in h;eauto;
      [|introv; simpl in *; unfold PBFTsys; ginv; eauto 3 with pbft; try apply replicas_never_stop].
    exrepnd.

    dup out2 as z.
    eapply output_system_on_event_ldata_implies_state_sm_on_event in z;eauto;
      [|introv; simpl in *; unfold PBFTsys; ginv; eauto 3 with pbft; try apply replicas_never_stop].
    exrepnd.

    pose proof (state_sm_before_event_some_between3 e1 e1 (PBFTreplicaSM i1) st) as q.
    repeat (autodimp q hyp); eauto 3 with eo; exrepnd.

    pose proof (state_sm_before_event_some_between3 e2 e2 (PBFTreplicaSM i2) st0) as w.
    repeat (autodimp w hyp); eauto 3 with eo; exrepnd.

    rename st into st1.
    rename st0 into st.
    rename s' into st2.
    rename s'0 into st0.

    eapply replies_from in out1; eauto.
    eapply replies_from in out2; eauto.
    exrepnd.

    subst.

    match goal with
    | [ H1 : committed_log _ _ = _, H2 : committed_log _ _ = _ |- _ ] =>
      rename H1 into com1; rename H2 into com2; dup com1 as com
    end.

    match goal with
    | [ H1 : find_first_reply _ _ _ = _, H2 : find_first_reply _ _ _ = _ |- _ ] =>
      rename H1 into ffr1; rename H2 into ffr2
    end.

    match goal with
    | [ H1 : find_last_reply_entry_corresponding_to_client _ _ = _,
             H2 : find_last_reply_entry_corresponding_to_client _ _ = _,
                  H3 : find_last_reply_entry_corresponding_to_client _ _ = _,
                       H4 : find_last_reply_entry_corresponding_to_client _ _ = _ |- _ ] =>
      rename H1 into fl1; rename H2 into fl2; rename H3 into fl3; rename H4 into fl4
    end.

    match goal with
    | [ H1 : reply2requests _ _ _ _ _ _ = _, H2 : reply2requests _ _ _ _ _ _ = _ |- _ ] =>
      rename H1 into r2rs1; rename H2 into r2rs2
    end.

    match goal with
    | [ H1 : request2info _ = _, H2 : request2info _ = _ |- _ ] =>
      rename H1 into r2i1; rename H2 into r2i2
    end.

    destruct (SeqNumDeq (next_to_execute st0) (next_to_execute st2)) as [d|d].

    {
      rewrite d in *.

      eapply PBFT_A_1_11_before in com;
        try exact com2; try (exact q0); try (exact w0); auto; eauto 3 with pbft eo;[].
      apply eq_digests_implies_eq_requests in com; subst.

      rewrite ffr1 in ffr2; ginv.

      pose proof (next_to_execute_from_before eo e1 e2 j1 j2 st2 st0) as u.
      repeat (autodimp u hyp);[].
      repnd.
      rewrite u0 in *.
      rewrite u in *.

      pose proof (same_states_if_same_next_to_execute eo e1 e2 j1 j2 st1 st) as v.
      repeat (autodimp v hyp); try (complete (allrw; tcsp));[].
      repnd.
      try rewrite v0 in *.
      try rewrite v in *.

      eapply matching_reply2requests_implies in r2rs1; try (exact r2rs2).
      repnd; subst.

      rewrite fl1 in *; ginv.
      rewrite fl2 in *; ginv.

      rewrite r2i1 in *; ginv.
      smash_pbft.
    }

    assert (seqnum2nat (next_to_execute st0) <> seqnum2nat (next_to_execute st2)) as d'.
    { intro xx; destruct d.
      destruct (next_to_execute st0), (next_to_execute st2); simpl in *; tcsp. }

    apply not_eq in d'; repndors;[|].

    {
      assert (next_to_execute st <= next_to_execute st2) as lenext by (allrw; simpl; omega).
      applydup next_to_execute_is_greater_than_one in z0; auto;[].

      rewrite <- ite_first_state_sm_on_event_as_before in q0.
      unfold ite_first in *.
      destruct (dec_isFirst e1) as [d1|d1]; ginv; subst; simpl in *;[].
      pose proof (last_reply_state_increases
                    eo (local_pred e1) j1 st2
                    (next_to_execute st)) as u.
      repeat (autodimp u hyp); autorewrite with eo; auto;
        try omega; eauto 3 with pbft eo;[].
      exrepnd.

      pose proof (same_states_if_same_next_to_execute eo e' e2 j j2 st' st) as v.
      repeat (autodimp v hyp); try (complete (allrw; auto)); eauto 4 with pbft eo;[].
      repnd.
      rewrite v in u0.

      applydup u0 in fl4.
      exrepnd.

      match goal with
      | [ H : context[reply2requests j1] |- _ ] => rename H into rep2req
      end.
      applydup reply2requests_implies_last_reply_state_extends in rep2req as ext.
      applydup ext in fl0.
      exrepnd.
      rewrite fl8 in *; ginv.

      assert (ts <= lre_timestamp e4) as lets by omega.

      autodimp fl5 hyp;[apply eq_nats_implies_eq_timestamps; omega|].
      autodimp fl9 hyp;[apply eq_nats_implies_eq_timestamps; omega|].
      autodimp out0 hyp;[apply eq_nats_implies_eq_timestamps; omega|].

      assert (lre_reply e4 = Some r1) as eqr1 by (pbft_dest_all x; try omega).

      assert (Some r1 = Some r2) as eqrs by congruence.
      ginv.
    }

    {
      assert (next_to_execute st1 <= next_to_execute st0) as lenext by (allrw; simpl; omega).
      applydup next_to_execute_is_greater_than_one in h0; auto;[].

      rewrite <- ite_first_state_sm_on_event_as_before in w0.
      unfold ite_first in *.
      destruct (dec_isFirst e2) as [d1|d1]; ginv; subst; simpl in *;[].
      pose proof (last_reply_state_increases
                    eo (local_pred e2) j2 st0
                    (next_to_execute st1)) as u.
      repeat (autodimp u hyp); autorewrite with eo; auto; try omega; eauto 3 with pbft eo;[].
      exrepnd.

      pose proof (same_states_if_same_next_to_execute eo e' e1 j j1 st' st1) as v.
      repeat (autodimp v hyp); try (complete (allrw; auto)); eauto 5 with pbft eo;[].
      repnd.
      rewrite v in u0.

      applydup u0 in fl2.
      exrepnd.

      match goal with
      | [ H : context[reply2requests j2] |- _ ] => rename H into rep2req
      end.
      applydup reply2requests_implies_last_reply_state_extends in rep2req as ext.
      applydup ext in fl0.
      exrepnd.
      rewrite fl8 in *; ginv.

      assert (ts <= lre_timestamp e0) as lets by omega.

      autodimp fl5 hyp;[apply eq_nats_implies_eq_timestamps; omega|].
      autodimp fl9 hyp;[apply eq_nats_implies_eq_timestamps; omega|].
      autodimp out14 hyp;[apply eq_nats_implies_eq_timestamps; omega|].

      assert (lre_reply e0 = Some r2) as eqr2 by (pbft_dest_all x; try omega).

      assert (Some r1 = Some r2) as eqrs by congruence.
      ginv.
    }
  Qed.


End PBFTagreement.
