# 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.

See also gl-mbe-fast.

### 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.