		Search-engine friendly clone of the ACL2 documentation.

Correctness

Blockchain-redundant-def-and-init-and-next

Invariant that the blockchain is redundant: definition, establishment, and preservation.

The state of each validator includes (their view of) the blockchain. This is initially empty, and gets extended, one or more blocks at a time, when anchors are committed. However, because of the stability properties of paths in the DAG, causal histories, etc., the full blockchain can always be recalculated from scratch, from the sequence of committed anchors and from the DAG. In other words, the blockchain state component is redundant.

Here we define the invariant, we prove that it holds in all initial states, and we prove that it is preserved by all transitions. Elsewhere we prove that the invariant holds in every reachable state.

Subtopics

Blockchain-redundant-p-of-next: Preservation of the invariant: if the invariant holds in a system state, it also holds in the next system state.
Validator-blockchain-redundant-p: Check if the blockchain of a validator is equal to its calculation from the committed anchors and DAG.
Blockchain-redundant-p: Definition of the invariant: the blockchain of each validator is redundant, equal to its calculation from the committed anchors and DAG.
Blockchain-redundant-p-when-init: Establishment of the invariant: the invariant holds in any initial state.