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

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 all-vals)
 (declare (xargs :guard (and (certificatep last-anchor)
                             (certificate-setp dag)
                             (block-listp blockchain)
                             (address-setp all-vals))))
 (declare
  (xargs
    :guard
    (and (in last-anchor dag)
         (evenp (certificate->round last-anchor))
         (active-committee-at-round (certificate->round last-anchor)
                                    blockchain all-vals))))
 (let ((__function__ 'collect-all-anchors))
   (declare (ignorable __function__))
   (collect-anchors last-anchor
                    (- (certificate->round last-anchor) 2)
                    0 dag blockchain all-vals)))

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

(defthm certificate-listp-of-collect-all-anchors
  (b*
   ((all-anchors
         (collect-all-anchors last-anchor dag blockchain all-vals)))
   (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 all-vals)))
   (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 all-vals)))
   (certificates-dag-paths-p all-anchors dag))))