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

2.5 信任和约定

原文链接

在上一节中，我们让 Alice 和 Bob 在玩石头剪刀布的时候可以以代币下注。但是，我们编写的应用程序版本有一个根本性的漏洞： Bob可以赢得每场比赛！

怎么可能呢？我们回顾一下 Alice 获胜的过程：

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

问题是这个版本的游戏只执行的是Bob 诚实的版本，换句话说这是完全遵循 Reach 程序的版本(包括在他私有的本地步骤中)。对于一个不诚实的 Bob 后端来说，可以执行一份不同的代码，通过 Alice 提供的 handA 的值计算后再出拳，这样Bob就能无往不利。

如果我们将 Bob 的代码更改为：

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.

在这个版本中，不像之前诚实的版本，Bob从来没有查询前端，所以上面没有看到Bob出什么手势的输出。无论Alice出什么，Bob都会赢。

如果Bob连胜了好几把，我们怎么知道他是作弊了还是运气真的站在他这边了呢？Reach有自动验证引擎，它可以从数学上证明这个版本中Bob总是获胜(即最终结果变量是0) ，这就表示Bob作弊了。我们可以在 Reach中添加这几行代码以做到这件事：

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语句使程序进行证明。

在加入这一段代码之前，当我们运行./reach compile时，它会输出消息：

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 是其中少数特别的，编译器不只是为这个属性插入运行时检查，而是在编译时进行数学证明，证明表达式始终为 true 。

在这个例子里，我们使用了 Reach 的自动验证引擎来证明Bob的攻击行为与我们预期的一致。但是理想的情况是 : 使用验证表明程序没有缺陷，即我们没有遭受攻击。

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

首先我们先恢复刚刚改动的地方:

tut-5-attack/index-bad.rsh

..    // ...
29        const handBob = declassify(interact.getHand());
..    // ...

并删去 tut-5-attack/index.rsh

..    // ...
35      require(handBob == (handAlice + 1) % 3);
36      assert(outcome == 0);
..    // ...

现在我们改变结算规则 : 在Alice获胜时，她只得到她自己的那份赌注，没有得到Bob的。

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

• 第 36 行中的 [0, 1]在正确版本中应该是[0, 2]。

当我们运行./ reach 编译tut-4-attack/index-bad.rsh时,它的报错如下：

tut-5-attack/index-bad.txt

编译器输出中有很多信息可以帮助有经验的程序员追踪问题。但最重要的几个部分是

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

这些自动验证可以帮助 Reach 程序员，即使他们没有写在代码里，Reach仍然会保护程序不发生这些类型的错误。

但是，我们也可以明确的在程序中添加一个断言，直接确保所有 Bob 出拳之前就看到 Alice 出拳结果的每个版本都被拒绝

我们将使用上一节中的 tut - 4 / index . rsh 版本，也就是 Bob 诚实的版本。（如果您需要查看它的内容，请单击前面的链接。）

在 Alice 发布之后、 Bob 运行本地步骤之前，我们添加一行：

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(() => {
29      interact.acceptWager(wager);
30      const handBob = declassify(interact.getHand());
31    });
..    // ...

• 第27行是一个额外的知识断言，即Bob此时不能知道Alice的值HandA。此时，这显然不可能，因为Alice在第21行已经公开HandA了。很多时候问题不会这么明显，Reach的自动验证引擎会考虑Bob所知道的值与Alice的机密值的相关性。

当我们运行新的 ./reach run时，它会报这个断言是错误的：

tut-5-attack/index-fails.txt

当发现错误和攻击时，仅仅修正它们还不够。一定要记得在代码里添加一个断言，使得如发生攻击或错误时，这个断言将无法成立。这样就可以确保不会遭受所有类似的攻击，并且不会再次发生错误。**

现在我们利用这个自动验证的概念，重写我们的“剪刀石头布”！使其更加安全可靠。

首先，我们定义剪刀石头布的规则！将其抽象化，先搭建逻辑框架再填入细节：

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行定义了计算游戏赢家的函数。

我们第一次写《剪刀石头布》的时候，我们说服您相信这个计算获胜者的公式是正确的，但是实际检查还是比较保险。检查的一种方法是实现一个 JavaScript 前端，它不与真正的用户交互，也不会随机生成值，而是返回特定的测试场景值，并检查输出是否符合预期。这是一种典型的调试方式，在Reach 中也可行。 Reach 允许我们将这样的测试用例直接写入 Reach 程序，作为验证断言。

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

但是， Reach 的自动验证允许我们表达关于程序行为的更有力的断言。例如，我们可以断言，无论 handA 和 handB 的值是什么，winner总是会返回正确的结果：

tut-5/index.rsh

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

我们可以指定，当handA, handB的值相同(无论是什么)时，winner总是返回平局：

tut-5/index.rsh

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

这两个例子都用到了forall ，这让Reach 程序员可以遍历程序中某部份的一些变量的所有可能值。你可能觉得证明这些定理很费时，因为必须遍历hand A和hand B的bits的可能性为1552518092300708935148,...(247位)...,468750892846853816057856种可能性（例如，以太坊使用256 位的无符号整数）。但实际上，在笔者 2015 年版的 MacBook Pro上，Reach只运行了不到半秒钟的时间。这是因为 Reach 使用了高级的符号执行引擎抽象地运算这个定理，而不一一考虑这些可能。

回到这个程序中，我们接着为 Alice 和 Bob 指定参与者交互接口。大部份都和以前一样，除了我们要为每个前端提供一个随机数。我们等下会用这个来保护Alice的手势。

tut-5/index.rsh

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

唯一不同的是第 21 行，它调用了 Reach 标准库中的 hasRandom 。

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

同样，我们只需要修改 JavaScript 前端的一行。第 21 行允许每个参与者的 Reach 代码根据需要生成随机数。

这两处修改看起来可能一样，但它们的含义完全不同。前一部分， Reach 程序的第 21 行，将 hasRandom 添加到后端需要前端提供的接口。第二部份， JavaScript 中的第 21 行，将 hasRandom 添加到前端提供给后端的实现中。

接下来是重点，我们将实现这个应用程序，并确保在Bob出拳之前Alice 的手势一直受到保护。首先 Alice 还是要公布赌注。然后我们让Alice 能出拳，但也要保密，这是一个加密承诺方案的场景。Reach 的标准库附带了 makecommitment ，这可以帮助你轻松完成这个任务。

tut-5/index.rsh

..    // ...
37    Alice.only(() => {
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把赌注付到合约中。

此时，我们可以声明知识断言，即 Bob 既不知道手势，也不知道“salt”，接着再继续他的程序。

关键是要把salt值纳入承诺，这样对同一值的几个承诺就不会都一样。另一个关键是先不要公开salt的值，一会儿再公开，因为如果攻击者知道一些可能值的范围，他们可以通过枚举，并与承诺的结果进行比较，最终得出我们要保密的值。

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 的手势还没有公开。

回到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的操作变成两步，Bob的操作只有一步，这使得Alice不会因为Bob通过"慢出"而输了游戏。

当我们编译这个版本时， Reach 的自动验证引擎证明了许多定理，并替我们避免了大量写这样一个简单的应用程序时可能犯的错误。那些试图编写去中心化应用程序的非Reach程序员得自己确保这些问题不存在。

如果您的程序不能正确运行，请查看完整的 tut - 5 / index . rsh 版本和 tut -5/index. mjs 版本，确保您正确地复制了所有内容！

现在，我们实现的剪刀石头布是安全的，无论是Alice或Bob都不能通过作弊，以保证取胜。然而，它还有最后一类在去中心化应用程序中常见的错误：不参与。我们将在下一步解决这个问题；确保不要发布这个版本，否则Alice在知道她会输的时候，可能就先退出游戏了！

你知道了吗?： 是非题： 由于区块链程序运行在一个单一的、全球的、经过公开检查和认证的共识网络上，你不需要像普通软件那样测试它们，它们运行在各种不同的平台和操作系统上。 答案是： 错

你知道了吗?： 是非题：编写处理财务信息的正确程序很容易，即使你犯了错误，区块链也支持“撤销”操作，允许你回滚到账本的早期版本，以纠正错误并收回损失的资金。 答案是： 错

你知道了吗?： 是非题：Reach 提供自动验证，以确保您的程序不会丢失、锁定或超支资金，并保证您的应用程序不会出现所有类别的错误。 答案是： 对

你知道了吗?： 是非题: Reach 为您提供了向程序添加自定义验证的工具，比如确保信息仅为一方所知，或者确保敏感算法的实现是正确的。 答案是： 对

欢迎关注Reach微信公众号 并在公众号目录 -> 加入群聊 选择加入官方开发者微信群与官方Discord群 与更多Reach开发者一起学习交流!