		Search-engine friendly clone of the ACL2 documentation.

Fault-tolerance

Pick-correct-validator

Pick a correct validator address, if present, from a set of addresses.

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

Correct validators are identified via the system state, so we pass a system state to this function. The correct validators are the keys of the map from addresses to validator states, in the system state.

We go through all the addresses in the set, returning the first one we find that is of a correct validator. We return nil if there is no correct validator address in the set.

We show that if this function returns an address, the address is in the input set, and it is the address of a correct validator. We show that if this function returns nil, then all the addresses are of faulty validators (expressed by saying that they have an empty intersection with the set of correct validators), because otherwise we would have found a correct one.

From the latter fact, we prove that this function will return an address if the following conditions are satisfied: the input set is a subset of a fault-tolerant committee, and the total stake of validators is more than f, i.e. the maximum tolerated stake of faulty validators (see max-faulty-for-total). The reason is that if pick-correct-validator returned nil, then, as proved in all-faulty-when-not-pick-correct-validator, all the validators in vals are faulty. But since we hypothesize that their stake is more than f, and since the fault tolerance hypothesis means that the total stake of faulty validators is no more than f, we have an impossibility. Thus pick-correct-validator must return an address, which, as proved in the other theorems, is in vals and is a correct validator. We use the committee-members-stake-monotone theorem to inject the appropriate facts into the proof. Given that vals is a subset of the committee members, but that vals is disjoint from correct addresses (by all-faulty-when-not-pick-correct-validator, we have that vals is in fact a subset of the committee's faulty members, whose total stake does not exceed f by fault tolerance, and thus the total stake of vals does not exceed f either, which contradicts the hypothesis that it does.

A related fact, which we also prove, is that, if the committee is fault-tolerant and not-empty, and the validators' total stake is at least the quorum, then the function will pick a correct validator. This is a simple consequence of the previous theorem, given that f < n - f when n \neq 0.

Definitions and Theorems

Function: pick-correct-validator

(defun pick-correct-validator (vals systate)
  (declare (xargs :guard (and (address-setp vals)
                              (system-statep systate))))
  (let ((__function__ 'pick-correct-validator))
    (declare (ignorable __function__))
    (b* (((when (emptyp vals)) nil)
         (val (head vals))
         ((when (in val (correct-addresses systate)))
          (address-fix val)))
      (pick-correct-validator (tail vals)
                              systate))))

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

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

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

(defthm pick-correct-validator-of-system-state-fix-systate
  (equal (pick-correct-validator vals (system-state-fix systate))
         (pick-correct-validator vals systate)))

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

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

Theorem: pick-correct-validator-in-set

(defthm pick-correct-validator-in-set
  (implies (pick-correct-validator vals systate)
           (in (pick-correct-validator vals systate)
               vals)))

Theorem: pick-correct-validator-is-correct

(defthm pick-correct-validator-is-correct
  (implies (pick-correct-validator vals systate)
           (in (pick-correct-validator vals systate)
               (correct-addresses systate))))

Theorem: all-faulty-when-not-pick-correct-validator

(defthm all-faulty-when-not-pick-correct-validator
  (implies (not (pick-correct-validator vals systate))
           (emptyp (intersect vals (correct-addresses systate)))))

Theorem: pick-correct-validator-when-fault-tolerant-and-gt-max-faulty

(defthm pick-correct-validator-when-fault-tolerant-and-gt-max-faulty
  (implies (and (address-setp vals)
                (subset vals (committee-members commtt))
                (committee-fault-tolerant-p commtt systate)
                (> (committee-members-stake vals commtt)
                   (committee-max-faulty-stake commtt)))
           (pick-correct-validator vals systate)))

Theorem: pick-correct-validator-when-fault-tolerant-and-geq-quorum

(defthm pick-correct-validator-when-fault-tolerant-and-geq-quorum
  (implies (and (address-setp vals)
                (subset vals (committee-members commtt))
                (committee-fault-tolerant-p commtt systate)
                (committee-nonemptyp commtt)
                (>= (committee-members-stake vals commtt)
                    (committee-quorum-stake commtt)))
           (pick-correct-validator vals systate)))