		Search-engine friendly clone of the ACL2 documentation.

Ordered-even-blocks

Ordered-even-p

Definition of the invariant: the blockchain of every correct validator has strictly increasing, even round numbers.

Definitions and Theorems

Theorem: ordered-even-p-necc

(defthm ordered-even-p-necc
  (implies (ordered-even-p systate)
           (implies (in val (correct-addresses systate))
                    (blocks-ordered-even-p
                         (validator-state->blockchain
                              (get-validator-state val systate))))))

Theorem: booleanp-of-ordered-even-p

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

Theorem: ordered-even-p-of-system-state-fix-systate

(defthm ordered-even-p-of-system-state-fix-systate
  (equal (ordered-even-p (system-state-fix systate))
         (ordered-even-p systate)))

Theorem: ordered-even-p-system-state-equiv-congruence-on-systate

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

Theorem: ordered-even-p-necc-fixing

(defthm ordered-even-p-necc-fixing
 (implies
   (and (ordered-even-p systate)
        (in (address-fix val)
            (correct-addresses systate)))
   (blocks-ordered-even-p (validator-state->blockchain
                               (get-validator-state val systate)))))

Theorem: evenp-of-last-when-ordered-even-p

(defthm evenp-of-last-when-ordered-even-p
 (implies
   (and (ordered-even-p systate)
        (last-blockchain-round-p systate)
        (in val (correct-addresses systate)))
   (evenp
        (validator-state->last (get-validator-state val systate)))))