Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Library procedure RG contradiction proof #163

Merged
merged 9 commits into from
Feb 19, 2024
Merged

Conversation

ailrst
Copy link
Contributor

@ailrst ailrst commented Feb 1, 2024

Implements the proof by contradiction style of procedure rely/guarantee.

This should be easier for boogie to reason about.

  • Adds cli flag to enable and choose the encoding to use
  • Adds direct expression spec construct to allow embeddeing boogie syntax we don't support via DIRECT :: "boogie literal expr" : bool, this isn't great because obviously variables and globals aren't captured for modifies inference etc

@l-kent
Copy link
Contributor

l-kent commented Feb 1, 2024

You probably shouldn't have committed whatever beans and beans2 are?

This way of embedding boogie directly in the specifications seems messy since it's inconsistent with the existing Ensures DIRECT: syntax? (Which was already not really ideal)

this isn't great because obviously variables and globals aren't captured for modifies inference etc

I don't think this should be a problem in practice for the external procedure rely/guarantees. It very much will be if you use it for the thread-level rely/guarantees

@ailrst ailrst force-pushed the procedure-rg-contra branch from a5fdc54 to d3afe35 Compare February 5, 2024 01:39
@ailrst
Copy link
Contributor Author

ailrst commented Feb 5, 2024

Beans is removed now,

This way of embedding boogie directly in the specifications seems messy since it's inconsistent with the existing Ensures DIRECT: syntax? (Which was already not really ideal)

I modelled the syntax on the boogie lambda/forall/exists syntax somewhat, it could be more consistent because we only need the direct syntax in the expression context, rather than every top-level declaration.

@ailrst ailrst changed the base branch from main to staging February 19, 2024 05:09
@ailrst ailrst merged commit 1acdef4 into staging Feb 19, 2024
1 check passed
@ailrst ailrst mentioned this pull request Feb 19, 2024
3 tasks
@ailrst ailrst deleted the procedure-rg-contra branch July 3, 2024 01:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants