		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificate

Fixtype of certificates.

This is a product type introduced by fty::defprod.

Fields

proposal — proposal
endorsers — address-set

We model a certificate as consisting of:

A proposal.
The addresses of the validators that endorsed the proposal, by signing it in addition to the author.

We do not model cryptographic signatures explicitly. The presence of an endorser address in a certificate models the fact that the validator with that address endorsed the proposal by signing it.

Subtopics

Certificate-fix: Fixing function for certificate structures.
Certificatep: Recognizer for certificate structures.
Certificate-equiv: Basic equivalence relation for certificate structures.
Make-certificate: Basic constructor macro for certificate structures.
Certificate->proposal: Get the proposal field from a certificate.
Certificate->endorsers: Get the endorsers field from a certificate.
Change-certificate: Modifying constructor for certificate structures.