		Search-engine friendly clone of the ACL2 documentation.

Certificates-of-validators

Accepted-certificates

Certificates accepted by a validator.

Signature
(accepted-certificates val systate) → certs
Arguments: val — Guard (addressp val).; systate — Guard (system-statep systate).
Returns: certs — Type (certificate-setp certs).

These are all the certificates that have been accepted by a validator, i.e. the certificates that they are in the buffer or DAG. When a validator authors a certificates, it adds it to the DAG, so it certainly ``accepts'' it. When a validator receives a certificate from the network, it adds it to the buffer, and then later it possibly moves it to the DAG.

Definitions and Theorems

Function: accepted-certificates

(defun accepted-certificates (val systate)
  (declare (xargs :guard (and (addressp val)
                              (system-statep systate))))
  (declare (xargs :guard (in val (correct-addresses systate))))
  (let ((__function__ 'accepted-certificates))
    (declare (ignorable __function__))
    (b* ((vstate (get-validator-state val systate)))
      (union (validator-state->dag vstate)
             (validator-state->buffer vstate)))))

Theorem: certificate-setp-of-accepted-certificates

(defthm certificate-setp-of-accepted-certificates
  (b* ((certs (accepted-certificates val systate)))
    (certificate-setp certs))
  :rule-classes :rewrite)

Theorem: in-owned-certificates-when-in-accepted-certificates

(defthm in-owned-certificates-when-in-accepted-certificates
  (implies (in cert
               (accepted-certificates val systate))
           (in cert (owned-certificates val systate))))

Theorem: accepted-certificates-of-address-fix-val

(defthm accepted-certificates-of-address-fix-val
  (equal (accepted-certificates (address-fix val)
                                systate)
         (accepted-certificates val systate)))

Theorem: accepted-certificates-address-equiv-congruence-on-val

(defthm accepted-certificates-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (accepted-certificates val systate)
                  (accepted-certificates val-equiv systate)))
  :rule-classes :congruence)

Theorem: accepted-certificates-of-system-state-fix-systate

(defthm accepted-certificates-of-system-state-fix-systate
  (equal (accepted-certificates val (system-state-fix systate))
         (accepted-certificates val systate)))

Theorem: accepted-certificates-system-state-equiv-congruence-on-systate

(defthm
     accepted-certificates-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (accepted-certificates val systate)
                  (accepted-certificates val systate-equiv)))
  :rule-classes :congruence)