		Search-engine friendly clone of the ACL2 documentation.

No-self-endorsed

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.

When a certificate is created, a pair is added to all the endorsers, while the other validators keep the same set of endorsed pairs, and thus the invariant is preserved for them. So it remains to show that the newly added pair has an author distinct from any endorser. For the certificate to be created, create-possiblep must hold, which indirectly calls create-signer-possiblep for all the correct endorsers. As we are considering a generic correct endorser in the proof, we can use its create-signer-possiblep to show that the author is not the endorser, so the addition of the new pair preserves the invariant.

When a certificate is stored into the DAG, the validator removes, from the set of endorsed pairs, the pair with the certificate's author and round, if present in the set. So if the set satsfied the invariant before, it also does after the removal. The other validators keep the same set of endorsed pairs, so the invariant is preserved.

The other kinds of events do not change any set of endorsed pairs, and thus the invariant is preserved for all validators.

Definitions and Theorems

Theorem: no-self-endorsed-p-of-create-next

(defthm no-self-endorsed-p-of-create-next
  (implies (and (no-self-endorsed-p systate)
                (create-possiblep cert systate))
           (no-self-endorsed-p (create-next cert systate))))

Theorem: no-self-endorsed-p-of-accept-next

(defthm no-self-endorsed-p-of-accept-next
  (implies (and (no-self-endorsed-p systate)
                (accept-possiblep msg systate))
           (no-self-endorsed-p (accept-next msg systate))))

Theorem: no-self-endorsed-p-of-advance-next

(defthm no-self-endorsed-p-of-advance-next
  (implies (and (no-self-endorsed-p systate)
                (advance-possiblep val systate))
           (no-self-endorsed-p (advance-next val systate))))

Theorem: no-self-endorsed-p-of-commit-next

(defthm no-self-endorsed-p-of-commit-next
  (implies (and (no-self-endorsed-p systate)
                (commit-possiblep val systate))
           (no-self-endorsed-p (commit-next val systate))))

Theorem: no-self-endorsed-p-of-event-next

(defthm no-self-endorsed-p-of-event-next
  (implies (and (no-self-endorsed-p systate)
                (event-possiblep event systate))
           (no-self-endorsed-p (event-next event systate))))