Certificate
Fixtype of certificates.
This is a product type introduced by fty::defprod.
Fields
- author — address
- round — posp
- transactions — transaction-list
- previous — address-set
- endorsers — address-set
We model a certificate as consisting of:
- The address of the validator who authored the certificate.
- The round number of the certificate.
- The transactions that the certificate is proposing
for inclusion in the blockchain.
- The addresses that, together with the previous round number,
identify the certificates from the previous round
that this certificate is based on.
(More on this below.)
- The addresses of the validators that endorsed this certificate,
by signing it in addition to the author.
A validator generates at most one certificate per round.
Thus, the combination of author and round number identifies
(at most) a unique certificate in a DAG.
This is a critical and non-trivial property,
which we prove as an invariant elsewhere.
A certificate is a vertex of the DAG.
The previous component of this fixtype models
the edges of the DAG, from this certificate to
the certificates in the previous round
with the authors specified by the set of addresses.
Because of the invariant mentioned above,
those certificates are uniquely determined.
Since we model the exchange of proposals and signatures
at a high level here,
we do not distinguish between proposals and certificates,
and instead model certificates
as containing the information that is relevant to our model.
We do not model cryptographic signatures explicitly.
The presence of the author and endorser addresses in a certificate
models the fact that they signed the certificate
(more precisely, the proposal that the certificate extends;
but again, we do not model proposals, only certificates).
Subtopics
- Certificatep
- Recognizer for certificate structures.
- Certificate-fix
- Fixing function for certificate structures.
- Make-certificate
- Basic constructor macro for certificate structures.
- Certificate-equiv
- Basic equivalence relation for certificate structures.
- Certificate->transactions
- Get the transactions field from a certificate.
- Change-certificate
- Modifying constructor for certificate structures.
- Certificate->round
- Get the round field from a certificate.
- Certificate->previous
- Get the previous field from a certificate.
- Certificate->endorsers
- Get the endorsers field from a certificate.
- Certificate->author
- Get the author field from a certificate.
