		Search-engine friendly clone of the ACL2 documentation.

Transitions-receive-certificate

Receive-certificate-possiblep

Check if a receive-certificate event is possible.

Signature
(receive-certificate-possiblep msg systate) → yes/no
Arguments: msg — Guard (messagep msg).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

The message must be present in the network, and the destination must be a correct validator. The latter condition is an invariant of the system, but we state it explicitly here because we put no requirements on the system state passed to this function. That and other invariants are formulated and proved elsewhere.

Definitions and Theorems

Function: receive-certificate-possiblep

(defun receive-certificate-possiblep (msg systate)
  (declare (xargs :guard (and (messagep msg)
                              (system-statep systate))))
  (let ((__function__ 'receive-certificate-possiblep))
    (declare (ignorable __function__))
    (and (in msg (get-network-state systate))
         (in (message->destination msg)
             (correct-addresses systate)))))

Theorem: booleanp-of-receive-certificate-possiblep

(defthm booleanp-of-receive-certificate-possiblep
  (b* ((yes/no (receive-certificate-possiblep msg systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: receive-certificate-possiblep-of-system-state-fix-systate

(defthm receive-certificate-possiblep-of-system-state-fix-systate
 (equal
      (receive-certificate-possiblep msg (system-state-fix systate))
      (receive-certificate-possiblep msg systate)))

Theorem: receive-certificate-possiblep-system-state-equiv-congruence-on-systate

(defthm
 receive-certificate-possiblep-system-state-equiv-congruence-on-systate
 (implies (system-state-equiv systate systate-equiv)
          (equal (receive-certificate-possiblep msg systate)
                 (receive-certificate-possiblep msg systate-equiv)))
 :rule-classes :congruence)