Require Export PBFTwf_checkpoint_state.


Section PBFTstate_info.

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

  Record StateInfo :=
    MkStateInfo
      {
        si_digest : PBFTdigest;
        si_seq    : SeqNum;
      }.

  Definition view_change2state_info (vc : ViewChange) : StateInfo :=
    MkStateInfo (view_change2digest vc) (view_change2seq vc).

  Definition checkpoint2state_info (cp : Checkpoint) : StateInfo :=
    MkStateInfo (checkpoint2digest cp) (checkpoint2seq cp).

End PBFTstate_info.
