		Search-engine friendly clone of the ACL2 documentation.

System-certificates

System-certs-of-next

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 create, by adding the created certificate to the set: the certificate is added to the network, and possibly to the author's DAG (if the author is correct). However, if there are no correct validators at all, there is actually no change to the set of system certificates; this is an impractical case, which in particular does not satisfy the normal fault tolerance assumptions.

An accept event just moves a certificate, from the network to a DAG. The whole set is unaffected.

An advance or commit event does not change any DAG or the network. So the set remains the same.

Definitions and Theorems

Theorem: validators-certs-of-create-next

(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: system-certs-of-create-next

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

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

(defthm system-certs-of-accept-next
  (implies (accept-possiblep msg systate)
           (equal (system-certs (accept-next msg systate))
                  (system-certs systate))))

Theorem: validators-certs-of-advance-next

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

(defthm system-certs-of-advance-next
  (implies (advance-possiblep val systate)
           (equal (system-certs (advance-next val systate))
                  (system-certs systate))))

Theorem: validators-certs-of-commit-next

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

(defthm system-certs-of-commit-next
  (implies (commit-possiblep val systate)
           (equal (system-certs (commit-next val systate))
                  (system-certs systate))))