2.7 Play and Play Again

In this section, we extend our application so that Alice and Bob will continue to play against each other until there is a clear winner, so if it is a draw they will continue playing.

This will only require a change to the Reach program, not the JavaScript frontend, but we will take the opportunity to modify the frontend so that timeouts can happen to both parties when they are asked to submit their hands. Let’s do that to get it out of the way and not distract from the main task of removing draws.

We’ll modify the Player interact object so that it will have a different getHand method.

..    // ...
20    const Player = (Who) => ({
21      ...stdlib.hasRandom,
22      getHand: async () => { // <-- async now
23        const hand = Math.floor(Math.random() * 3);
24        console.log(`${Who} played ${HAND[hand]}`);
25        if ( Math.random() <= 0.01 ) {
26          for ( let i = 0; i < 10; i++ ) {
27            console.log(`  ${Who} takes their sweet time sending it back...`);
28            await stdlib.wait(1);
29          }
30        }
31        return hand;
32      },
33      seeOutcome: (outcome) => {
34        console.log(`${Who} saw outcome ${OUTCOME[outcome]}`);
35      },
36      informTimeout: () => {
37        console.log(`${Who} observed a timeout`);
38      },
39    });
..    // ...

• Lines 25 through 30 moves the forced timeout code that we wrote for Bob’s acceptWager function into this method. We also change the threshold so that timeouts only happen 1% of the time. This isn’t a very interesting behavior, so we’ll make it much less frequent.

We also adjust Bob’s acceptWager function to remove the timeout code, since we’re testing that differently now. It’s just a matter of reverting to the simpler version from before.

..    // ...
41    await Promise.all([
42      backend.Alice(ctcAlice, {
43        ...Player('Alice'),
44        wager: stdlib.parseCurrency(5),
45        deadline: 10,
46      }),
47      backend.Bob(ctcBob, {
48        ...Player('Bob'),
49        acceptWager: (amt) => {
50          console.log(`Bob accepts the wager of ${fmt(amt)}.`);
51        },
52      }),
53    ]);
..    // ...

• Lines 49 through 51 have the simpler acceptWager method for Bob.

—

Now, let’s look at the Reach application. All of the details about the playing of the game and the interface to the players will remain the same. The only thing that’s going to be different is the order the actions take place.

It used to be that the steps were:

1. Alice sends her wager and commitment.

2. Bob accepts the wager and sends his hand.

3. Alice reveals her hand.

4. The game ends.

But, now because the players may submit many hands, but should only have a single wager, we’ll break these steps up differently, as follows:

1. Alice sends her wager.

2. Bob accepts the wager.

3. Alice sends her commitment.

4. Bob sends his hand.

5. Alice reveals her hand.

6. If it’s draw, return to step 3; otherwise, the game ends.

Let’s make these changes now.

..    // ...
45    Alice.only(() => {
46      const wager = declassify(interact.wager);
47      const deadline = declassify(interact.deadline);
48    });
49    Alice.publish(wager, deadline)
50      .pay(wager);
51    commit();
..    // ...

• Line 49 has Alice publish the wager and deadline.

• Line 50 has Alice pay the wager.

..    // ...
53    Bob.only(() => {
54      interact.acceptWager(wager);
55    });
56    Bob.pay(wager)
57      .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout));
58    
..    // ...

• Line 56 has Bob pay the wager.

• Line 58 does not have this consensus step commit.

—

It’s now time to begin the repeatable section of the application, where each party will repeatedly submit hands until the the outcome is not a draw. In normal programming languages, such a circumstance would be implemented with a while loop, which is exactly what we’ll do in Reach. However, while loops in Reach require extra care, as discussed in the guide on loops in Reach, so we’ll take it slow.

In the rest of a Reach program, all identifier bindings are static and unchangable, but if this were the case throughout all of Reach, then while loops would either never start or never terminate, because the loop condition would never change. So, a while loop in Reach can introduce a variable binding.

Next, because of Reach’s automatic verification engine, we must be able to make a statement about what properties of the program are invariant before and after a while loop body’s execution, a so-called "loop invariant".

Finally, such loops may only occur inside of consensus steps. That’s why Bob’s transaction was not committed, because we need to remain inside of the consensus to start the while loop. This is because all of the participants must agree on the direction of control flow in the application.

Here’s what the structure looks like:

..    // ...
59    var outcome = DRAW;
60    invariant( balance() == 2 * wager && isOutcome(outcome) );
61    while ( outcome == DRAW ) {
..    // ...

• Line 59 defines the loop variable, outcome.

• Line 60 states the invariant that the body of the loop does not change the balance in the contract account and that outcome is a valid outcome.

• Line 61 begins the loop with the condition that it continues as long as the outcome is a draw.

Now, let’s look at the body of the loop for the remaining steps, starting with Alice’s commitment to her hand.

..    // ...
62    commit();
63    
64    Alice.only(() => {
65      const _handAlice = interact.getHand();
66      const [_commitAlice, _saltAlice] = makeCommitment(interact, _handAlice);
67      const commitAlice = declassify(_commitAlice);
68    });
69    Alice.publish(commitAlice)
70      .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout));
71    commit();
..    // ...

• Line 62 commits the last transaction, which at the start of the loop is Bob’s acceptance of the wager, and at subsequent runs of the loop is Alice’s publication of her hand.

• Lines 64 through 71 are almost identical to the older version, except the wager is already known and paid.

..    // ...
73    unknowable(Bob, Alice(_handAlice, _saltAlice));
74    Bob.only(() => {
75      const handBob = declassify(interact.getHand());
76    });
77    Bob.publish(handBob)
78      .timeout(relativeTime(deadline), () => closeTo(Alice, informTimeout));
79    commit();
..    // ...

Similarly, Bob’s code is almost identical to the prior version, except that he’s already accepted and paid the wager.

..    // ...
81    Alice.only(() => {
82      const saltAlice = declassify(_saltAlice);
83      const handAlice = declassify(_handAlice);
84    });
85    Alice.publish(saltAlice, handAlice)
86      .timeout(relativeTime(deadline), () => closeTo(Bob, informTimeout));
87    checkCommitment(commitAlice, saltAlice, handAlice);
..    // ...

Alice’s next step is actually identical, because she is still revealing her hand in exactly the same way.

Next is the end of the loop.

..    // ...
89      outcome = winner(handAlice, handBob);
90      continue;
91    }
..    // ...

• Line 89 updates the outcome loop variable with the new value.

• Line 90 continues the loop. Unlike most programming languages, Reach requires that continue be explicitly written in the loop body.

The rest of the program could be exactly the same as it was before, except now it occurs outside of the loop, but we will simplify it, because we know that the outcome can never be a draw.

..    // ...
93    assert(outcome == A_WINS || outcome == B_WINS);
94    transfer(2 * wager).to(outcome == A_WINS ? Alice : Bob);
95    commit();
..    // ...

• Line 93 asserts that the outcome is never draw, which is trivially true because otherwise the while loop would not have exitted.

• Line 94 transfers the funds to the winner.

—

Let’s run the program and see what happens:

As usual, your results may differ, but you should be able to see single round victories like this, as well as multi-round fights and timeouts from either party.

If your version isn’t working, look at the complete versions of tut-7/index.rsh and tut-7/index.mjs to make sure you copied everything down correctly!

Now our implementation of Rock, Paper, Scissors! will always result in a pay-out, which is much more fun for everyone. In the next step, we’ll show how to exit "testing" mode with Reach and turn our JavaScript into an interactive Rock, Paper, Scissors! game with real users.

Check your understanding: How do you write an application in Reach that runs arbitrarily long, like a game of Rock, Paper, Scissors that is guaranteed to not end in a draw?

1. This is not possible, because all Reach programs are finitely long;

2. You can use a while loop that runs until the outcome of the game is decided.

Answer:

2; Reach supports while loops.

Check your understanding: When you check if a program with a while loop is correct, you need to have a property called a loop invariant. Which of the following statements have to be true about the loop invariant?

1. The part of the program before the while loop must establish the invariant.

2. The condition and the body of the loop must establish the invariant.

3. The negation of the condition and the invariant must establish any properties of the rest of the program.

Answer:

All of the above.