		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 with an associated non-nil (i.e. correct) validator state.

Definitions and Theorems

Function: correct-addresses-loop

(defun correct-addresses-loop (vstates)
 (declare (xargs :guard (validators-statep vstates)))
 (let ((__function__ 'correct-addresses-loop))
  (declare (ignorable __function__))
  (b* (((when (omap::emptyp vstates)) nil)
       ((mv addr vstate) (omap::head vstates)))
   (if vstate (insert (address-fix addr)
                      (correct-addresses-loop (omap::tail vstates)))
     (correct-addresses-loop (omap::tail vstates))))))

Theorem: address-setp-of-correct-addresses-loop

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

Theorem: correct-addresses-loop-subset

(defthm correct-addresses-loop-subset
  (implies (validators-statep vstates)
           (b* ((?addrs (correct-addresses-loop vstates)))
             (subset addrs (omap::keys vstates)))))

Theorem: in-of-correct-addresses-loop

(defthm in-of-correct-addresses-loop
  (implies
       (validators-statep vstates)
       (equal (in val (correct-addresses-loop vstates))
              (and (omap::assoc val vstates)
                   (validator-statep (omap::lookup val vstates))))))

Theorem: correct-addresses-loop-of-update

(defthm correct-addresses-loop-of-update
 (implies
  (and (validators-statep vstates)
       (addressp val)
       (validator-state-optionp vstate?))
  (equal (correct-addresses-loop (omap::update val vstate? vstates))
         (cond ((validator-statep vstate?)
                (insert val (correct-addresses-loop vstates)))
               ((in val (correct-addresses-loop vstates))
                (delete val (correct-addresses-loop vstates)))
               (t (correct-addresses-loop vstates))))))

Function: correct-addresses

(defun correct-addresses (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'correct-addresses))
    (declare (ignorable __function__))
    (correct-addresses-loop (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-subset

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

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)