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    });
..    // ...

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    ]);
..    // ...

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();
..    // ...

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

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 ) {
..    // ...

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

..    // ...
62    commit();
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();
..    // ...

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

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();
..    // ...

Let’s run the program and see what happens:

$ ./reach run

Bob accepts the wager of 5.

Alice played Paper

Bob played Rock

Bob saw outcome Alice wins

Alice saw outcome Alice wins

Alice went from 10 to 14.9999.

Bob went from 10 to 4.9999.


$ ./reach run

Bob accepts the wager of 5.

Alice played Rock

Bob played Rock

Alice played Paper

Bob played Scissors

Bob saw outcome Bob wins

Alice saw outcome Bob wins

Alice went from 10 to 4.9999.

Bob went from 10 to 14.9999.


$ ./reach run

Bob accepts the wager of 5.

Alice played Scissors

Bob played Rock

Bob saw outcome Bob wins

Alice saw outcome Bob wins

Alice went from 10 to 4.9999.

Bob went from 10 to 14.9999.

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.


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.


All of the above.