		Search-engine friendly clone of the ACL2 documentation.

Transitions-create

Create-endorser-possiblep

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

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

In addition to the conditions formalized in create-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-signer-possiblep, an endorser does not have access to the endorser addresses component of a certificate, because it only sees the proposal.

While create-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 also check that 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 validator has already endorsed a certificate with that author and round, but has not yet received the actual certificate from the network, and incorporated it into its own DAG. This check is not needed for the author, because it is an invariant, proved elsewhere, that the set of endorsed author-round pairs does not contain any pair with the validator as author.

Definitions and Theorems

Function: create-endorser-possiblep

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

Theorem: booleanp-of-create-endorser-possiblep

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

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

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

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

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

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

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

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

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