		Search-engine friendly clone of the ACL2 documentation.

Blockchains

Calculate-blockchain

Calculate a blockchain from a sequence of anchors and a DAG.

Signature
(calculate-blockchain anchors dag) → blockchain
Arguments: anchors — Guard (certificate-listp anchors).; dag — Guard (certificate-setp dag).
Returns: blockchain — Type (block-listp blockchain).

We call extend-blockchain starting with the empty blockchain and no committed certificates. We only returns the blockchain, discarding the committed certificate set.

The blockchain calculated from a sequence of anchors in a backward-closed subset of an unequivocal DAG is the same in the superset. This is based on the analogous property of extend-blockchain.

The blockchains calculated from a sequence of anchors in two backward-closed, individually and mutually unequivocal DAGs are the same in the two DAGs. This is based on the analogous property of extend-blockchain.

Definitions and Theorems

Function: calculate-blockchain

(defun calculate-blockchain (anchors dag)
  (declare (xargs :guard (and (certificate-listp anchors)
                              (certificate-setp dag))))
  (let ((__function__ 'calculate-blockchain))
    (declare (ignorable __function__))
    (b* (((mv blockchain &)
          (extend-blockchain anchors dag nil nil)))
      blockchain)))

Theorem: block-listp-of-calculate-blockchain

(defthm block-listp-of-calculate-blockchain
  (b* ((blockchain (calculate-blockchain anchors dag)))
    (block-listp blockchain))
  :rule-classes :rewrite)

Theorem: len-of-calculate-blockchain

(defthm len-of-calculate-blockchain
  (b* ((?blockchain (calculate-blockchain anchors dag)))
    (equal (len blockchain) (len anchors))))

Theorem: calculate-blockchain-of-nil

(defthm calculate-blockchain-of-nil
  (equal (calculate-blockchain nil dag)
         nil))

Theorem: nthcdr-of-calculate-blockchain

(defthm nthcdr-of-calculate-blockchain
  (implies (<= n (len anchors))
           (equal (nthcdr n (calculate-blockchain anchors dag))
                  (calculate-blockchain (nthcdr n anchors)
                                        dag))))

Theorem: calculate-blockchain-of-unequivocal-superdag

(defthm calculate-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 (calculate-blockchain anchors dag)
                  (calculate-blockchain anchors dag0))))

Theorem: calculate-blockchain-of-unequivocal-dags

(defthm calculate-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 (calculate-blockchain anchors dag1)
                  (calculate-blockchain anchors dag2))))