		Search-engine friendly clone of the ACL2 documentation.

Operations-blockchain

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