How the certificates in the system change (or not) for each transition.
The only kind of event that changes the set of system certificates
is
An
An
Theorem:
(defthm validators-certs-of-create-next (implies (and (subset vals (correct-addresses systate)) (address-setp vals)) (equal (validators-certs vals (create-next cert systate)) (if (in (certificate->author cert) vals) (insert (certificate-fix cert) (validators-certs vals systate)) (validators-certs vals systate)))))
Theorem:
(defthm system-certs-of-create-next (equal (system-certs (create-next cert systate)) (if (emptyp (correct-addresses systate)) (system-certs systate) (insert (certificate-fix cert) (system-certs systate)))))
Theorem:
(defthm validators-certs-of-accept-next (implies (and (subset vals (correct-addresses systate)) (address-setp vals) (accept-possiblep msg systate)) (equal (validators-certs vals (accept-next msg systate)) (if (in (message->destination msg) vals) (insert (message->certificate msg) (validators-certs vals systate)) (validators-certs vals systate)))))
Theorem:
(defthm system-certs-of-accept-next (implies (accept-possiblep msg systate) (equal (system-certs (accept-next msg systate)) (system-certs systate))))
Theorem:
(defthm validators-certs-of-advance-next (implies (and (subset vals (correct-addresses systate)) (address-setp vals) (advance-possiblep val systate)) (equal (validators-certs vals (advance-next val systate)) (validators-certs vals systate))))
Theorem:
(defthm system-certs-of-advance-next (implies (advance-possiblep val systate) (equal (system-certs (advance-next val systate)) (system-certs systate))))
Theorem:
(defthm validators-certs-of-commit-next (implies (and (subset vals (correct-addresses systate)) (address-setp vals) (commit-possiblep val systate)) (equal (validators-certs vals (commit-next val systate)) (validators-certs vals systate))))
Theorem:
(defthm system-certs-of-commit-next (implies (commit-possiblep val systate) (equal (system-certs (commit-next val systate)) (system-certs systate))))