		Search-engine friendly clone of the ACL2 documentation.

System-states

Update-validator-state

Update the state of a correct validator in the system.

Signature
(update-validator-state val vstate systate) → new-systate
Arguments: val — Guard (addressp val).; vstate — Guard (validator-statep vstate).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

The name of this function, which only operates on correct validators, is not completely parallel with get-validator-state, which may retrieve the nil state of a faulty validator. But we prefer the shorter name to update-correct-validator-state.

Definitions and Theorems

Function: update-validator-state

(defun update-validator-state (val vstate systate)
  (declare (xargs :guard (and (addressp val)
                              (validator-statep vstate)
                              (system-statep systate))))
  (declare (xargs :guard (in val (correct-addresses systate))))
  (let ((__function__ 'update-validator-state))
    (declare (ignorable __function__))
    (b* ((vstates (system-state->validators systate))
         (new-vstates (omap::update val vstate vstates)))
      (change-system-state systate
                           :validators new-vstates))))

Theorem: system-statep-of-update-validator-state

(defthm system-statep-of-update-validator-state
  (b* ((new-systate (update-validator-state val vstate systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: update-validator-state-of-system-state-fix-systate

(defthm update-validator-state-of-system-state-fix-systate
 (equal
      (update-validator-state val vstate (system-state-fix systate))
      (update-validator-state val vstate systate)))

Theorem: update-validator-state-system-state-equiv-congruence-on-systate

(defthm
    update-validator-state-system-state-equiv-congruence-on-systate
 (implies (system-state-equiv systate systate-equiv)
          (equal (update-validator-state val vstate systate)
                 (update-validator-state val vstate systate-equiv)))
 :rule-classes :congruence)

Theorem: all-addresses-of-update-validator-state

(defthm all-addresses-of-update-validator-state
 (implies
    (and (in val (all-addresses systate))
         (validator-statep vstate))
    (b* ((?new-systate (update-validator-state val vstate systate)))
      (equal (all-addresses new-systate)
             (all-addresses systate)))))

Theorem: correct-addresses-of-update-validator-state

(defthm correct-addresses-of-update-validator-state
 (implies
    (and (in val (correct-addresses systate))
         (validator-statep vstate))
    (b* ((?new-systate (update-validator-state val vstate systate)))
      (equal (correct-addresses new-systate)
             (correct-addresses systate)))))

Theorem: get-validator-state-of-update-validator-state

(defthm get-validator-state-of-update-validator-state
  (implies (and (in val1 (correct-addresses systate))
                (validator-statep vstate))
           (equal (get-validator-state
                       val
                       (update-validator-state val1 vstate systate))
                  (if (equal val val1)
                      vstate
                    (get-validator-state val systate)))))

Theorem: get-validator-state-of-update-validator-state-same

(defthm get-validator-state-of-update-validator-state-same
 (implies
  (and (in val (correct-addresses systate))
       (validator-statep vstate))
  (equal
   (get-validator-state val
                        (update-validator-state val vstate systate))
   vstate)))

Theorem: get-validator-state-of-update-validator-state-diff

(defthm get-validator-state-of-update-validator-state-diff
  (implies (and (in val1 (correct-addresses systate))
                (not (equal val val1))
                (validator-statep vstate))
           (equal (get-validator-state
                       val
                       (update-validator-state val1 vstate systate))
                  (get-validator-state val systate))))