		Search-engine friendly clone of the ACL2 documentation.

Dags

Dag-closedp

Check if a DAG is backward-closed.

That is, check if the previous certificates of each certificate in the DAG are all in the DAG. This is an invariant of the DAGs of validators, as proved elsewhere.

Adding a certificate whose previous certificates are in the DAG preserves the closure of the DAG; we prove this in dag-previous-in-dag-p-of-insert. It might be tempting to try and prove something like

(equal (dag-closedp (set::insert cert dag))
       (and (dag-closedp dag)
            (certificate-previous-in-dag-p cert dag)))

but that does not hold, because cert could be a predecessor certificate of some certificate in dag. So instead we prove the (right-to-left) implication.

Definitions and Theorems

Theorem: dag-closedp-necc

(defthm dag-closedp-necc
  (implies (dag-closedp dag)
           (implies (in cert dag)
                    (certificate-previous-in-dag-p cert dag))))

Theorem: booleanp-of-dag-closedp

(defthm booleanp-of-dag-closedp
  (b* ((yes/no (dag-closedp dag)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: dag-closedp-of-nil

(defthm dag-closedp-of-nil
  (dag-closedp nil))

Theorem: dag-closedp-of-insert

(defthm dag-closedp-of-insert
  (implies (and (certificatep cert)
                (certificate-setp dag)
                (dag-closedp dag)
                (certificate-previous-in-dag-p cert dag))
           (dag-closedp (insert cert dag))))