		Search-engine friendly clone of the ACL2 documentation.

Blockchain-redundant-def-and-init-and-next

Validator-blockchain-redundant-p

Check if the blockchain of a validator is equal to its calculation from the committed anchors and DAG.

Signature
(validator-blockchain-redundant-p vstate) → yes/no
Arguments: vstate — Guard (validator-statep vstate).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: validator-blockchain-redundant-p

(defun validator-blockchain-redundant-p (vstate)
 (declare (xargs :guard (validator-statep vstate)))
 (declare
     (xargs :guard (and (evenp (validator-state->last vstate))
                        (or (equal (validator-state->last vstate) 0)
                            (last-anchor vstate)))))
 (let ((__function__ 'validator-blockchain-redundant-p))
   (declare (ignorable __function__))
   (equal (validator-state->blockchain vstate)
          (calculate-blockchain (committed-anchors vstate)
                                (validator-state->dag vstate)))))

Theorem: booleanp-of-validator-blockchain-redundant-p

(defthm booleanp-of-validator-blockchain-redundant-p
  (b* ((yes/no (validator-blockchain-redundant-p vstate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: validator-blockchain-redundant-p-of-validator-state-fix-vstate

(defthm
     validator-blockchain-redundant-p-of-validator-state-fix-vstate
 (equal
     (validator-blockchain-redundant-p (validator-state-fix vstate))
     (validator-blockchain-redundant-p vstate)))

Theorem: validator-blockchain-redundant-p-validator-state-equiv-congruence-on-vstate

(defthm
 validator-blockchain-redundant-p-validator-state-equiv-congruence-on-vstate
 (implies (validator-state-equiv vstate vstate-equiv)
          (equal (validator-blockchain-redundant-p vstate)
                 (validator-blockchain-redundant-p vstate-equiv)))
 :rule-classes :congruence)