# [Reach教程翻译] 2.5 信任和约定

• Ivan
• 更新于 2021-11-24 00:04
• 阅读 1961

[Reach教程翻译] Reach是安全简单的Dapp开发语言 让用户可以像开发传统App一样开发DApp 目前使用Reach开发的智能合约可以部署在以太坊、Conflux、Algorand Reach官网 Reach官方文挡

# 2.5 信任和约定

``````\$ ./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 100 to 104.9999.
Bob went from 100 to 94.9999.``````

tut-5-attack/index.rsh

``````..    // ...
27    Bob.only(() => {
28      interact.acceptWager(wager);
29      const handBob = (handAlice + 1) % 3;
30    });
31    Bob.publish(handBob)
32      .pay(wager);
..    // ...``````

``````\$ ./reach run
Alice played Scissors
Bob accepts the wager of 5.
Alice saw outcome Bob wins
Bob saw outcome Bob wins
Alice went from 100 to 94.9999.
Bob went from 100 to 104.9999.``````

tut-5-attack/index.rsh

``````..    // ...
34    const outcome = (handAlice + (4 - handBob)) % 3;
35    require(handBob == (handAlice + 1) % 3);
36    assert(outcome == 0);
37    const            [forAlice, forBob] =
..    // ...``````
• 第35行要求使用Bob不诚实的版本证明。
• 第36行加入一个assert语句使程序进行证明。

tut-4/index.txt

``````Verifying for generic connector
Verifying when ALL participants are honest
Verifying when NO participants are honest
Verifying when ONLY "Alice" is honest
Verifying when ONLY "Bob" is honest
Checked 18 theorems; No failures!``````

tut-4-attack/index.txt

``````Verifying for generic connector
Verifying when ALL participants are honest
Verifying when NO participants are honest
Verifying when ONLY "Alice" is honest
Verifying when ONLY "Bob" is honest
Checked 18 theorems; No failures!``````
• 最后一行跟上面不一样了，他对我们的程序证明了更多的定理。它多证明了 5 个定理，而不是 1 个，是因为Reach在不同验证模式下都证明了这个定理。

Reach 在每个程序中都自动包含一些这样的断言。这就是为什么《石头剪刀布》的每一个版本运行完都显示检查了一系列的定理。为了看出这点，我们可以在程序中故意加入一个错误，看看这些定理的作用。

``````..    // ...
29        const handBob = declassify(interact.getHand());
..    // ...``````
``````..    // ...
35      require(handBob == (handAlice + 1) % 3);
36      assert(outcome == 0);
..    // ...``````

``````..    // ...
34    const [forA, forB] =
35          // was: outcome == 0 ? [0, 2] :
36          outcome == 0 ? [0, 1] : // &lt;-- Oops
37          outcome == 1 ? [1, 1] :
38          [2, 0];
39    transfer(forA * wager).to(A);
40    transfer(forB * wager).to(B);
41    commit();
..    // ...``````
• 第 36 行中的 [0, 1]在正确版本中应该是[0, 2]。

..
4 Verification failed:
5 when ALL participants are honest
6 of theorem: assert
7 msg: "balance zero at application exit"
9
10 // Violation Witness
11
12 const v71 = "Alice".interact.wager;
13 // ^ could = 1
14 // from: ./index-bad.rsh:11:10:property binding
15 const v74 = protect("Alice".interact.getHand());
16 // ^ could = 0
17 // from: ./index-bad.rsh:21:50:application
18 const v84 = protect("Bob".interact.getHand());
19 // ^ could = 2
20 // from: ./index-bad.rsh:29:48:application
21
22 // Theorem Formalization
23
24 const v93 = (v74 + (4 - v84)) % 3;
25 // ^ would be 2
26 const v100 = (v93 == 2) ? [1, 0 ] : (v93 == 0) ? [0, 2 ] : [1, 1 ];
27 // ^ would be [1, 0 ]
28 const v114 = 0 == (((v71 + v71) - (v100[0] v71)) - (v100[1] v71));
29 // ^ would be false
30 assert(v114);
31
..

• 第 7 行试图证明定理 : "程序结束时的余额是0，即没有代币被永远遗留在合约里。"
• 第 10 - 20 行描述了可能导致定理失败的值。
• 第 23 - 31 行概述了失败的定理。

tut-5-attack/index-fails.rsh

``````..    // ...
23    Alice.publish(wager, handAlice)
24      .pay(wager);
25    commit();
26
27    unknowable(Bob, Alice(handAlice));
28    Bob.only(() =&gt; {
29      interact.acceptWager(wager);
30      const handBob = declassify(interact.getHand());
31    });
..    // ...``````
• 第27行是一个额外的知识断言，即Bob此时不能知道Alice的值HandA。此时，这显然不可能，因为Alice在第21行已经公开HandA了。很多时候问题不会这么明显，Reach的自动验证引擎会考虑Bob所知道的值与Alice的机密值的相关性。

tut-5-attack/index-fails.txt

..
2 Verification failed:
3 of theorem unknowable("Bob", handAlice/77)
4 at ./index-fails.rsh:27:13:application
5
6 Bob knows of handAlice/77 because it is published.
..

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 = (handAlice, handBob) =>
7      ((handAlice + (4 - handBob)) % 3);
..    // ...``````
• 第 1 行是通常的 Reach 版本号。
• 第3行和第4行定义了可以出的手势，以及游戏的结果。
• 第6行和第7行定义了计算游戏赢家的函数。

tut-5/index.rsh

``````..    // ...
9    assert(winner(ROCK, PAPER) == B_WINS);
10    assert(winner(PAPER, ROCK) == A_WINS);
11    assert(winner(ROCK, ROCK) == DRAW);
..    // ...``````
• 第 9 行断言，当 Alice 出石头 而 Bob出布时，则胜者应该是 Bob

tut-5/index.rsh

``````..    // ...
13    forall(UInt, handA =>
14      forall(UInt, handB =>
15        assert(isOutcome(winner(handA, handB)))));
..    // ...``````

tut-5/index.rsh

``````..    // ...
17    forall(UInt, (hand) =>
18      assert(winner(hand, hand) == DRAW));
..    // ...``````

tut-5/index.rsh

``````..    // ...
20    const Player =
21          { ...hasRandom, // &lt;--- new!
22            getHand: Fun([], UInt),
23            seeOutcome: Fun([UInt], Null) };
..    // ...``````

tut-5/index.mjs

``````..    // ...
20    const Player = (Who) => ({
21      ...stdlib.hasRandom, // &lt;--- 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    });
..    // ...``````

tut-5/index.rsh

``````..    // ...
37    Alice.only(() =&gt; {
38      const wager = declassify(interact.wager);
39      const _handAlice = interact.getHand();
40      const [_commitAlice, _saltAlice] = makeCommitment(interact, _handAlice);
41      const commitAlice = declassify(_commitAlice);
42    });
43    Alice.publish(wager, commitAlice)
44      .pay(wager);
45    commit();
..    // ...``````
• 第 39 行有Alice获取她的手势，但没有公开。
• 第 40 行有她的承诺的手势。它还带有一个秘密的“salt”，在稍后会公开。
• 第 41 行Alice将承诺和赌注解密。
• 第 43 行让Alice公开，第 44 行则让Alice把赌注付到合约中。

tut-5/index.rsh

``````..    // ...
47    unknowable(Bob, Alice(_handAlice, _saltAlice));
48    Bob.only(() => {
49      interact.acceptWager(wager);
50      const handBob = declassify(interact.getHand());
51    });
52    Bob.publish(handBob)
53      .pay(wager);
54    commit();
..    // ...``````
• 第 47 行是知识断言。
• 第48至53行仍然与先前一样。
• 第 54 行是支付操作，但是我们还没计算赌注归谁，因为 Alice 的手势还没有公开。

tut-5/index.rsh

``````..    // ...
56    Alice.only(() => {
57      const saltAlice = declassify(_saltAlice);
58      const handAlice = declassify(_handAlice);
59    });
60    Alice.publish(saltAlice, handAlice);
61    checkCommitment(commitAlice, saltAlice, handAlice);
..    // ...``````
• 第 57-58 行是Alice将秘密信息解密。
• 第 60 行中Alice公开它。
• 第 61 行检查已发布的值是否与原始值匹配。诚实的参与者会这么做，但不诚实的参予者可能会违背这点。

tut-5/index.rsh

``````..    // ...
63    const outcome = winner(handAlice, handBob);
64    const                 [forAlice, forBob] =
65      outcome == A_WINS ? [       2,      0] :
66      outcome == B_WINS ? [       0,      2] :
67      /* tie           */ [       1,      1];
68    transfer(forAlice * wager).to(Alice);
69    transfer(forBob   * wager).to(Bob);
70    commit();
71
72    each([Alice, Bob], () => {
73      interact.seeOutcome(outcome);
74    });
..    // ...``````

\$ ./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 100 to 104.9999.
Bob went from 100 to 94.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 100 to 94.9999.
Bob went from 100 to 104.9999.
\$ ./reach run
Alice played Scissors
Bob accepts the wager of 5.
Bob played Scissors
Bob saw outcome Draw
Alice saw outcome Draw
Alice went from 10 to 99.9999.
Bob went from 10 to 99.9999.

Ivan