		Search-engine friendly clone of the ACL2 documentation.

Transitions-accept

Accept-possiblep

Check if an accept event is possible in a system state.

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

The val and cert parameters of this function are the corresponding components of the accept event.

The network must contain a message containing the certificate and the validator as destination.

The validator must be correct; only correct validators have DAGs in our model.

The validator must be able to calculate the active committee at the round of the certificate. The signers of the certificate must be members of the committee, and must form a quorum in that committee.

Finally, the validator's DAG must already contain all the previous certificates referenced by the new certificate, unless the round is 1.

Definitions and Theorems

Function: accept-possiblep

(defun accept-possiblep (val cert systate)
 (declare (xargs :guard (and (addressp val)
                             (certificatep cert)
                             (system-statep systate))))
 (let ((__function__ 'accept-possiblep))
  (declare (ignorable __function__))
  (b*
   ((msg (make-message-certificate :certificate cert
                                   :destination val))
    ((unless (in msg (get-network-state systate)))
     nil)
    ((unless (in (address-fix val)
                 (correct-addresses systate)))
     nil)
    ((validator-state vstate)
     (get-validator-state val systate))
    ((certificate cert) cert)
    ((proposal prop) cert.proposal)
    (commtt
         (active-committee-at-round prop.round vstate.blockchain))
    ((unless commtt) nil)
    (signers (certificate->signers cert))
    ((unless (subset signers (committee-members commtt)))
     nil)
    ((unless (>= (committee-members-stake signers commtt)
                 (committee-quorum-stake commtt)))
     nil)
    ((when (= prop.round 1)) t)
    ((unless
        (subset
             prop.previous
             (cert-set->author-set (certs-with-round (1- prop.round)
                                                     vstate.dag))))
     nil))
   t)))

Theorem: booleanp-of-accept-possiblep

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

Theorem: accept-possiblep-of-address-fix-val

(defthm accept-possiblep-of-address-fix-val
  (equal (accept-possiblep (address-fix val)
                           cert systate)
         (accept-possiblep val cert systate)))

Theorem: accept-possiblep-address-equiv-congruence-on-val

(defthm accept-possiblep-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (accept-possiblep val cert systate)
                  (accept-possiblep val-equiv cert systate)))
  :rule-classes :congruence)

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

(defthm accept-possiblep-of-certificate-fix-cert
  (equal (accept-possiblep val (certificate-fix cert)
                           systate)
         (accept-possiblep val cert systate)))

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

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

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

(defthm accept-possiblep-of-system-state-fix-systate
  (equal (accept-possiblep val cert (system-state-fix systate))
         (accept-possiblep val cert systate)))

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

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