		Search-engine friendly clone of the ACL2 documentation.

Operations-blockchain

Collect-anchors

Collect all the anchor certificates to commit.

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

The starting point is an anchor, current-anchor and an even round, previous-round, that precedes the anchor. The recursion terminates when this previous round reaches the last committed round: we return a singleton list with the current anchor. If the recursion does not terminate, we find the leader at the previous round under examination, and we use path-to-author+round to find the anchor, if any, at the previous round under examination reachable from the current anchor. If there is no such reachable previous anchor, we recursively examine the even round just before the previous one just examined, with the same current anchor; in the recursion, we will be looking for longer paths, from the same current anchor to a round further behind. If there is an anchor, it becomes the new current anchor, and we recursively examine its previous even round, but since we changed the current anchor, in the recursion DAG paths will be from the new current anchor. The recursive call will return a list of anchors that includes the anchor passed as first argument. thus, when that anchor changes (i.e. when the previous anchor is found), we add the old current anchor to the list. The resulting list of anchors is in inverse chronological order: the leftmost anchor is the newest one (i.e. greatest round number); the rightmost anchor is the oldest one (i.e. smallest round number).

Note that the last committed round is a natural number, not necessarily a positive one, because it is initially 0. Since the previous round eventually reaches the last committed round (at the end of the recursion), the previous round input of this ACL2 function is also a natural number, not necessarily positive.

Definitions and Theorems

Function: collect-anchors

(defun collect-anchors
       (current-anchor previous-round
                       last-committed-round dag vals)
 (declare (xargs :guard (and (certificatep current-anchor)
                             (natp previous-round)
                             (natp last-committed-round)
                             (certificate-setp dag)
                             (address-setp vals))))
 (declare (xargs :guard (and (evenp previous-round)
                             (> (certificate->round current-anchor)
                                previous-round)
                             (not (emptyp vals)))))
 (let ((__function__ 'collect-anchors))
  (declare (ignorable __function__))
  (b*
   (((unless (and (mbt (and (natp previous-round)
                            (evenp previous-round)
                            (natp last-committed-round)))
                  (> previous-round last-committed-round)))
     (list (certificate-fix current-anchor)))
    (previous-leader (leader-at-round previous-round vals))
    (previous-anchor?
         (path-to-author+round current-anchor
                               previous-leader previous-round dag)))
   (if previous-anchor?
       (cons (certificate-fix current-anchor)
             (collect-anchors previous-anchor? (- previous-round 2)
                              last-committed-round dag vals))
     (collect-anchors current-anchor (- previous-round 2)
                      last-committed-round dag vals)))))

Theorem: certificate-listp-of-collect-anchors

(defthm certificate-listp-of-collect-anchors
  (b* ((anchors (collect-anchors current-anchor previous-round
                                 last-committed-round dag vals)))
    (certificate-listp anchors))
  :rule-classes :rewrite)

Theorem: car-of-collect-anchors

(defthm car-of-collect-anchors
  (equal (car (collect-anchors current-anchor previous-round
                               last-committed-round dag vals))
         (certificate-fix current-anchor)))