		Search-engine friendly clone of the ACL2 documentation.

Ordered-blockchain

Ordered-blockchain-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 kind of event that modifies the blockchain is commit. All the other events leave the blockchain unchanged, and it is thus easy to prove that they preserve the invariant.

For commit event, we need to assume a previously proved invariant, namely last-blockchain-round. We use previously proved theorems about extend-blockchain and collect-anchors. We also need to open up commit-possiblep, to expose certain needed constraints on the involved round numbers. The last-blockchain-round-p assumption serves to tie the last committed round in the validator state to the round of the newest block of the blockchain prior to the addition of the new blocks, to complete the relieving of the hypotheses of the aforementioned theorems about extend-blockchain and collect-anchors.

Definitions and Theorems

Theorem: ordered-blockchain-p-of-create-next

(defthm ordered-blockchain-p-of-create-next
  (implies (ordered-blockchain-p systate)
           (ordered-blockchain-p (create-next cert systate))))

Theorem: ordered-blockchain-p-of-accept-next

(defthm ordered-blockchain-p-of-accept-next
  (implies (and (ordered-blockchain-p systate)
                (accept-possiblep msg systate))
           (ordered-blockchain-p (accept-next msg systate))))

Theorem: ordered-blockchain-p-of-advance-next

(defthm ordered-blockchain-p-of-advance-next
  (implies (and (ordered-blockchain-p systate)
                (advance-possiblep val systate))
           (ordered-blockchain-p (advance-next val systate))))

Theorem: ordered-blockchain-p-of-commit-next

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

Theorem: ordered-blockchain-p-of-event-next

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