		Search-engine friendly clone of the ACL2 documentation.

Reference

Gl-mbe

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 spec and impl are equal, throwing an error if not, and return spec.

However, when gl-mbe is symbolically executed, the equality of the two arguments is checked symbolically. If it can be proved (e.g., via a BDD equality or SAT check) that they are always equal, then impl is returned instead of spec, otherwise an error is produced.

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:

(let ((x-chop (gl-mbe x (logand (1- (ash 1 25)) x))))
   ...)

When GL symbolically executes this, it tries to prove that x and the logand expression are equivalent, that is, their symbolic representations evaluate to the same concrete values under all environments. If this can be proved, x-chop is bound to the logand result, which cuts off the upper bits of x, which may improve symbolic execution performance. However, logically gl-mbe just binds x-chop to x, so this logand term does not complicate reasoning about the specification.

Definitions and Theorems

Function: gl-mbe-fn

(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)))

Theorem: gl-mbe-gl-def

(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)))

Subtopics

Gl-mbe-fast: Like gl-mbe, but faster and without error checking during execution.