		Search-engine friendly clone of the ACL2 documentation.

Transitions-create-certificate

Create-certificate-author-possiblep

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

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

The input cert of this function is the certificate in the create-certificate 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-certificate-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-certificate-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 number of endorsers must be one less than the quorum, so that, with the author, there is a quorum of signatures. The aforementioned distinctness of the author from the endorsers ensures that they indeed form a quorum, i.e. that the author adds one to the quorum minus one.

The role of the all-vals input is explained in update-committee-with-transaction.

Definitions and Theorems

Function: create-certificate-author-possiblep

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

Theorem: booleanp-of-create-certificate-author-possiblep

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

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

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

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

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

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

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

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

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

Theorem: create-certificate-author-possiblep-of-address-set-fix-all-vals

(defthm
    create-certificate-author-possiblep-of-address-set-fix-all-vals
 (equal (create-certificate-author-possiblep
             cert vstate (address-set-fix all-vals))
        (create-certificate-author-possiblep cert vstate all-vals)))

Theorem: create-certificate-author-possiblep-address-set-equiv-congruence-on-all-vals

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