Feature request: more ways to conditionalize a ProofScript

[msaaltink]

The experimental functions goal_num_when and goal_num_ite are really useful for pulling out goals that need compicated scripts. Most of the time, for me, that's just the final goal(s) in a proof, dealing with the postcondition(s) or any points_to assertions. For that purpose, the interface is a bit awkward; I know this will be the last in the numbered list of goals, but do not know before running the proof what its number will be.

A few different things might make this more convenient and make proof scripts more robust:

• allow numbering from the end, rather than the front, so that the last goal is number -1, or with a separate goal_reverse_num_ite command that numbers the goals in reverse.
• attach some extra information to a goal, e.g. "establish the precondition of routine X called from line Y", or "show that the postcondition on line L is satisfied". These would be pretty helpful in cases of proof failure, and then there could be a goal_type_ite command to match the different types of generated goals (precondition of called routine, postcondition, points_to condition, ...)
• allow the user to attach labels to parts of a specification, then conditionalize a proof command for a particular label. e.g., llvm_named_precond "Input_is_nonnegative" (llvm_term {{ x >= 0 }}.
• have something like goal_when that looks at the goal itself. There are usually function names appearing in my postconditions that do not appear in other goals. This might be a bit fragile, though.

I'm sure you can think of more ideas. Anything like this might make the scripts more readable, more robust, and easier to write.

[kquick]

Discussion:

• Might want to be more explicit about goal naming.
• goal_when number name term might be useful.
• goal_num_ite nesting is awkward and complicated; maybe have a statement with a list of guards and a default.
• Currently runs the separate proof scripts from the beginning for each goal. Could have a single script with a number of sub-goals; some subtle things to think about with this and possibly have both modes for backward compatibility.

[robdockins]

I have two ideas in mind here that I think will meet most of the needs I have presently.

First: more careful tracking of the provenance of goals. In particular, I'd like to be able to tell the difference between goals generated by the simulator itself (memory safety and such) and goals that arise from the preconditions of overrides; for those, especially, I want to know what is the call site of the override, and what is the actual, original precondition statement (points_to, assert, etc).

Second, I'd like the ability to add arbitrary string "tags" to goals that I can use later to identify particular ones of interest; then I can use a goal_when_has_tag, or similar, to filter the goals.

Both of these basically require some mechanism to round-trip some additional metadata about goals through the symbolic simulator. I think this can be done by using What4 term annotations and a side lookup map on the SAW side.

[robdockins]

PR #1679 partially addresses this issue by implementing the ideas mentioned in the comment above.