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.

Sign up for GitHub

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

Jump to bottom

Remove usage of opaque from standard library #5781

Merged
merged 44 commits into from
Dec 2, 2024
Merged

Remove usage of opaque from standard library #5781

merged 44 commits into from
Dec 2, 2024

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Sep 18, 2024 •
edited
Loading

Description

  • Remove usage of opaque from standard library
  • Fix a bug in the substitution logic of hide/reveal statements

How has this been tested?

  • Standard library is verified by CI
  • Updated a CLI test to test for the fixed bug

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@MikaelMayer
Copy link
Member

I would expect to remove this attribute only when the new resolver works on all the existing Dafny files in our codebase, is that your plan too?

@keyboardDrummer keyboardDrummer marked this pull request as ready for review November 4, 2024 14:02
@keyboardDrummer keyboardDrummer enabled auto-merge (squash) November 4, 2024 14:02
@keyboardDrummer
Copy link
Member Author

I would expect to remove this attribute only when the new resolver works on all the existing Dafny files in our codebase, is that your plan too?

Hide works using the old resolver as well now, so I think this point is no longer relevant.

MikaelMayer
MikaelMayer previously approved these changes Nov 8, 2024
View reviewed changes
Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

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

What a huge simplification effort ! If it passes, I'm all in.

Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Serializer.dfy
assert wr.Bytes() == writer.Bytes() + Spec.Bracketed(obj, Spec.Member);

assert wr.Bytes() == writer.Bytes() + Spec.Bracketed(obj, Spec.Member) by {
hide *;
Copy link
Member

Choose a reason for hiding this comment

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

This is surprising. How does that work?

Copy link
Member Author

@keyboardDrummer keyboardDrummer Nov 12, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

I'm not sure. I don't see how the proof is possible without the body of Spec.Bracketed being visible, although I might have missed something. It might be good to understand this first. I'll work on a feature that will show what is hidden/revealed when using *.

Copy link
Member Author

Choose a reason for hiding this comment

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

Investigating this, I found a bug that prevented this hide * from having any effect. I resolved that bug and then I had to remove this hide * for it to still verify

@keyboardDrummer keyboardDrummer mentioned this pull request Nov 14, 2024
Merged
@keyboardDrummer keyboardDrummer merged commit f9daa74 into dafny-lang:master Dec 2, 2024
22 checks passed
@keyboardDrummer keyboardDrummer deleted the hideRevealStdLib branch December 2, 2024 15:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MikaelMayer MikaelMayer MikaelMayer approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@keyboardDrummer @MikaelMayer