How the certificates signed by a validator change (or not) for each transition.
The only kind of event that may change
the certificates signed by a validator
is
Theorem:
(defthm signed-certs-of-create-next (implies (in val (correct-addresses systate)) (equal (signed-certs val (create-next cert systate)) (if (in (address-fix val) (certificate->signers cert)) (insert (certificate-fix cert) (signed-certs val systate)) (signed-certs val systate)))))
Theorem:
(defthm signed-certs-of-accept-next (implies (and (in val (correct-addresses systate)) (accept-possiblep msg systate)) (equal (signed-certs val (accept-next msg systate)) (signed-certs val systate))))
Theorem:
(defthm signed-certs-of-advance-next (implies (and (in val (correct-addresses systate)) (advance-possiblep val1 systate)) (equal (signed-certs val (advance-next val1 systate)) (signed-certs val systate))))
Theorem:
(defthm signed-certs-of-commit-next (implies (and (in val (correct-addresses systate)) (commit-possiblep val1 systate)) (equal (signed-certs val (commit-next val1 systate)) (signed-certs val systate))))