		Search-engine friendly clone of the ACL2 documentation.

Transitions-create-certificate

Create-certificate-possiblep

Check if a create-certificate event is possible.

Signature
(create-certificate-possiblep cert systate) → yes/no
Arguments: cert — Guard (certificatep cert).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

The author of the certificate must be a validator in the system. The validator may be correct or faulty: nothing prevents a faulty validator from creating a good certificate signed by enough validators.

If the author is a correct validator, the round of the certificate must be the validator's current round. Correct validators always create certificates for their current round. If the author is a faulty validator, there is no such requirement: we make no assumptions on the internal state of a faulty validator. But note that the round cannot be completely arbitrary, because of some of the additional requirements, explained below.

There are no requirements on the transanctions, which we treat as opaque in our model, as explained in transactions.

The number of previous certificates must be N - F (where F is introduced in max-faulty-for-total), unless the round number is 1, in which case there must be no previous certificates.

The endorsers of the certificate must be validators of the system. They may be correct or faulty validators: nothing prevents a faulty validator from endorsing a certificate with a good signature.

The endorsers of the certificate must differ from the author. The author also signs the certificate, but the endorsers component of certificate only models the signers that differ from the author. Author and endorsers together form all the signers, returned by certificate->signers.

There must be N - F - 1 endorsers for the certificate (where F is introduced in max-faulty-for-total), which together with the validator itself makes N - F signers.

If the author is a correct validator, it must not already have, in its DAG, a certificate with the same author and round number: correct validators create at most one certificate per round. Additionally, each endorser that is a correct validator must not have, in its DAG or buffer, any certificate with the same author and round number, and must also not have alredy signed a proposal with the same author and round number; otherwise, the validator would not have signed this certificate. There are no such requirements on faulty authors and endorsers, because we make no assumptions on their internal states, and nothing prevents them from signing with good signatures. We use signers-do-not-have-author+round-p to check these conditions, treating all signers (author and endorsers) uniformly; for the author, it would suffice to check the DAG, but it makes no difference to also check the buffer and the signed author-round pairs.

If the author is a correct validator, it must have, in the DAG, all the previous certificates; if it did not, it would not create the new certificate. Similarly, for each endorser that is a correct validator, that endorser's DAG must have all the previous certificates; if they did not, they would not sign the certificate. There are no such requirements on faulty author and signers, because we make no assumptions on their internal states, and nothing prevents them from signing with good signatures. We use the signers-have-previous-certificates-p to check these conditions, treating all signers (author and endorsers) uniformly.

Since it is an invariant (proved elsewhere) that all the authors of certificates in DAGs are validators in the system, the requirement described in the previous paragraph implies that the addresses of the authors of the previous certificates of cert are addresses of validators in the system.

Definitions and Theorems

Function: create-certificate-possiblep

(defun create-certificate-possiblep (cert systate)
  (declare (xargs :guard (and (certificatep cert)
                              (system-statep systate))))
  (let ((__function__ 'create-certificate-possiblep))
    (declare (ignorable __function__))
    (b* (((certificate cert) cert)
         ((unless (in cert.author (all-addresses systate)))
          nil)
         (vstate (get-validator-state cert.author systate))
         ((unless (or (not vstate)
                      (equal cert.round
                             (validator-state->round vstate))))
          nil)
         ((unless (if (equal cert.round 1)
                      (emptyp cert.previous)
                    (= (cardinality cert.previous)
                       (quorum systate))))
          nil)
         ((unless (subset cert.endorsers (all-addresses systate)))
          nil)
         ((when (in cert.author cert.endorsers))
          nil)
         ((unless (= (cardinality cert.endorsers)
                     (1- (quorum systate))))
          nil)
         (signers (certificate->signers cert))
         ((unless (signers-do-not-have-author+round-p
                       signers cert.author cert.round systate))
          nil)
         ((unless (signers-have-previous-certificates-p
                       signers
                       cert.previous cert.round systate))
          nil))
      t)))

Theorem: booleanp-of-create-certificate-possiblep

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

Theorem: create-certificate-possiblep-of-system-state-fix-systate

(defthm create-certificate-possiblep-of-system-state-fix-systate
 (equal
      (create-certificate-possiblep cert (system-state-fix systate))
      (create-certificate-possiblep cert systate)))

Theorem: create-certificate-possiblep-system-state-equiv-congruence-on-systate

(defthm
 create-certificate-possiblep-system-state-equiv-congruence-on-systate
 (implies (system-state-equiv systate systate-equiv)
          (equal (create-certificate-possiblep cert systate)
                 (create-certificate-possiblep cert systate-equiv)))
 :rule-classes :congruence)

Theorem: no-author-dag-certificate-when-create-certificate-possiblep

(defthm no-author-dag-certificate-when-create-certificate-possiblep
 (implies
      (and (create-certificate-possiblep cert systate)
           (in (certificate->author cert)
               (correct-addresses systate)))
      (not (certificate-with-author+round
                (certificate->author cert)
                (certificate->round cert)
                (validator-state->dag
                     (get-validator-state (certificate->author cert)
                                          systate))))))