		Search-engine friendly clone of the ACL2 documentation.

Anchors

Collect-anchors

Collect all the anchor certificates to commit.

Signature
(collect-anchors current-anchor previous-round last-committed-round dag blockchain all-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).; blockchain — Guard (block-listp blockchain).; all-vals — Guard (address-setp all-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 previous-round reaches the last committed round: we return a singleton list with the current anchor. The last committed round is passed as input last-committed-round; it is initially 0, when there is no committed round yet. If previous-round is larger than the last-committed-round, we find the leader at previous-round, and we use path-to-author+round to find the anchor, if any, at previous-round reachable from the current anchor. If there is no such reachable previous anchor, we recursively examine the even round just before previous-round, 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 at previous-round, it becomes the new current-anchor, and we recursively examine its previous even round, but since we changed 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).

Since previous-round eventually reaches last-committed-round (at the end of the recursion), which is a natural number (i.e. a round number or 0), the previous-round input of this ACL2 function is also a natural number (i.e. a round number or 0).

In order to calculate the leader at previous-round, as it may also change during the recursion, we need to know the active committee at that round. So we pass the blockchain so far as an input to this function, and we require in the guard that the active committee is known at previous-round, which implies that it is also known at smaller rounds. Note that this blockchain input does not change in the recursion: it is simply the current blockchain, which this operation is not extending; this operation is just collecting the anchors with which the blockchain is (elsewhere) extended. It is an invariant (not captured here) that last-committed-round is in fact the round of the latest block (or 0 if the blockchain is empty): this is proved in last-blockchain-round.

The role of the all-vals input is explained in update-committee-with-transaction.

The returned list of anchors is never empty, and it always starts with (i.e. its car is) the current-anchor input, as we prove below.

The returned list of anchors has even, strictly increasing (right to left) round numbers, under suitable assumptions on some of the inputs.

The returned list of anchors consists of certificates that are all in the DAG and are connected by paths; see certificates-dag-paths-p.

We also show that the rounds of the returned anchors are all above the last committed round, provided that the round of the input anchor is. More precisely, we say that the lowest-numbered anchor round (i.e. the car of last, i.e. the rightmost one) is above the last committed round. This assumption is satisfied when this function is called. Note that, since we also proved that rounds are strictly increasing, proving that the rightmost anchor has round above the last committed one implies that all the other anchors do as well; but in any case we need the theorem in this form, with car of last, so it can be used to relieve the hypothesis in a theorem about extend-blockchain.

Definitions and Theorems

Function: collect-anchors

(defun collect-anchors
       (current-anchor previous-round last-committed-round
                       dag blockchain all-vals)
 (declare (xargs :guard (and (certificatep current-anchor)
                             (natp previous-round)
                             (natp last-committed-round)
                             (certificate-setp dag)
                             (block-listp blockchain)
                             (address-setp all-vals))))
 (declare
   (xargs
        :guard (and (evenp previous-round)
                    (> (certificate->round current-anchor)
                       previous-round)
                    (or (zp previous-round)
                        (active-committee-at-round
                             previous-round blockchain all-vals)))))
 (let ((__function__ 'collect-anchors))
  (declare (ignorable __function__))
  (b*
   (((unless
        (and (mbt (and (natp previous-round)
                       (evenp previous-round)
                       (natp last-committed-round)
                       (or (zp previous-round)
                           (active-committee-at-round
                                previous-round blockchain all-vals))
                       t))
             (> previous-round last-committed-round)))
     (list (certificate-fix current-anchor)))
    (commtt
     (active-committee-at-round previous-round blockchain all-vals))
    (previous-leader (leader-at-round previous-round commtt))
    (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 blockchain all-vals))
     (collect-anchors current-anchor (- previous-round 2)
                      last-committed-round
                      dag blockchain all-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 blockchain all-vals)))
    (certificate-listp anchors))
  :rule-classes :rewrite)

Theorem: consp-of-collect-anchors

(defthm consp-of-collect-anchors
  (b* ((anchors (collect-anchors current-anchor
                                 previous-round last-committed-round
                                 dag blockchain all-vals)))
    (consp anchors))
  :rule-classes :type-prescription)

Theorem: car-of-collect-anchors

(defthm car-of-collect-anchors
 (b* ((?anchors (collect-anchors current-anchor
                                 previous-round last-committed-round
                                 dag blockchain all-vals)))
   (equal (car anchors)
          (certificate-fix current-anchor))))

Theorem: certificates-ordered-even-p-of-collect-anchors

(defthm certificates-ordered-even-p-of-collect-anchors
 (implies
   (and (evenp (certificate->round current-anchor))
        (evenp previous-round)
        (< previous-round
           (certificate->round current-anchor)))
   (b*
     ((?anchors (collect-anchors current-anchor
                                 previous-round last-committed-round
                                 dag blockchain all-vals)))
     (certificates-ordered-even-p anchors))))

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

(defthm certificates-dag-paths-p-of-collect-anchors
 (implies
   (and (certificate-setp dag)
        (in current-anchor dag)
        (< previous-round
           (certificate->round current-anchor)))
   (b*
     ((?anchors (collect-anchors current-anchor
                                 previous-round last-committed-round
                                 dag blockchain all-vals)))
     (certificates-dag-paths-p anchors dag))))

Theorem: collect-anchors-above-last-committed-round

(defthm collect-anchors-above-last-committed-round
 (implies
   (> (certificate->round current-anchor)
      last-committed-round)
   (b*
     ((?anchors (collect-anchors current-anchor
                                 previous-round last-committed-round
                                 dag blockchain all-vals)))
     (> (certificate->round (car (last anchors)))
        last-committed-round))))