		Search-engine friendly clone of the ACL2 documentation.

Simultaneous-induction

Invariants-of-events-next

Preservation of a number of invariants by any sequence of zero or more events.

This is proved by simultaneous induction, involving all of the invariants.

The hypothesis that the genesis committee consists of validators in the system serves to prove the committees-in-system-p invariant.

A critical assumption is fault tolerance: all the committees that arise during the execution must be fault-tolerant.

Definitions and Theorems

Theorem: invariants-of-events-next

(defthm invariants-of-events-next
 (implies
  (and (subset (committee-members (genesis-committee))
               (all-addresses systate))
       (same-committees-p systate)
       (unequivocal-accepted-certificates-p systate)
       (last-anchor-voters-p systate)
       (omni-paths-p systate)
       (nonforking-anchors-p systate)
       (committed-redundant-p systate)
       (blockchain-redundant-p systate)
       (nonforking-blockchains-p systate)
       (same-owned-certificates-p systate)
       (no-self-messages-p systate)
       (no-self-buffer-p systate)
       (no-self-endorsed-p systate)
       (signer-records-p systate)
       (last-blockchain-round-p systate)
       (ordered-even-p systate)
       (accepted-certificate-committee-p systate)
       (signer-quorum-p systate)
       (previous-quorum-p systate)
       (backward-closed-p systate)
       (unequivocal-signed-certificates-p systate)
       (last-anchor-present-p systate)
       (committees-in-system-p systate)
       (rounds-in-committees-p systate)
       (events-possiblep events systate)
       (all-system-fault-tolerant-p events systate))
  (and
    (same-committees-p (events-next events systate))
    (unequivocal-accepted-certificates-p
         (events-next events systate))
    (last-anchor-voters-p (events-next events systate))
    (omni-paths-p (events-next events systate))
    (nonforking-anchors-p (events-next events systate))
    (committed-redundant-p (events-next events systate))
    (blockchain-redundant-p (events-next events systate))
    (nonforking-blockchains-p (events-next events systate))
    (same-owned-certificates-p (events-next events systate))
    (no-self-messages-p (events-next events systate))
    (no-self-buffer-p (events-next events systate))
    (no-self-endorsed-p (events-next events systate))
    (signer-records-p (events-next events systate))
    (last-blockchain-round-p (events-next events systate))
    (ordered-even-p (events-next events systate))
    (accepted-certificate-committee-p (events-next events systate))
    (signer-quorum-p (events-next events systate))
    (previous-quorum-p (events-next events systate))
    (backward-closed-p (events-next events systate))
    (unequivocal-signed-certificates-p (events-next events systate))
    (last-anchor-present-p (events-next events systate))
    (committees-in-system-p (events-next events systate))
    (rounds-in-committees-p (events-next events systate)))))