Intermediate · 30 minutes

Algorand Blockchain Development using Reach - Part 6: Looping to Determine the Winner

In this tutorial, the user will learn how to implement loops in Reach. This will require determining a winner to end the game and allow the wager to settle.

Kwame Bryan Developer Ambassador

February 11, 2021

JavaScript

Requirements

This is a continuation of a series of tutorials and assumes you have completed all of them previously. Many new concepts were introduced that many seasoned developers may not be accustomed too.
Link to previous tutorial 5

Background

You will need a background in a modern programming languages such as JavaScript to follow this tutorial. It is also recommended to use the Reach Docs as a guide.

First, we are going to update our index.rsh file to allow game play to continue until there is a clear winner. Let’s revisit the steps in our current implementation.

It used to be that the steps were:

Alice sends her wager and commitment.
Bob accepts the wager and sends his hand.
Alice reveals her hand.
The game ends.

The players may submit many hands but should only have a single wager. We’ll break these steps up differently, as follows:

Alice sends her wager.
Bob accepts the wager.
Alice sends her commitment.
Bob sends his hand.
Alice reveals her hand.
If it’s draw, return to Alice sending her commitment; otherwise, the game ends.

Let’s make these changes now in our index.rsh file.

 A.only(() => {
     const wager = declassify(interact.wager); });
A.publish(wager)
    .pay(wager);
commit();

The above code has Alice publish and pay the wager

B.only(() => {
    interact.acceptWager(wager); }); 
B.pay(wager)
    .timeout(DEADLINE, () => closeTo(A, informTimeout));

The above code has Bob pay the wager and 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 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.

Finding and using Invariants

Reach requires that while loops are annotated with loop invariants. A loop invariant is a property INV which is true before the loop starts and is true after the loop ends.

Consider the following program fragment

... before ...
var V = INIT;
invariant( INV );
while ( COND ) {
 ... body ...
 V = NEXT;
 continue; }
... after ...
assert(P);

We can summarize the properties that must be true about this code as follows:

before and V = INIT implies INV — The earlier part of the program must establish INV.
If COND and INV, then body and V = NEXT implies INV — The loop body can make use of the truth of the condition and the invariant to re-establish the invariant after V is mutated to NEXT.
! COND and INV and after implies P — The later part of the program can make use of the negation of the condition and the invariant to establish any future assertions.

Loop invariants only need to mention values that can vary because of the execution of the loop. In Reach, all bindings are immutable, except for those bound by while, so they never need to be mentioned.

While loops in Reach

var [ heap1, heap2 ] = [ 21, 21 ];
invariant(balance() == 2 * wagerAmount);
while ( heap1 + heap2 > 0 ) {
  ....
  [ heap1, heap2 ] = [ heap1 - 1, heap2 ];
  continue; }

A while statement may occur within a consensus step and is written

var LHS = INIT_EXPR;
invariant(INVARIANT_EXPR);
while( COND_EXPR ) BLOCK

where LHS is a valid left-hand side of an identifier definition where the expression INIT_EXPR is the right-hand side, and INVARIANT_EXPR is an expression, called the loop invariant, that must be true before and after every execution of the block BLOCK, and if COND_EXPR is true, then the block executes, and if not, then the loop terminates and control transfers to the continuation of the while statement. The identifiers bound by LHS are bound within INVARIANT_EXPR, COND_EXPR, BLOCK, and the tail of the while statement.

With a bit of theory we can now implement the repeatable section of the application. Reach’s automatic verification engine 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”.

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

outcome = DRAW; 
invariant(balance() == 2 * wager && isOutcome(outcome) );
while ( outcome == DRAW ) {

The above code defines the loop variable, outcome and 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. Lastly, 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.

commit();

A.only(() => {
    const _handA = interact.getHand();
    const [_commitA, _saltA] = makeCommitment(interact, _handA);
    const commitA = declassify(_commitA); });
    A.publish(commitA)
      .timeout(DEADLINE, () => closeTo(B, informTimeout));
    commit();

The above code 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. You should recognize from following this series that is almost identical to the previous implementation, except the wager is already known and paid.

unknowable(B, A(_handA, _saltA));
B.only(() => {
    const handB = declassify(interact.getHand()); });
B.publish(handB)
    .timeout(DEADLINE, () => closeTo(A, informTimeout));
commit();

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

A.only(() => {
    const [saltA, handA] = declassify([_saltA, _handA]); });
A.publish(saltA, handA)
    .timeout(DEADLINE, () => closeTo(B, informTimeout));
checkCommitment(commitA, saltA, handA);

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.

index.rsh

outcome = winner(handA, handB);
continue;}

The above code updates the outcome loop variable with the new value and 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.

assert(outcome == A_WINS || outcome == B_WINS);
transfer(2 * wager).to(outcome == A_WINS ? A : B);
commit();

each([A, B], () => {
    interact.seeOutcome(outcome); });
exit(); });

The above code asserts that the outcome is never draw, which is trivially true because otherwise the while loop would not have exitted and then transfers the funds to the winner. With that done we can now compile our program.

Compile and run the program

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

Your results will differ. Now our Rock, Paper, Scissors! game will always result in a pay-out, which is much more fun for everyone. :P 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 and use React and a web wallet to interact with our dApp. Till then

Final Source

index.mjs

import { loadStdlib } from '@reach-sh/stdlib';
import * as backend from './build/index.main.mjs';

(async () => {
  const stdlib = await loadStdlib();
  const startingBalance = stdlib.parseCurrency(10);
  const accAlice = await stdlib.newTestAccount(startingBalance);
  const accBob = await stdlib.newTestAccount(startingBalance);

  const fmt = (x) => stdlib.formatCurrency(x, 4);
  const getBalance = async (who) => fmt(await stdlib.balanceOf(who));
  const beforeAlice = await getBalance(accAlice);
  const beforeBob = await getBalance(accBob);

  const ctcAlice = accAlice.deploy(backend);
  const ctcBob = accBob.attach(backend, ctcAlice.getInfo());

  const HAND = ['Rock', 'Paper', 'Scissors'];
  const OUTCOME = ['Bob wins', 'Draw', 'Alice wins'];
  const Player = (Who) => ({
    ...stdlib.hasRandom,
    getHand: () => {
      const hand = Math.floor(Math.random() * 3);
      console.log(`${Who} played ${HAND[hand]}`);
      return hand;
    },
    seeOutcome: (outcome) => {
      console.log(`${Who} saw outcome ${OUTCOME[outcome]}`);
    },
    informTimeout: () => {
      console.log(`${Who} observed a timeout`);
    },
  });

  await Promise.all([
    backend.Alice(ctcAlice, {
      ...Player('Alice'),
      wager: stdlib.parseCurrency(5),
    }),
    backend.Bob(ctcBob, {
      ...Player('Bob'),
      acceptWager: async (amt) => { // <-- async now
        if ( Math.random() <= 0.5 ) {
          for ( let i = 0; i < 10; i++ ) {
            console.log(`  Bob takes his sweet time...`);
            await stdlib.wait(1); }
        } else {
          console.log(`Bob accepts the wager of ${fmt(amt)}.`);
        }
      },
    }),
  ]);

  const afterAlice = await getBalance(accAlice);
  const afterBob = await getBalance(accBob);

  console.log(`Alice went from ${beforeAlice} to ${afterAlice}.`);
  console.log(`Bob went from ${beforeBob} to ${afterBob}.`);

})();