		Search-engine friendly clone of the ACL2 documentation.

Transitions-receive-certificate

Receive-certificate-possiblep

Check if a certificate receipt 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 input msg of this function is the message in the receive-certificate 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-certificate-next, in our model certificates are broadcast to all validators, not just the ones in the committee.

We actually make the stronger check that the validator is a correct one. This is in fact an invariant, because create-certificate-next only creates messages with addresses of correct validators as destination. But we do not have that invariant available here, since we prove that from the definitions of the transitions, which therefore must be defined before we can prove the invariant.

The validator must be able to calculate the active committee for the certificate's round, and the signers of the certificate must form a quorum.

If the certificate's round is 1, the certificate must have no references to previous certificates.

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__))
  (b*
   (((unless (in (message-fix msg)
                 (get-network-state systate)))
     nil)
    (dest (message->destination msg))
    ((certificate cert)
     (message->certificate msg))
    ((unless (in dest (correct-addresses systate)))
     nil)
    (vstate (get-validator-state dest systate))
    (commtt
     (active-committee-at-round cert.round
                                (validator-state->blockchain vstate)
                                (all-addresses systate)))
    ((unless commtt) nil)
    (signers (certificate->signers cert))
    ((unless (subset signers (committee-members commtt)))
     nil)
    ((unless (= (cardinality signers)
                (committee-quorum commtt)))
     nil))
   (if (= cert.round 1)
       (= (cardinality cert.previous) 0)
     (b* ((prev-commtt (active-committee-at-round
                            (1- cert.round)
                            (validator-state->blockchain vstate)
                            (all-addresses systate))))
       (and prev-commtt
            (subset cert.previous
                    (committee-members prev-commtt))
            (= (cardinality cert.previous)
               (committee-quorum prev-commtt))))))))

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-message-fix-msg

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

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

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

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)