		Search-engine friendly clone of the ACL2 documentation.

Associated-certificates

Associated-certs

Certificates associated to a validator.

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

This is as explained in associated-certificates. 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: associated-certs

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

Theorem: certificate-setp-of-associated-certs

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

Theorem: message-certificate-in-associated-certs

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

Theorem: associated-certs-of-address-fix-val

(defthm associated-certs-of-address-fix-val
  (equal (associated-certs (address-fix val)
                           systate)
         (associated-certs val systate)))

Theorem: associated-certs-address-equiv-congruence-on-val

(defthm associated-certs-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (associated-certs val systate)
                  (associated-certs val-equiv systate)))
  :rule-classes :congruence)

Theorem: associated-certs-of-system-state-fix-systate

(defthm associated-certs-of-system-state-fix-systate
  (equal (associated-certs val (system-state-fix systate))
         (associated-certs val systate)))

Theorem: associated-certs-system-state-equiv-congruence-on-systate

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