		Search-engine friendly clone of the ACL2 documentation.

Successor-predecessor-intersection

Pick-successor/predecessor

Pick a certificate in the successor-predecessor intersection.

Signature
(pick-successor/predecessor dag1 dag2 cert1 cert2) → cert?
Arguments: dag1 — Guard (certificate-setp dag1).; dag2 — Guard (certificate-setp dag2).; cert1 — Guard (certificatep cert1).; cert2 — Guard (certificatep cert2).
Returns: cert? — Type (certificate-optionp cert?).

We pick the first one, but the exact choice does not matter. We show that, under the assumptions in not-empty-successor-predecessor-intersection, this function returns a certificate that is in the successors, in the predecessors, and in both DAGs.

Definitions and Theorems

Function: pick-successor/predecessor

(defun pick-successor/predecessor (dag1 dag2 cert1 cert2)
 (declare (xargs :guard (and (certificate-setp dag1)
                             (certificate-setp dag2)
                             (certificatep cert1)
                             (certificatep cert2))))
 (declare
      (xargs :guard (and (in cert1 dag1)
                         (in cert2 dag2)
                         (equal (certificate->round cert2)
                                (+ 2 (certificate->round cert1))))))
 (let ((__function__ 'pick-successor/predecessor))
   (declare (ignorable __function__))
   (b* ((common (intersect (successors cert1 dag1)
                           (predecessors cert2 dag2))))
     (if (emptyp common)
         nil
       (head common)))))

Theorem: certificate-optionp-of-pick-successor/predecessor

(defthm certificate-optionp-of-pick-successor/predecessor
  (b* ((cert? (pick-successor/predecessor dag1 dag2 cert1 cert2)))
    (certificate-optionp cert?))
  :rule-classes :rewrite)

Theorem: pick-successor/predecessor-in-successors

(defthm pick-successor/predecessor-in-successors
  (implies (pick-successor/predecessor dag1 dag2 cert1 cert2)
           (in (pick-successor/predecessor dag1 dag2 cert1 cert2)
               (successors cert1 dag1))))

Theorem: pick-successor/predecessor-in-predecessors

(defthm pick-successor/predecessor-in-predecessors
  (implies (pick-successor/predecessor dag1 dag2 cert1 cert2)
           (in (pick-successor/predecessor dag1 dag2 cert1 cert2)
               (predecessors cert2 dag2))))

Theorem: pick-successor/predecessor-in-dag1

(defthm pick-successor/predecessor-in-dag1
  (implies (and (certificate-setp dag1)
                (pick-successor/predecessor dag1 dag2 cert1 cert2))
           (in (pick-successor/predecessor dag1 dag2 cert1 cert2)
               dag1)))

Theorem: pick-successor/predecessor-in-dag2

(defthm pick-successor/predecessor-in-dag2
  (implies (and (certificate-setp dag2)
                (pick-successor/predecessor dag1 dag2 cert1 cert2))
           (in (pick-successor/predecessor dag1 dag2 cert1 cert2)
               dag2)))

Theorem: pick-successor/predecessor-not-nil

(defthm pick-successor/predecessor-not-nil
 (implies
      (and (certificate-setp dag1)
           (certificate-setp dag2)
           (certificate-set-unequivocalp dag1)
           (certificate-set-unequivocalp dag2)
           (certificate-sets-unequivocalp dag1 dag2)
           (equal (certificate->round cert2)
                  (+ 2 (certificate->round cert1)))
           (subset (cert-set->author-set (successors cert1 dag1))
                   (committee-members commtt))
           (subset (cert-set->author-set (predecessors cert2 dag2))
                   (committee-members commtt))
           (> (committee-members-stake
                   (cert-set->author-set (successors cert1 dag1))
                   commtt)
              (committee-max-faulty-stake commtt))
           (>= (committee-members-stake
                    (cert-set->author-set (predecessors cert2 dag2))
                    commtt)
               (committee-quorum-stake commtt)))
      (pick-successor/predecessor dag1 dag2 cert1 cert2)))