Write a theorem (and check it!) that would be false if timeouts were not supported or if escrows were not included

[jeapostrophe]

We know that timeouts and escrows are useful because they ensure that all parties will play honestly. However, we don't currently have any theorem that would be incorrect if the RPS protocol were written to not include the escrow (which is does) or the timeout (which it does not.)

For escrows, I think the answer is an "economic rationality" test where we prove that it is rational for A to reveal their hand, even if they are going to lose, to get back their escrow. The expected value of the next step would be greater than or equal to the expected value of the current step.

Step	A	B
(0) Before	0	0
(1) A commit	- (wager + escrow)	0
(2) B reveals	- (wager + escrow)	-wager
(3a) A reveals, A wins	(2 * wager + escrow)	0
(3b) A reveals, B wins	escrow	2 * wager
(3c) A reveals, Draw	wager + escrow	wager

The problem with this is that it is not rational for B to play with this rule. That means that we couldn't make this a general theorem to prove always, but merely make it a specific theorem about A.

For timeouts, I think we need to integrate something like "kill-safety" where a participant can stop acting and we need to handle the exception. In this case, timeouts are really just a way of implementing spontaneous participant death and we would actually FORCE every protocol to deal with it. I don't know how to do this robustly, however, with "participant classes" rather than just "participants".

[fare]

That would be the game theoretic safety theorem: for each player, the safety theorem says that even if the other players don't cooperate, they can get their stake out of the interaction, losing only a bounded amount of time and gas.

The difficulty in writing the theorem for RPS might be in defining what "the stake" of the player is, since each player expects a chance of losing their money in a fair way. One way around it would be to assume that each player will be satisfied if the interaction completes according to the rules, and that in any other case (i.e. timeout), they get restored to the resources they had at the beginning of the interaction, or a fair upgrade to it (e.g. they lose some bitcoin but gain more than equivalent ethereum from the other participant's collateral).

Indeed, timeouts are all about "kill safety": the various require statements (in Solidity parlance; verify in Bitcoin script) ensure that all transitions are valid, so that the only remaining invalid cases are timeouts—at least, in direct style. In indirect style, we implement the direct style on top of some verification layer, that does include explicitly losing stakes in additional ways, by making claims later proven invalid.

[fare]

Thinking of safety in terms of layers of abstractions crucially allows us to decompose the proof in small bits: proof of the high-level protocol, proof of each layer of implementation—where other DApp systems may have to deal with the full exponential formula for the complete expansion.

Thus—prove the protocol as written in terms of "must send" messages; then prove that the each "must send" is sufficiently implemented in terms of "may send" and timeout; then prove that sending synchronous consensual messages is implemented in terms of sending asynchronous messages off-chain plus using a verification contract to force synchronous publication on-chain in case of dispute; then prove that sending messages constrained by a complex validity requirement is implemented in terms of of making claims and arguing the validity of the claim with Game Semantics; etc.