		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificate-set-unequivocalp

Check if a set of certificates is unequivocal.

That is, check whether the certificates in the set have unique combinations of author and round. We check that any two certificates in the set with the same author and round are in fact the same certificates. This means that the certificates in the set are uniquely identified by their author and round.

This is an invariant on DAGs, and in fact on all the certificates in the system, enforced by the protocol under suitable fault tolerance conditions. Here we formulate the invariant.

The rule certificate-set-unequivocalp-of-insert is useful to prove the preservation of non-equivocation when a set of certificates is extended. Either the added certificate is already in the initial set, or the initial set has no certificate with the added certificate's author and round.

The theorem equal-certificate-authors-when-unequiv-and-same-round says that if the certificates in an unequivocal sets have all the same round, then two certificates in that set are the same if they have the same author. We phrase it as a rewrite rule in the typical form of an injectivity rewrite rule.

The theorem head-author-not-in-tail-authors-when-unequiv-and-all-same-round is mainly a consequence of the previous one, considering the first certificate in a set and a generic one in the rest of the set.

The previous theorem is used to prove cardinality-of-authors-when-unequiv-and-all-same-rounds, which says that the number of authors of a set of certificates all in the same round is the same as the number of those certificates: unequivocation means that there is a bijection between those authors and those certificates.

The previous theorem is used to prove cardinality-of-certificates-with-authors+round-when-subset, which in a sense specializes the previous one to the certificates returned by certificates-with-authors+round. Note that this returns certificates all in the same round, so they are in bijection with their authors, given that the certificates are unequivocal.

Definitions and Theorems

Theorem: certificate-set-unequivocalp-necc

(defthm certificate-set-unequivocalp-necc
  (implies (not (if (and (in cert1 certs)
                         (in cert2 certs)
                         (equal (certificate->author cert1)
                                (certificate->author cert2))
                         (equal (certificate->round cert1)
                                (certificate->round cert2)))
                    (if (equal cert1 cert2) t nil)
                  t))
           (not (certificate-set-unequivocalp certs))))

Theorem: booleanp-of-certificate-set-unequivocalp

(defthm booleanp-of-certificate-set-unequivocalp
  (b* ((yes/no (certificate-set-unequivocalp certs)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: certificate-set-unequivocalp-when-subset

(defthm certificate-set-unequivocalp-when-subset
  (implies (and (certificate-set-unequivocalp certs)
                (subset certs0 certs))
           (certificate-set-unequivocalp certs0)))

Theorem: certificate-set-unequivocalp-when-emptyp

(defthm certificate-set-unequivocalp-when-emptyp
  (implies (emptyp certs)
           (certificate-set-unequivocalp certs)))

Theorem: certificate-set-unequivocalp-of-insert

(defthm certificate-set-unequivocalp-of-insert
 (implies
  (certificate-setp certs)
  (equal
   (certificate-set-unequivocalp (insert cert certs))
   (and
    (certificate-set-unequivocalp certs)
    (or
      (in cert certs)
      (not (certificate-with-author+round (certificate->author cert)
                                          (certificate->round cert)
                                          certs)))))))

Theorem: equal-certificate-authors-when-unequiv-and-same-round

(defthm equal-certificate-authors-when-unequiv-and-same-round
  (implies (and (certificate-set-unequivocalp certs)
                (<= (cardinality (certificate-set->round-set certs))
                    1)
                (in cert1 certs)
                (in cert2 certs))
           (equal (equal (certificate->author cert1)
                         (certificate->author cert2))
                  (equal cert1 cert2))))

Theorem: head-author-not-in-tail-authors-when-unequiv-and-all-same-round

(defthm
    head-author-not-in-tail-authors-when-unequiv-and-all-same-round
  (implies (and (certificate-setp certs)
                (certificate-set-unequivocalp certs)
                (<= (cardinality (certificate-set->round-set certs))
                    1)
                (not (emptyp certs)))
           (not (in (certificate->author (head certs))
                    (certificate-set->author-set (tail certs))))))

Theorem: cardinality-of-authors-when-unequiv-and-all-same-rounds

(defthm cardinality-of-authors-when-unequiv-and-all-same-rounds
  (implies (and (certificate-setp certs)
                (certificate-set-unequivocalp certs)
                (<= (cardinality (certificate-set->round-set certs))
                    1))
           (equal (cardinality (certificate-set->author-set certs))
                  (cardinality certs))))

Theorem: cardinality-of-certificates-with-authors+round-when-subset

(defthm cardinality-of-certificates-with-authors+round-when-subset
 (implies
  (and (certificate-setp certs)
       (certificate-set-unequivocalp certs)
       (subset (address-set-fix authors)
               (certificate-set->author-set
                    (certificates-with-round round certs))))
  (equal (cardinality
              (certificates-with-authors+round authors round certs))
         (cardinality (address-set-fix authors)))))