The original link
In the last video, we let Alice and Bob bet with tokens while playing rock-paper-scissors. However, the version of the application we wrote had a fundamental flaw: Bob could win every race! How could that be? Let’s review how Alice won:
$ ./reach run
Alice played Rock
Bob accepts the wager of 5.
Bob played Scissors
Alice saw outcome Alice wins
Bob saw outcome Alice wins
Alice went from 10 to 14.9999.
Bob went from 10 to 4.9999.
Copy the codeThe problem is that Bob’s honest version is now being implemented, in other words a version that fully follows our Reach program (included in his private local steps). If Bob’s back end is dishonest, he can execute a different code, calculate the value of handA provided by Alice, and then punch, and Bob can get away with it. For example, if Bob’s code changes to: tut-5-attack/index.rsh
.// ...
25 B.only(() = > {
26 interact.acceptWager(wager);
27 const handB = (handA + 1) % 3; });
28 B.publish(handB)
29.pay(wager); .// ...
Copy the codeSo he would ignore the front end and just calculate the winning value. Running this version of the program, we see the following output:
$ ./reach run
Alice played Scissors
Bob accepts the wager of 5.
Alice saw outcome Bob wins
Bob saw outcome Bob wins
Alice went from 10 to 4.9999.
Bob went from 10 to 14.9999.
Copy the codeIn this version, unlike the honest version before, Bob never has a query front end, so none of the lines in the output above show what gestures Bob made. So no matter what Alice does, Bob wins. — If Bob wins several in a row, how do we know if he’s cheating or if luck is really on his side? Reach has an automatic validation engine that mathematically proves that Bob always wins in this version (i.e., the end result variable is 0), which means Bob cheated. We can do this by adding these lines to Reach: TUt-5-attack /index.rsh
.// ...
31 const outcome = (handA + (4 - handB)) % 3;
32 require(handB == (handA + 1) % 3);
33 assert(outcome == 0);
34 const [forA, forB] =
.. // ...
Copy the code- Line 32 asks to prove that this version of Bob is dishonest.
- Add an assert statement at line 33 to make the program prove.
Before adding this code, when we run./reach run, it prints the message: tu-4 /index.txt
. / /... 2 Verifying for generic connector 3 Verifying when ALL participants are honest 4 Verifying when NO participants are honest 5 Verifying when ONLY "Alice" is honest 6 Verifying when ONLY "Bob" is honest 7 Checked 16 theorems; No failures!Copy the codeBut now, it outputs the message: tut-5-attack/index.txt
. / /... 2 Verifying for generic connector 3 Verifying when ALL participants are honest 4 Verifying when NO participants are honest 5 Verifying when ONLY "Alice" is honest 6 Verifying when ONLY "Bob" is honest 7 Checked 21 theorems; No failures!Copy the code- Line 7 is different, it proves more theorems for our program. Because the proof of the theorem is different in different validation modes, it outputs 5 more, not 1.
— Many programming languages include such a determination, but Reach is one of the few exceptions where the compiler does not just insert a runtime check for this attribute, but does a mathematical proof at compile time that the expression is always true. In this example, we use Reach’s automatic validation engine to prove that Bob’s attack behavior is consistent with our expectations. But ideally, use validation to show that the program is not flawed, that we are not under attack. Reach automatically includes some of these assertions in every program. That’s why every version of our rock-Paper-Scissors run shows a series of theorems checked. To see this, we can put a deliberate error in the program and see how these theorems work. Now we intentionally change the settlement rules incorrectly: when Alice wins, she only gets her chips, not Bob’s. tut-5-attack/index-bad.rsh
.// ...
34 const [forA, forB] =
35 // was: outcome == 0 ? [0, 2] :
36 outcome == 0 ? [0.1] : // <-- Oops
37 outcome == 1 ? [1.1] :
38 [2.0];
39 transfer(forA * wager).to(A);
40 transfer(forB * wager).to(B);
41commit(); .// ...
Copy the code- The [0, 1] in line 36 would be [0, 2] in the correct version.
When we run./ reach to compile tut-5-attack/index-bad.rsh, it returns the following error: tut-5-attack/index-bad.txt
Verification failed:
when ALL participants are honest
of theorem: assert
msg: "balance assertion"
at ./index-bad.rsh:45:11:application
// Violation witness
const interact_Alice_wager = 2;
// ^ from interaction at ./index-bad.rsh:14:12:application
const handA/4 = 2;
// ^ from evaluating interact("Alice")."getHand"() at ./index-bad.rsh:20:50:application
// Theorem formalization
const outcome/26 = (handA/4 + (4 - ((handA/4 + 1) % 3))) % 3;
// ^ would be 0
const v37 = (outcome/26 == 0) ? [0, 1] : ((outcome/26 == 1) ? [1, 1] : [2, 0]);
// ^ would be [0, 1]
assert(0 == (((interact_Alice_wager + interact_Alice_wager) - (v37[0] * interact_Alice_wager)) - (v37[1] * interact_Alice_wager)));
Copy the codeThere is a lot of information in the compiler output that can help an experienced programmer track down problems. The most important parts are
- Line 7 attempts to prove the theorem: “The balance at the end of the program is 0, i.e., no token is left in the contract forever.”
- Line 8 indicates that this happens when the program exits from line 45, prompting the programmer to check the code on line 45.
- Lines 10-14 describe the values that can cause the theorem to fail.
- Lines 16-21 outline the theorem of failure.
These automated validations can help Reach programmers. Even if they are not written out in code, Reach still prevents programs from having these types of errors. However, we can also explicitly add an assertion to the program that directly ensures that every version of Alice’s punch that sees Bob’s punch before Alice’s punch is rejected. We’ll use the tu-4 / index.rsh version from the previous section, which is Bob’s honest version. (If you need to view its contents, click the previous link.) After Alice posted, but before Bob ran the local step, we added a line of code: tut-5-attack/ index-defe.rsh
.// ...
21 A.publish(wager, handA)
22 .pay(wager);
23 commit();
24
25 unknowable(B, A(handA));
26 B.only(() = > {
27 interact.acceptWager(wager);
28 consthandB = declassify(interact.getHand()); }); .// ...
Copy the code- Line 25 is an additional knowledge assertion that Bob cannot know Alice’s value HandA at this time. In this case, this is obviously not possible because Alice already exposes HandA in line 21. Many times the problem is not so obvious, and Reach’s automated validation engine takes into account the correlation between Bob’s known value and Alice’s secret value.
When we run the new./reach run, it will report that this assertion is incorrect: tut-5-attack/ index-defe.txt!
. 3 of theorem unknowable("Bob", handA/7) 4 at ./index-fails.rsh:25:17:application 5 ..Copy the codeWhen errors and attacks are found, it’s not enough to fix them. Be sure to add an assertion to your code so that it will not be true if similar attacks or errors occur. This ensures that we do not suffer from all similar attacks and that the error does not happen again. — Now let’s take advantage of this concept of automatic validation and rewrite our rock-paper-Scissors! Make it safer and more reliable. First, we define rock-paper-scissors rules! To abstract it, build the logical framework and then fill in the details: TUt-5 /index.rsh
1 'reach 0.1';
2
3 const [ isHand, ROCK, PAPER, SCISSORS ] = makeEnum(3);
4 const [ isOutcome, B_WINS, DRAW, A_WINS ] = makeEnum(3);
5
6 const winner = (handA, handB) = >
7 ((handA + (4 - handB)) % 3); .// ...
Copy the code- Line 1 is the usual Reach version number.
- Lines 3 and 4 define the gestures that can be made and the consequences of the game.
- Lines 6 and 7 define the function that calculates the winner of the game.
When we first wrote rock-paper-Scissors, we convinced you that the formula for calculating winners was correct, but it was safer to have the program actually check. One way to check is to implement a JavaScript front end that doesn’t interact with real users and doesn’t randomly generate values, but instead returns specific test scenario values and checks that the output is as expected. This is a typical debugging approach and is also available in Reach. In Reach, we can write such test cases directly into the Reach program as validation assertions. tut-5/index.rsh
.// ...
9 assert(winner(ROCK, PAPER) == B_WINS);
10 assert(winner(PAPER, ROCK) == A_WINS);
11assert(winner(ROCK, ROCK) == DRAW); .// ...
Copy the code- Line 9 asserts that when Alice plays rock and Bob plays cloth, the winner should be Bob
In Reach, however, we can use automated validation to express stronger assertions about program behavior. For example, we can assert that winner will always return the correct result regardless of the values of handA and handB: Tu-5 /index.rsh
.// ...
13 forall(UInt, handA= >
14 forall(UInt, handB= >
15assert(isOutcome(winner(handA, handB))))); .// ...
Copy the codeWe can specify that when handA, handB have the same value (whatever it is), winner always returns a draw: tu-5 /index.rsh
.// ...
17 forall(UInt, (hand) = >
18assert(winner(hand, hand) == DRAW)); .// ...
Copy the codeBoth examples use Forall, which allows the Reach programmer to iterate through all possible values of some variable in a part of the sequence. You may think that prove the theorem is very time consuming, because must traverse the hand and hand B bits of possibility: 1552518092300708935148,… (There are 247 in the middle)… , 468750892846853816057856 possibility (etheric fang, for example, use 256 – bit unsigned integer). In fact, on my 2015 MacBook Pro, Reach took less than half a second. This is because Reach uses an advanced symbolic execution engine to compute the theorem abstractly, rather than considering each of these possibilities. Back in the program, we then specify the actor interaction interfaces for Alice and Bob. Most of it is the same as before, except now we need to provide a random number for each front end. This random number is going to be used to protect Alice’s gesture. tut-5/index.rsh
.// ...
20 const Player =
21 { ...hasRandom, // <--- new!
22 getHand: Fun([], UInt),
23seeOutcome: Fun([UInt], Null) }; .// ...
Copy the codeThe only difference is line 21, which calls hasRandom in the Reach library. tut-5/index.mjs
.// ...
20 const Player = (Who) = > ({
21. stdlib.hasRandom,// <--- new!
22 getHand: () = > {
23 const hand = Math.floor(Math.random() * 3);
24 console.log(`${Who} played ${HAND[hand]}`);
25 return hand;
26 },
27 seeOutcome: (outcome) = > {
28 console.log(`${Who} saw outcome ${OUTCOME[outcome]}`);
29 },
30}); .// ...
Copy the codeAgain, we only need to modify one line of the JavaScript front end. Line 21 allows each participant’s Reach code to generate random numbers as needed. These two changes may look the same, but they mean very different things. The previous section, line 21 of the Reach program, adds hasRandom to the interface that the back end requires the front end to provide. The second part, line 21 in JavaScript, adds hasRandom to the implementation that the front end provides to the back end. Here’s the point, we’ll implement the application and make sure Alice’s gesture is protected until Bob throws a punch. First Alice still has to announce the bet. And then we let Alice be able to throw a punch, but also keep it secret, and it’s a cryptographic promise scene. Reach’s standard library comes with Makecommitment, which can help you with this task easily. tut-5/index.rsh
.// ...
36 A.only(() = > {
37 const _handA = interact.getHand();
38 const [_commitA, _saltA] = makeCommitment(interact, _handA);
39 const [wager, commitA] = declassify([interact.wager, _commitA]); });
40 A.publish(wager, commitA)
41 .pay(wager);
42commit(); .// ...
Copy the code- In line 37 Alice decides her gesture, but does not make it public.
- Line 38 Alice promises the gesture. Also with a secret “salt” that will be revealed later.
- Line 39 Alice decrypts the promise and bet.
- Line 40 Alice exposes them, and line 41 tells Alice to pay the bet into the contract.
At this point, we can declare the knowledge assertion “Bob knows neither gesture nor” salt “, and continue with his program.
The key is to include the SALT value in the commitment so that the commitment to the same handA value is not always the same. Another key is not to disclose the salt values until later, because if an attacker knows the range of possible values, they can enumerate, compare them with the promised results, and finally arrive at the values we want to keep secret.
tut-5/index.rsh
.// ...
44 unknowable(B, A(_handA, _saltA));
45 B.only(() = > {
46 interact.acceptWager(wager);
47 const handB = declassify(interact.getHand()); });
48 B.publish(handB)
49 .pay(wager);
50commit(); .// ...
Copy the code- Line 44 is a knowledge assertion.
- Lines 45 through 49 remain the same as before.
- Line 50 is the payment operation, but we haven’t calculated the bet yet, because Alice’s gesture isn’t public yet.
Back to Alice, now she can reveal her secret. tut-5/index.rsh
.// ...
52 A.only(() = > {
53 const [saltA, handA] = declassify([_saltA, _handA]); });
54 A.publish(saltA, handA);
55checkCommitment(commitA, saltA, handA); .// ...
Copy the code- Line 53 shows Alice decrypting the secret message.
- Alice exposes it in line 54.
- Line 55 checks that the published value matches the original value. Honest participants will do this, but dishonest participants may violate it.
The rest of the program is the same as the original version, except the name of the result has been changed: Tu-5 /index.rsh
.// ...
57 const outcome = winner(handA, handB);
58 const [forA, forB] =
59 outcome == A_WINS ? [2.0] :
60 outcome == B_WINS ? [0.2] :
61 [1.1];
62 transfer(forA * wager).to(A);
63 transfer(forB * wager).to(B);
64 commit();
65
66 each([A, B], () = > {
67 interact.seeOutcome(outcome); });
68 exit(); });
Copy the codeSince we haven’t made any real changes to the front end, the output from running./ Reach Run is the same as before:
$ ./reach run Alice played Scissors Bob accepts the wager of 5. Bob played Paper 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 Alice played Paper Bob accepts the wager of 5. 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 Alice played Scissors Bob accepts the wager of 5 Bob saw outcome Draw Alice saw outcome Draw Alice went from 10 to 9.9999. Bob went from 10 to 9.9999.Copy the codeSo far, nothing has changed on the front end, but essentially Alice’s actions have become two steps and Bob’s actions have only one, which keeps Alice from losing the game because Bob “slows down”. When we compiled this version, Reach’s automatic validation engine proved many theorems and saved us from the mistakes we might have made when writing such a simple application in large numbers. Non-reach programmers who try to write decentralized applications have to make sure they don’t.
If your program doesn’t work correctly, check out the full tuT-5 / index.rsh version and tut-5 / index.mjs version to make sure you copied everything correctly!
Now, our implementation of rock-paper-scissors is safe, and neither Alice nor Bob can cheat to be sure of winning. However, it has a final category of mistakes that are common in decentralized applications: non-participation. We will address this issue in the next step; Make sure you don’t release this version, or Alice might quit the game before she knows she’s going to lose!
Do you know? :
Is the topic:
Because blockchain programs run on a single, global, publicly checked and certified consensus network, you don’t need to test them like normal software, they run on a variety of different platforms and operating systems.
Answer: wrong
Do you know? :
Is the topic:
It’s easy to write the right program to process financial information, and even if you make a mistake, the blockchain supports an “undo” operation that allows you to roll back to an earlier version of the ledger to correct the mistake and recover lost money.
The answer is: no
Do you know? :
Is the topic:
Reach provides automatic validation to ensure that your program does not lose, lock up or overspend, and that your application does not suffer from all categories of errors.
The answer is: yes
Do you know? :
Is the topic:
Reach gives you the tools to add custom validation to your program, such as ensuring that information is only known to one party or that the implementation of sensitive algorithms is correct.
The answer is: yes
2.4 Bets and wagers
2.6 Handling the Timeout Problem