		Search-engine friendly clone of the ACL2 documentation.

Transitions-create-certificate

Create-certificate-endorsers-possiblep

Check if a certificate creation event is possible, from the point of view of all the certificate's endorsers.

Signature
(create-certificate-endorsers-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.

An endorser may be correct or faulty. If it is correct, it must satisfy the conditions formalized in create-certificate-endorser-possiblep. If it is faulty, it is not bound by any condition.

Note that, if there are (as normal) multiple correct endorsers, the conditions involving committees as viewed by the endorsers imply at least some agreement among the blockchains of the validators, enough to make consistent checks involving the committee. As proved in same-committees, it is a system invariant that different validators agree on the committees they can both calculate, because of the invariant that blockchains never fork. Thus, in each state, which satisfies the invariant, starting with an initial state, the conditions on the possibility of a create-certificate event do not impose any more agreement requirements than already implied by the invariants. As already observed in create-certificate-signer-possiblep, all of this can be made even more clear and persuasive in a planned more detailed model of AleoBFT that includes explicit proposal and signature exchanges.

Note that we instantiate the all-vals parameter of create-certificate-endorser-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.

Definitions and Theorems

Function: create-certificate-endorsers-possiblep-loop

(defun create-certificate-endorsers-possiblep-loop
       (cert endorsers systate)
  (declare (xargs :guard (and (certificatep cert)
                              (address-setp endorsers)
                              (system-statep systate))))
  (let ((__function__ 'create-certificate-endorsers-possiblep-loop))
    (declare (ignorable __function__))
    (b* (((when (emptyp endorsers)) t)
         (endorser (head endorsers))
         ((unless (in endorser (correct-addresses systate)))
          (create-certificate-endorsers-possiblep-loop
               cert (tail endorsers)
               systate))
         ((unless (create-certificate-endorser-possiblep
                       cert
                       (get-validator-state endorser systate)
                       (all-addresses systate)))
          nil))
      (create-certificate-endorsers-possiblep-loop
           cert (tail endorsers)
           systate))))

Theorem: booleanp-of-create-certificate-endorsers-possiblep-loop

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

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

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

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

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

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

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

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

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

Function: create-certificate-endorsers-possiblep

(defun create-certificate-endorsers-possiblep (cert systate)
  (declare (xargs :guard (and (certificatep cert)
                              (system-statep systate))))
  (let ((__function__ 'create-certificate-endorsers-possiblep))
    (declare (ignorable __function__))
    (create-certificate-endorsers-possiblep-loop
         cert (certificate->endorsers cert)
         systate)))

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

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

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

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

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

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

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

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

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

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