		Search-engine friendly clone of the ACL2 documentation.

Certificates-of-validators

Owned-certificates

Certificates owned by a validator.

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

This is as explained in certificates-of-validators. It consists of the certificates in the DAG and buffer, as well as the ones in the network addressed to the validator.

This is only defined for correct validators. Faulty validators have no internal state, and no messages addresses to them.

Definitions and Theorems

Function: owned-certificates

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

Theorem: certificate-setp-of-owned-certificates

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

Theorem: message-certificate-in-owned-certificates

(defthm message-certificate-in-owned-certificates
  (implies (in (message-fix msg)
               (get-network-state systate))
           (in (message->certificate msg)
               (owned-certificates (message->destination msg)
                                   systate))))

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

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

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

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

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

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

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

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