		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 that applies to the DAGs in the system. Here we just define the predicate.

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-certs-with-authors+round-when-subset, which in a sense specializes the previous one to the certificates returned by certs-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.

The theorem certs-same-round-unequiv-intersect-when-authors-intersect says that if two sets of unequivocal certificates with the same round have at least one common author, then there is at least one common certificate to the two sets. This is because, as proved in equal-certificate-authors-when-unequiv-and-same-round, there is a bijection between unequivocal certificates with the same round and their authors. The theorem certs-same-round-unequiv-intersect-when-authors-intersect is proved as follows: take an author in the intersection of authors (the head); use head-of-certs-with-author-in-certs-when-author-in-authors twice to show that there is a certificate in both sets with that author; use equal-certificate-authors-when-unequiv-and-same-round to show that they are the same certificate; thus that same certificate is in both sets of certificates, which therefore have a non-empty intersection.

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-of-nil

(defthm certificate-set-unequivocalp-of-nil
  (certificate-set-unequivocalp nil))

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-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 (cert-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-setp certs)
                (certificate-set-unequivocalp certs)
                (<= (cardinality (cert-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 (cert-set->round-set certs))
                    1)
                (not (emptyp certs)))
           (not (in (certificate->author (head certs))
                    (cert-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 (cert-set->round-set certs))
                    1))
           (equal (cardinality (cert-set->author-set certs))
                  (cardinality certs))))

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

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

Theorem: certs-same-round-unequiv-intersect-when-authors-intersect

(defthm certs-same-round-unequiv-intersect-when-authors-intersect
 (implies
  (and (certificate-setp certs1)
       (certificate-setp certs2)
       (certificate-set-unequivocalp (union certs1 certs2))
       (<= (cardinality (cert-set->round-set (union certs1 certs2)))
           1)
       (not (emptyp (intersect (cert-set->author-set certs1)
                               (cert-set->author-set certs2)))))
  (not (emptyp (intersect certs1 certs2)))))