Validator-state
Fixtype of states of a (correct) validator.
This is a product type introduced by fty::defprod.
Fields
- round — posp
- dag — certificate-set
- proposed — proposal-address-set-map
- endorsed — proposal-set
- last — natp
- blockchain — block-list
- committed — certificate-set
As explained in validator-states,
faulty validators are modeled with no internal state.
So this fixtype only models the state of correct validators.
We model the state of a correct validator as consisting of:
- The current round number that the validator is at.
- The DAG of certificates, modeled as a set.
Invariants about the uniqueness of author and round combinations
are stated and proved elsewhere.
- A finite map from each proposal created by the validator
to the set of addresses of validators who have endorsed the proposal.
When the validator has enough endorsements for a proposal,
it creates a certificate out of the proposal and its endorsements,
and adds that certificate to its DAG.
- A set of endorsed proposals.
These are proposals received from other validators,
which the validator has endorsed by sending a signature.
The validator needs to keep track of these signed proposals
to avoid endorsing two equivocal proposals,
i.e. two different proposals with the same author and round.
After endorsing a proposal,
it may take time for the validator to receive
the full certificate with that proposal,
if it receives it at all;
so it is necessary to keep track of endorsed proposals.
- The number of the last round at which
the validator has committed an anchor,
or 0 if no anchor has been committe yet.
- The blockchain as seen by the validator.
We model it as a list of blocks from right to left,
i.e. the rightmost block is the oldest/earliest one
and the leftmost block is the newest/latest one.
We leave the genesis block implicit:
the rightmost block in our list is actually
the block just after the genesis block.
The blockchain is actually calculable from other state components,
as proved elsewhere.
However, the reasons (i.e. proof) of this redundancy are somewhat complex,
and thus it is better to include the blockchain in the validator state,
so that the state transitions can be defined in a more natural way.
- The set of all the certificates that have been committed so far,
i.e. whose transactions have been included in the blockchain.
These include not just the anchors,
but also the certificates reachable from the anchors via the DAG edges.
This state component serves to calculate the new certificates
to be committed the next time anchors are committed,
by computing the full causal history of each anchor
but removing the already committed certificates.
This state component actually calculable from other state components,
as proved elsewhere.
However, for the same reason explained above for the blockchain component,
it is best to leave this component in the state,
for a more natural definition of the state transitions.
The address of the validator, which never changes,
is captured outside this fixtype,
in the map from validator addresses to validator states
that is in the system state.
There are many invariants on validator states,
such as the ones mentioned above.
These are stated and proved elsewhere.
Validators in AleoBFT include more information than modeled here,
but this model is sufficient for our current purposes.
Subtopics
- Validator-state-fix
- Fixing function for validator-state structures.
- Make-validator-state
- Basic constructor macro for validator-state structures.
- Validator-state-equiv
- Basic equivalence relation for validator-state structures.
- Validator-statep
- Recognizer for validator-state structures.
- Validator-state->proposed
- Get the proposed field from a validator-state.
- Validator-state->committed
- Get the committed field from a validator-state.
- Validator-state->endorsed
- Get the endorsed field from a validator-state.
- Validator-state->blockchain
- Get the blockchain field from a validator-state.
- Change-validator-state
- Modifying constructor for validator-state structures.
- Validator-state->round
- Get the round field from a validator-state.
- Validator-state->last
- Get the last field from a validator-state.
- Validator-state->dag
- Get the dag field from a validator-state.
