		Search-engine friendly clone of the ACL2 documentation.

Certificates

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 validator 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 references; these define the edges of the DAG. It is a system invariant, proved elsewhere, that certificates in DAGs are uniquely identified by their author and round.
The addresses of the validators that endorsed this certificate, by signing it in addition to the author.

We do not model cryptographic signatures explicitly. The presence of the author and endorser addresses in a certificate models the fact that the author and endorsers signed the certificate (more precisely, the proposal that the certificate extends; but as explained in certificates, we do not model proposals explicitly).

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.