		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-keys

(defthm correct-addresses-loop-subset-keys
  (implies (validators-statep vstates)
           (subset (correct-addresses-loop vstates)
                   (omap::keys vstates))))

Theorem: lookup-nonnil-of-correct-addresses-loop

(defthm lookup-nonnil-of-correct-addresses-loop
  (implies (and (validators-statep vstates)
                (in addr (correct-addresses-loop vstates)))
           (omap::lookup addr vstates))
  :rule-classes (:rewrite :type-prescription))

Theorem: in-of-correct-addresses-loop

(defthm in-of-correct-addresses-loop
  (implies (validators-statep vstates)
           (iff (in addr (correct-addresses-loop vstates))
                (and (omap::assoc addr vstates)
                     (cdr (omap::assoc addr vstates))))))

Theorem: correct-addresses-loop-of-update

(defthm correct-addresses-loop-of-update
 (implies
   (and (addressp val)
        (validator-statep vstate)
        (validators-statep vstates))
   (equal (correct-addresses-loop (omap::update val vstate vstates))
          (if vstate (insert val (correct-addresses-loop vstates))
            (delete val
                    (correct-addresses-loop vstates))))))

Theorem: nil-not-in-correct-addresses-loop

(defthm nil-not-in-correct-addresses-loop
  (not (in nil (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-all-addresses

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

Theorem: correct-addresses-subset-keys-validators

(defthm correct-addresses-subset-keys-validators
  (subset (correct-addresses systate)
          (omap::keys (system-state->validators systate))))

Theorem: in-all-addresses-when-in-correct-addresses

(defthm in-all-addresses-when-in-correct-addresses
  (implies (in val (correct-addresses systate))
           (in val (all-addresses systate))))

Theorem: lookup-nonnil-of-correct-addresses

(defthm lookup-nonnil-of-correct-addresses
  (implies (in addr (correct-addresses systate))
           (omap::lookup addr
                         (system-state->validators systate)))
  :rule-classes (:rewrite :type-prescription))

Theorem: nonempty-all-addresses-when-correct-validator

(defthm nonempty-all-addresses-when-correct-validator
  (implies (in val (correct-addresses systate))
           (not (emptyp (all-addresses systate)))))

Theorem: not-nil-in-correct-addresses

(defthm not-nil-in-correct-addresses
  (not (in nil (correct-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)