		Search-engine friendly clone of the ACL2 documentation.

Transitions-receive

Receive-possiblep

Check if a certificate receipt event is possible.

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

The input msg of this function is the message in the receive event; see event.

The messages must be in the network.

The destination must be a validator in the system. Recall that, as explained in create-next, in our model certificates are broadcast to all validators, not just the ones in the committee.

Definitions and Theorems

Function: receive-possiblep

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

Theorem: booleanp-of-receive-possiblep

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

Theorem: receive-possiblep-of-message-fix-msg

(defthm receive-possiblep-of-message-fix-msg
  (equal (receive-possiblep (message-fix msg)
                            systate)
         (receive-possiblep msg systate)))

Theorem: receive-possiblep-message-equiv-congruence-on-msg

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

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

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

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

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