		Search-engine friendly clone of the ACL2 documentation.

Transitions-create

Create-author-possiblep

Check if a certificate creation event is possible, from the point of view of a correct author.

Signature
(create-author-possiblep cert vstate) → yes/no
Arguments: cert — Guard (certificatep cert).; vstate — Guard (validator-statep vstate).
Returns: yes/no — Type (booleanp yes/no).

The input cert of this function is the certificate in the create event; see event. The input vstate is the state of the validator whose address is the certificate's author. See the (indirect) callers of this function.

In addition to the conditions formalized in create-signer-possiblep, a correct validator authors a certificate if additional conditions are satisfied. This function puts these additional conditions together with the conditions in that function.

Unlike an endorser, an author can check conditions on the endorser addresses component of the certificate. This is because, after generating and sending a proposal, and receiving endorsements, has access to those endorsements, which it can check before creating the certificate.

The round of the certificate must be the current round of the validator. A correct validator only creates (at most) one certificate per round, and does so for the current round every time.

The author must be distinct from the endorsers. This corresponds to the fact that an author sends proposals to, and collects endorsements from, validators other than itself.

Recall that create-signer-possiblep has already checked that the active committee at the certificate's round is known, and that the author is a member of that committee. Here the author also checks that the endorsers are in the committee. This corresponds to the fact that the author accepts endorsements only from members of the committe.

The total stake of the signers must be at least the quorum stake of the active committee for the certificate's round. This is the proper generalization to stake of the analogous condition on number of validators. For the latter, the condition is equality between the number of signers and the quorum number. With stake, the granularity is a whole validator (it either signs or not), and the total stake may not be exactly equal to the quorum stake, because the signers may have arbitrary amounts of stake. So the proper condition with stake is that the quorum stake is an (inclusive) lower bound.

Definitions and Theorems

Function: create-author-possiblep

(defun create-author-possiblep (cert vstate)
 (declare (xargs :guard (and (certificatep cert)
                             (validator-statep vstate))))
 (let ((__function__ 'create-author-possiblep))
   (declare (ignorable __function__))
   (b*
     (((certificate cert) cert)
      ((validator-state vstate) vstate)
      ((unless (create-signer-possiblep cert vstate))
       nil)
      ((unless (= cert.round vstate.round))
       nil)
      ((when (in cert.author cert.endorsers))
       nil)
      (commtt
           (active-committee-at-round cert.round vstate.blockchain))
      ((unless (subset cert.endorsers
                       (committee-members commtt)))
       nil)
      ((unless
            (>= (committee-members-stake (certificate->signers cert)
                                         commtt)
                (committee-quorum-stake commtt)))
       nil))
     t)))

Theorem: booleanp-of-create-author-possiblep

(defthm booleanp-of-create-author-possiblep
  (b* ((yes/no (create-author-possiblep cert vstate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: create-author-possiblep-of-certificate-fix-cert

(defthm create-author-possiblep-of-certificate-fix-cert
  (equal (create-author-possiblep (certificate-fix cert)
                                  vstate)
         (create-author-possiblep cert vstate)))

Theorem: create-author-possiblep-certificate-equiv-congruence-on-cert

(defthm create-author-possiblep-certificate-equiv-congruence-on-cert
  (implies (certificate-equiv cert cert-equiv)
           (equal (create-author-possiblep cert vstate)
                  (create-author-possiblep cert-equiv vstate)))
  :rule-classes :congruence)

Theorem: create-author-possiblep-of-validator-state-fix-vstate

(defthm create-author-possiblep-of-validator-state-fix-vstate
  (equal (create-author-possiblep cert (validator-state-fix vstate))
         (create-author-possiblep cert vstate)))

Theorem: create-author-possiblep-validator-state-equiv-congruence-on-vstate

(defthm
 create-author-possiblep-validator-state-equiv-congruence-on-vstate
 (implies (validator-state-equiv vstate vstate-equiv)
          (equal (create-author-possiblep cert vstate)
                 (create-author-possiblep cert vstate-equiv)))
 :rule-classes :congruence)