System-certificates
Certificates in the system.
We introduce an operation to collect all the certificates in the system.
Certificates are in validator DAGs and in network messages.
We define this notion here,
and we prove theorems about its initial value,
and about how its value changes in response to events.
Subtopics
- System-certs-of-next
- How the certificates in the system
change (or not) for each transition.
- Validators-certs
- Certificates from the DAGs of a set of (correct) validators.
- System-certs
- Certificates in the system.
- System-certs-when-init
- Initially, there are no certificates in the system.
