		Search-engine friendly clone of the ACL2 documentation.

Transitions-timer-expires

Timer-expires-possiblep

Check if a timer-expires event is possible.

Signature
(timer-expires-possiblep val systate) → yes/no
Arguments: val — Guard (addressp val).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

The val input of this function is the address in the timer-expires event; see event.

The validator must be a correct one. We only model round advancement in correct validators. Faulty validators have no internal state in our model.

The timer of the validator must be running.

Definitions and Theorems

Function: timer-expires-possiblep

(defun timer-expires-possiblep (val systate)
  (declare (xargs :guard (and (addressp val)
                              (system-statep systate))))
  (let ((__function__ 'timer-expires-possiblep))
    (declare (ignorable __function__))
    (b* (((unless (in (address-fix val)
                      (correct-addresses systate)))
          nil)
         ((validator-state vstate)
          (get-validator-state val systate)))
      (timer-case vstate.timer :running))))

Theorem: booleanp-of-timer-expires-possiblep

(defthm booleanp-of-timer-expires-possiblep
  (b* ((yes/no (timer-expires-possiblep val systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: timer-expires-possiblep-of-address-fix-val

(defthm timer-expires-possiblep-of-address-fix-val
  (equal (timer-expires-possiblep (address-fix val)
                                  systate)
         (timer-expires-possiblep val systate)))

Theorem: timer-expires-possiblep-address-equiv-congruence-on-val

(defthm timer-expires-possiblep-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (timer-expires-possiblep val systate)
                  (timer-expires-possiblep val-equiv systate)))
  :rule-classes :congruence)

Theorem: timer-expires-possiblep-of-system-state-fix-systate

(defthm timer-expires-possiblep-of-system-state-fix-systate
  (equal (timer-expires-possiblep val (system-state-fix systate))
         (timer-expires-possiblep val systate)))

Theorem: timer-expires-possiblep-system-state-equiv-congruence-on-systate

(defthm
   timer-expires-possiblep-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (timer-expires-possiblep val systate)
                  (timer-expires-possiblep val systate-equiv)))
  :rule-classes :congruence)