		Search-engine friendly clone of the ACL2 documentation.

Transitions-certify

Certify-possiblep

Check if a certify event is possible.

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

The cert parameter of this function is the corresponding component of the certify event. The other component of the event is not needed in this predicate.

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 immediately certifying 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.

Definitions and Theorems

Function: certify-possiblep

(defun certify-possiblep (cert systate)
  (declare (xargs :guard (and (certificatep cert)
                              (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)))
         ((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 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)
                            systate)
         (certify-possiblep cert 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 systate)
                  (certify-possiblep cert-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 (system-state-fix systate))
         (certify-possiblep cert 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 systate)
                  (certify-possiblep cert systate-equiv)))
  :rule-classes :congruence)