		Search-engine friendly clone of the ACL2 documentation.

Anchors-extension

Collect-anchors-to-append-of-collect-anchors

Extension theorem for collect-anchors, for a single DAG.

This is proved by induction on the anchors that form the extension. We have two anchors, anchor and anchor1, with the latter coming strictly after the former. In order to prove this theorem by induction, we formulate it over a generic round round between anchor (inclusive) and anchor1 (exclusive), which matches the previous-round formal of collect-anchors, and is in fact its measured subset that is involved in the induction.

In the base case, round is the round of anchor, and the equality to prove reduces to:

(equal (cons anchor1
             (collect-anchors anchor
                              (- (certificate->round anchor) 2)
                              0 dag blockchain))
       (append (list anchor)
               (collect-anchors anchor
                                (- (certificate->round anchor) 2)
                                0 dag blockchain)))

The cons on the left side arises thanks to the dag-omni-paths-p hypothesis, which tells us that there is a path from anchor1 to anchor. The (list anchor) on the right side is the result of the call of collect-anchors which is the first argument of append. The second argument of append is unchanged. Clearly, the two sides are equal.

In the step case, round is later than anchor. Both calls of collect-anchors on round expand to terms involving the same recursive calls, and the induction hypothesis ensures equality.

Definitions and Theorems

Theorem: collect-anchors-to-append-of-collect-anchors

(defthm collect-anchors-to-append-of-collect-anchors
 (implies
  (and
    (certificate-setp dag)
    (dag-has-committees-p dag blockchain)
    (dag-in-committees-p dag blockchain)
    (in anchor dag)
    (evenp (certificate->round anchor))
    (equal
         (certificate->author anchor)
         (leader-at-round
              (certificate->round anchor)
              (active-committee-at-round (certificate->round anchor)
                                         blockchain)))
    (dag-omni-paths-p anchor dag)
    (in anchor1 dag)
    (evenp (certificate->round anchor1))
    (natp round)
    (evenp round)
    (< round (certificate->round anchor1))
    (>= round (certificate->round anchor)))
  (equal
   (collect-anchors anchor1 round 0 dag blockchain)
   (append (collect-anchors anchor1
                            round (certificate->round anchor)
                            dag blockchain)
           (collect-anchors anchor (- (certificate->round anchor) 2)
                            0 dag blockchain)))))