Assert that a particular symbolic object is equivalent to a second form, and use the second in place of the first.
(gl-mbe spec impl) is defined to simply check whether its two arguments
This is most useful when symbolically executing in AIG mode. For example, suppose that through a series of shifting operations, the symbolic representation of some numeric operand X is expanded to thousands of bits. However, the user knows that only the bottom 25 bits may be non-zero. Then the following form may speed up the rest of the computation involving X by cutting off all the upper bits, which are known to be zero:
When GL symbolically executes this, it tries to prove that
See also gl-mbe-fast.
(defun gl-mbe-fn (spec impl spec-form impl-form) (declare (xargs :guard t)) (mbe :logic spec :exec (prog2$ (or (equal spec impl) (er hard? 'gl-mbe "GL-MBE failure: ~x0 and ~x1 unequal.~% ~ Values: ~x2 versus ~x3." spec-form impl-form spec impl)) spec)))
(defthm gl-mbe-gl-def (equal (gl-mbe-fn spec impl spec-form impl-form) (if (gl-assert (acl2::always-equal spec impl) :msg (msg "GL-MBE failure: ~x0 and ~x1 unequal." spec-form impl-form)) impl spec)) :rule-classes ((:definition :install-body nil)))