		Search-engine friendly clone of the ACL2 documentation.

Transitions-create

Create-possiblep

Check if a certificate creation event is possible.

Signature
(create-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 event; see event.

If the author is correct, the conditions in create-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-endorsers-possiblep must also hold, which only actually constrain correct 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.

Note that there are no constraints on the addresses of faulty signers (author or endorsers). Recall that our model of system states only explicitly includes correct validators, whose addresses are the ones in correct-addresses.

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

Definitions and Theorems

Function: create-possiblep

(defun create-possiblep (cert systate)
 (declare (xargs :guard (and (certificatep cert)
                             (system-statep systate))))
 (let ((__function__ 'create-possiblep))
   (declare (ignorable __function__))
   (b*
     (((certificate cert) cert)
      ((unless (or (not (in cert.author
                            (correct-addresses systate)))
                   (create-author-possiblep
                        cert
                        (get-validator-state cert.author systate))))
       nil)
      ((unless (create-endorsers-possiblep cert systate))
       nil))
     t)))

Theorem: booleanp-of-create-possiblep

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

Theorem: author-quorum-when-create-possiblep

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

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

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

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

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

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

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

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

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