		Search-engine friendly clone of the ACL2 documentation.

Last-anchor-present

Last-anchor-present-p-of-next

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

For each kind of event, we first prove a theorem (or two in the case of commit) about the preservation of last-anchor being not nil, which we use in the proof of the main theorem for each event.

The definition of last-anchor depends on the DAG, blockchain, and last committed round of a validator. The proofs are based on how the events modify (or not) these components.

A create event modifies the DAG of the author but not its blockchain or last committed round. However, in general the extension of a set of certificates preserves the fact that cert-with-author+round is not nil (see cert-with-author+round-of-insert-iff), although technically it may not return the same certificate, unless one assumes unequivocation (which is not needed here). For validators different from the author, there is no change to the DAG or last committed round.

An accept event modifies the DAG of the target validator but not its blockchain or last committed round. However, similarly to the create case, the extension of the DAG preserves the fact that cert-with-author+round is not nil.

A commit event modifies the blockchain and last committed round of the target validator, but not its DAG. The event is conditioned by commit-possiblep, which requires the presence in the DAG of the certificate that becomes the new last anchor. But we need to show that the extension of the blockchain does not affect the choice of the leader for that round, so we use active-committee-at-round-of-extend-blockchain-no-change and additional rules to discharge its hypotheses, similarly to other invariant preservation proofs that involve calculations of committees. This needs the already proved invariants that blocks have ordered even rounds and that the last committed block is the one of the latest block. Our theorem for this case of commit is last-anchor-not-nil-of-commit-next-same, while last-anchor-not-nil-of-commit-next-diff takes care of the case of a validator that is not the event's target, whose DAG, blockchain, and last committed round do not change.

An advance event does not change any DAG or blockchain or last committed round, so the preservation of the invariant is easy to prove.

Definitions and Theorems

Theorem: last-anchor-not-nil-of-create-next

(defthm last-anchor-not-nil-of-create-next
  (implies
       (and (in val (correct-addresses systate))
            (last-anchor (get-validator-state val systate)))
       (last-anchor
            (get-validator-state val (create-next cert systate)))))

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

(defthm last-anchor-present-p-of-create-next
  (implies (last-anchor-present-p systate)
           (last-anchor-present-p (create-next cert systate))))

Theorem: last-anchor-not-nil-of-accept-next

(defthm last-anchor-not-nil-of-accept-next
  (implies
       (and (in val (correct-addresses systate))
            (last-anchor (get-validator-state val systate))
            (accept-possiblep msg systate))
       (last-anchor
            (get-validator-state val (accept-next msg systate)))))

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

(defthm last-anchor-present-p-of-accept-next
  (implies (and (last-anchor-present-p systate)
                (accept-possiblep msg systate))
           (last-anchor-present-p (accept-next msg systate))))

Theorem: last-anchor-not-nil-of-advance-next

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

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

(defthm last-anchor-present-p-of-advance-next
  (implies (and (last-anchor-present-p systate)
                (advance-possiblep msg systate))
           (last-anchor-present-p (advance-next msg systate))))

Theorem: last-anchor-not-nil-of-commit-next-diff

(defthm last-anchor-not-nil-of-commit-next-diff
  (implies
       (and (in val1 (correct-addresses systate))
            (not (equal (address-fix val1)
                        (address-fix val)))
            (commit-possiblep val systate)
            (last-anchor (get-validator-state val1 systate)))
       (last-anchor
            (get-validator-state val1 (commit-next val systate)))))

Theorem: last-anchor-not-nil-of-commit-next-same

(defthm last-anchor-not-nil-of-commit-next-same
  (implies
       (and (last-blockchain-round-p systate)
            (ordered-blockchain-p systate)
            (commit-possiblep val systate)
            (addressp val))
       (last-anchor
            (get-validator-state val (commit-next val systate)))))

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

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

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

(defthm last-anchor-present-p-of-event-next
  (implies (and (last-blockchain-round-p systate)
                (ordered-blockchain-p systate)
                (last-anchor-present-p systate)
                (event-possiblep event systate))
           (last-anchor-present-p (event-next event systate))))