Fault-tolerance
Fault tolerance.
In typical BFT systems, which have fixed sets of validators,
the notion of fault tolerance applies to the system as a whole,
based on the (fixed) number of correct and faulty validators:
the system is fault-tolerant if the actual number of faulty validators
does not exceed f, which is calculated from the total n,
as formalized in max-faulty-for-total
(applied to numbers of validators instead of stake).
With dynamic committees with stake, the notion applies to
every committee that arises during the execution of the protocol,
in terms of stake instead of numbers of validators.
It has to be an assumption on every such committee:
it cannot be checked by validators,
who do not know which validator is correct vs. faulty.
Here we formalize this notion for committees,
which is then used as a hypothesis for
certain correctness theorems of our formal development.
Subtopics
- Pick-correct-validator
- Pick a correct validator address, if present,
from a set of addresses.
- Committee-correct-members
- Addresses of the correct validators in a committee.
- Committee-faulty-members
- Addresses of the faulty validators in a committee.
- All-system-committees-fault-tolerant-p
- Check if all the system states
in an execution from a system state via a sequence of events
are fault-tolerant.
- Validator-committees-fault-tolerant-p
- Check if the active committees calculated by a validator
are all fault-tolerant.
- Committee-fault-tolerant-p
- Check if a committee is fault-tolerant.
- System-committees-fault-tolerant-p
- Check if a system state is fault-tolerant.
