		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.

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.

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))))
          (subset (make-endorsement-messages prop cert.endorsers)
                  (get-network-state systate)))
         ((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))
      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)