		Search-engine friendly clone of the ACL2 documentation.

Dags

Unequivocal-previous-certificates

Some theorems about retrieving the previous certificates of a certificate in unequivocal DAGs.

The first theorem says that the previous cerfificates referenced by a certificate in a backward-closed subset of a DAG of unequivocal certificates are the same in the superset. Note that the non-equivocation of the superset implies the non-equivocation of the subset, but the backward closure of the subset does not imply the backward closure of the superset. The latter is not needed, in fact. The backward closure of the subset establishes the hypothesis of certs-with-authors+round-of-unequivocal-superset in unequivocal-certs-with-authors+round, that the previous authors of the certificate are all in the round just before the certificate.

The second theorem says that the previous certificates referenced by a common certificate of two backward-closed unequivocal and mutually unequivocal DAGs are the same in the two DAGs. The backward closure of the two sets establishes the hypothesis of certs-with-authors+round-of-unequivocal-sets in unequivocal-certs-with-authors+round, that the previous authors of the certificate are all in the round just before the certificate, in both sets.

Definitions and Theorems

Theorem: previous-certificates-of-unequivocal-superdag

(defthm previous-certificates-of-unequivocal-superdag
 (implies
     (and (certificate-setp dag0)
          (certificate-setp dag)
          (subset dag0 dag)
          (certificate-set-unequivocalp dag)
          (dag-closedp dag0)
          (in cert dag0)
          (or (not (equal (certificate->round cert) 1))
              (emptyp (certificate->previous cert))))
     (equal (certs-with-authors+round (certificate->previous cert)
                                      (1- (certificate->round cert))
                                      dag)
            (certs-with-authors+round (certificate->previous cert)
                                      (1- (certificate->round cert))
                                      dag0))))

Theorem: previous-certificates-of-unequivocal-dags

(defthm previous-certificates-of-unequivocal-dags
 (implies
     (and (certificate-setp dag1)
          (certificate-setp dag2)
          (certificate-sets-unequivocalp dag1 dag2)
          (certificate-set-unequivocalp dag1)
          (certificate-set-unequivocalp dag2)
          (dag-closedp dag1)
          (dag-closedp dag2)
          (in cert dag1)
          (in cert dag2)
          (or (not (equal (certificate->round cert) 1))
              (emptyp (certificate->previous cert))))
     (equal (certs-with-authors+round (certificate->previous cert)
                                      (1- (certificate->round cert))
                                      dag1)
            (certs-with-authors+round (certificate->previous cert)
                                      (1- (certificate->round cert))
                                      dag2))))