		Search-engine friendly clone of the ACL2 documentation.

Committed-redundant-def-and-init-and-next

Validator-committed-redundant-p

Check if the set of committed certificates of a validator is the causal history of its last committed anchor.

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

Definitions and Theorems

Function: validator-committed-redundant-p

(defun validator-committed-redundant-p (vstate)
 (declare (xargs :guard (validator-statep vstate)))
 (declare (xargs :guard (or (equal (validator-state->last vstate) 0)
                            (last-anchor vstate))))
 (let ((__function__ 'validator-committed-redundant-p))
  (declare (ignorable __function__))
  (equal
    (validator-state->committed vstate)
    (if (equal (validator-state->last vstate) 0)
        nil
      (certificate-causal-history (last-anchor vstate)
                                  (validator-state->dag vstate))))))

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

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

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

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

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

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