		Search-engine friendly clone of the ACL2 documentation.

Last-anchor-voters-def-and-init-and-next

Last-anchor-voters-p-of-next

Preservation of the invariant: if the invariant holds in a system state, it also holds in the next system state.

A create or accept event does not modify the last committed anchor. It may add certificates to the DAG, which may be successors of the last committed anchor, but since successors is monotone, the inequality of more than f voting stake is preserved.

A commit event changes the last committed anchor, but its preconditions include the fact that the new anchor has more than f voting stake. Since our invariant is phrased in terms of successors certificates, we need a lemma that relates the stake of successors to the voting stake returned by leader-stake-votes; this needs non-equivocation because leader-stake-votes would count the stake of equivocal certificates multiple times, while cert-set->author-set applied to successors-loop counts the stake of each author only once. Since the event also extends the blockchain, as in other proofs we need to show that the extension of the blockchain does not modify the committee active at the round of the successors.

An advance event does not change the last committed anchor or the DAG, and thus the successors of the anchor.

Definitions and Theorems

Theorem: validator-last-anchor-voters-p-of-create-next

(defthm validator-last-anchor-voters-p-of-create-next
  (implies
       (and (system-committees-fault-tolerant-p systate)
            (no-self-endorsed-p systate)
            (signer-records-p systate)
            (signer-quorum-p systate)
            (unequivocal-dags-p systate)
            (same-committees-p systate)
            (last-anchor-present-p systate)
            (create-possiblep cert systate)
            (in val (correct-addresses systate))
            (validator-last-anchor-voters-p
                 (get-validator-state val systate)))
       (validator-last-anchor-voters-p
            (get-validator-state val (create-next cert systate)))))

Theorem: last-anchor-voters-p-of-create-next

(defthm last-anchor-voters-p-of-create-next
  (implies (and (last-anchor-voters-p systate)
                (system-committees-fault-tolerant-p systate)
                (no-self-endorsed-p systate)
                (signer-records-p systate)
                (signer-quorum-p systate)
                (unequivocal-dags-p systate)
                (same-committees-p systate)
                (last-anchor-present-p systate)
                (create-possiblep cert systate))
           (last-anchor-voters-p (create-next cert systate))))

Theorem: validator-last-anchor-voters-p-of-accept-next

(defthm validator-last-anchor-voters-p-of-accept-next
  (implies
       (and (system-committees-fault-tolerant-p systate)
            (signer-quorum-p systate)
            (unequivocal-signed-certs-p systate)
            (unequivocal-dags-p systate)
            (same-committees-p systate)
            (last-anchor-present-p systate)
            (accept-possiblep msg systate)
            (messagep msg)
            (in val (correct-addresses systate))
            (validator-last-anchor-voters-p
                 (get-validator-state val systate)))
       (validator-last-anchor-voters-p
            (get-validator-state val (accept-next msg systate)))))

Theorem: last-anchor-voters-p-of-accept-next

(defthm last-anchor-voters-p-of-accept-next
  (implies (and (last-anchor-voters-p systate)
                (system-committees-fault-tolerant-p systate)
                (signer-quorum-p systate)
                (unequivocal-signed-certs-p systate)
                (unequivocal-dags-p systate)
                (same-committees-p systate)
                (last-anchor-present-p systate)
                (accept-possiblep msg systate)
                (messagep msg))
           (last-anchor-voters-p (accept-next msg systate))))

Theorem: validator-last-anchor-voters-p-of-advance-next

(defthm validator-last-anchor-voters-p-of-advance-next
  (implies
       (and (advance-possiblep val systate)
            (in val1 (correct-addresses systate))
            (validator-last-anchor-voters-p
                 (get-validator-state val1 systate)))
       (validator-last-anchor-voters-p
            (get-validator-state val1 (advance-next val systate)))))

Theorem: last-anchor-voters-p-of-advance-next

(defthm last-anchor-voters-p-of-advance-next
  (implies (and (last-anchor-voters-p systate)
                (advance-possiblep val systate))
           (last-anchor-voters-p (advance-next val systate))))

Theorem: stake-of-successors-loop-to-leader-stake-votes

(defthm stake-of-successors-loop-to-leader-stake-votes
 (implies
     (and (certificate-setp certs)
          (certificate-set-unequivocalp certs)
          (addressp prev)
          (<= (cardinality (cert-set->round-set certs))
              1))
     (equal (committee-members-stake
                 (cert-set->author-set (successors-loop certs prev))
                 commtt)
            (leader-stake-votes prev certs commtt))))

Theorem: stake-of-successors-to-leader-stake-votes

(defthm stake-of-successors-to-leader-stake-votes
  (implies
       (and (certificate-setp dag)
            (certificate-set-unequivocalp dag))
       (equal (committee-members-stake
                   (cert-set->author-set (successors cert dag))
                   commtt)
              (leader-stake-votes
                   (certificate->author cert)
                   (certs-with-round (1+ (certificate->round cert))
                                     dag)
                   commtt))))

Theorem: validator-last-anchor-voters-p-of-commit-next

(defthm validator-last-anchor-voters-p-of-commit-next
  (implies
       (and (last-blockchain-round-p systate)
            (ordered-blockchain-p systate)
            (unequivocal-dags-p systate)
            (commit-possiblep val systate)
            (addressp val)
            (in val1 (correct-addresses systate))
            (validator-last-anchor-voters-p
                 (get-validator-state val1 systate)))
       (validator-last-anchor-voters-p
            (get-validator-state val1 (commit-next val systate)))))

Theorem: last-anchor-voters-p-of-commit-next

(defthm last-anchor-voters-p-of-commit-next
  (implies (and (last-anchor-voters-p systate)
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate)
                (unequivocal-dags-p systate)
                (commit-possiblep val systate)
                (addressp val))
           (last-anchor-voters-p (commit-next val systate))))

Theorem: last-anchor-voters-p-of-event-next

(defthm last-anchor-voters-p-of-event-next
  (implies (and (last-anchor-voters-p systate)
                (system-committees-fault-tolerant-p systate)
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate)
                (no-self-endorsed-p systate)
                (signer-records-p systate)
                (signer-quorum-p systate)
                (unequivocal-signed-certs-p systate)
                (unequivocal-dags-p systate)
                (same-committees-p systate)
                (last-anchor-present-p systate)
                (event-possiblep event systate))
           (last-anchor-voters-p (event-next event systate))))