Require Export MicroBFTcount.


Section MicroBFTprops1.


  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 accepted_counter_if_know_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)
        /\ kc_knows (microbft_data_rdata rq) s2
        /\ kc_Tknows ui s2
        /\ kc_trust2owner ui = MicroBFT_primary
        /\ kc_trust_has_id ui i
        /\ commit_ui rq = ui
        /\ commit_n rq = r
        /\ not_primary R = true.
  Proof.
    introv h.
    apply accepted_counter_if_received_UI_primary in h.
    exrepnd.
    exists s s1 s2 ui rq.
    simpl.
    dands; auto; unfold MicroBFT_data_knows; simpl; subst; eauto 3 with microbft;[].
    unfold request_in_log; simpl; smash_microbft.
  Qed.


  Lemma node_backup1_backup2_or_primary :
    forall i,
      MicroBFTheader.node2name i =  MicroBFT_backup1
      \/ MicroBFTheader.node2name i =  MicroBFT_backup2
      \/ MicroBFTheader.node2name i =  MicroBFT_primary.
  Proof.
    destruct i; dands; eauto.
  Qed.

  Lemma request_was_verified :
    forall {eo : EventOrdering} (e : Event) (l : LOG_state) (u : USIG_state) r,
      (loc e = MicroBFT_backup1 \/ loc e = MicroBFT_backup2)
      -> M_state_sys_on_event MicroBFTsys e LOGname = Some l
      -> M_state_sys_on_event MicroBFTsys e USIGname = Some u
      -> kc_knows (microbft_data_rdata r) l
      -> verify_hash_usig (Build_HashData (commit_n r) (ui_pre (commit_ui r))) (ui2digest (commit_ui r)) (usig_local_keys u) = true.
  Proof.
    introv isr eqst1 eqst2 unl.

    unfold kc_Tknows in unl; simpl in unl.
    unfold MicroBFT_data_knows in unl; simpl in unl.

    rewrite M_state_sys_on_event_unfold in eqst1.
    rewrite M_state_sys_on_event_unfold in eqst2.

    apply map_option_Some in eqst1.
    apply map_option_Some in eqst2.
    exrepnd; try rev_Some.

    rewrite eqst1 in eqst2; ginv.

    revert dependent u.
    revert dependent l.
    revert dependent a.
    destruct isr as [isr1|isr2].

    { (* backup1*)
      rewrite isr1; simpl.

      (* WARNING *)
      clear isr1.

      induction e as [e ind] using predHappenedBeforeInd;[]; introv run stl inlog stu.

      rewrite M_run_ls_on_event_unroll2 in run.

      {
        apply map_option_Some in run; exrepnd; rev_Some.
        applydup M_run_ls_before_event_ls_is_microbft in run1; exrepnd; subst.

        unfold M_run_ls_on_this_one_event in run0; simpl in *.
        apply map_option_Some in run0; exrepnd; rev_Some.
        autorewrite with microbft in *.

        Time microbft_dest_msg Case; repeat(simpl in *; autorewrite with microbft in *; smash_microbft);
          try (complete (rewrite M_run_ls_before_event_unroll_on in run1;
                           destruct (dec_isFirst e); [| eapply ind in run1; eauto; eauto 3 with eo]; smash_microbft)).
      }
    }

    { (* backup2 *)
      rewrite isr2; simpl.

      (* WARNING *)
      clear isr2.

      induction e as [e ind] using predHappenedBeforeInd;[]; introv run stl inlog stu.

      rewrite M_run_ls_on_event_unroll2 in run.

      {
        apply map_option_Some in run; exrepnd; rev_Some.
        applydup M_run_ls_before_event_ls_is_microbft in run1; exrepnd; subst.

        unfold M_run_ls_on_this_one_event in run0; simpl in *.
        apply map_option_Some in run0; exrepnd; rev_Some.
        autorewrite with microbft in *.

        Time microbft_dest_msg Case; repeat(simpl in *; autorewrite with microbft in *; smash_microbft);
          try (complete (rewrite M_run_ls_before_event_unroll_on in run1;
                           destruct (dec_isFirst e); [| eapply ind in run1; eauto; eauto 3 with eo]; smash_microbft)).
      }
    }
  Qed.

  Lemma M_run_ls_on_event_MicroBFT_to_compoments :
    forall i {eo : EventOrdering} (e : Event) j s l u,
      loc e = MicroBFTheader.node2name i
      -> M_run_ls_on_event (MicroBFTlocalSys i) e = Some (MicroBFTlocalSys_new j s u l)
      -> M_state_sys_on_event MicroBFTsys e MAINname = Some s
         /\ M_state_sys_on_event MicroBFTsys e USIGname = Some u
         /\ M_state_sys_on_event MicroBFTsys e LOGname = Some l.
  Proof.
    introv eqrep h.
    unfold M_state_sys_on_event.
    allrw.
    unfold M_state_ls_on_event.
    unfold state_of_component. simpl in *.
    pose proof (node_backup1_backup2_or_primary i) as xx.
    destruct xx as [xx| [xx| xx]];
      rewrite xx in eqrep; clear xx;
      dands; eauto; apply map_option_Some; eexists; dands; eauto.
  Qed.



End MicroBFTprops1.
