Document refinement for method specs

[robdockins]

Sometimes, it might be useful to state a weaker/more specific method specification for a function (say, to make it more obvious that an override applies at a given call site), or to assemble a more general method specification from a collection of more specific ones (e.g., I can prove something for n in {2, 4, 6, 8}; now I want to show it holds for all even 0 < n < 10). I believe both use cases can be supported with the concept of a specification "refinement". Basically, the idea is that a user states a spec they would like to prove, and then supplies a list of already proved overrides; the system attempts to prove that the stated spec refines the collection of given specifications. We should be able to do this via the same mechanism that SAW uses when it encounters a call to an overridden function normally.

The script API I have in mind looks very similar to the verify command; the difference is just that we don't examine the code of the given function at all, and just attempt to directly use the given overrides.

new_ovr <- llvm_refine_spec module "function_name" overrides spec_to_prove tactic;

[msaaltink]

I have wanted this feature on some past projects, so it would be a welcome addition.

The API you suggest looks fine, although may be redundant: both the module and function name are implied by the overrides, which ought to all be for some single function in a single module.

[robdockins]

I think PR #1692 is ready to go, however, I want to leave this ticket open to track the moving of this feature from experimental phase to current, and for writing documentation and changelog entries.

We should also implement this feature for the JVM system. I think the implementation will be broadly similar.