		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, which we need to filter out, 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 even, strictly increasing (right to left) rounds, and the anchors have even, strictly increasing (right to left) rounds, 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 even, strictly increasing rounds. The theorem assumes that the list of anchors is not empty, which is always the case when this function is called. This is an important property, which serves to show the preservation of the invariant that blockchains always have even, 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, as also mentioned there.

We show that extending the blockchain does not change the active committee at a round, if that committee can be calculated in the original blockchain. As a consequence, collecting anchors is not affected by the extension of the blockchain, as proved for collect-anchors and collect-all-anchors.

We show that if a blockchain is extended using anchors that are all in the DAG and connected by paths (i.e. satisfying certificates-dag-paths-p, the set of all new committed certificates is the union of the old ones with the causal history of the latest anchor. Based on just the definition of extend-blockchain, we should take the union of the causal histories of all the anchors, but since they are all connected by paths, the causal history of the latest anchor (the car) includes the causal history of all the other anchors, and therefore the final set of committed certificates is the union of that latest causal history with the previous committed certificates. But this theorem also covers the case of an empty list of anchors, in which case there is no change in the set of committed certificates.

The extension of a blockchain with some anchors in a backward-closed subset of an unequivocal DAG is the same in the superset. This is because causal histories satisfy a similar property.

The extensions of a blockchain with some anchors in two backward-closed, individualy and mutually unequivocal DAGs are the same in the two DAGs. This is because causal histories satisfy a similar property.

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))))
  (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 (certificate-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: len-of-extend-blockchain

(defthm len-of-extend-blockchain
  (b* (((mv ?new-blockchain ?new-committed-certs)
        (extend-blockchain anchors
                           dag blockchain committed-certs)))
    (equal (len new-blockchain)
           (+ (len blockchain) (len anchors)))))

Theorem: extend-blockchain-of-nil

(defthm extend-blockchain-of-nil
  (equal (extend-blockchain nil dag blockchain committed-certs)
         (mv (block-list-fix blockchain)
             (certificate-set-fix committed-certs))))

Theorem: extend-blockchain-of-append

(defthm extend-blockchain-of-append
  (b* (((mv blocks comms)
        (extend-blockchain (append anchors2 anchors1)
                           dag blocks0 comms0))
       ((mv blocks1 comms1)
        (extend-blockchain anchors1 dag blocks0 comms0))
       ((mv blocks2 comms2)
        (extend-blockchain anchors2 dag blocks1 comms1)))
    (and (equal blocks blocks2)
         (equal comms comms2))))

Theorem: consp-of-extend-blockchain

(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: extend-blockchain-as-append

(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: nthcdr-of-extend-blockchain

(defthm nthcdr-of-extend-blockchain
 (implies
  (<= n (len anchors))
  (equal
      (nthcdr n
              (mv-nth 0
                      (extend-blockchain anchors dag blocks comms)))
      (mv-nth 0
              (extend-blockchain (nthcdr n anchors)
                                 dag blocks comms)))))

Theorem: blocks-last-round-of-extend-blockchain

(defthm blocks-last-round-of-extend-blockchain
 (implies (consp 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: blocks-ordered-even-p-of-extend-blockchain

(defthm blocks-ordered-even-p-of-extend-blockchain
 (implies (and (certificates-ordered-even-p anchors)
               (blocks-ordered-even-p blockchain)
               (consp anchors)
               (> (certificate->round (car (last anchors)))
                  (blocks-last-round blockchain)))
          (b* (((mv ?new-blockchain ?new-committed-certs)
                (extend-blockchain anchors
                                   dag blockchain committed-certs)))
            (blocks-ordered-even-p new-blockchain))))

Theorem: active-committee-at-round-of-extend-blockchain-no-change

(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-ordered-even-p new-blockchain)
         (active-committee-at-round round blockchain all-vals))
    (equal (active-committee-at-round round new-blockchain all-vals)
           (active-committee-at-round round blockchain all-vals)))))

Theorem: collect-anchors-of-extend-blockchain-no-change

(defthm collect-anchors-of-extend-blockchain-no-change
  (b* (((mv new-blockchain &)
        (extend-blockchain anchors
                           dag blockchain committed-certs)))
    (implies
         (and (block-listp blockchain)
              (blocks-ordered-even-p new-blockchain)
              (or (zp previous-round)
                  (active-committee-at-round
                       previous-round blockchain all-vals)))
         (equal (collect-anchors current-anchor
                                 previous-round last-committed-round
                                 dag new-blockchain all-vals)
                (collect-anchors current-anchor
                                 previous-round last-committed-round
                                 dag blockchain all-vals)))))

Theorem: collect-all-anchors-of-extend-blockchain-no-change

(defthm collect-all-anchors-of-extend-blockchain-no-change
 (b* (((mv new-blockchain &)
       (extend-blockchain anchors
                          dag blockchain committed-certs)))
  (implies
   (and (block-listp blockchain)
        (blocks-ordered-even-p new-blockchain)
        (active-committee-at-round (certificate->round last-anchor)
                                   blockchain all-vals))
   (equal
       (collect-all-anchors last-anchor dag new-blockchain all-vals)
       (collect-all-anchors last-anchor dag blockchain all-vals)))))

Theorem: new-committed-certs-of-extend-blockchain

(defthm new-committed-certs-of-extend-blockchain
  (implies
       (and (certificate-setp dag)
            (certificate-set-unequivocalp dag)
            (certificates-dag-paths-p anchors dag)
            (certificate-setp committed-certs))
       (b* (((mv & new-committed-certs)
             (extend-blockchain anchors
                                dag blockchain committed-certs)))
         (equal new-committed-certs
                (if (consp anchors)
                    (union (certificate-causal-history (car anchors)
                                                       dag)
                           committed-certs)
                  committed-certs)))))

Theorem: extend-blockchain-of-unequivocal-superdag

(defthm extend-blockchain-of-unequivocal-superdag
 (implies
   (and (certificate-setp dag0)
        (certificate-setp dag)
        (subset dag0 dag)
        (certificate-set-unequivocalp dag)
        (dag-closedp dag0)
        (set::list-in anchors dag0))
   (equal (extend-blockchain anchors dag blockchain committed-certs)
          (extend-blockchain anchors
                             dag0 blockchain committed-certs))))

Theorem: extend-blockchain-of-unequivocal-dags

(defthm extend-blockchain-of-unequivocal-dags
 (implies
  (and (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)
       (set::list-in anchors dag1)
       (set::list-in anchors dag2))
  (equal (extend-blockchain anchors dag1 blockchain committed-certs)
         (extend-blockchain anchors
                            dag2 blockchain committed-certs))))