		Search-engine friendly clone of the ACL2 documentation.

Blockchains

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's causal history (which includes the anchor itself), 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.

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)