Require Export MicroBFTprops0.
Require Export MicroBFTsubs.
Require Export MicroBFTbreak.
Require Export ComponentSM6.


Section MicroBFTcount.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { dtc                 : DTimeContext          }.
  Context { microbft_context    : MicroBFT_context      }.
  Context { m_initial_keys      : MicroBFT_initial_keys }.
  Context { u_initial_keys      : USIG_initial_keys     }.
  Context { usig_hash           : USIG_hash             }.
  Context { microbft_auth       : MicroBFT_auth         }.

  Lemma M_output_ls_on_input_is_log_new_implies :
    forall u r v o,
      M_output_ls_on_input (LOGlocalSys u) (log_new r) = (LOGlocalSys v, o)
      -> in_log r v.
  Proof.
    introv out.
    unfold M_output_ls_on_input in out; simpl in *.
    unfold M_run_smat_on_inputs in out; simpl in *.
    unfold M_run_update_on_inputs in out; simpl in *.
    unfold M_break in *; simpl in *; ginv.
    inversion out; auto; simpl; tcsp.
  Qed.

  Lemma invalid_request_false_implies_ui2rep_eq :
    forall R r s,
      invalid_commit R r s = false
      -> ui2rep (commit_ui r) = MicroBFT_primary.
  Proof.
    introv inv; unfold invalid_commit, valid_commit, is_primary in *; smash_microbft_2.
  Qed.
  Hint Resolve invalid_request_false_implies_ui2rep_eq : microbft.

  Lemma invalid_request_false_implies_not_primary :
    forall R r s,
      invalid_commit R r s = false
      -> not_primary R = true.
  Proof.
    introv inv; unfold invalid_commit, valid_commit, is_primary in *; smash_microbft_2.
  Qed.
  Hint Resolve invalid_request_false_implies_not_primary : microbft.

  (* This uses compositional reasoning, but using [LOG_comp]'s spec defined in
     [M_output_ls_on_input_is_committed_implies] *)
  Lemma accepted_counter_if_received_UI_primary :
    forall {eo : EventOrdering}
           (e  : Event)
           (R  : MicroBFT_node)
           (r  : nat)
           (i  : nat)
           (l  : list name),
      In (send_accept (accept r i) l) (M_output_ls_on_event (MicroBFTlocalSys R) e)
      ->
      exists (s  : MAIN_state)
             (s1 : USIG_state)
             (s2 : LOG_state)
             (ui : UI)
             (rq : Commit),
        M_run_ls_on_event (MicroBFTlocalSys R) e = Some (MicroBFTlocalSys_new R s s1 s2)
        /\ in_log rq s2
        /\ commit_n rq = r
        /\ commit_ui rq = ui
        /\ ui2counter ui = i
        /\ ui2rep ui = MicroBFT_primary
        /\ not_primary R = true.
  Proof.
    introv h.
    apply M_output_ls_on_event_as_run in h; exrepnd.
    rename ls' into ls.
    rewrite M_run_ls_on_event_unroll2; allrw; simpl.
    applydup M_run_ls_before_event_ls_is_microbft in h1; exrepnd; subst.
    apply in_M_output_ls_on_this_one_event_implies in h0; exrepnd; simpl in *.
    unfold M_run_ls_on_this_one_event; simpl; allrw; simpl.

    rewrite M_break_snd_eq2 in h2.
    rewrite M_break_option_map_fst_eq.
    unfold statefund_nm in *; simpl in *.
    match goal with
    | [ H : context[M_break ?a ?b ?c] |- _ ] => remember (M_break a b c) as mb; symmetry in Heqmb
    end.
    simpl in *.
    rewrite Heqmb in h2; rewrite Heqmb.
    repnd; simpl in *.

    autorewrite with microbft comp in *.

    Time microbft_dest_msg Case; simpl in *; tcsp; ginv; repeat smash_microbft_2; ginv;
      repeat (use_m_break_call_comp out;
                destruct out; simpl in *; repeat smash_microbft_2;
                  repndors; ginv; tcsp).

    exrepnd; subst.
    applydup M_output_ls_on_input_is_log_new_implies in Heqout0.
    eexists; eexists; eexists; eexists; eexists; dands; try reflexivity; eauto 3 with microbft.
  Qed.

End MicroBFTcount.
