		Search-engine friendly clone of the ACL2 documentation.

Signed-certificates

Signed-certs-of-next

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 create, because all the others do not change the set of system certificates, as proved in system-certs-of-next, which are a superset of the signed certificates. Whether the set of signed certificates actually changes depends on whether the validator is a signer of the certificate or not; so our theorem for create has a conditional. The theorems for the other kinds of events assert that there is no change in the set of signed certificates.

Definitions and Theorems

Theorem: signed-certs-of-create-next

(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: signed-certs-of-accept-next

(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: signed-certs-of-advance-next

(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: signed-certs-of-commit-next

(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))))