		Search-engine friendly clone of the ACL2 documentation.

Successor-predecessor-intersection

Pick-successor/predecessor-properties

Key properties of pick-successor/predecessor.

This combines and generalizes the theorems proved in pick-successor/predecessor, by using stronger hypotheses on the DAGs that imply the specific properties used in those previous theorems. The hypotheses on the DAGs are all invariants, as proved elsewhere. The key properties are that the picked certificate is among the successors of cert1 in the first DAG, among the precedessors of cert2 in the second DAG, and also in both DAGs.

We prove four lemmas that serve to establish hypotheses in the theorems in pick-successor/predecessor from the more general hypothesis in this theorem.

Definitions and Theorems

Theorem: pick-successor/predecessor-properties

(defthm pick-successor/predecessor-properties
 (implies
  (and
   (certificate-setp dag1)
   (certificate-setp dag2)
   (certificate-set-unequivocalp dag1)
   (certificate-set-unequivocalp dag2)
   (certificate-sets-unequivocalp dag1 dag2)
   (in cert2 dag2)
   (equal (certificate->round cert2)
          (+ 2 (certificate->round cert1)))
   (dag-has-committees-p dag1 blockchain1)
   (dag-has-committees-p dag2 blockchain2)
   (dag-in-committees-p dag1 blockchain1)
   (dag-in-committees-p dag2 blockchain2)
   (same-active-committees-p blockchain1 blockchain2)
   (dag-predecessor-quorum-p dag2 blockchain2)
   (>
     (committee-members-stake
          (cert-set->author-set (successors cert1 dag1))
          (active-committee-at-round (1+ (certificate->round cert1))
                                     blockchain1))
     (committee-max-faulty-stake
          (active-committee-at-round (1+ (certificate->round cert1))
                                     blockchain1))))
  (b* ((cert (pick-successor/predecessor dag1 dag2 cert1 cert2)))
    (and (in cert (successors cert1 dag1))
         (in cert (predecessors cert2 dag2))
         (in cert dag1)
         (in cert dag2)))))