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

subsumespec_app1, subsumespec_app2 #660

Closed
andrew-appel opened this issue Feb 1, 2023 · 1 comment · Fixed by #661
Closed

subsumespec_app1, subsumespec_app2 #660

andrew-appel opened this issue Feb 1, 2023 · 1 comment · Fixed by #661

Comments

@andrew-appel
Copy link
Collaborator

In floyd/forward.v, the lemmas subsumespec_app1 and subsumespec_app1 take forever.
Same for tycontext_sub_Gprog_app1, tycontext_sub_Gprog_app2.

Perhaps with explicitly instantiated arguments to funspec_sub_si_refl, these lemmas would be instantaneous.
@andrew-appel
Copy link
Collaborator Author

Solution: apply seplog.funspec_sub_si_refl instead of apply funspec_sub_si_refl.
I've fixed this in a branch that may or may not make into master someday, but this fix can also be applied independently at any time.

andrew-appel added a commit that referenced this issue Feb 2, 2023
@andrew-appel
Use (new) bool2val instead of Val.of_bool
48ebe2b 
This P.R. implements the suggestion in issue #625.
It's an experiment, as in some cases it breaks existing VST proofs
at `forward_if` and related tactics.  The changes required in those
proofs are generally positive (simplifies proof scripts).
See further discussion at #625.  closes #625

Incidentally and unrelated:  closes #660
@andrew-appel andrew-appel mentioned this issue Feb 2, 2023
Merged
andrew-appel added a commit that referenced this issue Feb 7, 2023
@andrew-appel
Use (new) bool2val instead of Val.of_bool (#661)
416b6df 
* Use (new) bool2val instead of Val.of_bool

This P.R. implements the suggestion in issue #625.
It's an experiment, as in some cases it breaks existing VST proofs
at `forward_if` and related tactics.  The changes required in those
proofs are generally positive (simplifies proof scripts).
See further discussion at #625.  closes #625

Incidentally and unrelated:  closes #660

* Adjustment for 32/64-bit portability
* Fix memory blowup; bring verif_strlib up to date in 64-bit mode
* Fix up a proof in tweetnacl
* Bring mailbox up to date with bool2val
* simplify_new_temp in fwd_result, in connection with new bool2val stuff
* Flesh out simplify_new_temp hint DB; bring 32-bit examples up to date
* Update CHANGES file
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Use (new) bool2val instead of Val.of_bool PrincetonUniversity/VST
1 participant
@andrew-appel