search

AlacrisIO / meta

Internal management of Legicash/Legilogic/Alacris
0 stars 0 forks source link

Check game-theoretic safety properties #159

Open fare opened 5 years ago

fare commented 5 years ago

The main advantage of our approach over that of other people who use formal methods to verify smart contracts is that we have this explicit notion of multiple participants, out of which we can extract game-theoretic safety properties for each participant, that are not expressible in participant-agnostic formalisms. Let's make sure we prove at least some such properties for RPS and have a way to express them explicitly if we cannot derive them fully implicitly.

fare commented 4 years ago

The possible? and eventual? predicates in an @A block, or a variant thereof, should be adversarial: it should take into account the fact that B will actively try to make it not happen.

fare commented 4 years ago

Do something with the correct quantifiers for now. See #166 for the next level.

fare commented 4 years ago

Also, Jay's fair_game predicates are extremely round about. Hopefully, it should be possible to say at a point before A choses his hand something like possible? (outcome == A_WINS), which either assumes the content inside possible? is all-seeing of the bindings at the end of the interaction, or we have an explicit label feature and COMEFROM feature such that we can express possible? END(outcome == A_WINS) at the point where we assert it's a possible future.

Then there's the matter of the quantifiers: existence with or without a winning strategy, against or not against the other participant's winning strategies.