		Search-engine friendly clone of the ACL2 documentation.

Correctness

No-self-endorsed

Invariant that the recorded author-round pairs of endorsed certificates are from other validators.

When a new certificate is created, it is endorsed by validators other than the author of the certificate: create-possiblep checks that condition, and create-next extends the set of endorsed pairs of each endorser with the certificate's author and round. Thus, if the new set did not contain the validator's address, the new set does not contain it either. The other events either leave the set of endorsed pairs unchanged or remove pairs from it, thus preserving the absence of the validator's address in the set.

Subtopics

No-self-endorsed-p-of-next: Preservation of the invariant: if the invariant holds in a system state, it also holds in the next system state.
No-self-endorsed-p: Definition of the invariant: every pair in the endorsed set of a correct validator does not have the validator's address.
No-self-endorsed-p-when-init: Establishment of the invariant: the invariant holds in any initial system state.
No-self-endorsed-p-when-reachable: The invariant holds in every reachable state.
No-self-endorsed-p-of-events-next: Preservation of the invariant by multiple transitions.