		Search-engine friendly clone of the ACL2 documentation.

Dags

Certificates-dag-paths-p

Check if a list of zero or more certificates are all in a DAG and are connected by paths.

Signature
(certificates-dag-paths-p certs dag) → yes/no
Arguments: certs — Guard (certificate-listp certs).; dag — Guard (certificate-setp dag).
Returns: yes/no — Type (booleanp yes/no).

That is, if the list is (c1 .. cn), this predicate says whether each ci is in the DAG and there is a path from each ci to ci+1. The predicate is t if the list is empty. The predicate is t if the list is a singleton whose element is in the DAG; no paths are required in this case. If there are two or more certificates in the list, then there must be paths between each contiguous elements.

Definitions and Theorems

Function: certificates-dag-paths-p

(defun certificates-dag-paths-p (certs dag)
 (declare (xargs :guard (and (certificate-listp certs)
                             (certificate-setp dag))))
 (let ((__function__ 'certificates-dag-paths-p))
  (declare (ignorable __function__))
  (b*
   (((when (endp certs)) t)
    (cert (car certs))
    ((unless (in cert dag)) nil)
    ((when (endp (cdr certs))) t)
    (cert1 (cadr certs))
    ((unless (<= (certificate->round cert1)
                 (certificate->round cert)))
     nil)
    ((unless
       (equal (path-to-author+round cert (certificate->author cert1)
                                    (certificate->round cert1)
                                    dag)
              cert1))
     nil))
   (certificates-dag-paths-p (cdr certs)
                             dag))))

Theorem: booleanp-of-certificates-dag-paths-p

(defthm booleanp-of-certificates-dag-paths-p
  (b* ((yes/no (certificates-dag-paths-p certs dag)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: certificates-dag-paths-p-of-nil

(defthm certificates-dag-paths-p-of-nil
  (certificates-dag-paths-p nil dag))

Theorem: certificates-dag-paths-p-member-in-dag

(defthm certificates-dag-paths-p-member-in-dag
  (implies (and (certificates-dag-paths-p certs dag)
                (member-equal cert certs))
           (in cert dag)))

Theorem: list-in-when-certificates-dag-paths-p

(defthm list-in-when-certificates-dag-paths-p
  (implies (certificates-dag-paths-p certs dag)
           (set::list-in certs dag)))