Property Verification for the frame stack semantics#58
Merged
Conversation
…or the k step problem
MTLEVR
changed the title
berpeti
reviewed
Feb 4, 2026
| intros t. | ||
|
|
||
| Ltac strip_IH_precond IH := | ||
| (* By this point, the induction hypothesis is an implication list. Note that this tactic |
Collaborator
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?)
| ]. | ||
|
|
||
| Ltac base_case_mult precond heq' h t := | ||
| (* We need to return h and the precondition to the goal, before the loop begins. *) |
Collaborator
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.
…Formalization into gergo_symbolic
Collaborator
Author
|
I've addressed all the comments, plus I've added some more documenting comments to SymbTheorems and SymbExamples as well. |
berpeti
approved these changes
Feb 17, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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.