2 教程 - 2.5 信任和约定 - 《Reach CN》

原文链接
在上一节中，我们让 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 10 to 14.9999.
Bob went from 10 to 4.9999.

问题是，现在执行的是Bob 诚实的版本，换句话说这是完全遵循我们 Reach 程序的版本 ( 包括在他私有的本地步骤中 ) 。如果 Bob 的后端不诚实，他可以执行一份不同的代码，通过 Alice 提供的 handA 的值计算后再出拳，这样 Bob 就能无往不利。
例如 : 如果 Bob 的代码更改为：
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);
..    // ...

那么他会忽略前端，直接计算能获胜的值。
运行这个版本的程序，我们看到的输出如下：

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

在这个版本中，不像之前诚实的版本，Bob从来没有查询前端，所以上面的输出里没有任何一行显示Bob出什么手势。此时无论Alice出什么，Bob都会赢。
—
如果Bob连胜了好几把，我们怎么知道他是作弊了还是运气真的站在他这边了呢？
Reach有自动验证引擎，它可以从数学上证明这个版本中Bob总是获胜 ( 即最终结果变量是0 ) ，这就表示Bob作弊了。我们可以在 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] =
..    // ...

32行要求证明这个版本 Bob 不诚实。
第33行加入一个 assert 语句使程序进行证明。

在加入这一段代码之前，当我们运行 ./reach run 时，它会输出消息：
tut-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!

但现在，它输出消息：
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!

第 7 行跟上面不一样了，他对我们的程序证明了更多的定理。因为在不同的验证模式下，定理的证明是不同的，所以它多输出 5 个，不止是 1 个。

—
许多编程语言都包含这样的判定，但 Reach 是其中少数特别的，编译器不只是为这个属性插入运行时检查，而是在编译时进行数学证明，证明表达式始终为 true 。
在这个例子里，我们使用了 Reach 的自动验证引擎来证明Bob的攻击行为与我们预期的一致。但是理想的情况是 : 使用验证表明程序没有缺陷，即我们没有遭受攻击。
Reach 在每个程序中都自动包含一些这样的断言。这就是为什么我们石头剪刀布的每一个版本运行完都会显示检查了一系列的定理。为了看出这点，我们可以在程序中故意加入一个错误，看看这些定理的作用。
现在我们故意错误修改结算规则 : 在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-5-attack/index-bad.rsh 时,它的报错如下：
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)));

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

第 7 行试图证明定理 : “程序结束时的余额是0，即没有代币被永远遗留在合约里。”
第 8 行指出，这发生在程序从第 45 行退出时，它提示程序员检查第45行的代码。
第 10 - 14 行描述了可能导致定理失败的值。
第 16 - 21 行概述了失败的定理。

这些自动验证可以帮助 Reach 程序员。即使他们没有在代码里写出来，Reach仍然会防止程序发生这些类型的错误。
—
但是，我们也可以明确的在程序中添加一个断言，直接确保所有 Bob 出拳之前就看到 Alice 出拳结果的每个版本都被否决。
我们将使用上一节中的 tut - 4 / index . rsh 版本，也就是 Bob 诚实的版本。（如果您需要查看它的内容，请单击前面的链接。）
在 Alice 发布之后、 Bob 运行本地步骤之前，我们添加一行代码：
tut-5-attack/index-fails.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      const handB = declassify(interact.getHand()); });
..    // ...

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

当我们运行新的 ./reach run时，它会报这个断言是错误的：
tut-5-attack/index-fails.txt!

..
  3  of theorem unknowable("Bob", handA/7)
  4  at ./index-fails.rsh:25:17:application
  5
..

在发现错误和攻击时，仅仅修正它们还不够。一定要记得在代码里添加一个断言，使得发生类似的攻击或错误时，这个断言将不成立。这样就可以确保我们不会遭受所有类似的攻击，并且不会再次发生错误。
—
现在我们利用这个自动验证的概念，重写我们的“石头剪刀布”！使其更加安全可靠。
首先，我们定义石头剪刀布的规则！将其抽象化，先搭建逻辑框架再填入细节：
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);
..    // ...

第 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

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

第 37 行中 Alice 决定她的手势，但没有公开。
第 38 行 Alice 对手势承诺。同时带有一个秘密的“salt”，在稍后会公开。
第 39 行 Alice 将承诺和赌注解密。
第 40 行 Alice 将它们公开，第 41 行则让 Alice 把赌注支付到合约中。

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

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

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

第 44 行是知识断言。
第 45 至 49 行仍然与先前一样。
第 50 行是支付操作，但是我们还没计算赌注归谁，因为 Alice 的手势还没有公开。

回到Alice这边，现在她可以公开她的秘密了。
tut-5/index.rsh

..    // ...
52    A.only(() => {
53      const [saltA, handA] = declassify([_saltA, _handA]); });
54    A.publish(saltA, handA);
55    checkCommitment(commitA, saltA, handA);
..    // ...

第 53 行是Alice将秘密信息解密。
第 54 行中Alice公开它。
第 55 行检查已发布的值是否与原始值匹配。诚实的参与者会这么做，但不诚实的参予者可能会违背这点。

程序的其余部分都与原始版本相同，只是结果的名称改变了一下：
tut-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(); });

由于我们没有对前端做任何实质改变，运行./ reach run的输出还是跟以前一样：

$ ./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 played Scissors
Bob saw outcome Draw
Alice saw outcome Draw
Alice went from 10 to 9.9999.
Bob went from 10 to 9.9999.

目前为止，前端没有任何变化，但本质上Alice的操作变成两步，Bob的操作只有一步，这使得Alice不会因为Bob通过”慢出”而输了游戏。
当我们编译这个版本时， Reach 的自动验证引擎证明了许多定理，并替我们避免了大量写这样一个简单的应用程序时可能犯的错误。那些试图编写去中心化应用程序的非Reach程序员得自己确保这些问题不存在。

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

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

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

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

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

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