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.
This justifies the generic name validator-state for this fixtype,
as opposed to something like correct-validator-state.
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 later.
- A buffer of certificates that the validator has received
but has not been able to put into the DAG yet
because some of its causal history is missing.
Certificates move from the buffer to the DAG
once their causal history is in the DAG.
The buffer is modeled as a set,
since ordering does not matter,
given the way we formalize (later) certificate movement.
- 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,
but we need to model this aspect to enforce that
there will not be different certificates, in the system,
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 one
and the leftmost block is the newest one.
We leave the genesis block implicit:
the rightmost block in our list is actually
the block just after the genesis block.
This blockchain state component of the validator should be redundant,
calculable from the DAG state component
and from information about the committed rounds.
This is the case also because we do not model garbage collection.
However, it is more convenient to explicate the blockchain
in order to define the state transition system,
and then to prove its redundancy as an invariant,
since the proof may require a bit of work.
- 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 state component should be redundant,
calculable from other state components,
but for now we model it explicitly,
because that is closer to the implementation.
- 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
in system-state.
Invariants on validator states,
such as the aforementioned uniqueness of
author and round combinations in the DAG certificates,
as well as others like disjointness of DAG and buffer,
are formalized later.
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.
