2.7 The game will continue until a tie is judged

2.7 The game will continue until a tie is judged

Original link


In this section, we will continue to write our application so that Alice and Bob can continue to fight after the tie, until there is a winner; that is, if the result is a tie, they will continue.
We only need to modify the Reach program without modifying the JavaScript front-end, but in order to deal with the situation of fighting again in a tie, we will modify the front-end, because now two people need to add a "timeout" mechanism when they punch. (Remember that originally we only added a "timeout" mechanism when Bob punches.)
Let's first adjust the getHand method of the interactive object Player:
tut-7/index.mjs

.. //... 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 }); .. //... Copy code
  • Lines 25 to 30 move the mandatory timeout code in Bob's acceptWager function to this method. We have also adjusted so that the timeout has a 1% probability. Because this behavior is not interesting, the frequency of its occurrence is greatly reduced.

Because we are testing differently now, we removed the timeout code in Bob's acceptWager function, which is actually reverting to the previous simple version. We also removed the timeout code in Bob's acceptWager function, because the way we test is now different. So restore this part to the previous simple version.
tut-7/index.mjs

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

-
Now, let's look Reach applications. All the details of the game and the player interface will remain unchanged. The only difference is the order in which the game actions occur.
The previous steps are:

  1. Alice issues her bet.
  2. Bob places a bet and plays.
  3. Alice also played.
  4. game over.

However, now because the player can submit multiple punch gestures, but only one bet, we will adjust these steps as follows:

  1. Alice made her bet.
  2. Bob places a bet.
  3. Alice places a bet.
  4. Bob plays the cards.
  5. Alice plays the cards.
  6. If it is a tie, return to step 4; otherwise, the game is over.

Now, we will start to make these changes:
tut-7/index.rsh

.. //... 42 A.only( () => { 43 const wager = declassify(interact.wager); }); 44 A.publish(wager) 45 .pay(wager); 46 commit(); .. //... Copy code
  • Line 44 Alice makes the public and pays the bet.

tut-7/index.rsh

.. //... 48 B.only( () => { 49 interact.acceptWager(wager); }); 50 B.pay(wager) 51 .timeout(DEADLINE, () => closeTo(A, informTimeout )); 52 .. //... duplicated code
  • On line 50 Bob pays the bet.
  • Note! No consensus step is submitted on line 52.

-
You can now start implementing the game again, and this time, the two sides will be repeated punches until the results are not tied. In a normal programming language, this situation would be achieved through a while loop, and the same is true for Reach. However, the while loop in Reach requires special care, as discussed in the Reach loop guide , so let's take it slow.
In the rest of the Reach program, all identifier binding values are static and unchangeable, but if this is the case throughout Reach, the while loop will never start or never terminate, because the loop condition never change. Therefore, the while loop in Reach allows the introduction of variable binding values.
Next, in order for Reach's automatic verification engine to work, we must declare which properties of the program are unchanged before and after the while loop body is executed. This is the so-called " loop invariant ".
Finally, such a loop may only happen In the consensus step. This is why Bob's transaction was not submitted just now, because we need to stay within the consensus to run the while loop. This is to allow all participants to agree on the direction of control flow in the application.
The structure is like this:
tut-7/index.rsh

.. //... 53 var outcome = DRAW; 54 invariant(balance() == 2 * wager && isOutcome(outcome) ); 55 while (outcome == DRAW) { .. //... Copy code
  • Line 53 defines the loop variable outcome.
  • Line 54 declares the loop invariant, which is the balance of the contract account, and the effective outcome.
  • Line 55 starts the loop with the condition that as long as the result is a tie, the loop will continue.

Now, let's look at the other steps in the loop, starting with the promise of Alice's opponent's card.
tut-7/index.rsh

.. //... 56 commit(); 57 58 A.only( () => { 59 const _handA = interact.getHand(); 60 const [_commitA, _saltA] = makeCommitment(interact, _handA); 61 const commitA = declassify(_commitA); }); 62 A.publish(commitA) 63 .timeout(DEADLINE, () => closeTo(B, informTimeout)); 64 commit(); .. //... Copy code
  • Line 56 commits the last transaction. At the beginning of the loop, Bob accepts the bet, and then Alice issues her gesture.
  • Lines 58 to 64 are the same as the previous version except that the bet is known and paid.

tut-7/index.rsh

.. //... 66 unknowable(B, A(_handA, _saltA)); 67 B.only( () => { 68 const handB = declassify(interact.getHand()); }); 69 B.publish (handB) 70 .timeout(DEADLINE, () => closeTo(A, informTimeout)); 71 commit(); .. //... Copy code

Similarly, Bob's code is the same as the previous version except that the bet is accepted and paid.
tut-7/index.rsh

.. //... 73 A.only( () => { 74 const [saltA, handA] = declassify([_saltA, _handA]); }); 75 A.publish(saltA, handA) 76 .timeout( DEADLINE, () => closeTo(B, informTimeout)); 77 checkCommitment(commitA, saltA, handA); .. //... Copy code

Alice's next step is actually the same, because she still posts her gestures in exactly the same way.
Next is the last part of the loop.
tut-7/index.rsh

.. //... 79 outcome = winner(handA, handB); 80 continue ;} .. //... Copy code
  • Line 79 updates the loop variable outcome.
  • The 80th line continues the loop. Unlike most programming languages, Reach requires an explicit continue in the loop body.

The rest of the program takes place outside of the loop, but the content can be exactly the same as before, but we will simplify it because we know that the result will never be a tie.
tut-7/index.rsh

.. //... 82 assert(outcome == A_WINS || outcome == B_WINS); 83 transfer( 2 * wager).to(outcome == A_WINS? A: B); 84 commit(); 85 86 each ([A, B], () => { 87 interact.seeOutcome (outcome);}); 88 Exit ();}); duplicated code
  • Line 82 asserts that the result is not a tie, which is obviously correct, otherwise we would not exit the while loop.
  • Line 83 transfers the funds to the winner.

-
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. Copy code


As before, the results of your run may be different, but you should also see that sometimes there is a winner in a single round, and sometimes there are multiple rounds and delays from both sides.

If your version does not work properly, please check tut-7/index. Rsh and tut-7/index. Mj and make sure you copied everything correctly!

Now, our rock-paper-scissors game will definitely be a winner, which makes the game more interesting. In the next step , we will show how to use Reach to exit the "test" mode and turn our JavaScript into a "rock, paper, scissors" game that interacts with real users.

Did you know?

How to write an arbitrarily long-running application in Reach, such as a rock-paper-scissors game that is guaranteed not to end in a tie?

  1. This is impossible, because all Reach programs are of limited duration;
  2. You can use a while loop to run until the result of the game is determined.

The answer is: 2; Reach supports while loop.


Did you know?

When you check whether a program with a while loop is correct, you need to have an attribute called a loop invariant. Regarding loop invariants, which of the following statements are correct?

  1. The part of the program before the while loop declares invariants.
  2. Conditions and loop bodies must declare invariants.
  3. The negation of conditions and invariants must declare any attributes in the rest of the code.

The answer is: all of the above

Previous: 2.6 Handling of timeout issues

Next: 2.8 Interactive and autonomous operation