		Search-engine friendly clone of the ACL2 documentation.

Quorum-intersection

Pick-common-correct-validator

Pick a common correct validator address from two sets of addresses.

Signature
(pick-common-correct-validator vals1 vals2 systate) → val?
Arguments: vals1 — Guard (address-setp vals1).; vals2 — Guard (address-setp vals2).; systate — Guard (system-statep systate).
Returns: val? — Type (address-optionp val?).

This is just pick-correct-validator applied to the intersection of the two sets. The significance of this is that, as explained in quorum-intersection, we want to intersect two quora (represented by vals1 and vals2 here), and pick a correct validator common to the two sets.

Definitions and Theorems

Function: pick-common-correct-validator

(defun pick-common-correct-validator (vals1 vals2 systate)
  (declare (xargs :guard (and (address-setp vals1)
                              (address-setp vals2)
                              (system-statep systate))))
  (let ((__function__ 'pick-common-correct-validator))
    (declare (ignorable __function__))
    (pick-correct-validator (intersect vals1 vals2)
                            systate)))

Theorem: address-optionp-of-pick-common-correct-validator

(defthm address-optionp-of-pick-common-correct-validator
  (b* ((val? (pick-common-correct-validator vals1 vals2 systate)))
    (address-optionp val?))
  :rule-classes :rewrite)

Theorem: pick-common-correct-validator-of-system-state-fix-systate

(defthm pick-common-correct-validator-of-system-state-fix-systate
  (equal (pick-common-correct-validator
              vals1 vals2 (system-state-fix systate))
         (pick-common-correct-validator vals1 vals2 systate)))

Theorem: pick-common-correct-validator-system-state-equiv-congruence-on-systate

(defthm
 pick-common-correct-validator-system-state-equiv-congruence-on-systate
 (implies
  (system-state-equiv systate systate-equiv)
  (equal (pick-common-correct-validator vals1 vals2 systate)
         (pick-common-correct-validator vals1 vals2 systate-equiv)))
 :rule-classes :congruence)