		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) → 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).
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, including the possibility that there is no leader because the committee is empty (although this never happens, due to invariants proved elsewhere), 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 the 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, proved elsewhere, that last-committed-round is in fact the round of the latest block (or 0 if the blockchain is empty).

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)
 (declare (xargs :guard (and (certificatep current-anchor)
                             (natp previous-round)
                             (natp last-committed-round)
                             (certificate-setp dag)
                             (block-listp blockchain))))
 (declare
  (xargs
   :guard
   (and
       (evenp previous-round)
       (> (certificate->round current-anchor)
          previous-round)
       (or (zp previous-round)
           (active-committee-at-round previous-round blockchain)))))
 (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))
          t))
       (> previous-round last-committed-round)))
     (list (certificate-fix current-anchor)))
    (commtt (active-committee-at-round previous-round blockchain))
    ((unless (committee-nonemptyp commtt))
     (collect-anchors current-anchor (- previous-round 2)
                      last-committed-round dag blockchain))
    (previous-leader (leader-at-round previous-round commtt))
    (previous-anchor?
         (path-to-author+round current-anchor
                               previous-leader previous-round dag))
    ((unless previous-anchor?)
     (collect-anchors current-anchor (- previous-round 2)
                      last-committed-round dag blockchain)))
   (cons (certificate-fix current-anchor)
         (collect-anchors previous-anchor? (- previous-round 2)
                          last-committed-round dag blockchain)))))

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)))
   (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)))
   (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)))
  (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)))
     (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)))
     (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)))
     (> (certificate->round (car (last anchors)))
        last-committed-round))))