-
Notifications
You must be signed in to change notification settings - Fork 19
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
Discard invalid actions #99
Conversation
LGTM. @annenkov what do you think? |
Looks good. Basically, an action can be dropped if one can prove that there is no derivation that evaluates the action. |
I have an itch that this is related to something like the inversion tactic, but I haven't had the time to think deeply about this. |
execution/theories/Blockchain.v
Outdated
+ now rewrite_environment_equiv. | ||
+ assumption. |
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 actually liked the previous version better. Basically, intuition
solves only a couple of goals automatically and the rest is still bullet points. I try to use intuition
followed by some tactic that solves most (or better - all) of the remaining goals after intuition.
Also, intuition
can be slow and sometimes uses axioms coming from heterogeneous equality without your consent, I find it quite annoying. So, intuition
is a powerful tool, but it this case maybe it's better to use something simpler. I guess repeat split;auto
will have the same effect.
But I don't mind if you think it's better.
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 I prefer repeat split; auto
since it reduces the size of the proof as much as intuition
but is much faster.
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 have pushed an even shorter proof that avoids intuition
and bullet points.
Both are ok with me
from my phone
…On Thu, Jun 17, 2021, 12:36 4ever2 ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In execution/theories/Blockchain.v
<#99 (comment)>:
> + now rewrite_environment_equiv.
- + assumption.
I think I prefer repeat split; auto since it reduces the size of the
proof as much as intuition but is much faster.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#99 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AABTNTTCMFRSI3LTIDYO3OLTTHF4FANCNFSM462M5HZQ>
.
|
chain_state_queue prev_bstate = act :: acts -> | ||
chain_state_queue next_bstate = acts -> | ||
act_is_from_account act -> | ||
(forall bstate new_acts, ~ inhabited (ActionEvaluation prev_bstate act bstate new_acts)) -> |
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.
Nit: You can avoid some steps in future proofs by making it ActionEvaluation prev_bstate act bstate new_acts -> False
.
If nobody objects, I'm going to merge the PR then. |
I did have some feedback above :) |
Closes #93