|
|
|---|
|
|
|
|---|
Extend the blockchain with one or more anchors.
(extend-blockchain anchors dag blockchain committed-certs) → (mv new-blockchain new-committed-certs)
The list of anchors passed to this function is calculated via collect-anchors. Thus, it is ordered from newest (left) to oldest (right), and so we extend the blockchain from right to left, by cdring down the list of anchors and processing the cdr before the car. This function also takes and returns the set of all the committed certificates, since we need to exclude, from the causal history of each anchor, the certificates that have already been committed.
When we reach the end of the list of anchors, we return the blockchain and committed certificates unchanged. Otherwise, we first extend them with the anchors in the cdr. Then we take the anchor at the car, we calculate its causal history, and we subtract the already committed certificates: the result is the set of certificate to commit in this block. So we collect all the transactions from the certificates, we form a block, and we add it to the blockchain. The round of the block is the one of the anchor. We also update the set of committed certificates, and return it along with the blockchain.
We show that if the initial blockchain has
strictly increasing rounds (right to left),
and the anchors have even, strictly increasing rounds (right to left),
and the newest block of the original blockchain
has a round below the last anchor in the list
(unless the original blockchain is empty),
then the new blockchain has strictly increasing rounds as well.
This theorem expresses an important property,
which serves to show the preservation of
the invariant that blockchains always have strictly increasing rounds.
Note that the hypothesis about
the car of last having round above
the newest block of the original blockchain
matches a property we proved of collect-anchors,
i.e.
Function:
(defun extend-blockchain (anchors dag blockchain committed-certs) (declare (xargs :guard (and (certificate-listp anchors) (certificate-setp dag) (block-listp blockchain) (certificate-setp committed-certs)))) (declare (xargs :guard (cert-list-evenp anchors))) (let ((__function__ 'extend-blockchain)) (declare (ignorable __function__)) (b* (((when (endp anchors)) (mv (block-list-fix blockchain) (certificate-set-fix committed-certs))) ((mv blockchain committed-certs) (extend-blockchain (cdr anchors) dag blockchain committed-certs)) (anchor (car anchors)) (hist-certs (cert-causal-history anchor dag)) (certs-to-commit (difference hist-certs committed-certs)) (transs (transactions-from-certificates certs-to-commit)) (block (make-block :transactions transs :round (certificate->round anchor))) (blockchain (cons block blockchain)) (committed-certs (union committed-certs certs-to-commit))) (mv blockchain committed-certs))))
Theorem:
(defthm block-listp-of-extend-blockchain.new-blockchain (b* (((mv ?new-blockchain ?new-committed-certs) (extend-blockchain anchors dag blockchain committed-certs))) (block-listp new-blockchain)) :rule-classes :rewrite)
Theorem:
(defthm certificate-setp-of-extend-blockchain.new-committed-certs (b* (((mv ?new-blockchain ?new-committed-certs) (extend-blockchain anchors dag blockchain committed-certs))) (certificate-setp new-committed-certs)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-extend-blockchain (b* (((mv ?new-blockchain ?new-committed-certs) (extend-blockchain anchors dag blockchain committed-certs))) (equal (consp new-blockchain) (or (consp blockchain) (consp anchors)))))
Theorem:
(defthm extend-blockchain-as-append (b* (((mv new-blockchain &) (extend-blockchain anchors dag blockchain committed-certs))) (equal new-blockchain (append (take (- (len new-blockchain) (len blockchain)) new-blockchain) (block-list-fix blockchain)))))
Theorem:
(defthm blocks-last-round-of-extend-blockchain (implies (and (consp anchors) (cert-list-evenp anchors)) (b* (((mv ?new-blockchain ?new-committed-certs) (extend-blockchain anchors dag blockchain committed-certs))) (equal (blocks-last-round new-blockchain) (certificate->round (car anchors))))))
Theorem:
(defthm blocks-orderedp-of-extend-blockchain (implies (and (cert-list-orderedp anchors) (cert-list-evenp anchors) (blocks-orderedp blockchain) (> (certificate->round (car (last anchors))) (blocks-last-round blockchain))) (b* (((mv ?new-blockchain ?new-committed-certs) (extend-blockchain anchors dag blockchain committed-certs))) (blocks-orderedp new-blockchain))))
Theorem:
(defthm active-committee-at-round-of-extend-blockchain-no-change (b* (((mv new-blockchain &) (extend-blockchain anchors dag blockchain committed-certs))) (implies (and (block-listp blockchain) (blocks-orderedp new-blockchain) (active-committee-at-round round blockchain)) (equal (active-committee-at-round round new-blockchain) (active-committee-at-round round blockchain)))))
Theorem:
(defthm extend-blockchain-of-certificate-list-fix-anchors (equal (extend-blockchain (certificate-list-fix anchors) dag blockchain committed-certs) (extend-blockchain anchors dag blockchain committed-certs)))
Theorem:
(defthm extend-blockchain-certificate-list-equiv-congruence-on-anchors (implies (certificate-list-equiv anchors anchors-equiv) (equal (extend-blockchain anchors dag blockchain committed-certs) (extend-blockchain anchors-equiv dag blockchain committed-certs))) :rule-classes :congruence)
Theorem:
(defthm extend-blockchain-of-certificate-set-fix-dag (equal (extend-blockchain anchors (certificate-set-fix dag) blockchain committed-certs) (extend-blockchain anchors dag blockchain committed-certs)))
Theorem:
(defthm extend-blockchain-certificate-set-equiv-congruence-on-dag (implies (certificate-set-equiv dag dag-equiv) (equal (extend-blockchain anchors dag blockchain committed-certs) (extend-blockchain anchors dag-equiv blockchain committed-certs))) :rule-classes :congruence)
Theorem:
(defthm extend-blockchain-of-block-list-fix-blockchain (equal (extend-blockchain anchors dag (block-list-fix blockchain) committed-certs) (extend-blockchain anchors dag blockchain committed-certs)))
Theorem:
(defthm extend-blockchain-block-list-equiv-congruence-on-blockchain (implies (block-list-equiv blockchain blockchain-equiv) (equal (extend-blockchain anchors dag blockchain committed-certs) (extend-blockchain anchors dag blockchain-equiv committed-certs))) :rule-classes :congruence)
Theorem:
(defthm extend-blockchain-of-certificate-set-fix-committed-certs (equal (extend-blockchain anchors dag blockchain (certificate-set-fix committed-certs)) (extend-blockchain anchors dag blockchain committed-certs)))
Theorem:
(defthm extend-blockchain-certificate-set-equiv-congruence-on-committed-certs (implies (certificate-set-equiv committed-certs committed-certs-equiv) (equal (extend-blockchain anchors dag blockchain committed-certs) (extend-blockchain anchors dag blockchain committed-certs-equiv))) :rule-classes :congruence)