Property Verification for the frame stack semantics#58
Property Verification for the frame stack semantics#58
Conversation
…or the k step problem
MTLEVR
changed the title
| | |- _ => idtac | ||
| end | ||
| end. | ||
|
|
There was a problem hiding this comment.
Are the following two tactics necessary?
| intros t. | ||
|
|
||
| Ltac strip_IH_precond IH := | ||
| (* By this point, the induction hypothesis is an implication list. Note that this tactic |
There was a problem hiding this comment.
This explanation is not detailed enough. Could you provide some more insights? (Where is this tactic used, what kind of goals it should reshape?)
| Import ListNotations. | ||
|
|
||
|
|
||
| Ltac contains_match := |
There was a problem hiding this comment.
All these tactics should have explanations as comments (some tactics tactics already have it). One line is sufficient for simpler ones.
| | |- _ => | ||
| lazymatch goal with | ||
| | |- ex _ => eexists;solve_terminated | ||
| | |- _ /\ _ => split;[solve_final_state|solve_final_postcond] |
There was a problem hiding this comment.
This supposes that the goal is shaped in a consistent way. At the beginning of the file, please provide a longer comment to explain the purpose of these tactics, and describe how the goal should be "shaped" for them to be usable.
| ]. | ||
|
|
||
| Ltac base_case_mult precond heq' h t := | ||
| (* We need to return h and the precondition to the goal, before the loop begins. *) |
There was a problem hiding this comment.
I don't understand this comment. Isn't this about initialising the loop based on the precondition and current goal? Then "return" is confusing, "passing as an argument" to the tactic loop is better phrased.
| | idtac "Unexpected error: could not solve terminated program" | ||
| ]. | ||
|
|
||
| (* HACK: it is way easier, to handle cases with 1 and more than 1 symbolic variables separately. |
There was a problem hiding this comment.
Where does this appear? separate_cases_0 and the rest?
2 participants
This pull request is for the property verification tactics that I've described in my master's thesis.
src/Symbolic/SymbTheorems.v contains theorems needed for the verification tactics.
src/Symbolic/SymbTactics.v contains the property verification tactic solve_symbolically, as well as helper tactics. Note that the tactic itself is described twice, once for a single symbolic variable, and once for multiple symbolic variables. Due to the complexity (and lack of proper semantics) of Ltac I was not able to adequately merge these. Tactic notations are given to merge these two tactics.
src/Symbolic/SymbExamples.v contains examples for the solve_symbolically tactic.