		Search-engine friendly clone of the ACL2 documentation.

Dags

Predecessors

Set of the certificates in a DAG that are precedessors of a certificate in a DAG.

Signature
(predecessors cert dag) → certs
Arguments: cert — Guard (certificatep cert).; dag — Guard (certificate-setp dag).
Returns: certs — Type (certificate-setp certs).

These are the destination certificates of the edges in the DAG that have the certificate cert as source. These edges are outgoing edges of cert.

Here `precedessor' refers to the fact that the return certificates are in the (immediately) preceding round of cert (unless cert is in round 1, in which case this function returns the empty set), even though the directed edges point backwards.

If the certificate is at round 1, we return the empty set. Otherwise, we return the certificates at the previous round that are authored by the previous authors in the certificate. All the returned certificates are in the round just before cert.

Definitions and Theorems

Function: predecessors

(defun predecessors (cert dag)
 (declare (xargs :guard (and (certificatep cert)
                             (certificate-setp dag))))
 (declare (xargs :guard (in cert dag)))
 (let ((__function__ 'predecessors))
   (declare (ignorable __function__))
   (if (equal (certificate->round cert) 1)
       nil
     (certificates-with-authors+round (certificate->previous cert)
                                      (1- (certificate->round cert))
                                      dag))))

Theorem: certificate-setp-of-predecessors

(defthm certificate-setp-of-predecessors
  (b* ((certs (predecessors cert dag)))
    (certificate-setp certs))
  :rule-classes :rewrite)

Theorem: predecessors-subset-of-dag

(defthm predecessors-subset-of-dag
  (implies (certificate-setp dag)
           (b* ((?certs (predecessors cert dag)))
             (subset certs dag))))

Theorem: predecessors-subset-of-previous-round

(defthm predecessors-subset-of-previous-round
 (implies
   (certificate-setp dag)
   (b* ((?certs (predecessors cert dag)))
     (subset certs
             (certificates-with-round (1- (certificate->round cert))
                                      dag)))))

Theorem: certificate-set->round-set-of-predecessors

(defthm certificate-set->round-set-of-predecessors
  (implies
       (certificate-setp dag)
       (equal (certificate-set->round-set (predecessors cert dag))
              (if (emptyp (predecessors cert dag))
                  nil
                (insert (1- (certificate->round cert))
                        nil)))))

Theorem: head-of-predecessors-in-predecessors

(defthm head-of-predecessors-in-predecessors
  (implies (not (emptyp (predecessors cert dag)))
           (in (head (predecessors cert dag))
               (predecessors cert dag))))

Theorem: head-of-predecessors-in-dag

(defthm head-of-predecessors-in-dag
  (implies (and (certificate-setp dag)
                (not (emptyp (predecessors cert dag))))
           (in (head (predecessors cert dag))
               dag)))

Theorem: round-in-predecessors-is-one-less

(defthm round-in-predecessors-is-one-less
  (implies (and (certificate-setp dag)
                (in cert1 (predecessors cert dag)))
           (equal (certificate->round cert1)
                  (1- (certificate->round cert)))))

Theorem: round-of-head-of-predecessors

(defthm round-of-head-of-predecessors
 (implies (and (certificate-setp dag)
               (not (emptyp (predecessors cert dag))))
          (equal (certificate->round (head (predecessors cert dag)))
                 (1- (certificate->round cert)))))