		Search-engine friendly clone of the ACL2 documentation.

G-call

A shape-spec representing a function call.

Note: This is an advanced topic. You should first read term-level-reasoning to see whether this is of interest, then be familiar with shape-specs before reading this.

G-CALL is the constructor for a shape-spec representing a function call. Usage:

(g-call <function name>
        <list of argument shape-specs>
        <inverse function>)

This yields a G-APPLY object (see symbolic-objects):

(g-apply <function name>
         <list of argument symbolic objects>)

The inverse function field does not affect the symbolic object that is generated from the g-call object, but it determines how we attempt to prove the coverage obligation.

The basic coverage obligation for assigning some variable V a shape spec SS is that for every possible value of V satisfying the hypotheses, there must be an environment under which the symbolic object derived from SS evaluates to that value. The coverage proof must show that there exists such an environment.

Providing an inverse function INV basically says:

"If we need (FN ARGS) to evaluate to VAL, then ARGS should be (INV VAL)."

So to prove that (G-CALL FN ARGS INV) covers VAL, we first prove that ARGS cover (INV VAL), then that (FN (INV VAL)) equals VAL. The argument that this works is:

We first prove ARGS covers (INV VAL) -- that is, there exists some environment E under which the symbolic objects derived from ARGS evaluate to (INV VAL).
Since (FN (INV VAL)) equals VAL, this same environment E suffices to make the symbolic object (FN ARGS) evaluate to VAL.

We'll now show an example. We build on the memory example discussed in term-level-reasoning. Suppose we want to initially assign a memory object mem a symbolic value under which address 1 has been assigned a 10-bit integer. That is, we want to be able to assume only the following about mem:

(signed-byte-p 10 (access-mem 1 mem))

Assuming our memory follows the standard record rules, i.e.

(update-mem addr (access-mem addr mem) mem) = mem,

we can represent any such memory as

(update-mem 1 <some 10-bit integer> <some memory>)

Our shape-spec for this will therefore be:

(g-call 'update-mem
        (list 1
              (g-integer (list 0 1 2 3 4 5 6 7 8 9)) ;; 10-bit integer
              (g-var 'mem)) ;; free variable
        <some inverse function>)

What is an appropriate inverse? The inverse needs to take any memory satisfying our assumption and generate the list of necessary arguments to update-mem that fit this template. The following works:

(lambda (m) (list 1 (access-mem 1 m) m))

because for any value m satisfying our assumptions,

the first argument returned is 1, which is covered by our shape-spec 1
the second argument returned will (by the assumption) be a 10-bit integer, which is covered by our g-number shape-spec
the third argument returned matches our g-var shape-spec since anything at all is covered by it
the final term we end up with is:
```
(update-mem 1 (access-mem 1 m) m)
```
which (by the record rule above) equals m.

GL tries to manage coverage proofs itself, and when using G-CALL constructs some rules besides the ones it typically uses may be necessary -- for example, the redundant record update rule used here. You may add these rules to the rulesets used for coverage proofs as follows:

(acl2::add-to-ruleset gl::shape-spec-obj-in-range-backchain
                      redundant-mem-update)
(acl2::add-to-ruleset gl::shape-spec-obj-in-range-open
                      redundant-mem-update)

There are two rulesets because these are used in slightly different phases of the coverage proof.

This feature has not yet been widely used and the detailed mechanisms for (e.g.) adding rules to the coverage strategy are likely to change.