		Search-engine friendly clone of the ACL2 documentation.

Operations-blockchain

Transactions-from-certificates

Collect all the transactions from a set of certficates.

Signature
(transactions-from-certificates certs) → transs
Arguments: certs — Guard (certificate-setp certs).
Returns: transs — Type (transaction-listp transs).

When an anchor is committed, a new block is added to the blockchain, containing all the transactions from the anchor and from its preceding certificates (in the sense that there are DAG paths from the anchor to them), except for the certificates whose transactions have already been added to the blockchain. After computing the set of certificates whose transactions must be included in a block, we call this function to put all those transactions together. We put them together according to the ACL2 total order on certificates; the exact order does not matter, so long as all validators use the same order. The Bullshark paper postulates a consistent but unspecified order.

Definitions and Theorems

Function: transactions-from-certificates

(defun transactions-from-certificates (certs)
 (declare (xargs :guard (certificate-setp certs)))
 (let ((__function__ 'transactions-from-certificates))
  (declare (ignorable __function__))
  (cond
       ((emptyp certs) nil)
       (t (append (certificate->transactions (head certs))
                  (transactions-from-certificates (tail certs)))))))

Theorem: transaction-listp-of-transactions-from-certificates

(defthm transaction-listp-of-transactions-from-certificates
  (b* ((transs (transactions-from-certificates certs)))
    (transaction-listp transs))
  :rule-classes :rewrite)