		Search-engine friendly clone of the ACL2 documentation.

Transitions

Transitions-augment

Transitions for proposal augmentation.

Here we define the system state changes caused by augment events.

When a correct validator receives an endorsement from another validator, it records the endorsement, associated with the pending proposal. The endorsement must come from a validator in the active committee for the proposal's round.

This kind of events only makes sense for correct validators. Faulty validators do not have an explicit internal state in our model, so there is nothing to record in their internal state. However, as defined in the transitions for certify events, faulty validators can still make use of endorsements, by using multiple ones at once, as part of creating a certificate.

Subtopics

Augment-next: New system state resulting from an augment event.
Augment-possiblep: Check if an augment event is possible in a system state.