		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificate-sets-unequivocalp

Check if two sets of certificates are mutually unequivocal.

This is similar to certificate-set-unequivocalp (note the singular `set' vs. the plural `sets'), but checks certificates from different sets. It requires that if both sets have certificates with the same author and round, the certificates must be equal.

This is an invariant that applies across DAGs of different validators. Here we just formulate that invariant.

Note that this invariant does not imply that the two sets are unequivocal: one set may well have multiple different certificates with the same author and round, so long as that combination of author and round does not appear in the other set.

The rule certificate-sets-unequivocalp-of-insert is useful to prove the preservation of mutual non-equivocation when one of the two sets of certificates is extended. This is similar to certificate-set-unequivocalp-of-insert in certificate-set-unequivocalp, but more complicated due to the presence of two sets. Either the new certificate is already in the set being extended, or it is in the set not being extended, or the set not being extended has no certificate with the added certificate's author and round. For the second of these three cases, we need the additional hypothesis that the set not being extended is unequivocal. Otherwise, consider the situation of an empty first, a second set consisting of two equivocal certificates, and the addition of one of these two certificates to the first set: the resulting pair of sets is equivocal; but the non-equivocation of the second set prevents that.

The theorem certificate-set-unequivocalp-of-union says that given two sets of certificates that are individually and jointly unequivocal, their union is unequivocal. This is is easy to prove by cases of where the two witness certificates come from.

Definitions and Theorems

Theorem: certificate-sets-unequivocalp-necc

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

Theorem: booleanp-of-certificate-sets-unequivocalp

(defthm booleanp-of-certificate-sets-unequivocalp
  (b* ((yes/no (certificate-sets-unequivocalp certs1 certs2)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: certificate-sets-unequivocalp-commutative

(defthm certificate-sets-unequivocalp-commutative
  (equal (certificate-sets-unequivocalp certs1 certs2)
         (certificate-sets-unequivocalp certs2 certs1)))

Theorem: certificate-sets-unequivocalp-when-subsets

(defthm certificate-sets-unequivocalp-when-subsets
  (implies (and (certificate-sets-unequivocalp certs1 certs2)
                (subset certs01 certs1)
                (subset certs02 certs2))
           (certificate-sets-unequivocalp certs01 certs02)))

Theorem: certificate-sets-unequivocalp-when-emptyp

(defthm certificate-sets-unequivocalp-when-emptyp
  (implies (or (emptyp certs1) (emptyp certs2))
           (certificate-sets-unequivocalp certs1 certs2)))

Theorem: certificate-sets-unequivocalp-of-same-set

(defthm certificate-sets-unequivocalp-of-same-set
  (equal (certificate-sets-unequivocalp certs certs)
         (certificate-set-unequivocalp certs)))

Theorem: certificate-sets-unequivocalp-of-same-set-converse

(defthm certificate-sets-unequivocalp-of-same-set-converse
  (equal (certificate-set-unequivocalp certs)
         (certificate-sets-unequivocalp certs certs)))

Theorem: certificate-sets-unequivocalp-of-insert

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

Theorem: certificate-set-unequivocalp-of-union

(defthm certificate-set-unequivocalp-of-union
  (implies (and (certificate-set-unequivocalp certs1)
                (certificate-set-unequivocalp certs2)
                (certificate-sets-unequivocalp certs1 certs2))
           (certificate-set-unequivocalp (union certs1 certs2))))