		Search-engine friendly clone of the ACL2 documentation.

System-states

Faulty-addresses

Set of the addresses of all the faulty validator in the system.

Signature
(faulty-addresses systate) → addrs
Arguments: systate — Guard (system-statep systate).
Returns: addrs — Type (address-setp addrs).

These are the keys in the map with an associated faulty validator state, or equivalently the difference between the set of all the validator addresses and the set of all the correct validator addresses.

Definitions and Theorems

Function: faulty-addresses

(defun faulty-addresses (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'faulty-addresses))
    (declare (ignorable __function__))
    (difference (all-addresses systate)
                (correct-addresses systate))))

Theorem: address-setp-of-faulty-addresses

(defthm address-setp-of-faulty-addresses
  (b* ((addrs (faulty-addresses systate)))
    (address-setp addrs))
  :rule-classes :rewrite)

Theorem: faulty-addresses-subset-all-addresses

(defthm faulty-addresses-subset-all-addresses
  (subset (faulty-addresses systate)
          (all-addresses systate)))

Theorem: faulty-addresses-of-system-state-fix-systate

(defthm faulty-addresses-of-system-state-fix-systate
  (equal (faulty-addresses (system-state-fix systate))
         (faulty-addresses systate)))

Theorem: faulty-addresses-system-state-equiv-congruence-on-systate

(defthm faulty-addresses-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (faulty-addresses systate)
                  (faulty-addresses systate-equiv)))
  :rule-classes :congruence)