		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).

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 (address-fix val)
                                    (validator-state-fix 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: all-addresses-of-update-validator-state

(defthm all-addresses-of-update-validator-state
 (implies
    (in (address-fix val)
        (correct-addresses systate))
    (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
    (in (address-fix val)
        (correct-addresses systate))
    (b* ((?new-systate (update-validator-state val vstate systate)))
      (equal (correct-addresses new-systate)
             (correct-addresses systate)))))

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

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

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

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

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

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

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

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

Theorem: update-validator-state-of-address-fix-val

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

Theorem: update-validator-state-address-equiv-congruence-on-val

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

Theorem: update-validator-state-of-validator-state-fix-vstate

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

Theorem: update-validator-state-validator-state-equiv-congruence-on-vstate

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

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)