		Search-engine friendly clone of the ACL2 documentation.

Anchors

Collect-all-anchors

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

Signature
(collect-all-anchors last-anchor dag blockchain) → all-anchors
Arguments: last-anchor — Guard (certificatep last-anchor).; dag — Guard (certificate-setp dag).; blockchain — Guard (block-listp blockchain).
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.

The guard requires that the active committee can be calculated for the round of last-anchor. This is a little more than needed to satisfy the guard of collect-anchors (which just need the committee for two rounds before that one), but it is slightly simpler, and in fact satisfied when we call collect-all-anchors.

The returned list of anchors satisfies certificates-dag-paths-p.

Definitions and Theorems

Function: collect-all-anchors

(defun collect-all-anchors (last-anchor dag blockchain)
 (declare (xargs :guard (and (certificatep last-anchor)
                             (certificate-setp dag)
                             (block-listp blockchain))))
 (declare
  (xargs
    :guard
    (and (in last-anchor dag)
         (evenp (certificate->round last-anchor))
         (active-committee-at-round (certificate->round last-anchor)
                                    blockchain))))
 (let ((__function__ 'collect-all-anchors))
   (declare (ignorable __function__))
   (collect-anchors last-anchor
                    (- (certificate->round last-anchor) 2)
                    0 dag blockchain)))

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

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

Theorem: car-of-collect-all-anchors

(defthm car-of-collect-all-anchors
  (b*
   ((?all-anchors (collect-all-anchors last-anchor dag blockchain)))
   (equal (car all-anchors)
          (certificate-fix last-anchor))))

Theorem: certificates-dag-paths-p-of-collect-all-anchors

(defthm certificates-dag-paths-p-of-collect-all-anchors
 (implies
  (and (certificate-setp dag)
       (in last-anchor dag))
  (b*
   ((?all-anchors (collect-all-anchors last-anchor dag blockchain)))
   (certificates-dag-paths-p all-anchors dag))))