		Search-engine friendly clone of the ACL2 documentation.

No-self-endorsed

No-self-endorsed-p

Definition of the invariant: every pair in the endorsed set of a correct validator does not have the validator's address.

We express this by saying that retrieving, from the set of endorsed pairs of a validator, the ones with the validator's address yields the empty set.

Definitions and Theorems

Theorem: no-self-endorsed-p-necc

(defthm no-self-endorsed-p-necc
 (implies
  (no-self-endorsed-p systate)
  (implies
   (in val (correct-addresses systate))
   (equal
    (address+pos-pairs-with-address
      val
      (validator-state->endorsed (get-validator-state val systate)))
    nil))))

Theorem: booleanp-of-no-self-endorsed-p

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

Theorem: no-self-endorsed-p-of-system-state-fix-systate

(defthm no-self-endorsed-p-of-system-state-fix-systate
  (equal (no-self-endorsed-p (system-state-fix systate))
         (no-self-endorsed-p systate)))

Theorem: no-self-endorsed-p-system-state-equiv-congruence-on-systate

(defthm no-self-endorsed-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (no-self-endorsed-p systate)
                  (no-self-endorsed-p systate-equiv)))
  :rule-classes :congruence)

Theorem: no-self-endorsed-p-necc-fixing

(defthm no-self-endorsed-p-necc-fixing
 (implies
  (and (no-self-endorsed-p systate)
       (in (address-fix val)
           (correct-addresses systate)))
  (equal
   (address+pos-pairs-with-address
      val
      (validator-state->endorsed (get-validator-state val systate)))
   nil)))