Event
Fixtype of events.
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :propose → event-propose
- :endorse → event-endorse
- :augment → event-augment
- :certify → event-certify
- :accept → event-accept
- :advance → event-advance
- :commit → event-commit
The system changes its state (see system-state)
in response to the following events:
- A validator creates a proposals
and broadcasts it to some destinations.
- A validator endorses a proposal received from another validator,
and sends an endorsement (signature) back to the other validator.
- A validator augments a proposal it has previously created
with an endorsemenet received from another validator.
- A validator certifies a proposal
for which it has received enough endorsements,
creating a certificate and sending it to some destinations.
- A validator accepts a certificate received from another validator.
- A validator advances its round.
- A validator commits anchors.
The exact meaning of these different kinds of events is formalized
as the transitions of the labeled state transition system.
Note that certificates (and proposals)
are not necessarily broadcast to all the (correct) validators,
but instead the events indicate the destination addresses.
For the purpose of proving blockchain nonforking and other properties,
there is in fact no need to require broadcasts to go to all validators;
however, it is important for other kinds of properties,
so we may revise the model accordingly,
or perhaps create another version of the model for that.
Subtopics
- Event-fix
- Fixing function for event structures.
- Event-case
- Case macro for the different kinds of event structures.
- Eventp
- Recognizer for event structures.
- Event-equiv
- Basic equivalence relation for event structures.
- Event-propose
- Event-certify
- Event-endorse
- Event-augment
- Event-accept
- Event-commit
- Event-advance
- Event-kind
- Get the kind (tag) of a event structure.
