A shape-spec representing a function call.
(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:
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'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
(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:
because for any value m satisfying our assumptions,
(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.