		Search-engine friendly clone of the ACL2 documentation.

Signer-records

Signer-records-p

Definition of the invariant: for every certificate signed by a correct validator, the validator has a record of that certificate.

We express this on the set of signed certificates defined by signed-certs.

Definitions and Theorems

Theorem: signer-records-p-necc

(defthm signer-records-p-necc
 (implies
  (signer-records-p systate)
  (implies (and (in signer (correct-addresses systate))
                (in cert (signed-certs signer systate)))
           (signer-record-p (certificate->author cert)
                            (certificate->round cert)
                            (get-validator-state signer systate)))))

Theorem: booleanp-of-signer-records-p

(defthm booleanp-of-signer-records-p
  (b* ((yes/no (signer-records-p systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: signer-records-p-of-system-state-fix-systate

(defthm signer-records-p-of-system-state-fix-systate
  (equal (signer-records-p (system-state-fix systate))
         (signer-records-p systate)))

Theorem: signer-records-p-system-state-equiv-congruence-on-systate

(defthm signer-records-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (signer-records-p systate)
                  (signer-records-p systate-equiv)))
  :rule-classes :congruence)