		Search-engine friendly clone of the ACL2 documentation.

Last-blockchain-round

Last-blockchain-round-p

Definition of the invariant: for each correct validator in the system, the last committed round is 0 if the blockchain is empty, or the round of the newest block in the blockchain otherwise.

Definitions and Theorems

Theorem: last-blockchain-round-p-necc

(defthm last-blockchain-round-p-necc
  (implies
       (last-blockchain-round-p systate)
       (implies (in val (correct-addresses systate))
                (b* (((validator-state vstate)
                      (get-validator-state val systate)))
                  (equal vstate.last
                         (blocks-last-round vstate.blockchain))))))

Theorem: booleanp-of-last-blockchain-round-p

(defthm booleanp-of-last-blockchain-round-p
  (b* ((yes/no (last-blockchain-round-p systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: last-blockchain-round-p-of-system-state-fix-systate

(defthm last-blockchain-round-p-of-system-state-fix-systate
  (equal (last-blockchain-round-p (system-state-fix systate))
         (last-blockchain-round-p systate)))

Theorem: last-blockchain-round-p-system-state-equiv-congruence-on-systate

(defthm
   last-blockchain-round-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (last-blockchain-round-p systate)
                  (last-blockchain-round-p systate-equiv)))
  :rule-classes :congruence)

Theorem: last-blockchain-round-p-necc-fixing

(defthm last-blockchain-round-p-necc-fixing
  (implies (and (last-blockchain-round-p systate)
                (in (address-fix val)
                    (correct-addresses systate)))
           (b* (((validator-state vstate)
                 (get-validator-state val systate)))
             (equal vstate.last
                    (blocks-last-round vstate.blockchain)))))