		Search-engine friendly clone of the ACL2 documentation.

Correctness

Properties-blockchain

Some properties of the operations on blockchains.

Some of these come in two forms, analogous to properties proved elsewhere: one form about the consistency of the growing DAG of a single validator, and one form about the consistency across DAGs of different validators.

Subtopics

New-committed-certs-of-extend-blockchain: If a blockchain is extended by anchors that are all in the DAG and connected by paths, the set of all new committed certificates is the union of the old ones with the causal history of the latest anchor.
Extend-blockchain-of-unequivocal-dags: The extensions of a blockchain with some anchors in two backward-closed unequivocal and mutually unequivocal DAGs are the same in the two DAGs.
Calculate-blockchain-of-unequivocal-dags: The blockchains calculated from a sequence of anchors in two backward-closed unequivocal and mutually unequivocal DAGs are the same in the two DAGs.
Calculate-blockchain-of-unequivocal-dag-superset: The blockchain calculated from a sequence of anchors in a backward-closed subset of an unequivocal DAG is the same in the superset.
Extend-blockchain-of-unequivocal-dag-superset: The extension of a blockchain with some anchors in a backward-closed subset of an unequivocal DAG is the same in the superset.
Certificate-list-pathp-of-collect-anchors: The anchors returned by collect-anchors are all in the DAG and are all connected by paths.
Certificate-list-pathp-of-committed-anchors: The anchors returned by committed-anchors are all in the DAG and are all connected by paths.
Certificate-list-pathp-of-collect-all-anchors: The anchors returned by collect-all-anchors are all in the DAG and are all connected by paths.