		Search-engine friendly clone of the ACL2 documentation.

Event-commit

Event-commit->validator

Get the validator field from a event-commit.

Signature
(event-commit->validator x) → validator
Arguments: x — Guard (eventp x).
Returns: validator — Type (addressp validator).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: event-commit->validator$inline

(defun event-commit->validator$inline (x)
  (declare (xargs :guard (eventp x)))
  (declare (xargs :guard (equal (event-kind x) :commit)))
  (let ((__function__ 'event-commit->validator))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and (equal (event-kind x) :commit) x)))
           (address-fix (std::da-nth 0 (cdr x))))
         :exec (std::da-nth 0 (cdr x)))))

Theorem: addressp-of-event-commit->validator

(defthm addressp-of-event-commit->validator
  (b* ((validator (event-commit->validator$inline x)))
    (addressp validator))
  :rule-classes :rewrite)

Theorem: event-commit->validator$inline-of-event-fix-x

(defthm event-commit->validator$inline-of-event-fix-x
  (equal (event-commit->validator$inline (event-fix x))
         (event-commit->validator$inline x)))

Theorem: event-commit->validator$inline-event-equiv-congruence-on-x

(defthm event-commit->validator$inline-event-equiv-congruence-on-x
  (implies (event-equiv x x-equiv)
           (equal (event-commit->validator$inline x)
                  (event-commit->validator$inline x-equiv)))
  :rule-classes :congruence)

Theorem: event-commit->validator-when-wrong-kind

(defthm event-commit->validator-when-wrong-kind
  (implies (not (equal (event-kind x) :commit))
           (equal (event-commit->validator x)
                  (address-fix nil))))