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

Expand Mr. Solver heterogeneity, improve monadification for SHA512 example #1686

Merged
merged 18 commits into from
Jun 10, 2022

Conversation

m-yac
Copy link
Contributor

@m-yac m-yac commented Jun 7, 2022

This PR has two main parts:

  • (506b072) Extend Mr. Solver's heterogeneous notion of equality to function refinement and co-inductive hypothesis widening.
  • (e98a6be) Remove all usages of openOpenTerm and fixes some other bugs involving free variables in Monadification

The former enabled the refinement processBlock |= processBlock_spec to go through, and the latter enabled processBlocks_spec to monadify. Of course, both of these also needed other, smaller, changes - each commit should be self-contained enough to review individually.

My final batch of commits at the end are to make progress on processBlocks |= processBlocks_spec (note the "s"es), but this refinement does not yet go through, so it is commented out.

@m-yac m-yac added the subsystem: MRSolver Issues related to the Mr. Solver monadic-recursive solver in Heapster label Jun 7, 2022
@m-yac m-yac requested a review from eddywestbrook June 7, 2022 21:10
Copy link
Contributor

@eddywestbrook eddywestbrook left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It mostly looks good to me, but I didn't quite follow all the details... However, because it seems to work and has been tested, I'm comfortable with this change

@eddywestbrook eddywestbrook added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Jun 10, 2022
@mergify mergify bot merged commit 3dfa6b6 into master Jun 10, 2022
@mergify mergify bot deleted the mr-solver/sha512-3 branch June 10, 2022 22:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: MRSolver Issues related to the Mr. Solver monadic-recursive solver in Heapster
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants