Require Export PBFTwell_formed_log.


Section PBFTwf.

  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 update_state_new_view_preserves_wf :
    forall i s1 nv s2 msgs,
      update_state_new_view i s1 nv = (s2, msgs)
      -> well_formed_log (log s1)
      -> well_formed_log (log s2).
  Proof.
    introv upd wf.
    unfold update_state_new_view in upd; smash_pbft.
  Qed.
  Hint Resolve update_state_new_view_preserves_wf : pbft.

End PBFTwf.


Hint Resolve update_state_new_view_preserves_wf : pbft.
