		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. If previous-round is larger than 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 has even round numbers, if current-anchor has an even round number and if previous-round is even.

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
          (or (zp previous-round)
              (active-committee-at-round previous-round blockchain))
          t))
       (> (nfix previous-round)
          (nfix last-committed-round))))
     (list (certificate-fix current-anchor)))
    (commtt (active-committee-at-round previous-round blockchain))
    ((unless (committee-nonemptyp commtt))
     (collect-anchors current-anchor
                      (- (nfix 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
                      (- (nfix previous-round) 2)
                      last-committed-round dag blockchain)))
   (cons (certificate-fix current-anchor)
         (collect-anchors previous-anchor?
                          (- (nfix 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: 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: cert-list-evenp-of-collect-anchors

(defthm cert-list-evenp-of-collect-anchors
 (implies
   (and (evenp (certificate->round current-anchor))
        (evenp previous-round))
   (b* ((?anchors
             (collect-anchors current-anchor previous-round
                              last-committed-round dag blockchain)))
     (cert-list-evenp anchors))))

Theorem: cert-list-orderedp-of-collect-anchors

(defthm cert-list-orderedp-of-collect-anchors
 (implies
   (< previous-round
      (certificate->round current-anchor))
   (b* ((?anchors
             (collect-anchors current-anchor previous-round
                              last-committed-round dag blockchain)))
     (cert-list-orderedp anchors))))

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

(defthm collect-anchors-above-last-committed-round
 (implies
   (> (certificate->round current-anchor)
      (nfix last-committed-round))
   (b* ((?anchors
             (collect-anchors current-anchor previous-round
                              last-committed-round dag blockchain)))
     (> (certificate->round (car (last anchors)))
        (nfix last-committed-round))))
 :rule-classes
 ((:linear
   :trigger-terms
   ((certificate->round
     (car (last (collect-anchors current-anchor
                                 previous-round last-committed-round
                                 dag blockchain))))))))

Theorem: collect-anchors-of-certificate-fix-current-anchor

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

Theorem: collect-anchors-certificate-equiv-congruence-on-current-anchor

(defthm
     collect-anchors-certificate-equiv-congruence-on-current-anchor
 (implies
      (certificate-equiv current-anchor current-anchor-equiv)
      (equal (collect-anchors current-anchor previous-round
                              last-committed-round dag blockchain)
             (collect-anchors current-anchor-equiv previous-round
                              last-committed-round dag blockchain)))
 :rule-classes :congruence)

Theorem: collect-anchors-of-nfix-previous-round

(defthm collect-anchors-of-nfix-previous-round
  (equal (collect-anchors current-anchor (nfix previous-round)
                          last-committed-round dag blockchain)
         (collect-anchors current-anchor previous-round
                          last-committed-round dag blockchain)))

Theorem: collect-anchors-nat-equiv-congruence-on-previous-round

(defthm collect-anchors-nat-equiv-congruence-on-previous-round
 (implies
      (acl2::nat-equiv previous-round previous-round-equiv)
      (equal (collect-anchors current-anchor previous-round
                              last-committed-round dag blockchain)
             (collect-anchors current-anchor previous-round-equiv
                              last-committed-round dag blockchain)))
 :rule-classes :congruence)

Theorem: collect-anchors-of-nfix-last-committed-round

(defthm collect-anchors-of-nfix-last-committed-round
  (equal (collect-anchors current-anchor previous-round
                          (nfix last-committed-round)
                          dag blockchain)
         (collect-anchors current-anchor previous-round
                          last-committed-round dag blockchain)))

Theorem: collect-anchors-nat-equiv-congruence-on-last-committed-round

(defthm collect-anchors-nat-equiv-congruence-on-last-committed-round
  (implies
       (acl2::nat-equiv last-committed-round
                        last-committed-round-equiv)
       (equal (collect-anchors current-anchor previous-round
                               last-committed-round dag blockchain)
              (collect-anchors current-anchor previous-round
                               last-committed-round-equiv
                               dag blockchain)))
  :rule-classes :congruence)

Theorem: collect-anchors-of-certificate-set-fix-dag

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

Theorem: collect-anchors-certificate-set-equiv-congruence-on-dag

(defthm collect-anchors-certificate-set-equiv-congruence-on-dag
  (implies
       (certificate-set-equiv dag dag-equiv)
       (equal (collect-anchors current-anchor previous-round
                               last-committed-round dag blockchain)
              (collect-anchors current-anchor
                               previous-round last-committed-round
                               dag-equiv blockchain)))
  :rule-classes :congruence)

Theorem: collect-anchors-of-block-list-fix-blockchain

(defthm collect-anchors-of-block-list-fix-blockchain
  (equal (collect-anchors current-anchor
                          previous-round last-committed-round
                          dag (block-list-fix blockchain))
         (collect-anchors current-anchor previous-round
                          last-committed-round dag blockchain)))

Theorem: collect-anchors-block-list-equiv-congruence-on-blockchain

(defthm collect-anchors-block-list-equiv-congruence-on-blockchain
  (implies
       (block-list-equiv blockchain blockchain-equiv)
       (equal (collect-anchors current-anchor previous-round
                               last-committed-round dag blockchain)
              (collect-anchors current-anchor
                               previous-round last-committed-round
                               dag blockchain-equiv)))
  :rule-classes :congruence)