		Search-engine friendly clone of the ACL2 documentation.

Transitions-create-certificate

Create-certificate-endorser-possiblep

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

Signature
(create-certificate-endorser-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 an endorser of the certificate. See the (indirect) callers of this function.

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

Recall that, as noted in create-certificate-signer-possiblep, an endorser does not have access to the endorser addresses component of a certificate, because it only sees the proposal.

While create-certificate-signer-possiblep checks that the DAG has no certificate already with the same author and round, which is sufficient for the author to check, an endorser must check more than that: the buffer of the endorser must not contain a certificate with the same author and round; and the set of endorsed author-round pairs does not already contain the author-round pair of the certificate. The presence of a pair in this set indicates that the validators has already endorsed a certificate with that author and round, but has not yet received the actual certificate from the network.

For the certificate author, in create-certificate-author-possiblep, it is not necessary to check the buffer and author-round pairs: as proved in no-self-buffer, a validator never has a certificate authored by itself in the buffer, or an author-round pair whose author component is the validator's address. So it suffices to check the DAG for the author.

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

Definitions and Theorems

Function: create-certificate-endorser-possiblep

(defun create-certificate-endorser-possiblep (cert vstate all-vals)
 (declare (xargs :guard (and (certificatep cert)
                             (validator-statep vstate)
                             (address-setp all-vals))))
 (let ((__function__ 'create-certificate-endorser-possiblep))
  (declare (ignorable __function__))
  (b*
   (((certificate cert) cert)
    ((validator-state vstate) vstate)
    ((unless
         (create-certificate-signer-possiblep cert vstate all-vals))
     nil)
    ((when (certificate-with-author+round
                cert.author cert.round vstate.buffer))
     nil)
    ((when (in (make-address+pos :address cert.author
                                 :pos cert.round)
               vstate.endorsed))
     nil))
   t)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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