		Search-engine friendly clone of the ACL2 documentation.

Dags

Successors

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

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

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

Here `successor' refers to the fact that the returned certificates are in the (immediately) successive round of cert, even though the directed edges point backwards.

We obtain all the certificates from the successive round, and then we filter the ones that have an edge to cert, i.e. that have the author of cert in the previous component.

Definitions and Theorems

Function: successors-loop

(defun successors-loop (certs prev)
  (declare (xargs :guard (and (certificate-setp certs)
                              (addressp prev))))
  (let ((__function__ 'successors-loop))
    (declare (ignorable __function__))
    (b* (((when (emptyp certs)) nil)
         (cert (head certs)))
      (if (in prev (certificate->previous cert))
          (insert (certificate-fix cert)
                  (successors-loop (tail certs) prev))
        (successors-loop (tail certs) prev)))))

Theorem: certificate-setp-of-successors-loop

(defthm certificate-setp-of-successors-loop
  (b* ((successors (successors-loop certs prev)))
    (certificate-setp successors))
  :rule-classes :rewrite)

Theorem: successors-loop-subset

(defthm successors-loop-subset
  (implies (certificate-setp certs)
           (b* ((?successors (successors-loop certs prev)))
             (subset successors certs))))

Theorem: in-of-successors-loop

(defthm in-of-successors-loop
  (implies (certificate-setp certs)
           (equal (in cert (successors-loop certs prev))
                  (and (in cert certs)
                       (in prev (certificate->previous cert))))))

Theorem: successors-loop-monotone

(defthm successors-loop-monotone
  (implies (and (certificate-setp certs1)
                (certificate-setp certs2)
                (subset certs1 certs2))
           (subset (successors-loop certs1 prev)
                   (successors-loop certs2 prev))))

Theorem: certificate-set->round-set-of-successors-loop

(defthm certificate-set->round-set-of-successors-loop
 (implies
    (equal (certificate-set->round-set certs)
           (if (emptyp certs)
               nil
             (insert round nil)))
    (equal (certificate-set->round-set (successors-loop certs prev))
           (if (emptyp (successors-loop certs prev))
               nil
             (insert round nil)))))

Theorem: successors-loop-member-and-previous

(defthm successors-loop-member-and-previous
  (implies (and (certificate-setp certs)
                (in cert (successors-loop certs prev)))
           (and (in cert certs)
                (in prev (certificate->previous cert)))))

Function: successors

(defun successors (cert dag)
  (declare (xargs :guard (and (certificatep cert)
                              (certificate-setp dag))))
  (declare (xargs :guard (in cert dag)))
  (let ((__function__ 'successors))
    (declare (ignorable __function__))
    (successors-loop
         (certificates-with-round (1+ (certificate->round cert))
                                  dag)
         (certificate->author cert))))

Theorem: certificate-setp-of-successors

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

Theorem: successors-subset-of-next-round

(defthm successors-subset-of-next-round
  (b* ((?certs (successors cert dag)))
    (subset certs
            (certificates-with-round (1+ (certificate->round cert))
                                     dag))))

Theorem: successors-subset-of-dag

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

Theorem: successors-monotone

(defthm successors-monotone
  (implies (and (certificate-setp dag1)
                (certificate-setp dag2)
                (subset dag1 dag2))
           (subset (successors cert dag1)
                   (successors cert dag2))))

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

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

Theorem: certificate->round-of-element-of-successors

(defthm certificate->round-of-element-of-successors
  (implies (and (certificate-setp dag)
                (in cert1 (successors cert dag)))
           (equal (certificate->round cert1)
                  (1+ (certificate->round cert)))))