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

Allow use of Cryptol property names as simplification rules #1755

Merged
merged 9 commits into from
Oct 18, 2022

Conversation

samcowger
Copy link
Contributor

Allow users to prove Cryptol properties by name, without unfolding, and use them as simplification rules in SAW. (The former was already possible, this PR introduces the latter as a new capability.) See the included regression test for an example.

Better than the earlier approach, this leverages the fact that every unfoldable
constant is constructed with a `Just body` and restricts unfolding to happen
within `ruleAsProp`. Also, pipe a `SharedContext` to `ruleAsProp` to allow
leveraging `scApplyAllBeta` to beta-reduce the unfolded term before checking
rule well-formedness again.
Also, previous commits' references to `ruleAsProp` should have been to
`ruleOfProp`.
@samcowger samcowger self-assigned this Oct 17, 2022
@samcowger
Copy link
Contributor Author

For some reason, I'm only just now seeing these CI failures when running tests on my machine. Review may not yet be appropriate, so I'm going to demote this to draft status while I poke around.

@samcowger samcowger marked this pull request as draft October 17, 2022 21:34
@samcowger samcowger marked this pull request as ready for review October 18, 2022 01:39
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.

Looks good, thanks Sam!

@samcowger samcowger 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 Oct 18, 2022
@mergify mergify bot merged commit 2ae9d9b into master Oct 18, 2022
@mergify mergify bot deleted the feature/cryptol-property-unfolding branch October 18, 2022 22:25
weaversa added a commit to weaversa/aes-rust that referenced this pull request Nov 3, 2022
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
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants