		Search-engine friendly clone of the ACL2 documentation.

Transitions-create

Create-endorsers-possiblep

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

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

An endorser may be correct or faulty. If it is correct, it must satisfy the conditions formalized in create-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, and checked by this predicate, imply at least some agreement among the blockchains of the validators, enough to make consistent checks involving the committee. As proved elsewhere, 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 event do not impose any more agreement requirements than already implied by the invariants. As already observed in create-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.

Definitions and Theorems

Function: create-endorsers-possiblep-loop

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

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

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

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

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

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

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

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

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

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

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

Theorem: create-endorser-possiblep-when-create-endorsers-possiblep-loop

(defthm
     create-endorser-possiblep-when-create-endorsers-possiblep-loop
  (implies
       (and (create-endorsers-possiblep-loop cert endorsers systate)
            (in endorser endorsers)
            (in endorser (correct-addresses systate)))
       (create-endorser-possiblep
            cert
            (get-validator-state endorser systate))))

Function: create-endorsers-possiblep

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

Theorem: booleanp-of-create-endorsers-possiblep

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

Theorem: create-endorser-possiblep-when-create-endorsers-possiblep

(defthm create-endorser-possiblep-when-create-endorsers-possiblep
  (implies (and (create-endorsers-possiblep cert systate)
                (in endorser (certificate->endorsers cert))
                (in endorser (correct-addresses systate)))
           (create-endorser-possiblep
                cert
                (get-validator-state endorser systate))))

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

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

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

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

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

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

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

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