		Search-engine friendly clone of the ACL2 documentation.

Transitions-certify

Certify-possiblep

Check if a certify event is possible.

Signature
(certify-possiblep cert dests systate) → yes/no
Arguments: cert — Guard (certificatep cert).; dests — Guard (address-setp dests).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

The cert and dests parameters of this function are the corresponding components of the certify event.

The validator in question is the author of the certificate.

If the validator is faulty, for each endorser in the certificate, there must be a message, in the network, from that endorser, for the proposal of the certificate. As a special case, if the certificate has no endorsers, no such message is required to be in the network: nothing prevents a faulty validator from authoring a proposal and then certifying it with no additional signatures; the certificate will not be accepted by correct validators, but the certificate can still be generated.

Another constraint we put on faulty validators is that they send the certificate to at least a validator. Similarly to an analogous requirement in propose-possiblep, this is not a real restriction, but just a modeling convenience: since faulty validators have no internal state, if a faulty validator created a certificate but sent it to nobody, there would be no change in the system state; that is, it would be the same as no event. In other words, a certify event models the case in which at least one message with the certificate is added to the network.

If the validator is correct, no message is required to be in the network, because endorsing signatures are incorporated into the validator state via separate augment events. The certify event can happen when the proposal of the certificate is a pending one in the validator state, the endorsers are the ones associated to the proposal in the map, and the signers (author and endorsers) form a quorum in the active committee for the proposal's round. Since the validator already has the certificate, it does not send it to itself; but as discussed in transitions-certify, we do not put any constraints on which other validators the certificate is sent to. Unlike for faulty validators, there is no constraint that the certificate is sent to at least another validator: even if no certificate messages are added to the network, the certificate is still added to the validator's DAG, and thus there is some system change.

It is an invariant, proved elsewhere, that the endorsers of each proposal in the proposed map of a correct validator are members of the active committee at the proposal's round. But this invariant is not available here, as we define certify transitions, and thus we use committee-validators-stake to measure the stake of the signers.

Definitions and Theorems

Function: certify-possiblep

(defun certify-possiblep (cert dests systate)
 (declare (xargs :guard (and (certificatep cert)
                             (address-setp dests)
                             (system-statep systate))))
 (let ((__function__ 'certify-possiblep))
   (declare (ignorable __function__))
   (b*
     (((certificate cert) cert)
      ((proposal prop) cert.proposal)
      ((when (not (in prop.author
                      (correct-addresses systate))))
       (and (subset (make-endorsement-messages prop cert.endorsers)
                    (get-network-state systate))
            (not (emptyp (address-set-fix dests)))))
      ((when (in prop.author (address-set-fix dests)))
       nil)
      ((validator-state vstate)
       (get-validator-state prop.author systate))
      (prop+endors (omap::assoc prop vstate.proposed))
      ((unless prop+endors) nil)
      ((unless (equal cert.endorsers (cdr prop+endors)))
       nil)
      (commtt
           (active-committee-at-round prop.round vstate.blockchain))
      ((unless commtt) nil)
      (signers (certificate->signers cert))
      ((unless (>= (committee-validators-stake signers commtt)
                   (committee-quorum-stake commtt)))
       nil))
     t)))

Theorem: booleanp-of-certify-possiblep

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

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

(defthm certify-possiblep-of-certificate-fix-cert
  (equal (certify-possiblep (certificate-fix cert)
                            dests systate)
         (certify-possiblep cert dests systate)))

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

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

Theorem: certify-possiblep-of-address-set-fix-dests

(defthm certify-possiblep-of-address-set-fix-dests
  (equal (certify-possiblep cert (address-set-fix dests)
                            systate)
         (certify-possiblep cert dests systate)))

Theorem: certify-possiblep-address-set-equiv-congruence-on-dests

(defthm certify-possiblep-address-set-equiv-congruence-on-dests
  (implies (address-set-equiv dests dests-equiv)
           (equal (certify-possiblep cert dests systate)
                  (certify-possiblep cert dests-equiv systate)))
  :rule-classes :congruence)

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

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

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

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