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.
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.
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.
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.
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