Require Export MicroBFTprops1.


Section MicroBFTprops2.

  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         }.


  Definition MkMicroBFTtrustedSM (u : USIG_state) : trustedSM :=
    MktrustedSM
      _ _ _
      (build_mp_sm USIG_update u).

  Lemma ex_M_byz_run_ls_on_event_MicroBFTlocalSys :
    forall {eo : EventOrdering} (e : Event) n,
      (exists u, M_byz_run_ls_on_event (MicroBFTlocalSys n) e = Some (M_t (MkMicroBFTtrustedSM u)))
      \/ (exists s u l, M_byz_run_ls_on_event (MicroBFTlocalSys n) e = Some (M_nt (MicroBFTlocalSys_new n s u l))).
  Proof.
    introv.
    remember (M_byz_run_ls_on_event (MicroBFTlocalSys n) e) as run; symmetry in Heqrun.

    pose proof (M_byz_compose_step2 e (MicroBFTlocalSys n) (USIG_comp n)) as q.
    repeat (autodimp q hyp); eauto 3 with microbft comp;[].
    exrepnd.
    clear l q1 q0.
    unfold M_byz_state_ls_on_event in *.
    rewrite Heqrun in q2; simpl in *.
    apply map_option_Some in q2; exrepnd; subst; simpl in *.
    symmetry in q0.
    rewrite q1.

    destruct a; simpl in *; ginv.

    { right.
      apply option_map_Some in q0; exrepnd; subst; simpl in *.
      apply M_byz_run_ls_on_event_M_run_ls_on_event in q1.
      apply M_run_ls_on_event_ls_is_microbft in q1.
      exrepnd; subst.
      eexists; eexists; eexists; reflexivity. }

    { left.
      eapply M_byz_run_ls_on_event_some_M_t_implies in q1; simpl; eauto; eauto 3 with microbft.
      simpl in *; repnd.
      rewrite q0.
      exists (state_of_trusted t); auto. }
  Qed.


  Lemma ex_M_byz_run_ls_before_event_MicroBFTlocalSys :
    forall {eo : EventOrdering} (e : Event) n,
      (exists (u : USIG_state),
          M_byz_run_ls_before_event (MicroBFTlocalSys n) e = Some (M_t (MkMicroBFTtrustedSM u)))
      \/
      (exists s u l,
          M_byz_run_ls_before_event (MicroBFTlocalSys n) e = Some (M_nt (MicroBFTlocalSys_new n s u l))).
  Proof.
    introv.
    rewrite M_byz_run_ls_before_event_unroll_on.
    destruct (dec_isFirst e) as [d|d].

    { right.
      rewrite MicroBFTlocalSys_as_new.
      eexists; eexists; eexists; eauto. }

    apply ex_M_byz_run_ls_on_event_MicroBFTlocalSys.
  Qed.

  Lemma MicroBFT_M_byz_run_ls_on_event_unroll_sp :
    forall {eo : EventOrdering}
           (e  : Event)
           (r  : MicroBFT_node),
      (exists s u l,
          M_byz_run_ls_on_event (MicroBFTlocalSys r) e
          = M_byz_run_ls_on_this_one_event (MicroBFTlocalSys_new r s u l) e
          /\ M_byz_run_ls_before_event (MicroBFTlocalSys r) e
             = Some (M_nt ((MicroBFTlocalSys_new r s u l))))
      \/
      (exists u,
          M_byz_run_ls_on_event (MicroBFTlocalSys r) e
          = Some (M_t (fst (run_trustedSM_on_trigger_info (MkMicroBFTtrustedSM u) (trigger e))))
          /\ M_byz_run_ls_before_event (MicroBFTlocalSys r) e
             = Some (M_t (MkMicroBFTtrustedSM u))).
  Proof.
    introv.
    rewrite M_byz_run_ls_on_event_unroll.
    destruct (dec_isFirst e) as [d|d]; simpl.

    { left.
      rewrite MicroBFTlocalSys_as_new.
      eexists; eexists; eexists; dands; eauto.
      rewrite M_byz_run_ls_before_event_unroll_on.
      destruct (dec_isFirst e); tcsp. }

    pose proof (ex_M_byz_run_ls_before_event_MicroBFTlocalSys e r) as w.
    repndors; exrepnd; allrw; simpl.

    { right; eexists; eauto. }

    left.
    eexists; eexists; eexists; eauto.
  Qed.


  Lemma USIG_preserves_id :
    forall {eo : EventOrdering} (e : Event) n l s1 s2,
      loc e = MicroBFTheader.node2name n
      -> usig_id s1 = n
      -> run_sm_on_inputs_trusted (USIG_sm_new s1) l = s2
      -> usig_id s2 = n.
  Proof.
    induction l; introv eqloc eqid run; simpl in *; tcsp.

    { autorewrite with microbft in *; simpl in *; subst; tcsp. }

    pose proof (run_sm_on_inputs_trusted_cons
                  _ _ _ (USIG_sm_new s1) a l) as w.
    simpl in *; rewrite w in run; auto; clear w;[].

    unfold USIG_update in run; destruct a; repnd; simpl in *;
      [|apply IHl in run; auto];[].
    apply IHl in run; auto.
  Qed.


  Lemma preserves_usig_id :
    forall {eo : EventOrdering} (e : Event) n u,
      loc e = MicroBFTheader.node2name n
      -> M_byz_state_ls_on_event_of_trusted (MicroBFTlocalSys n) e = Some u
      -> usig_id u = n.
  Proof.
    intros eo; induction e as [e ind] using predHappenedBeforeInd;[]; introv eqloc eqst.

    pose proof (M_byz_compose_step_trusted e (MicroBFTlocalSys n) (USIG_comp n)) as h.
    repeat (autodimp h hyp); eauto 3 with comp microbft;[].
    exrepnd.
    rewrite eqst in h2; ginv; simpl.

    pose proof (USIG_preserves_id
                  e n l s1
                  (run_sm_on_inputs_trusted (USIG_sm_new s1) l)) as q.
    repeat (autodimp q hyp).

    rewrite unroll_M_byz_state_ls_before_event_of_trusted in h1.
    destruct (dec_isFirst e) as [d|d].

    { apply option_map_Some in h1; exrepnd; subst; simpl in *.
      unfold find_trusted_sub in h1; simpl in h1; ginv. }

    apply ind in h1; autorewrite with eo; eauto 2 with eo.
  Qed.


  Lemma preserves_usig_id2 :
    forall {eo : EventOrdering} (e : Event) n ls u,
      loc e = MicroBFTheader.node2name n
      -> M_run_ls_on_event (MicroBFTlocalSys n) e = Some ls
      -> state_of_component USIGname ls = Some u
      -> usig_id u = n.
  Proof.
    introv eqloc run eqst.
    apply (preserves_usig_id e n u); auto.
    unfold M_byz_state_ls_on_event_of_trusted; simpl.
    applydup @M_run_ls_on_event_M_byz_run_ls_on_event in run as z; rewrite z; simpl.
    apply M_run_ls_on_event_ls_is_microbft in run; exrepnd; subst; simpl in *; tcsp.
  Qed.


End MicroBFTprops2.
