		Search-engine friendly clone of the ACL2 documentation.

Unequivocal-signed-certificates

Unequivocal-signed-certs-p-of-next

Preservation of the invariant: if the invariant holds in a system state, it also holds in the next system state.

The only kind of event that may change the set of signed certificates is create, which adds the certificate to each signer. To show that no equivocation is introduced, we make use of not-signer-record-p-when-create-possiblep and signer-record-p-when-author+round-in-signed-certs, to effectively derive a contradiction should the new certificate have the same author and round as some existing certificate. The rule certificate-set-unequivocalp-of-insert introduces cert-with-author+round, which is why signer-record-p-when-author+round-in-signed-certs is phrased in terms of that certificate retrieval function.

The other kinds of events do not change the sets of signed certificates, and thus it is easy to prove the preservation of the invariant.

Definitions and Theorems

Theorem: certificate-set-unequivocalp-of-create-next

(defthm certificate-set-unequivocalp-of-create-next
 (implies
   (and (signer-records-p systate)
        (in signer (correct-addresses systate))
        (certificate-set-unequivocalp (signed-certs signer systate))
        (create-possiblep cert systate)
        (no-self-endorsed-p systate))
   (certificate-set-unequivocalp
        (signed-certs signer (create-next cert systate)))))

Theorem: unequivocal-signed-certs-p-of-create-next

(defthm unequivocal-signed-certs-p-of-create-next
  (implies (and (unequivocal-signed-certs-p systate)
                (signer-records-p systate)
                (no-self-endorsed-p systate)
                (create-possiblep cert systate))
           (unequivocal-signed-certs-p (create-next cert systate))))

Theorem: unequivocal-signed-certs-p-of-accept-next

(defthm unequivocal-signed-certs-p-of-accept-next
  (implies (and (unequivocal-signed-certs-p systate)
                (accept-possiblep msg systate))
           (unequivocal-signed-certs-p (accept-next msg systate))))

Theorem: unequivocal-signed-certs-p-of-advance-next

(defthm unequivocal-signed-certs-p-of-advance-next
  (implies (and (unequivocal-signed-certs-p systate)
                (advance-possiblep val systate))
           (unequivocal-signed-certs-p (advance-next val systate))))

Theorem: unequivocal-signed-certs-p-of-commit-next

(defthm unequivocal-signed-certs-p-of-commit-next
  (implies (and (unequivocal-signed-certs-p systate)
                (commit-possiblep val systate))
           (unequivocal-signed-certs-p (commit-next val systate))))

Theorem: unequivocal-signed-certs-p-of-event-next

(defthm unequivocal-signed-certs-p-of-event-next
  (implies (and (unequivocal-signed-certs-p systate)
                (signer-records-p systate)
                (no-self-endorsed-p systate)
                (event-possiblep event systate))
           (unequivocal-signed-certs-p (event-next event systate))))