		Search-engine friendly clone of the ACL2 documentation.

Transitions-create-certificate

Create-certificate-signer-possiblep

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

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

A certificate is signed by author and endorsers, so the signers are the author and the endorsers; see certificate->signers. A correct (i.e. non-faulty) signer, whether author or endorser, signs a certificate only if certain conditions are met; these conditions are checked against the signer's state. This ACL2 function formalizes the conditions that are common to author and endorsers, i.e. signers in general. Further conditions for the author are formalized in create-certificate-author-possiblep; further conditions for the endorsers are formalized in create-certificate-endorser-possiblep.

The endorsers only see the proposal, not the whole certificate, so in our model they can only check conditions on the certificate components except the endorser addresses; even though we model certificate creation as an atomic event, we still need to model the right checks at the right times. As a consequence, this predicate only checks conditions on the certificate components except the endorser addresses, since it applies to all signers.

The first condition is that the signer must be able to calculate the active committee at the certificate's round. That is, its local blockchain must be sufficiently far along. If the validator cannot calculate the active committee, it is unable to author or endorse a certificate for that round, so this event cannot happen from the point of view of the validator.

That committee is used to check that the author of the certificate is a member of the committee: only validators in the active committee for a round can create certificates for that round. In the case of the certificate's author, this condition corresponds to the fact that a (correct) author would generate a certificate only if the author knows to be in the active committee. In the case of an endorser, this condition represents a check made by the endorser on the proposal.

The DAG of the signer must not already have a certificate with the given author and round. This is to prevent equivocation, i.e. the existence of two different certificates with the same author and round. Further conditions about this apply to endorsers, but here we are defining conditions common to author and endorsers.

If the round of the certificate is 1, it must have no references to previous certificates, because there is no round 0. If the round of the certificate is not 1, the following additional requirements apply.

The signer's DAG must include all the previous certificates referenced by the certificate. These are the certificates at the round just before the certificate's round whose authors are in the previous component of the certificate. We express this condition by saying that the authors of all the certificates at the round before the certificate are a superset of the authors in the previous component. When the signer is the author, this condition serves to ensure the backward closure of the DAG, i.e. that if the DAG includes a certificate, it also includes all its predecessors. When the signer is an endorser, this condition corresponds to the fact that, before endorsing a certificate from another validator, a validator checks it against the predecessors (something not explicit in our model), and therefore the validator must have those predecessors in the DAG.

The referenced certificates in the previous round must form a quorum. However, note that the active committee of the previous round may differ from the one of the certificate's round. Since we already checked that the active committee of the certificate round is known to the signer whose conditions we are checking, it follows that the active committee at the previous round is also known, as proved in active-committee-at-round.

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

Definitions and Theorems

Function: create-certificate-signer-possiblep

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

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

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

Theorem: active-committee-at-round-when-create-certificate-signer-possiblep

(defthm
 active-committee-at-round-when-create-certificate-signer-possiblep
 (implies
     (create-certificate-signer-possiblep cert vstate all-vals)
     (active-committee-at-round (certificate->round cert)
                                (validator-state->blockchain vstate)
                                all-vals))
 :rule-classes :forward-chaining)

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

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

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

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

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

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

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

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

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

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

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

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