		Search-engine friendly clone of the ACL2 documentation.

Anchors

Collect-anchors-in-unequivocal-closed-dags

Some theorems about collect-anchors applied on unequivocal, backward-closed DAGs.

The first theorem says that the anchors collected, starting from an anchor, from a backward-closed subset of an unequivocal DAG are the same in the superset. The anchor collection in question is the one expressed by the collect-anchors operation, which collects anchors starting from a given one down to a given round (or 0 for all rounds). If the starting anchor is in the subset, it must also be in the superset, and collecting the anchors in the superset yields the same result as collecting the anchors in the subset. That is, the collection of anchors is stable under DAG growth. This builds on the stability property of paths under DAG growth, expressed by the theorem path-to-author+round-of-unequivocal-superdag in paths-in-unequivocal-closed-dags; the collection of anchors is based on the paths, both present and absent paths, which that theorem shows to be stable under DAG growth. The proof is fairly simple, by induction on collect-anchors.

The second theorem says that the anchors collected, starting from a common anchor, from two backward-closed, (individually and mutually) unequivocal DAGs are the same in the two DAGs. The proof is also by induction on collect-anchors: although there are two calls with different arguments, the measured subset (i.e. previous-round) is the same in both calls. We need more hypotheses (which are implied by already proved invariants), to ensure that the two blockchains result in the same committees, and thus in the same leaders at each round of interest.

Definitions and Theorems

Theorem: collect-anchors-of-unequivocal-superdag

(defthm collect-anchors-of-unequivocal-superdag
 (implies
    (and (certificate-setp dag0)
         (certificate-setp dag)
         (subset dag0 dag)
         (certificate-set-unequivocalp dag)
         (dag-closedp dag0)
         (in current-anchor dag0))
    (equal (collect-anchors current-anchor previous-round
                            last-committed-round dag blockchain)
           (collect-anchors current-anchor previous-round
                            last-committed-round dag0 blockchain))))

Theorem: collect-anchors-of-unequivocal-dags

(defthm collect-anchors-of-unequivocal-dags
 (implies
      (and (certificate-setp dag1)
           (certificate-setp dag2)
           (certificate-set-unequivocalp dag1)
           (certificate-set-unequivocalp dag2)
           (certificate-sets-unequivocalp dag1 dag2)
           (dag-closedp dag1)
           (dag-closedp dag2)
           (dag-has-committees-p dag1 blockchain1)
           (dag-has-committees-p dag2 blockchain2)
           (same-active-committees-p blockchain1 blockchain2)
           (in current-anchor dag1)
           (in current-anchor dag2)
           (< previous-round
              (certificate->round current-anchor)))
      (equal (collect-anchors current-anchor previous-round
                              last-committed-round dag1 blockchain1)
             (collect-anchors current-anchor
                              previous-round last-committed-round
                              dag2 blockchain2))))