Validator-state
Fixtype of states of a (correct) validator.
This is a product type introduced by fty::defprod.
Fields
- round — posp
- dag — certificate-set
- buffer — certificate-set
- endorsed — address+pos-set
- last — natp
- blockchain — block-list
- committed — certificate-set
- timer — timer
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 buffer of certificates that the validator has received
but has not been able to put into the DAG yet
because some of its predecessor certificates
(identified by the previous certificate component)
are not in the DAG yet.
Certificates move from the buffer to the DAG
once their predecessors are in the DAG.
This is in fact an important invariant, stated and proved elsewhere.
The buffer is modeled as a set,
since ordering does not matter,
given the way we formalize certificate movement
as non-deterministic choice.
- A set of pairs, each consisting of an address and a positive integer,
which represents the author-round combinations
for which the validator has endorsed proposals by signing them.
When a (correct) validator receives a (valid) proposal,
not only it signs the proposal and sends the signature back to the sender,
but also it keeps track of which proposals it has signed
to avoid signing different proposals
for the same combination of author and round
(such different proposals would come from a faulty validator):
this is a critical property to guarantee non-equivocation.
Here we model the exchange of proposals and signatures
at a more abstract level, not explicitly,
but we still need to model this aspect to enforce that
there will not be equivocal certificates,
with the same combination of author and round number.
The use of this component of the state of a correct validator
is explained in the definition of
which events are possible and which new states they lead to.
- The number of the last round at which
this validator has committed an anchor.
- 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 nodes 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
but removing the already committed certificates.
This is actually calculable from other state components,
as proved elsewhere.
However, for the same reason outlined 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 state of the timer; see timer.
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.
Subtopics
- Validator-state-fix
- Fixing function for validator-state structures.
- Validator-statep
- Recognizer 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-state->committed
- Get the committed field from a validator-state.
- Change-validator-state
- Modifying constructor for validator-state structures.
- Validator-state->endorsed
- Get the endorsed field from a validator-state.
- Validator-state->buffer
- Get the buffer field from a validator-state.
- Validator-state->blockchain
- Get the blockchain field from a validator-state.
- Validator-state->timer
- Get the timer field from a validator-state.
- 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.
