Invariant-blockchain-redundant
Invariant that the blockchain is redundant.
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.
It still seems convenient to include that state component
in the definition of (correct) validator states,
so that the definition of the state transitions is more natural,
closer to how the protocol actually works.
But we prove this redundancy as an invariant of the protocol.
Subtopics
- System-blockchain-redundantp-of-commit-anchors-next
- Preservation of the invariant by commit-anchors events.
- System-blockchain-redundantp-of-events-next
- Preservation of the invariant by every sequence of events.
- System-blockchain-redundantp-of-create-certificate-next
- Preservation of the invariant by create-certificate events.
- System-blockchain-redundantp-of-store-certificate-next
- Preservation of the invariant by store-certificate events.
- Validator-blockchain-redundantp
- Check if the blockchain of a validator
is equal to its calculation from the committed anchors and DAG.
- System-blockchain-redundantp-of-receive-certificate-next
- Preservation of the invariant by receive-certificate events.
- System-blockchain-redundantp-when-reachable
- The invariant holds in every reachable state.
- System-blockchain-redundantp-of-timer-expires-next
- Preservation of the invariant by timer-expires events.
- System-blockchain-redundantp-of-advance-round-next
- Preservation of the invariant by advance-round events.
- System-blockchain-redundantp-of-event-next
- Preservation of the invariant by all the events.
- System-blockchain-redundantp
- Definition of the invariant:
the blockchain of a validator is redundant,
equal to its calculation from the committed anchors and DAG.
- System-blockchain-redundantp-when-system-state-initp
- Establishment of the invariant:
the invariant holds on any initial state.
