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.
- The addresses of the validators that endorsed this certificate,
by signing it in addition to the author.
We do not model the signing process here,
but having a record of the signers (author and endorsers) serves
to define the behavior and invariants of the model.
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.
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.
Since we model the exchange of proposals and signatures
at a high level here,
we do not distinguish between batch headers and batch certificates,
and instead model certificates directly,
as containing the information that is relevant to our model.
The signatures are implicit:
a certificate as modeled here is implicitly validated and signed
by a quorum of validators (author and endorsers).
Subtopics
- Certificate-fix
- Fixing function for certificate structures.
- Certificatep
- Recognizer 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.
