		Search-engine friendly clone of the ACL2 documentation.

Operations-anchors

Collect-all-anchors

Collect all the anchors in a DAG, starting from a given anchor.

Signature
(collect-all-anchors last-anchor dag vals) → all-anchors
Arguments: last-anchor — Guard (certificatep last-anchor).; dag — Guard (certificate-setp dag).; vals — Guard (address-setp vals).
Returns: all-anchors — Type (certificate-listp all-anchors).

This is a specialization of collect-anchors that does not stop at the last committed rounds, but instead goes all the way to the start of the DAG.

The input last-anchor is a certificate (not necessarily an anchor, although normally it is when this function is called) at an even round. We collect that anchor, and all the ones at preceding even rounds recursively reachable from this certificate; see collect-anchors for details of the process.

Definitions and Theorems

Function: collect-all-anchors

(defun collect-all-anchors (last-anchor dag vals)
  (declare (xargs :guard (and (certificatep last-anchor)
                              (certificate-setp dag)
                              (address-setp vals))))
  (declare
       (xargs :guard (and (in last-anchor dag)
                          (evenp (certificate->round last-anchor))
                          (not (emptyp vals)))))
  (let ((__function__ 'collect-all-anchors))
    (declare (ignorable __function__))
    (collect-anchors last-anchor
                     (- (certificate->round last-anchor) 2)
                     0 dag vals)))

Theorem: certificate-listp-of-collect-all-anchors

(defthm certificate-listp-of-collect-all-anchors
  (b* ((all-anchors (collect-all-anchors last-anchor dag vals)))
    (certificate-listp all-anchors))
  :rule-classes :rewrite)