		Search-engine friendly clone of the ACL2 documentation.

Transitions-store-certificate

Store-certificate-possiblep

Check if a certificate storage event is possible.

Signature
(store-certificate-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 inputs of this function are the address and certificate in the store-certificate event; see event.

When a certificate is received, the (correct) validator puts it into the buffer. From there, it is moved to the DAG when the DAG contains all the certificates referenced in the previous component of the certificate. This is the reason for the buffer: certificates may be received out of order, and so we need a staging area (the buffer) for certificates that cannot be added to the DAG yet.

The address val of the validator indicated in the event must be a correct validator of the system; we do not model the internal state of faulty validators. The certificate must be in the buffer of the validator. If the certificate's round number is 1, there is no further requirement, because there are no previous certificates. Otherwise, we obtain the certificates in the DAG at the previous round, and we check that their authors contain the addresses in the previous component of the certificate.

Definitions and Theorems

Function: store-certificate-possiblep

(defun store-certificate-possiblep (val cert systate)
 (declare (xargs :guard (and (addressp val)
                             (certificatep cert)
                             (system-statep systate))))
 (let ((__function__ 'store-certificate-possiblep))
   (declare (ignorable __function__))
   (b* (((certificate cert) cert)
        ((unless (in (address-fix val)
                     (correct-addresses systate)))
         nil)
        ((validator-state vstate)
         (get-validator-state val systate))
        ((unless (in (certificate-fix cert)
                     vstate.buffer))
         nil)
        ((when (equal cert.round 1)) t)
        (all-previous-round-certs
             (certificates-with-round (1- cert.round)
                                      vstate.dag))
        (all-previous-round-authors
             (certificate-set->author-set all-previous-round-certs))
        ((unless (subset cert.previous
                         all-previous-round-authors))
         nil))
     t)))

Theorem: booleanp-of-store-certificate-possiblep

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

Theorem: store-certificate-possiblep-of-address-fix-val

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

Theorem: store-certificate-possiblep-address-equiv-congruence-on-val

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

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

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

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

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

Theorem: store-certificate-possiblep-of-system-state-fix-systate

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

Theorem: store-certificate-possiblep-system-state-equiv-congruence-on-systate

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