		Search-engine friendly clone of the ACL2 documentation.

System-states

Correct-addresses

Set of the addresses of all the correct validators in the system.

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

These are the keys in the map, which only includes correct validators, as explained in validators-state.

Definitions and Theorems

Function: correct-addresses

(defun correct-addresses (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'correct-addresses))
    (declare (ignorable __function__))
    (omap::keys (system-state->validators systate))))

Theorem: address-setp-of-correct-addresses

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

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

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

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

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