		Search-engine friendly clone of the ACL2 documentation.

Blockchains

Extend-blockchain

Extend the blockchain with one or more anchors.

Signature
(extend-blockchain anchors dag blockchain committed-certs) → (mv new-blockchain new-committed-certs)
Arguments: anchors — Guard (certificate-listp anchors).; dag — Guard (certificate-setp dag).; blockchain — Guard (block-listp blockchain).; committed-certs — Guard (certificate-setp committed-certs).
Returns: new-blockchain — Type (block-listp new-blockchain).; new-committed-certs — Type (certificate-setp 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.

Definitions and Theorems

Function: extend-blockchain

(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: block-listp-of-extend-blockchain.new-blockchain

(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: certificate-setp-of-extend-blockchain.new-committed-certs

(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: extend-blockchain-of-certificate-list-fix-anchors

(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: extend-blockchain-certificate-list-equiv-congruence-on-anchors

(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: extend-blockchain-of-certificate-set-fix-dag

(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: extend-blockchain-certificate-set-equiv-congruence-on-dag

(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: extend-blockchain-of-block-list-fix-blockchain

(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: extend-blockchain-block-list-equiv-congruence-on-blockchain

(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: extend-blockchain-of-certificate-set-fix-committed-certs

(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: extend-blockchain-certificate-set-equiv-congruence-on-committed-certs

(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)