Simplified symbolic objects useful for coverage proofs in GL.

Shape specifiers are a simplified format of GL symbolic objects, capable of representing Booleans, numbers, conses, free variables, and function calls. While less expressive than full-fledged symbolic objects, shape spec objects make it easier to prove coverage lemmas necessary for proving theorems by symbolic simulation. Here, we document common constructions of shape-spec objects and what it means to prove coverage.

Shape spec objects are analogues of symbolic objects, but with several tweaks that make it more straightforward to prove that a given concrete object is covered:

- Symbolic objects contain arbitrary Boolean formulas (BDDs or AIGs), whereas shape specifiers are restricted to contain only independent Boolean variables. Therefore, every bit in a shape specifier is independent from every other bit.
- The
:g-apply symbolic object construct is replaced by the:g-call shape specifier construct. The:g-call object has an additional field that holds a user-provided inverse function, which is useful for proving coverage; see g-call.

Shape spec objects may be created using the following constructors (roughly in order of usefulness). Additionally, a non-keyword atom is a shape spec representing itself:

(G-BOOLEAN <num>) - Represents a Boolean.
num (a natural number) may not be repeated in any other:G-BOOLEAN or:G-NUMBER construct in the shape-spec. (G-INTEGER <list-of-nums>) - Represents a two's-complement integer with bits corresponding to the list,
least significant bit first. Rationals and complex rationals are also
available; see symbolic-objects. A :G-INTEGER construct with a list of
length
N represents integersX where(<= (- (expt 2 (+ -1 n))) x) and(< x (expt 2 (+ -1 n))) . Thelist-of-nums must be natural numbers, may not repeat, and may not occur in any other:G-BOOLEAN or:G-INTEGER /:G-NUMBER construct. (G-NUMBER (list <list-of-nums>)) - Same as the
G-INTEGER form above, for backward compatibility. (cons <Car> <Cdr>) - Represents a cons; Car and Cdr should be well-formed shape specifiers.
(G-VAR <name>) - A free variable that may represent any object. This is primarily useful when using GL's term-level capabilities; see term-level-reasoning.
(G-CALL <fnname> <arglist> <inverse>) - Represents a call of the named function applied to the given arguments.
The
inverse does not affect the symbolic object generated, which is(:G-APPLY <fnname> . <arglist>) , but is used in the coverage proof; see g-call. This construct is primarily useful when using GL's term-level capabilities; see term-level-reasoning. (G-ITE <test> <then> <else>) - Represents an if/then/else, where
test ,then , andelse are shape specs.

In order to prove a theorem by symbolic simulation, one binds each variable
mentioned in the theorem to a symbolic object and then symbolically simulates
the conclusion of the theorem on these symbolic objects. If the result is
true, what can we conclude? It depends on the coverage of the symbolic inputs.
For example, one might symbolically simulate the term

To make these determinations easier, shape spec objects are somewhat restricted. Whereas symbolic objects generally use BDDs (or AIGs, depending on the mode) to represent individual Booleans or bits of numeric values (see symbolic-objects), shape specs instead use natural numbers representing Boolean variables. Additionally, shape specs are restricted such that no Boolean variable number may be used more than once among the bindings for the variables of a theorem; this prevents interdependencies among them.

While in general it is a difficult problem to determine whether a symbolic
object can evaluate to a given concrete object, a function

(implies (and (natp a) (< a 4) (natp b) (< b 4)) (shape-spec-obj-in-range (list a-binding b-binding) (list a b)))

When proving a theorem using the GL clause processor, variable bindings are
given as shape specs so that coverage obligations may be stated in terms of

- G-call
- A shape-spec representing a function call.
- Flex-bindings
- Shape specifiers for
:g-bindings , more flexible than auto-bindings. - Auto-bindings
- Simplified shape specifiers for
:g-bindings . - G-int
- Create a g-binding for an integer.