-
Notifications
You must be signed in to change notification settings - Fork 63
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
Fix examples after en tree #1827
base: master
Are you sure you want to change the base?
Conversation
…nto heapster-ide-info
…edMb.hs, to help with GHC 9 support
…nged the names of all of its operationsto use 'Named' as a suffix instead of just using a prime
It didn't feel like using manual proves was instructive, so that's why I automated it. I would assume that more automation will be created for refinements, so hopfully what I wrote is a step in the right direction. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've given this a look, mostly focusing on the tutorial. I have not looked deeply at the details of the proofs themselves, so if there is a particular proof that you would like me to give closer scrutiny, let me know.
Import CompMExtraNotation. Open Scope fun_syntax. | ||
(* The following 2 lines allows better automatio*) | ||
Require Import Examples.common. | ||
Require Import Coq.Program.Tactics. (* Great tacticals, move to automation. Perhaps `Require Export`? *) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure how to read this comment. Does this belong in a tutorial?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess not.
Lemma no_errors_add_mistyped (x: bitvector 64) : | ||
spec_refines_eq (add_mistyped x) (safety_spec (x)). | ||
Proof. solve_trivial_spec 0 0. | ||
|
||
(* After rewriting the terms for clarity, you can see the | ||
remaining goal says that an `ErrorS` is a refinement of | ||
`RetS`. In other words, it's trying to prove that a trivially | ||
pure function has an error. That's obviously false. *) | ||
clarify_goal_tutorial. | ||
Abort. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this be surrounded with code blocks ``` ... ```
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good catch.
``` | ||
|
||
Lemma no_errors_incr_ptr (x: bitvector 64) : | ||
spec_refines_eq (incr_ptr x) (safety_spec x). | ||
Proof. solve_trivial_spec 0 0. Qed.``` | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this code block is missing a closing ```
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed in latest commit.
entails anything). | ||
important steps are handled by custom automation. | ||
|
||
TODO: This proof is involved. Perhaps add some more details? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, I definitely think so! Are you planning to resolve this TODO in this PR, or are you leaving this as future work?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a good point. The description more or less gets to the limit of what I understand, without going into technical details. Do you have any suggestion of how to improve this section?
We can also just commit the comment and leave it super high level at this point.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ideally, we would include a more detailed tutorial that goes into the nuances of spec_refines
proofs involving loops. But writing such a tutorial would take a fair bit of effort, so I can understand if you don't want to do that here. My recommendation would be to:
- Remove this TODO (since TODOs in a tutorial look out of place), and
- Open an issue as a reminder to write this more detailed tutorial.
#xor_swap_proofs.v | ||
xor_swap_proofs.v | ||
xor_swap_rust_gen.v | ||
#xor_swap_rust_proofs.v | ||
c_data_gen.v | ||
#c_data_proofs.v | ||
c_data_proofs.v |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm surprised that this isn't adding back more of the _proofs.v
files that you've changed in this PR, such as arrays_proofs.v
. Any reason not to?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I haven't finished the proofs in arrays_proofs.v
, I only fixed the first one which is the one mentioned in the tutorial.
(*This is a prototype of a tactic to solve all signed inequalities for | ||
Boolean vectors, as long as there is no overflow. Ideally, if the | ||
tactic fails, it will show you the bounds you need to prove that thre | ||
is no overflow. You probably missed them in your invariants. | ||
|
||
The idea is pretty simple: convert everything to to `Int` and, becasue | ||
there is no overflow, we can remove the module quantifiers and crush | ||
it with standard lia. | ||
|
||
TO DO: | ||
|
||
- Support all arith relations eq[ ], lt[ ], gt[ ], le[✓], ge[ ] | ||
|
||
- Don't directly apply rewrites to all subgoals for efficiency | ||
|
||
- Recognize when there is a terminal "node" to apply `lia`. Right now | ||
we attempt lia at every step, whcih is wasteful. | ||
|
||
*) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is probably worth having a discussion about independently of this PR. Can you open an issue to track the design and discussion of this feature?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Added #1836
|
||
Qed. | ||
|
||
(* The old version |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A personal thing, but I'd favor just removing the old, commented-out versions. They'll still exist in the git
history if we want to look at them again in the future.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fair enough.
typo Co-authored-by: Ryan Scott <rscott@galois.com>
typo Co-authored-by: Ryan Scott <rscott@galois.com>
typo Co-authored-by: Ryan Scott <rscott@galois.com>
Typo Co-authored-by: Ryan Scott <rscott@galois.com>
…Inc/saw-script into Fix-Examples-After-EnTree
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@RyanGlScott , thank you for the review. I think I have addressed all of your points, except the question regarding the TODO. Let me know what you think.
Import CompMExtraNotation. Open Scope fun_syntax. | ||
(* The following 2 lines allows better automatio*) | ||
Require Import Examples.common. | ||
Require Import Coq.Program.Tactics. (* Great tacticals, move to automation. Perhaps `Require Export`? *) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess not.
Lemma no_errors_add_mistyped (x: bitvector 64) : | ||
spec_refines_eq (add_mistyped x) (safety_spec (x)). | ||
Proof. solve_trivial_spec 0 0. | ||
|
||
(* After rewriting the terms for clarity, you can see the | ||
remaining goal says that an `ErrorS` is a refinement of | ||
`RetS`. In other words, it's trying to prove that a trivially | ||
pure function has an error. That's obviously false. *) | ||
clarify_goal_tutorial. | ||
Abort. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good catch.
``` | ||
|
||
Lemma no_errors_incr_ptr (x: bitvector 64) : | ||
spec_refines_eq (incr_ptr x) (safety_spec x). | ||
Proof. solve_trivial_spec 0 0. Qed.``` | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed in latest commit.
``` | ||
|
||
The arguments `e1`, `e2` and `p1` correspond to the length `len`, the | ||
The arguments `e0`, `e1` and `p1` correspond to the length `len`, the |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good point. Added some text.
entails anything). | ||
important steps are handled by custom automation. | ||
|
||
TODO: This proof is involved. Perhaps add some more details? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a good point. The description more or less gets to the limit of what I understand, without going into technical details. Do you have any suggestion of how to improve this section?
We can also just commit the comment and leave it super high level at this point.
#xor_swap_proofs.v | ||
xor_swap_proofs.v | ||
xor_swap_rust_gen.v | ||
#xor_swap_rust_proofs.v | ||
c_data_gen.v | ||
#c_data_proofs.v | ||
c_data_proofs.v |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I haven't finished the proofs in arrays_proofs.v
, I only fixed the first one which is the one mentioned in the tutorial.
(*This is a prototype of a tactic to solve all signed inequalities for | ||
Boolean vectors, as long as there is no overflow. Ideally, if the | ||
tactic fails, it will show you the bounds you need to prove that thre | ||
is no overflow. You probably missed them in your invariants. | ||
|
||
The idea is pretty simple: convert everything to to `Int` and, becasue | ||
there is no overflow, we can remove the module quantifiers and crush | ||
it with standard lia. | ||
|
||
TO DO: | ||
|
||
- Support all arith relations eq[ ], lt[ ], gt[ ], le[✓], ge[ ] | ||
|
||
- Don't directly apply rewrites to all subgoals for efficiency | ||
|
||
- Recognize when there is a terminal "node" to apply `lia`. Right now | ||
we attempt lia at every step, whcih is wasteful. | ||
|
||
*) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Added #1836
|
||
Qed. | ||
|
||
(* The old version |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fair enough.
This PR updates some of the examples and the tutorial to the new Heapster semantics with EnTrees.
We should wait for
heapster-ide-info
to be merged so we can merge directly intomaster
.