		Search-engine friendly clone of the ACL2 documentation.

Transitions-store

Store-possiblep

Check if a certificate storage event is possible.

Signature
(store-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 event; see event.

When a certificate is received, the (correct) validator puts it into the buffer: see transitions-receive. 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.

Importantly, a validator stores the certificate into the DAG only if its signers form a quorum in the active committee for the certificate's round, of which they must be members. Thus, the validator must be able to calculate (from its blockchain) the committee for the certificate's round, in order to perform the check. This check is important because, in our formal model, nothing prevents the creation of a new certificate with signers completely disjoint from the validator's committee; these would have to be faulty signers, but it can still happen. So this bad certificate could very well cause equivocation, if a validator blindly stored it into the DAG. Instead, by having the receiving validator check the signers, we avoid that, as proved elsewhere.

The address val of the validator indicated in the event must be a correct validator of the system. The certificate must be in the buffer of the validator. If the certificate's round number is 1, there is no requirement on the previous certificates, 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-possiblep

(defun store-possiblep (val cert systate)
 (declare (xargs :guard (and (addressp val)
                             (certificatep cert)
                             (system-statep systate))))
 (let ((__function__ 'store-possiblep))
  (declare (ignorable __function__))
  (b*
   (((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)
    ((certificate cert) cert)
    (commtt
         (active-committee-at-round cert.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 (= cert.round 1)) t)
    ((unless
        (subset
             cert.previous
             (cert-set->author-set (certs-with-round (1- cert.round)
                                                     vstate.dag))))
     nil))
   t)))

Theorem: booleanp-of-store-possiblep

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

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

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

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

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

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

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

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

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

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

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

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

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