Shape-specs
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.
Creating Shape Spec Objects
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 integers X where (<= (- (expt 2 (+ -1 n))) x) and
(< x (expt 2 (+ -1 n))). The list-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, and else are
shape specs.
What is a Coverage Proof?
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 (< (+ A B) 7) with
A and B bound to symbolic objects representing two-bit natural
numbers and recieve a result of T. From this, it would be fallacious to
conclude (< (+ 6 8) 7), because the symbolic simulation didn't cover the
case where A was 6 and B 7. In fact, it isn't certain that we can
conclude (< (+ 2 2) 7) from our symbolic simulation, because the symbolic
object bindings for A and B might have interedependencies such that
A and B can't simultaneously represent 2. (For example, the bindings
could be such that bit 0 of A and B are always opposite.) In order
to prove a useful theorem from the result of such a symbolic simulation, we
must show that some set of concrete input vectors is covered by the symbolic
objects bound to A and B. But in general, it is a tough
computational problem to determine the set of concrete input vectors that are
covered by a given symbolic input vector.
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
SHAPE-SPEC-OBJ-IN-RANGE can make that determination about shape specs.
SHAPE-SPEC-OBJ-IN-RANGE takes two arguments, a shape spec and some object,
and returns T if that object is in the coverage set of the shape spec, and NIL
otherwise. Therefore, if we wish to conclude that shape specs bound to A
and B cover all two-bit natural numbers, we may prove the following
theorem:
(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
SHAPE-SPEC-OBJ-IN-RANGE. The shape specs are converted to symbolic
objects and may be parametrized based on some restrictions from the hypotheses,
restricting their range further. Thus, in order to prove a theorem about
fixed-length natural numbers, for example, one may provide a shape specifier
that additionally covers negative integers of the given length; parametrization
can then restrict the symbolic inputs used in the simulation to only cover the
naturals, while the coverage proof may still be done using the simpler,
unparametrized shape spec.
Subtopics
- 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.
