		Search-engine friendly clone of the ACL2 documentation.

Transitions-create-certificate

Create-certificate-possiblep

Check if a certificate creation 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 input cert of this function is the certificate in the create-certificate event; see event.

Author and endorsers must be in the system. Recall that the system includes all possible validators in all possible committees. More specific checks about author and endorsers being in the committee are formalized in create-certificate-signer-possiblep.

If the author is correct, the conditions in create-certificate-author-possiblep must be satisfied. If the author is faulty, there are no requirements from the author's point of view.

The conditions in create-certificate-endorsers-possiblep must also hold, which may concern correct and faulty endorsers.

Although the author and some endorsers may be faulty, under suitable fault tolerance conditions, there are enough signers to guarantee that the new certificate does not cause equivocation, i.e. does not have the same author and round as an existing certificate. This is proved as the non-equivocation of certificates. Here the fault tolerance conditions has to be stated for each committee.

Note that we instantiate the all-vals parameter of create-certificate-author-possiblep with the set of all the addresses of all validators in the system; that is indeed the rols of all-vals, as explained in update-committee-with-transaction.

If the author of the certificate is correct, then it can calculate the active committees at the certificate's round, and the certificate's signers form a quorum in that committee. This derives from the definition, but provides a way to obtain this fact in proofs without having to open create-certificate-possiblep and some of the functions it calls.

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)
     ((unless (subset cert.endorsers (all-addresses systate)))
      nil)
     ((unless (or (not (in cert.author
                           (correct-addresses systate)))
                  (create-certificate-author-possiblep
                       cert
                       (get-validator-state cert.author systate)
                       (all-addresses systate))))
      nil)
     ((unless (create-certificate-endorsers-possiblep cert 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: author-quorum-when-create-certificate-possiblep

(defthm author-quorum-when-create-certificate-possiblep
 (implies
   (and (in (certificate->author cert)
            (correct-addresses systate))
        (create-certificate-possiblep cert systate))
   (b*
     ((commtt
           (active-committee-at-round
                (certificate->round cert)
                (validator-state->blockchain
                     (get-validator-state (certificate->author cert)
                                          systate))
                (all-addresses systate))))
     (and commtt
          (subset (certificate->signers cert)
                  (committee-members commtt))
          (equal (cardinality (certificate->signers cert))
                 (committee-quorum commtt))))))

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

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

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

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

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)