		Search-engine friendly clone of the ACL2 documentation.

Nonforking-blockchains-next

Nonforking-blockchains-p-of-next

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

The only event that may modify blockchains is commit. To prove that blockchains in the new state do not fork, we do not need to assume that in the old state: it suffices to assume the non-forking of anchors in the old state, along with a number of other invariants, and then we use the already proved preservation of that and other invariants to show the non-forking of blockchains in the new state. First we prove a theorem, lists-noforkp-of-calculate-blockchain-when-anchors, that lifts the non-forking of two anchor sequences to the non-forking of two blockchains calculated from the anchors from two DAGs. In lists-noforkp-of-blockchain-of-commit-next, which provides most of the desired proof, we instantiate lists-noforkp-of-calculate-blockchain-when-anchors with the committed anchors in the new state, and the DAGs in the new state, which are the same as in the old state (commit does not change any DAGs). We need to use the redundancy of the blockchains invariant to rephrase the blockchains in terms of calculate-blockchain, so that lists-noforkp-of-calculate-blockchain-when-anchors applies. The main theorem nonforking-blockchains-p-of-commit-next is then proved easily from lists-noforkp-of-blockchain-of-commit-next.

The other kinds of events do not modify the blockchain, and thus the preservation of non-forking is easy to prove.

Definitions and Theorems

Theorem: nonforking-blockchains-p-of-create-next

(defthm nonforking-blockchains-p-of-create-next
  (implies (and (nonforking-blockchains-p systate)
                (create-possiblep cert systate))
           (nonforking-blockchains-p (create-next cert systate))))

Theorem: nonforking-blockchains-p-of-accept-next

(defthm nonforking-blockchains-p-of-accept-next
  (implies (and (nonforking-blockchains-p systate)
                (accept-possiblep msg systate))
           (nonforking-blockchains-p (accept-next msg systate))))

Theorem: nonforking-blockchains-p-of-advance-next

(defthm nonforking-blockchains-p-of-advance-next
  (implies (and (nonforking-blockchains-p systate)
                (advance-possiblep val systate))
           (nonforking-blockchains-p (advance-next val systate))))

Theorem: lists-noforkp-of-calculate-blockchain-when-anchors

(defthm lists-noforkp-of-calculate-blockchain-when-anchors
  (implies (and (lists-noforkp anchors1 anchors2)
                (certificate-setp dag1)
                (certificate-setp dag2)
                (certificate-sets-unequivocalp dag1 dag2)
                (certificate-set-unequivocalp dag1)
                (certificate-set-unequivocalp dag2)
                (dag-closedp dag1)
                (dag-closedp dag2)
                (certificates-dag-paths-p anchors1 dag1)
                (certificates-dag-paths-p anchors2 dag2))
           (lists-noforkp (calculate-blockchain anchors1 dag1)
                          (calculate-blockchain anchors2 dag2))))

Theorem: lists-noforkp-of-blockchain-of-commit-next

(defthm lists-noforkp-of-blockchain-of-commit-next
 (implies
  (and (backward-closed-p systate)
       (last-blockchain-round-p systate)
       (ordered-blockchain-p systate)
       (signer-quorum-p systate)
       (unequivocal-dags-p systate)
       (same-committees-p systate)
       (signer-quorum-p systate)
       (dag-previous-quorum-p systate)
       (last-anchor-present-p systate)
       (omni-paths-p systate)
       (nonforking-anchors-p systate)
       (committed-redundant-p systate)
       (blockchain-redundant-p systate)
       (commit-possiblep val systate)
       (addressp val)
       (in val1 (correct-addresses systate))
       (in val2 (correct-addresses systate)))
  (lists-noforkp
       (validator-state->blockchain
            (get-validator-state val1 (commit-next val systate)))
       (validator-state->blockchain
            (get-validator-state val2 (commit-next val systate))))))

Theorem: nonforking-blockchains-p-of-commit-next

(defthm nonforking-blockchains-p-of-commit-next
  (implies (and (backward-closed-p systate)
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate)
                (signer-quorum-p systate)
                (unequivocal-dags-p systate)
                (same-committees-p systate)
                (signer-quorum-p systate)
                (dag-previous-quorum-p systate)
                (last-anchor-present-p systate)
                (omni-paths-p systate)
                (nonforking-anchors-p systate)
                (committed-redundant-p systate)
                (blockchain-redundant-p systate)
                (commit-possiblep val systate)
                (addressp val))
           (nonforking-blockchains-p (commit-next val systate))))

Theorem: nonforking-blockchains-p-of-event-next

(defthm nonforking-blockchains-p-of-event-next
  (implies (and (nonforking-blockchains-p systate)
                (backward-closed-p systate)
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate)
                (unequivocal-dags-p systate)
                (same-committees-p systate)
                (signer-quorum-p systate)
                (dag-previous-quorum-p systate)
                (last-anchor-present-p systate)
                (omni-paths-p systate)
                (nonforking-anchors-p systate)
                (committed-redundant-p systate)
                (blockchain-redundant-p systate)
                (event-possiblep event systate))
           (nonforking-blockchains-p (event-next event systate))))