|
|
|---|
|
|
|
|---|
GL's term-level proof support
The traditional way of using GL to prove a theorem is to give a bit-level description of each variable of the theorem as a shape spec in the :g-bindings argument of def-gl-thm -- X is a 10-bit integer, Y is a three-entry Boolean list, etc. In this mode of operation, the goal is for every function to be able to symbolically execute and produce a purely bit-level symbolic object as its output.
This style of reasoning is somewhat restrictive. ACL2 code is often written in a way that makes this sort of symbolic execution expensive. For example, suppose we want a structure that maps integer keys to values. For best execution speed, we might represent this as a stobj array. For best ease of reasoning, we might represent it as a record (as in books/misc/records.lisp), since these have nice, intuitive, hypothesis-free rules about them. For symbolic execution performance, on the other hand, we might decide that a simple alist is the best representation. But if we've written the code in one of the other styles, then we'd like to be able to escape the suboptimal symbolic execution this entails.
We have added features to GL which provide a way around these problems by allowing for term-level reasoning as well as bit-level:
Warning: These features require careful setup of a rewriting theory with good normal forms. It's difficult to debug problems with them. In many ways they may not yet be ready for prime time.
Elaborating on our memory example, suppose we are trying to prove something about a program that loads and stores from computed addresses in a 1024-entry memory of 32-bit unsigned numbers. For good execution speed when running concrete simulations, we might represent this memory as a stobj containing a 1024-element array. However, this doesn't perform well when proving theorems about this representation using GL, because at each update to a symbolic address we must modify several (perhaps all) entries in the array representation: if our update is
(update-mem <sym_address> <sym_value> <arr>)
then at each address i of the array we must store an object representing:
if (sym_address == i) then sym_value else arr[i].
We might do better if we didn't try to compute an explicit interpretation of the array after each update, but instead simply tracked the updates in chronological order, as in an alist. To illustrate how to do this, suppose that our updater, accessor, and creator functions are, respectively,
First, tell GL never to open the definitions of these functions:
(gl::gl-set-uninterpreted update-mem) (gl::gl-set-uninterpreted access-mem) (gl::gl-set-uninterpreted create-mem)
Now, when GL encounters updates, rather than computing a new explicit symbolic representation for the memory, it will return a term representation, such as
(update-mem addr1 val1 (update-mem addr2 val2 (create-mem))).
To make this work, we just need to provide rewrite rules so that GL can reason about accesses:
(gl::def-gl-rewrite access-of-create (equal (access-mem addr (create-mem)) (and (natp addr) (< addr 1024) 0))) (gl::def-gl-rewrite access-of-update (equal (access-mem addr (update-mem waddr val mem)) (if (equal (nfix addr) (nfix waddr)) val (access-mem addr mem))))
Suppose that somewhere in our program we have an update as follows:
(let ((mem (if special-condition (update-mem addr val mem) mem))) ...)
At this point, simulating with just the rules we have above, our proof will probably fail because a subsequent access of the memory won't be resolved by the access-of-update rule: we no longer have a term of the form
(access-mem addr (update-mem waddr val mem))
but rather
(access-mem addr (if cond (update-mem waddr val mem) mem)).
We could fix this by introducing a new rule:
(gl::def-gl-rewrite access-of-if (equal (access-mem addr (if c mem1 mem2)) (if c (access-mem addr mem1) (access-mem addr mem2))))
This is probably the easiest solution if ACCESS-MEM is the only important function that must interact with UPDATE-MEM. An alternative is to write a rule that merges the two branches into a single term. A branch merge rule can accomplish this:
(gl::def-gl-branch-merge merge-conditional-update (equal (if cond (update-mem addr val mem) mem) (update-mem addr (if cond val (access-mem addr mem)) mem)))
This isn't necessarily cheap -- in order to apply this rule, we need to find the previous value of addr in mem, and this symbolic lookup is relatively expensive, since it may need to traverse all the updates in mem to construct the symbolic value of the access.
Traditionally, to do a proof in GL one must supply, for each free variable of the theorem, a shape specifier, which tells GL how to create a symbolic object to represent that variable. After GL finishes the symbolic execution portion of the proof, the shape specifiers must be shown to be appropriate given the assumptions about each variable; it therefore generates proof obligations of the form:
(implies (<hypotheses> var) (shape-spec-obj-in-range <shape-spec> var))
These are called coverage obligations. Shape-spec-obj-in-range says that the value var is expressible by the given shape-spec; that is, the shape-spec covers all possible values of var satisfying the hyps. For example, if the shape-spec is the :g-integer construct for a 10-bit integer, then the shape-spec-obj-in-range term reduces to:
(and (integerp var) (< var (expt 2 9)) (<= (- (expt 2 9)) var)).
Since the new GL capabilities described above allow manipulation of term-level symbolic objects, it can be useful to supply term-level shape specifiers. This can be done using the G-CALL and G-VAR constructs.
A G-VAR construct is simply a free variable; it can represent any object whatsoever, so its coverage obligations are trivial.
A G-CALL represents a function call. It takes three arguments:
The symbolic term resulting from this shape spec is simply the application (G-APPLY) of FN to the symbolic objects derived from ARGS. INV is an extra piece of information that tells us how to prove coverage. Its usage is discussed in g-call.
GL now has the ability to generate fresh Boolean variables in addition to the ones existing in the user-provided shape spec. It does this anytime an IF condition's value ends up as a term-level object, i.e. a G-APPLY (function call) or G-VAR (free variable). The mapping between these term-level objects and the generated Boolean variables are stored as we symbolically execute and can be reused if the same condition is encountered again. Careful use of this feature can allow GL to work without giving such detailed shape specifiers.
For example, suppose that we don't want to assume anything about our memory variable, but we know that for any slot we access, we'll only use 5 bits of the stored value: perhaps our accessors always take (LOGHEAD 5 x) of the slot. We can assign a G-VAR object to the memory; that way it can represent any object at all. We then want to arrange things so that at every access, we generate 5 new Boolean variables for the integer bits of that access (if we haven't already done so). Here is one rule that will accomplish that:
(gl::def-gl-rewrite loghead-5-of-access-mem ;; We don't want this rule to apply to an update-mem term, so this syntaxp ;; hyp prevents that. We also should only apply this if ADDR is a concrete ;; object; we'd need a different strategy for symbolic addresses. (implies (syntaxp (and (not (and (consp mem) (gl::g-apply-p mem) (eq (gl::g-apply->fn mem) 'update-mem))) (gl::general-concrete-p addr))) (equal (loghead 5 (access-mem addr mem)) (logcons (if (logbitp 0 (access-mem addr mem)) 1 0) (logcons (if (logbitp 1 (access-mem addr mem)) 1 0) (logcons (if (logbitp 2 (access-mem addr mem)) 1 0) (logcons (if (logbitp 3 (access-mem addr mem)) 1 0) (logcons (if (logbitp 4 (access-mem addr mem)) 1 0) 0))))))))
Performing this rewrite will cause GL to generate a Boolean variable for each of these LOGBITP terms, because they produce term-level objects that are then used in IF tests.
Using this strategy makes it harder to generate counterexamples. In fact, it is impossible to generally solve the problem of generating counterexamples when using this strategy. A satisfying assignment from a SAT solver gives us an assignment of values to our Boolean variables. But these Boolean variables each just correspond to some term, which may be an arbitrary nesting of functions. To map this Boolean-level counterexample to an ACL2-level counterexample, we are then left with finding an assignment for some variables that makes a series of terms take certain truth values, which is undecidable. In the next section, we describe a heuristic method for generating counterexamples that works in practice when applied carefully.
Furthermore, unless this strategy is used with utmost care, it is likely that proofs will fail due to detection of "counterexamples" that are actually impossible. For example, we might generate a Boolean variable for (integerp x) and another one for (logbitp 0 x). But these two terms are not independent; in fact, (logbitp 0 x) implies (integerp x). If we don't let the SAT solver know about these constraints, it might find false counterexamples. This can't render GL unsound, but may lead to failed proofs. You may provide rules for generating constraints among these Boolean variables to solve this kind of problem: see def-gl-boolean-constraint.
The situation described above (where every field is accessed via LOGHEAD and via concrete address) is a particularly good one for this strategy, since then all we need to know about each field are its LOGBITPs, which are all independent.
Our strategy for generating counterexamples when using automatic Boolean variable generation is to provide rules for manipulating assignments. For example:
(gl::def-glcp-ctrex-rewrite ((logbitp n x) t) (x (logior (ash 1 n) x))) (gl::def-glcp-ctrex-rewrite ((logbitp n x) nil) (x (logand (lognot (ash 1 n)) x)))
These two rules, respectively, say:
DEF-GLCP-CTREX-REWRITE can also take a keyword argument :test, which can do a syntactic check on the variables matched. E.g., we could ensure that N was a constant in the rules above:
(gl::def-glcp-ctrex-rewrite ((logbitp n x) t) (x (logior (ash 1 n) x)) :test (quotep n))
Note that these rules are purely heuristic, have no bearing on the soundness of GL, and do not require any proofs. Getting them wrong may cause GL to generate false counterexamples, however.
Another rule that would be useful in the memory example above:
(gl::def-glcp-ctrex-rewrite ((access-mem addr mem) val) (mem (update-mem addr val mem)) :test (quotep addr))