		Search-engine friendly clone of the ACL2 documentation.

Transitions-accept

Accept-possiblep

Check if a certificate acceptance event is possible.

Signature
(accept-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 accept event; see event.

The messages must be in the network.

The destination must be a correct 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.

The certificate's signers must form a quorum in the active committee for the certificate's round, of which they must be members. Thus, the validator must be able to calculate (from its blockchain) the committee for the certificate's round, in order to perform the check. This check is important because, in our formal model, nothing prevents the creation of a new certificate with signers completely disjoint from the validator's committee; these would have to be faulty signers, but it can still happen. So this bad certificate could very well cause equivocation, if a validator blindly accepted it. Instead, by having the receiving validator check the signers, we avoid that, as proved elsewhere.

If the certificate's round number is 1, there is no requirement on the previous certificates, because there are no previous certificates. Otherwise, we obtain the certificates in the DAG at the previous round, and we check that their authors contain the addresses in the previous component of the certificate.

Definitions and Theorems

Function: accept-possiblep

(defun accept-possiblep (msg systate)
 (declare (xargs :guard (and (messagep msg)
                             (system-statep systate))))
 (let ((__function__ 'accept-possiblep))
   (declare (ignorable __function__))
   (b*
     (((unless (in (message-fix msg)
                   (get-network-state systate)))
       nil)
      (dest (message->destination msg))
      ((unless (in dest (correct-addresses systate)))
       nil)
      ((validator-state vstate)
       (get-validator-state dest systate))
      ((certificate cert)
       (message->certificate msg))
      (commtt
           (active-committee-at-round cert.round vstate.blockchain))
      ((unless commtt) nil)
      (signers (certificate->signers cert))
      ((unless (subset signers (committee-members commtt)))
       nil)
      ((unless (>= (committee-members-stake signers commtt)
                   (committee-quorum-stake commtt)))
       nil)
      ((when (= cert.round 1)) t)
      ((unless (subset cert.previous
                       (certificate-set->author-set
                            (certs-with-round (1- cert.round)
                                              vstate.dag))))
       nil))
     t)))

Theorem: booleanp-of-accept-possiblep

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

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

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

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

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

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

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

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

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