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

Heapster multi-way or eliminations #1690

Merged
merged 14 commits into from
Jun 17, 2022
Merged

Heapster multi-way or eliminations #1690

merged 14 commits into from
Jun 17, 2022

Conversation

eddywestbrook
Copy link
Contributor

This PR changes Heapster's or elimination rule so that it can eliminate multiple nested or permissions in one step. That is, the or elimination rule can now eliminate a right-nested disjunction of the form p1 or (p2 or (... or pn)) into the n different cases p1, p2, ..., pn in one step. The translation of multi-way or elimination uses a single multi-way sum elimination function called eithers. The benefit of this change is that it reduces the size of the extracted Coq specifications when there are disjunctive types with many cases, such as a Rust enum type with a large number of constructors, because those types used to require n-1 nested calls to the either elimination function, each of which had to duplicate all of the types being eliminated.

@eddywestbrook eddywestbrook requested a review from m-yac June 16, 2022 01:16
@eddywestbrook
Copy link
Contributor Author

Whoops, looks like the mbox proofs do not work with this change yet...

Copy link
Contributor

@m-yac m-yac left a comment

Choose a reason for hiding this comment

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

LGTM.

@m-yac m-yac added PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster labels Jun 17, 2022
@mergify mergify bot merged commit 8be2c1d into master Jun 17, 2022
@mergify mergify bot deleted the heapster/elim-ors branch June 17, 2022 22:56
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: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants