		Search-engine friendly clone of the ACL2 documentation.

System-certificates

System-certs

Certificates in the system.

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

We union the DAGs of all correct validators with the certificates in all the messages in the network.

Definitions and Theorems

Function: system-certs

(defun system-certs (systate)
 (declare (xargs :guard (system-statep systate)))
 (let ((__function__ 'system-certs))
  (declare (ignorable __function__))
  (union
       (validators-certs (correct-addresses systate)
                         systate)
       (message-set->certificate-set (get-network-state systate)))))

Theorem: certificate-setp-of-system-certs

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

Theorem: in-system-certs-when-in-some-dag

(defthm in-system-certs-when-in-some-dag
 (implies
  (and
      (in val (correct-addresses systate))
      (in cert
          (validator-state->dag (get-validator-state val systate))))
  (in cert (system-certs systate))))

Theorem: in-system-certs-when-in-network

(defthm in-system-certs-when-in-network
  (implies (in msg (get-network-state systate))
           (in (message->certificate msg)
               (system-certs systate))))

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

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

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

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