Scilla实战演练¶

HelloWorld¶

首先，我们来编写具有以下规范的经典 HelloWorld.scilla 合约：

此合约中有一个不可变的合约参数 owner ，由合约的创建者初始化。该参数是不可变的，即意味着一旦在合约部署期间进行初始化，其值就无法更改。其中 owner 是 ByStr20 类型（表示 20 字节地址的十六进制字节字符串）。
此合约中有一个 String 类型的可变字段 welcome_msg 且被初始化为 "" 。此处的可变性是指，即使在部署合约后也可以修改变量的值。
owner 且 只有她 才能够通过接口 setHello 修改 welcome_msg 。该接口将 msg （ String 类型）作为输入，并允许 owner 将 welcome_msg 的值设置为 msg 。
此合约有一个接口 getHello ，允许任何带有 welcome_msg 的调用者调用。此外 getHello 不会接受任何输入。

定义合约、不可变参数和可变字段¶

我们将使用关键字 contract 来作为声明一个合约的开始。关键字后跟合约的名称，而在我们的示例中就是 HelloWorld 。综上，以下代码片段声明了一个 HelloWorld 合约。

contract HelloWorld

注解

在目前的实现中，一个 Scilla 合约只能包含一个单一的合约声明，因此任何跟在 contract 关键字之后的代码都是合约声明的一部分。换句话说，没有明确的关键字来声明合约定义的结束。

声明合约后，接下来是其不可变参数的声明，其代码块由 () 包裹。每个不可变参数都通过以下方式声明： vname: vtype ，其中 vname 是参数名称，vtype 是参数类型。不可变参数由 , 分隔。根据规范，合约将只有一个 ByStr20 类型的不可变参数 owner ，具体参考以下代码片段。

(owner: ByStr20)

合约中的可变字段通过关键字 field 声明。每个可变字段以下列方式声明： field vname : vtype = init_val ，其中 vname 是字段名称，vtype 是它的类型，init_val 是字段必须被初始化的值。 HelloWorld 合约有一个 String 类型的可变字段 welcome_msg ，且被初始化为 "" 。具体实现参考以下代码片段：

field welcome_msg : String = ""

在此阶段，我们的 HelloWorld.scilla 合约将具有以下形式，其中包括合约名称、不可变参数和可变字段：

contract HelloWorld
(owner: ByStr20)

field welcome_msg : String = ""

定义接口即Transitions¶

像 setHello 这样的接口在 Scilla 中被称为 transitions 。 Transitions类似于其他语言中的函数或方法。然而，他们有一个重要的区别，大多数语言允许它们的函数或方法被并行运行的线程”中断” ，但 Scilla 不会让transitions被中断，以此来确保不会出现所谓的重入问题。

注解

术语 transition 来自 Scilla 中的底层计算模型，它遵循通信自动机。 Scilla 中的合约是具有某种状态的自动机。自动机的状态可以使用 transition 来更改，该 transition 采用先前状态和输入并产生新的状态。访问维基百科条目以阅读有关 transition 系统的更多信息。

使用关键字 transition 声明一个 transition 。使用关键字 end 声明 transition 代码块的结束。 transition 关键字后跟 transition 名称，在我们的示例中为 setHello 。然后是 () 内的输入参数。每个输入参数由 , 分隔，并以以下格式声明： vname : vtype 。根据规范， setHello 只接受一个 String 类型的名为 msg 的参数。具体参照以下代码片段：

transition setHello (msg : String)

transition 声明之后是 transition 的主体部分。下面给出了第一个transition的代码段，此代码段为调用 setHello (msg : String) 以设置 welcome_msg ：

transition setHello (msg : String)
  is_owner = builtin eq owner _sender;
  match is_owner with
  | False =>
    e = {_eventname : "setHello"; code : not_owner_code};
    event e
  | True =>
    welcome_msg := msg;
    e = {_eventname : "setHello"; code : set_hello_code};
    event e
  end
end

首先，使用第 2 行中的指令 builtin eq owner _sender 来检查 transition 的调用者是否与 owner 相等。为了比较两个地址，我们使用定义为函数 eq 的 builtin 运算符。该运算符返回布尔值 True 或 False 。

注解

Scilla 内部定义了一些具有特殊语义的变量。这些特殊变量通常以 _ 为前缀。例如，Scilla 中的 _sender 是指调用当前合约的帐户地址。

根据比较的结果，transition 通过不同的分支来进行模式匹配，其语法如下面的代码片段所示。

match expr with
| pattern_1 => expr_1
| pattern_2 => expr_2
end

上面的代码检查 expr 的计算结果是否与 pattern_1 或 pattern_2 匹配。如果 expr 的计算结果与 pattern_1 匹配，那么接下来要执行的表达式将是 expr_1 。否则，如果 expr 的计算结果与 pattern_2 匹配，那么接下来要执行的表达式就是 expr_2 。

因此，以下代码块实现了类似于 if-then-else 的指令：

match expr with
| True  => expr_1
| False => expr_2
end

调用者不是所有者¶

如果调用者与 owner 不同，则 transition 会进入 False 分支，即合约使用指令 event 来触发一个事件。

事件是指存储在区块链上供所有人查看的信号。如果用户使用客户端应用程序调用合约的 transition，客户端应用程序就可以监听合约可能触发的事件，并提醒用户。

更具体地说，这种情况下的事件代码如下：

e = {_eventname : "setHello"; code : not_owner_code};

一个事件由许多 vname : value 对组成，并由 ; 分隔。在一对花括号 {} 内。一个事件必须包含必填字段 _eventname ，同时也可以包含其他字段，例如上面示例中的 code 字段。

注解

在我们的示例中，我们选择使用 transition 的名称来命名事件的名称，但时你可以选择任何其他名称。不过呢，还是建议你以易读性为标准来命名，即使用执行事件的那部分代码的名称来命名事件。

调用者是所有者¶

如果调用者是 owner ，则合约允许调用者将可变字段 welcome_msg 的值设置为输入参数 msg 。这些是通过以下指令完成的：

welcome_msg := msg;

注解

给可变字段赋值是使用运算符 := 完成的。

和前面的例子一样，合约随后会触发一个 code 值为 set_hello_code 的事件。

库定义¶

Scilla 合约会有一些辅助库，它们声明合约的纯功能组件，即没有状态操作的组件。使用关键字 library 然后跟上库名称，就完成了在合约的开始部分中库的声明。在我们当前的示例中，库声明如下所示：

library HelloWorld

该库可能包含使用 let ident = expr 定义的效用函数和程序常量。在我们的示例中，库定义的部分只包含错误代码的定义：

let not_owner_code  = Uint32 1
let set_hello_code  = Uint32 2

到这里为止，我们的合约片段会变成下面这个样子：

library HelloWorld

 let not_owner_code  = Uint32 1
 let set_hello_code  = Uint32 2


 contract HelloWorld
 (owner: ByStr20)

 field welcome_msg : String = ""

 transition setHello (msg : String)
   is_owner = builtin eq owner _sender;
   match is_owner with
   | False =>
     e = {_eventname : "setHello"; code : not_owner_code};
     event e
   | True =>
     welcome_msg := msg;
     e = {_eventname : "setHello"; code : set_hello_code};
     event e
   end
 end

增加另一个 Transition¶

我们现在可以增加第二个 transition getHello() ，它允许客户端应用程序知道 welcome_msg 是什么。声明与 setHello (msg : String) 类似，只是 getHello() 不带参数。

transition getHello ()
    r <- welcome_msg;
    e = {_eventname: "getHello"; msg: r};
    event e
end

注解

读取到本地可变字段（即将当前合约中定义的字段读取到本地）是使用运算符 <- 完成的。

在 transition getHello() 中，我们将首先从可变字段中读取，然后构造并触发事件。

Scilla 版本号¶

合约一旦在网络上部署，就无法更改。因此需要指定合约是用哪个版本的 Scilla 编写的，以确保即使对 Scilla 规范进行更改，合约的行为也不会改变。

合约的 Scilla 版本是使用关键字 scilla_version 声明的：

scilla_version 0

版本声明必须出现在任何库或合约代码之前。

代码完整示例¶

下面给出了实现所需规范的完整合约，其中我们使用 (* *) 结构添来添加注释：

(* HelloWorld contract *)

(***************************************************)
(*                 Scilla version                  *)
(***************************************************)

scilla_version 0

(***************************************************)
(*               Associated library                *)
(***************************************************)
library HelloWorld

let not_owner_code  = Uint32 1
let set_hello_code  = Uint32 2

(***************************************************)
(*             The contract definition             *)
(***************************************************)

contract HelloWorld
(owner: ByStr20)

field welcome_msg : String = ""

transition setHello (msg : String)
  is_owner = builtin eq owner _sender;
  match is_owner with
  | False =>
    e = {_eventname : "setHello"; code : not_owner_code};
    event e
  | True =>
    welcome_msg := msg;
    e = {_eventname : "setHello"; code : set_hello_code};
    event e
  end
end

transition getHello ()
  r <- welcome_msg;
  e = {_eventname: "getHello"; msg: r};
  event e
end

示例二：众筹¶

在本节中，我们展示了一个运行众筹活动的稍微复杂的合约。在众筹活动中，项目所有者希望通过社区捐款筹集资金。

假设所有者（ owner ）希望一直运行该活动，直到在区块链（ max_block ）上达到某个预定的区块高度。所有者还希望提高最低数量的 QA（ goal ），否则项目将无法启动。因此，合约具有三个不可变参数 owner 、 max_block 和 goal 。

不可变参数会在部署合约时提供。在这一点上，我们希望添加一个合理性检查，其中 goal 必须是一个严格意义上的正数。如果合约中的 goal 意外地以 0 值进行初始化，则该合约就不会被部署。

到目前为止，捐赠给该活动的总金额存储在字段 _balance 中。Scilla中的任何合约都有一个隐式的 _balance 字段，类型为 Uint128 ，在合同部署时初始化为0，它包含了区块链上合约账户中QA的数量。

如果所有者能在规定的时间内达到目标，则视为众筹成功。如果众筹失败，捐款将返还给在竞选期间捐款的项目支持者。并且需要支持者有明确要求退款的操作。

合约包含两个可变字段：

backers ：从贡献者地址（类型为 ByStr20 的值）到贡献金额的字段映射，用类型为 Uint128 的值表示。由于最初没有支持者，因此此映射被初始化为 ``Emp``（即空）映射。该映射使合约能够注册捐赠者，以此防止重复捐赠并在活动失败时可以退还资金。

funded ：一个布尔值的标志，初始化为 False ，指所有者是否已经在活动结束后转移了资金。

该合约包含三个 transitions ： Donate () 允许任何人为众筹活动捐款， GetFunds () **仅允许所有者**提取捐赠金额并将其转账给 owner ，以及 ClaimBack() 允许贡献者在活动不成功时取回他们的捐款。

合约参数的合理性检查¶

为了确保 goal 是一个严格的正数，我们使用了一个合约约束：

with
  let zero = Uint128 0 in
  builtin lt zero goal
=>

上面 with 和 => 之间的布尔表达式在合约部署期间进行判断，只有判断结果为 True 时才会部署合约。这确保了合约不会被错误地将 goal 的值以 0 的进行部署。

读取当前区块高度¶

截止日期以区块高度给出，因此要检查是否已过截止日期，我们必须将截止日期与当前区块高度进行比较。

当前块高度读取如下：

blk <- & BLOCKNUMBER;

区块高度在 Scilla 中有一个专用类型 BNum ，以免将它们与常规无符号整数混淆。

注解

从区块链读取数据是使用运算符 <- & 完成的。且区块链数据不能直接从合约中更新。

读取以及更新当前余额¶

在部署合约时，活动的目标由所有者在不可变参数 goal 中指定。要检查是否达到目标，我们必须将筹集的总额与目标进行比较。

QA 筹集的金额存储在区块链上的合约账户中，可以通过隐式声明的 _balance 字段访问，如下所示：

bal <- _balance;

Money 表示为 Uint128 类型的值。

注解

像任何其他合约字段一样， _balance 字段是使用运算符 <- 读取的。但是， _balance 字段只能通过接受来自传入 messages 的资金（使用指令 accept ）或通过明确地将资金转移到其他帐户（使用如下所述的 send 指令）来更新。

发送 Messages¶

在 Scilla 中， transitions 可以通过两种方式传输数据。一种方法是通过 events ，如前一个示例中所述。另一种是通过使用指令 send 发送 messages。

send 用于向其他帐户发送 messages，以便调用另一个智能合约上的 transitions，或者将资金转移到用户帐户。另一方面， events 是智能合约可以用来将数据传输到客户端应用程序的分派信号。

要定义 message，我们可以使用与定义 events 时类似的语法：

msg = {_tag : ""; _recipient : owner; _amount : bal; code : got_funds_code};

message 必须包含必填的 message 字段 _tag 、_recipient 和 _amount 。 _recipient 字段是消息要发送到的区块链地址（类型为 ByStr20 ）， _amount 字段是要转移到该帐户的 QA 数量。

_tag 字段的值表示的是要部署在 _recipient 地址的合约调用的 transition（ String 类型）的名称。如果 _recipient 是用户帐户的地址，则忽略 _tag 的值，因此为简单起见，我们这里定义为空，即 "" 。

注解

为了能够同时退还合约和用户帐户（对于使用钱包合约进行捐赠的支持者非常有用），请使用 ZRC-5 中的标准 transition 名称，如 AddFunds 。

除了必填字段之外，message 还可以包含其他字段，例如上面的代码所示。但是，如果 message 的接收者是合约，则附加字段的名称和类型必须与在接收者合约上调用的 transition 参数相同。

发送 message 是使用 send 指令完成的，该指令将 messages 列表作为参数。由于我们在众筹合约中一次只会发送一条 message，因此我们定义了一个库函数 one_msg 来构造一个由 message 组成的列表：

let one_msg =
  fun (msg : Message) =>
  let nil_msg = Nil {Message} in
    Cons {Message} msg nil_msg

要发送 message，我们首先构造 message，并将其插入列表，然后发送：

msg = {_tag : ""; _recipient : owner; _amount : bal; code : got_funds_code};
msgs = one_msg msg;
send msgs

Procedures¶

Scilla 合约的 transitions 通常需要执行相同的小指令序列。为了防止代码重复，合约可以定义许多 procedures，这些 procedures 可以通过合约的 transitions 调用。procedures 还有助于将合约代码分成独立的、自包含的部分，这些部分更容易阅读和单独推理。

使用关键字 procedure 来声明 procedure。procedure 的结束使用关键字 end 声明。 procedure 关键字后面是 transition 名称，然后是 () 中的输入参数，然后是 procedure 的语句。

在我们的示例中，名为 Donate 的 transition 将在三种情况下触发一个 event ：如果捐赠在截止日期之后发生，则触发一个错误 event ；如果捐赠者以前捐赠过，则触发另一个错误 event；由于大部分 event 触发代码是相同的，我们决定定义一个名为 DonationEvent 的 procedure，负责发出正确的 event：

procedure DonationEvent (failure : Bool, error_code : Int32)
  match failure with
  | False =>
    e = {_eventname : "DonationSuccess"; donor : _sender;
         amount : _amount; code : accepted_code};
    event e
  | True =>
    e = {_eventname : "DonationFailure"; donor : _sender;
         amount : _amount; code : error_code};
    event e
  end
end

该 procedure 接受两个参数：一个 Bool 类型，代表捐赠是否失败；一个代表当失败发生时，失败类型的错误代码。

procedure 会对参数 failure 进行 match 。如果捐赠没有失败，错误代码将被忽略，并触发一个名为 DonationSuccess 的 event。否则，如果捐赠失败，则触发一个名为 DonationFailure 的 event，该 event 带有作为 procedure 的第二个参数进行传递的错误代码。

下面的代码展示了如何使用参数 True 和 0 调用名为 DonationEvent 的procedure：

c = True;
err_code = Int32 0;
DonationEvent c err_code;

注解

特殊参数 _sender 、 _origin 和 _amount 对 procedure 是可用的，即使 procedure 是由 transition 而不是由传入消息调用的。没有必要将这些特殊参数作为实参传递给 procedure。

注解

procedures 与库函数相似，它们可以从任何 transition 中调用(只要 transition 是在 procedures 之后定义的)。但是两者也有不同之处，标准库函数不能访问合约状态，procedures 不能有返回值。

procedures 与 transitions 有点类似，因为它们都可以访问和更改合约状态，以及读取传入消息和发送传出消息。但是，procedures 不能在链上调用，只能从合约外部调用 transitions，因此 procedures 可以被视为私有 transitions。

代码完整示例¶

完整的众筹合约代码如下

(***************************************************)
(*                 Scilla version                  *)
(***************************************************)

scilla_version 0

(***************************************************)
(*               Associated library                *)
(***************************************************)
import BoolUtils

library Crowdfunding

let one_msg =
  fun (msg : Message) =>
    let nil_msg = Nil {Message} in
    Cons {Message} msg nil_msg

let blk_leq =
  fun (blk1 : BNum) =>
  fun (blk2 : BNum) =>
    let bc1 = builtin blt blk1 blk2 in
    let bc2 = builtin eq blk1 blk2 in
    orb bc1 bc2

let get_funds_allowed =
  fun (cur_block : BNum) =>
  fun (max_block : BNum) =>
  fun (balance : Uint128) =>
  fun (goal : Uint128) =>
    let in_time = blk_leq cur_block max_block in
    let deadline_passed = negb in_time in
    let target_not_reached = builtin lt balance goal in
    let target_reached = negb target_not_reached in
    andb deadline_passed target_reached

let claimback_allowed =
  fun (balance : Uint128) =>
  fun (goal : Uint128) =>
  fun (already_funded : Bool) =>
    let target_not_reached = builtin lt balance goal in
    let not_already_funded = negb already_funded in
    andb target_not_reached not_already_funded

let accepted_code = Int32 1
let missed_deadline_code = Int32 2
let already_backed_code  = Int32 3
let not_owner_code  = Int32 4
let too_early_code  = Int32 5
let got_funds_code  = Int32 6
let cannot_get_funds  = Int32 7
let cannot_reclaim_code = Int32 8
let reclaimed_code = Int32 9

(***************************************************)
(*             The contract definition             *)
(***************************************************)
contract Crowdfunding

(*  Parameters *)
(owner     : ByStr20,
max_block : BNum,
goal      : Uint128)

(* Contract constraint *)
with
  let zero = Uint128 0 in
  builtin lt zero goal
=>

(* Mutable fields *)
field backers : Map ByStr20 Uint128 = Emp ByStr20 Uint128
field funded : Bool = False

procedure DonationEvent (failure : Bool, error_code : Int32)
  match failure with
  | False =>
    e = {_eventname : "DonationSuccess"; donor : _sender;
         amount : _amount; code : accepted_code};
    event e
  | True =>
    e = {_eventname : "DonationFailure"; donor : _sender;
         amount : _amount; code : error_code};
    event e
  end
end

procedure PerformDonate ()
  c <- exists backers[_sender];
  match c with
  | False =>
    accept;
    backers[_sender] := _amount;
    DonationEvent c accepted_code
  | True =>
    DonationEvent c already_backed_code
  end
end

transition Donate ()
  blk <- & BLOCKNUMBER;
  in_time = blk_leq blk max_block;
  match in_time with
  | True  =>
    PerformDonate
  | False =>
    t = True;
    DonationEvent t missed_deadline_code
  end
end

procedure GetFundsFailure (error_code : Int32)
  e = {_eventname : "GetFundsFailure"; caller : _sender;
       amount : _amount; code : error_code};
  event e
end

procedure PerformGetFunds ()
  bal <- _balance;
  tt = True;
  funded := tt;
  msg = {_tag : ""; _recipient : owner; _amount : bal; code : got_funds_code};
  msgs = one_msg msg;
  send msgs
end

transition GetFunds ()
  is_owner = builtin eq owner _sender;
  match is_owner with
  | False =>
    GetFundsFailure not_owner_code
  | True =>
    blk <- & BLOCKNUMBER;
    bal <- _balance;
    allowed = get_funds_allowed blk max_block bal goal;
    match allowed with
    | False =>
      GetFundsFailure cannot_get_funds
    | True =>
      PerformGetFunds
    end
  end
end

procedure ClaimBackFailure (error_code : Int32)
  e = {_eventname : "ClaimBackFailure"; caller : _sender;
       amount : _amount; code : error_code};
  event e
end

procedure PerformClaimBack (amount : Uint128)
  delete backers[_sender];
  msg = {_tag : ""; _recipient : _sender; _amount : amount; code : reclaimed_code};
  msgs = one_msg msg;
  e = { _eventname : "ClaimBackSuccess"; caller : _sender; amount : amount; code : reclaimed_code};
  event e;
  send msgs
end

transition ClaimBack ()
  blk <- & BLOCKNUMBER;
  after_deadline = builtin blt max_block blk;
  match after_deadline with
  | False =>
    ClaimBackFailure too_early_code
  | True =>
    bal <- _balance;
    f <- funded;
    allowed = claimback_allowed bal goal f;
    match allowed with
    | False =>
      ClaimBackFailure cannot_reclaim_code
    | True =>
      res <- backers[_sender];
      match res with
      | None =>
        (* Sender has not donated *)
        ClaimBackFailure cannot_reclaim_code
      | Some v =>
        PerformClaimBack v
      end
    end
  end
end

示例三：代币交易所¶

在第三个例子中，我们来看一下用 Scilla 编写的合约是如何通过相互传递消息和读取彼此的状态来进行交互的。作为我们的示例应用程序，我们选择了一个简化的代币转换合约，其中用户可以将一种类型的同质化代币交换为另一种类型。

同质化代币¶

回想一下，同质化代币是指与其他相同类型的代币难以区分的代币。例如，1美元钞票与任何其他1美元钞票没有区别(至少在用于支付商品、服务或其他代币时没有区别)。

Zilliqa 合约参考库提供了常用合约类型的规范和参考实现， ZRC2 标准为同质化代币指定了一个标准，我们将在本例中使用它。我们不会详细讨论代币合约是如何工作的，只是指出实现代币转换所需的几个重要方面。

交易规范¶

我们希望我们的简单转换支持以下功能：

该交易所有许多上市的代币，这些代币可以彼此自由转换。每个列出的代币都由其代币代简称标识(例如，”USD” 表示美元)。
交易所应该始终有一个管理员。管理员负责批准代币合约，并将其在交易所上市。管理员可以将管理员角色传递给其他人。
任何用户都可以在交易所下单。为了下单，用户指定他想要出售哪个代币，他提供多少代币，他想购买哪个代币，以及他想要多少代币作为回报。该合约跟踪每一个活跃的（不匹配的）订单。
当用户试图下单出售一些代币时，交易所会检查用户是否确实有这些代币要出售。如果他确实有，那么交易所就会索取这些代币并持有它们，直到订单匹配为止。
任何用户都可以匹配交易所的活跃订单。为了匹配到订单，用户必须明确指定要匹配的订单。
当用户试图匹配订单时，交易所会检查该用户是否确实拥有订单发布者想要购买的代币。如果他确实有，那么交易所就会将订单下发时所要求的代币转移到订单匹配器，并将下单者想要从订单匹配器购买的代币转移给他。在代币被转移之后，交易所会删除已完成的订单。

为了使示例简洁，我们的交易所将不支持下架代币、取消订单、限时订单、订单排序以便订单匹配器获得尽可能好的交易、订单的部分匹配、确保交易所不被滥用、交易手续费等。我们鼓励读者通过实现未实现的功能来进一步熟悉 Scilla。

管理员角色¶

交易所必须始终有管理员，包括首次部署时。管理员可能会随着时间的推移而改变，因此我们定义了一个可变字段 admin 来跟踪当前管理员，并将其初始化为 initial_admin ，它作为一个不可变参数给出：

contract SimpleExchange
(
  initial_admin : ByStr20 with end
)

field admin : ByStr20 with end = initial_admin

admin 字段的类型是 ByStr20 with end ，这是一种地址类型。正如在前面的例子中， ByStr20 是长度为 20 的字符串类型，但我们现在要添加额外的要求，当该字符串被解释为网络上的地址时，该地址必须在使用中，并且该地址处的内容必须满足 with 和 end 关键字之间的任何内容。

在这种情况下， with 和 end 之间没有任何内容，因此我们没有额外的要求。但是，该地址必须由用户或其他合约使用 - 否则 Scilla 将不接受其具有合法地址类型。（当交易所与列出的代币合约交互时，我们将更详细地介绍地址类型。）

有多个 transition 需要检查 _sender 是否为当前的 admin ，因此让我们定义一个 procedure 来检查这种情况：

procedure CheckSenderIsAdmin()
  current_admin <- admin;
  is_admin = builtin eq _sender current_admin;
  match is_admin with
  | True =>  (* Nothing to do *)
  | False =>
    (* Construct an exception object and throw it *)
    e = { _exception : "SenderIsNotAdmin" };
    throw e
  end
end

如果 _sender 是当前管理员，则什么也不会发生，调用此 procedure 的任何 transition 都可以继续。但是，如果``_sender`` 是其他人，则该 procedure 会引发异常，从而导致当前事务中止。

我们希望管理员能够将管理员角色传递给其他人，因此我们定义我们的第一个 transition SetAdmin ，如下：

transition SetAdmin(new_admin : ByStr20 with end)
  (* Only the former admin may appoint a new admin *)
  CheckSenderIsAdmin;
  admin := new_admin
end

transition 会应用 procedure CheckSenderIsAdmin ，如果没有抛出异常，则发送者确实是当前管理员，因此允许将管理员角色传递给其他人。新管理员必须同样是正在使用的地址。

Intermezzo：代表代币所有者转移代币¶

在我们继续向我们的交易所添加功能之前，我们必须首先了解代币合约如何在用户之间转移代币。

ZRC2 代币标准定义了一个字段 balances 来跟踪每个用户拥有多少代币：

field balances: Map ByStr20 Uint128

然而，这对我们的交易所并不是特别有用，因为代币合约不允许交易所转移属于交易所本身以外的其他人的代币。

相反的，ZRC2 标准定义了另一个字段 allowances ，拥有令牌的用户可以使用它来允许另一个用户部分访问所有者的令牌：

field allowances: Map ByStr20 (Map ByStr20 Uint128)

例如，如果 Alice 给了 Bob 100 个代币的配额，那么代币合约中的 allowances 映射将包含值 allowances[<address of Alice>][<address of Bob>] = 100 。这会允许 Bob 使用这 100 个 Alice 的代币，就像使用他自己的一样。（Alice 当然可以提取配额，只要 Bob 还没有花掉这些代币）。

在用户下订单之前，用户应该向交易所提供他想要出售的代币额度以支付订单。然后用户才可以下订单，同时交易所会检查配额是否足够。然后交易所会将代币转移到自己的账户中持有，直到订单匹配为止。

类似地，在用户匹配订单之前，用户应该向交易所提供下单者想要购买的代币的配额。然后用户才可以匹配订单，同时交易所会检查配额是否足够。然后，交易所将这些代币转移给下订单的用户，并将代币转移给匹配的用户，这些转移的代币就是在下订单时转移给自己的那些。

为了检查用户提供给交易所的当前配额，我们需要在代币地址类型中指定 allowances 字段。我们会像下面这样做：

ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end

与 admin 字段一样，我们要求地址正在使用中。此外，还必须满足 with 和 end 之间的要求：

关键字 contract 指定：地址必须由合约使用，而不是由用户使用。
关键字 field 指定：相关合约必须包含具有指定名称和指定类型的可变字段。

上架新币¶

交易所跟踪其上市代币，即允许在交易所交易哪些代币。我们通过定义从代币代码（ String ）到代币地址的映射来实现这一点。

field listed_tokens :
  Map String (ByStr20 with contract
                             field allowances : Map ByStr20 (Map ByStr20 Uint128)
                      end)
  = Emp String (ByStr20 with contract
                               field allowances : Map ByStr20 (Map ByStr20 Uint128)
                        end)

只有允许管理员上架新代币，因此我们在这里再次利用 procedure CheckSenderIsAdmin 。

此外，我们只想上架与之前上架的代币具有不同代币代码的代币。为此，我们定义了一个 procedure CheckIsTokenUnlisted 来检查代币代码是否被定义为 listed_tokens 映射中的键。：

library SimpleExchangeLib

let false = False

...

contract SimpleExchange (...)

...

procedure ThrowListingStatusException(
  token_code : String,
  expected_status : Bool,
  actual_status : Bool)
  e = { _exception : "UnexpectedListingStatus";
       token_code: token_code;
       expected : expected_status;
       actual : actual_status };
  throw e
end

procedure CheckIsTokenUnlisted(
  token_code : String
  )
  (* Is the token code listed? *)
  token_code_is_listed <- exists listed_tokens[token_code];
  match token_code_is_listed with
  | True =>
    (* Incorrect listing status *)
    ThrowListingStatusException token_code false token_code_is_listed
  | False => (* Nothing to do *)
  end
end

这次我们定义了一个辅助 procedure ThrowListingStatusException ，它无条件地抛出异常。这将在我们稍后编写用于下订单的 transition 时有用，因为我们需要检查订单中涉及的代币是否已上架。

我们还在合约的库中定义了常量 false 。这是因为 Scilla 要求所有值在用于计算之前都必须命名。在库代码中定义常量可以防止我们用常量定义混淆 transition 代码：

(* Incorrect listing status *)
false = False; (* We don't want to do it like this *)
ThrowListingStatusException token_code false token_code_is_listed

有了帮助 procedure ，我们现在可以定义 transition ListToken 了，如下所示：

transition ListToken(
  token_code : String,
  new_token : ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end
  )
  (* Only the admin may list new tokens.  *)
  CheckSenderIsAdmin;
  (* Only new token codes are allowed.  *)
  CheckIsTokenUnlisted token_code;
  (* Everything is ok. The token can be listed *)
  listed_tokens[token_code] := new_token
end

下单¶

要下订单，用户必须指定他想要出售的代币代码和数量，以及他想要购买的代币代码和数量。如果没有代币代码上架，我们将调用 procedure ThrowListingStatusException 过程：

transition PlaceOrder(
  token_code_sell : String,
  sell_amount : Uint128,
  token_code_buy: String,
  buy_amount : Uint128
  )
  (* Check that the tokens are listed *)
  token_sell_opt <- listed_tokens[token_code_sell];
  token_buy_opt <- listed_tokens[token_code_buy];
  match token_sell_opt with
  | Some token_sell =>
    match token_buy_opt with
    | Some token_buy =>
      ...
    | None =>
      (* Unlisted token *)
      ThrowListingStatusException token_code_buy true false
    end
  | None =>
    (* Unlisted token *)
    ThrowListingStatusException token_code_sell true false
  end
end

如果两个代币都上架了，我们必须首先检查用户是否为交易所提供了足够的配额。当另一个用户匹配订单时，我们将需要类似的检查，因此我们定义了一个帮助 procedure CheckAllowance 来执行检查：

procedure CheckAllowance(
  token : ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end,
  expected : Uint128
  )
  ...
end

为了执行检查，我们需要远程读取代币合约中的配额字段。我们对 _sender 给交易所的配额感兴趣，其地址由一个特殊的不可变字段 _this_address 给出，所以我们想远程读取代币合约中的配额 allowances[_sender][_this_address] 的值。

Scilla 中的远程读取是使用运算符 <- & 执行的，我们使用 . 指定我们要远程读取的合约的符号。因此，远程读取的整个语句如下：

actual_opt <-& token.allowances[_sender][_this_address];

就像我们执行本地读取映射一样，从远程映射读取的结果是一个可选值。如果对于 v 计算结果为 Some v ，则用户向交易所提供了 v 代币的配额，如果结果为 None ，则用户根本没有提供配额。因此，我们需要对结果进行模式匹配以获得实际的配额：

(* Find actual allowance. Use 0 if None is given *)
actual = match actual_opt with
         | Some x => x
         | None => zero
         end;

为方便起见，我们再次在合约库中定义常量 zero = Uint128 0 。

我们现在可以将实际配额与我们期望的配额进行比较，如果实际配额不足，则抛出异常：

is_sufficient = uint128_le expected actual;
  match is_sufficient with
  | True => (* Nothing to do *)
  | False =>
    ThrowInsufficientAllowanceException token expected actual
  end

函数 uint128_le 是一个实用函数，它对 Uint128 类型的值执行小于或等于比较。该函数是在标准库的 IntUtils 部分定义的，所以为了使用该函数，我们必须将 IntUtils 导入合约，这部分定义在 scilla_version 之后，合约库定义之前：

scilla_version 0

import IntUtils

library SimpleExchangeLib
...

我们还利用辅助 procedure ThrowInsufficientAllowanceException 在配额不足时抛出异常，因此 procedure CheckAllowance 最终如下所示：

procedure ThrowInsufficientAllowanceException(
  token : ByStr20,
  expected : Uint128,
  actual : Uint128)
  e = { _exception : "InsufficientAllowance";
       token: token;
       expected : expected;
       actual : actual };
  throw e
end

procedure CheckAllowance(
  token : ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end,
  expected : Uint128
  )
  actual_opt <-& token.allowances[_sender][_this_address];
  (* Find actual allowance. Use 0 if None is given *)
  actual = match actual_opt with
           | Some x => x
           | None => zero
           end;
  is_sufficient = uint128_le expected actual;
  match is_sufficient with
  | True => (* Nothing to do *)
  | False =>
    ThrowInsufficientAllowanceException token expected actual
  end
end

transition PlaceOrder(
  token_code_sell : String,
  sell_amount : Uint128,
  token_code_buy: String,
  buy_amount : Uint128
  )
  (* Check that the tokens are listed *)
  token_sell_opt <- listed_tokens[token_code_sell];
  token_buy_opt <- listed_tokens[token_code_buy];
  match token_sell_opt with
  | Some token_sell =>
    match token_buy_opt with
    | Some token_buy =>
      (* Check that the placer has allowed sufficient funds to be accessed *)
      CheckAllowance token_sell sell_amount;
      ...
    | None =>
      (* Unlisted token *)
      ThrowListingStatusException token_code_buy true false
    end
  | None =>
    (* Unlisted token *)
    ThrowListingStatusException token_code_sell true false
  end
end

如果用户给了交易所足够的额度，交易所可以向代币合约发送消息，以便从交易所自己的余额中转移代币。我们需要在代币合约上调用的 transition 称为 TransferFrom ，而不是 Transfer ，后者从发送者自己的代币余额中转移资金，而不是从发送者允许的其他人余额中转移资金。

由于消息看起来很像订单匹配时我们需要的消息，因此我们使用合约库中的辅助函数生成消息（我们还需要一个新的常量 true ）：

library SimpleExchangeLib

let true = True

...

let one_msg : Message -> List Message =
  fun (msg : Message) =>
    let mty = Nil { Message } in
    Cons { Message } msg mty

let mk_transfer_msg : Bool -> ByStr20 -> ByStr20 -> ByStr20 -> Uint128 -> Message =
  fun (transfer_from : Bool) =>
  fun (token_address : ByStr20) =>
  fun (from : ByStr20) =>
  fun (to : ByStr20) =>
  fun (amount : Uint128) =>
    let tag = match transfer_from with
              | True => "TransferFrom"
              | False => "Transfer"
              end
    in
    { _recipient : token_address;
     _tag : tag;
     _amount : Uint128 0;  (* No Zil are transferred, only custom tokens *)
     from : from;
     to : to;
     amount : amount }

let mk_place_order_msg : ByStr20 -> ByStr20 -> ByStr20 -> Uint128 -> List Message =
  fun (token_address : ByStr20) =>
  fun (from : ByStr20) =>
  fun (to : ByStr20) =>
  fun (amount : Uint128) =>
    (* Construct a TransferFrom messsage to transfer from seller's allowance to exhange *)
    let msg = mk_transfer_msg true token_address from to amount in
    (* Create a singleton list *)
    one_msg msg

contract SimpleExchange (...)

...

transition PlaceOrder(
  token_code_sell : String,
  sell_amount : Uint128,
  token_code_buy: String,
  buy_amount : Uint128
  )
  (* Check that the tokens are listed *)
  token_sell_opt <- listed_tokens[token_code_sell];
  token_buy_opt <- listed_tokens[token_code_buy];
  match token_sell_opt with
  | Some token_sell =>
    match token_buy_opt with
    | Some token_buy =>
      (* Check that the placer has allowed sufficient funds to be accessed *)
      CheckAllowance token_sell sell_amount;
      (* Transfer the sell tokens to the exchange for holding. Construct a TransferFrom message to the token contract. *)
      msg = mk_place_order_msg token_sell _sender _this_address sell_amount;
      (* Send message when the transition completes. *)
      send msg;
      ...
    | None =>
      (* Unlisted token *)
      ThrowListingStatusException token_code_buy true false
    end
  | None =>
    (* Unlisted token *)
    ThrowListingStatusException token_code_sell true false
  end
end

最后，我们需要存储新订单，以便用户将来可以匹配订单。为此，我们定义了一个新类型 Order ，它包含最终匹配订单时所需的所有信息：

(* Order placer, sell token, sell amount, buy token, buy amount *)
type Order =
| Order of ByStr20
           (ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end)
           Uint128
           (ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end)
           Uint128

Order 类型的值由类型构造函数 Order 、代币地址和要出售的代币数量以及代币地址和要购买的代币数量给出。

我们现在需要一个包含从订单号（类型为 Uint128 ）到 Order 的映射的字段，它表示当前活动的订单。此外，我们将需要一种生成唯一订单号的方法，因此我们将定义一个字段来保存要使用的下一个订单号：

field active_orders : Map Uint128 Order = Emp Uint128 Order

field next_order_no : Uint128 = zero

要添加新订单，我们需要生成一个新订单号，将生成的订单号和新订单存储在 active_orders 映射中，最后增加 next_order_no 字段（使用库常量 one = Uint128 1 ），以便为生成下一个订单。我们将把它放在一个辅助 procedure AddOrder 中，并在 transition PlaceOrder 中添加一个对该 procedure 的调用：

procedure AddOrder(
  order : Order
  )
  (* Get the next order number *)
  order_no <- next_order_no;
  (* Add the order *)
  active_orders[order_no] := order;
  (* Update the next_order_no field *)
  new_order_no = builtin add order_no one;
  next_order_no := new_order_no
end

transition PlaceOrder(
  token_code_sell : String,
  sell_amount : Uint128,
  token_code_buy: String,
  buy_amount : Uint128
  )
  (* Check that the tokens are listed *)
  token_sell_opt <- listed_tokens[token_code_sell];
  token_buy_opt <- listed_tokens[token_code_buy];
  match token_sell_opt with
  | Some token_sell =>
    match token_buy_opt with
    | Some token_buy =>
      (* Check that the placer has allowed sufficient funds to be accessed *)
      CheckAllowance token_sell sell_amount;
      (* Transfer the sell tokens to the exchange for holding. Construct a TransferFrom message to the token contract. *)
      msg = mk_place_order_msg token_sell _sender _this_address sell_amount;
      (* Send message when the transition completes. *)
      send msg;
      (* Create order and add to list of active orders  *)
      order = Order _sender token_sell sell_amount token_buy buy_amount;
      AddOrder order
    | None =>
      (* Unlisted token *)
      ThrowListingStatusException token_code_buy true false
    end
  | None =>
    (* Unlisted token *)
    ThrowListingStatusException token_code_sell true false
  end
end

PlaceOrder 现在已经完成，但还缺少一件事。 ZRC2 代币标准规定，当执行 transition TransferFrom 时，代币将消息发送给接收者和 _sender （称为发起者），以此来通知他们传输成功。这些通知称为回调。由于我们的交易所在卖出代币上执行 transition TransferFrom ，并且由于交易所是这些代币的接收者，我们需要指定可以处理这两个回调的 transition ——如果我们不这样做，那么回调将不会被识别，从而导致整个 PlaceOrder 交易失败。

代币合约通知代币转移的接收者，因为此类通知增加了额外的保护措施，以防止将代币转移到无法处理代币所有权的合约的风险。例如，如果有人在本节的第一个示例中将代币转移到 HelloWorld 合约，那么代币将被永久锁定，因为 HelloWorld 合约无法对代币进行任何操作。

我们的交易所只能处理有活跃订单的代币，但原则上没有什么可以阻止用户不下订单就向交易所转账，所以我们需要确保交易所只涉及代币自己发起的转账。因此，我们定义了一个 procedure CheckInitiator ，如果交换涉及它本身没有启动的代币传输，它会抛出异常，并从所有回调 transition 中调用该 procedure ：

procedure CheckInitiator(
  initiator : ByStr20)
  initiator_is_this = builtin eq initiator _this_address;
  match initiator_is_this with
  | True => (* Do nothing *)
  | False =>
    e = { _exception : "UnexpecedTransfer";
         token_address : _sender;
         initiator : initiator };
    throw e
  end
end

transition RecipientAcceptTransferFrom (
  initiator : ByStr20,
  sender : ByStr20,
  recipient : ByStr20,
  amount : Uint128)
  CheckInitiator initiator
end

transition TransferFromSuccessCallBack (
  initiator : ByStr20,
  sender : ByStr20,
  recipient : ByStr20,
  amount : Uint128)
  CheckInitiator initiator
end

匹配订单¶

对于 transition MatchOrder ，我们可以利用上一节中定义的许多辅助函数和 procedure 。

用户指定他希望匹配的订单。然后我们在 active_orders 映射中查找订单号，如果找不到订单则抛出异常：

transition MatchOrder(
  order_id : Uint128)
  order <- active_orders[order_id];
  match order with
  | Some (Order order_placer sell_token sell_amount buy_token buy_amount) =>
    ...
  | None =>
    e = { _exception : "UnknownOrder";
         order_id : order_id };
    throw e
  end
end

为了匹配订单，匹配者必须提供足够的买入代币额度。这是由我们之前定义的 procedure CheckAllowance 检查的，因此我们在这里简单地重用该 procedure ：

transition MatchOrder(
  order_id : Uint128)
  order <- active_orders[order_id];
  match order with
  | Some (Order order_placer sell_token sell_amount buy_token buy_amount) =>
    (* Check that the placer has allowed sufficient funds to be accessed *)
    CheckAllowance buy_token buy_amount;
    ...
  | None =>
    e = { _exception : "UnknownOrder";
         order_id : order_id };
    throw e
  end
end

我们现在需要生成两条转账消息：一条消息是买入代币上的 TransferFrom 消息，将匹配者的配额转移给下订单的用户，另一条消息是卖出代币上的 Transfer 消息，将被持有的代币转移到订单匹配器。同样的，我们定义辅助函数来生成消息：

 library SimpleExchangeLib

 ...

 let two_msgs : Message -> Message -> List Message =
   fun (msg1 : Message) =>
   fun (msg2 : Message) =>
     let first = one_msg msg1 in
     Cons { Message } msg2 first

 let mk_make_order_msgs : ByStr20 -> Uint128 -> ByStr20 -> Uint128 ->
                           ByStr20 -> ByStr20 -> ByStr20 -> List Message =
   fun (token_sell_address : ByStr20) =>
   fun (sell_amount : Uint128) =>
   fun (token_buy_address : ByStr20) =>
   fun (buy_amount : Uint128) =>
   fun (this_address : ByStr20) =>
   fun (order_placer : ByStr20) =>
   fun (order_maker : ByStr20) =>
     (* Construct a Transfer messsage to transfer from exchange to maker *)
     let sell_msg = mk_transfer_msg false token_sell_address this_address order_maker sell_amount in
     (* Construct a TransferFrom messsage to transfer from maker to placer *)
     let buy_msg = mk_transfer_msg true token_buy_address order_maker order_placer buy_amount in
     (* Create a singleton list *)
     two_msgs sell_msg buy_msg

...

contract SimpleExchange (...)

...

transition MatchOrder(
   order_id : Uint128)
   order <- active_orders[order_id];
   match order with
   | Some (Order order_placer sell_token sell_amount buy_token buy_amount) =>
     (* Check that the placer has allowed sufficient funds to be accessed *)
     CheckAllowance buy_token buy_amount;
     (* Create the two transfer messages and send them *)
     msgs = mk_make_order_msgs sell_token sell_amount buy_token buy_amount _this_address order_placer _sender;
     send msgs;
     ...
   | None =>
     e = { _exception : "UnknownOrder";
          order_id : order_id };
     throw e
   end
 end

由于订单现在已经匹配，所以不应再将其列为活动订单，因此我们删除 active_orders 中的条目：

transition MatchOrder(
  order_id : Uint128)
  order <- active_orders[order_id];
  match order with
  | Some (Order order_placer sell_token sell_amount buy_token buy_amount) =>
    (* Check that the placer has allowed sufficient funds to be accessed *)
    CheckAllowance buy_token buy_amount;
    (* Create the two transfer messages and send them *)
    msgs = mk_make_order_msgs sell_token sell_amount buy_token buy_amount _this_address order_placer _sender;
    send msgs;
    (* Order has now been matched, so remove it *)
    delete active_orders[order_id]
  | None =>
    e = { _exception : "UnknownOrder";
         order_id : order_id };
    throw e
  end
end

transition MatchOrder 到此就结束了，但我们需要定义一个额外的回调 transition。下订单时，我们执行了 transition TransferFrom ，但现在我们也执行 transition Transfer ，这会产生不同的回调：

transition TransferSuccessCallBack (
  initiator : ByStr20,
  sender : ByStr20,
  recipient : ByStr20,
  amount : Uint128)
  (* The exchange only accepts transfers that it itself has initiated.  *)
  CheckInitiator initiator
end

请注意，我们不需要指定处理从 transition Transfer 中接收代币的 transition，因为交易所永远不会将自己作为接收者执行 Transfer 。通过完全不定义回调 transition，我们还处理了用户以交易所作为接收方进行转账的情况，因为接收方回调在交易所上不会有匹配的 transition，这将导致整个转账交易失败。

代码完整示例¶

我们现在已经准备好指定整个合约的一切：

scilla_version 0

import IntUtils

library SimpleExchangeLib

(* Order placer, sell token, sell amount, buy token, buy amount *)
type Order =
| Order of ByStr20
           (ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end)
           Uint128
           (ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end)
           Uint128

(* Helper values and functions *)
let true = True
let false = False

let zero = Uint128 0
let one = Uint128 1

let one_msg : Message -> List Message =
  fun (msg : Message) =>
    let mty = Nil { Message } in
    Cons { Message } msg mty

let two_msgs : Message -> Message -> List Message =
  fun (msg1 : Message) =>
  fun (msg2 : Message) =>
    let first = one_msg msg1 in
    Cons { Message } msg2 first

let mk_transfer_msg : Bool -> ByStr20 -> ByStr20 -> ByStr20 -> Uint128 -> Message =
  fun (transfer_from : Bool) =>
  fun (token_address : ByStr20) =>
  fun (from : ByStr20) =>
  fun (to : ByStr20) =>
  fun (amount : Uint128) =>
    let tag = match transfer_from with
              | True => "TransferFrom"
              | False => "Transfer"
              end
    in
    { _recipient : token_address;
     _tag : tag;
     _amount : Uint128 0;  (* No Zil are transferred, only custom tokens *)
     from : from;
     to : to;
     amount : amount }

let mk_place_order_msg : ByStr20 -> ByStr20 -> ByStr20 -> Uint128 -> List Message =
  fun (token_address : ByStr20) =>
  fun (from : ByStr20) =>
  fun (to : ByStr20) =>
  fun (amount : Uint128) =>
    (* Construct a TransferFrom messsage to transfer from seller's allowance to exhange *)
    let msg = mk_transfer_msg true token_address from to amount in
    (* Create a singleton list *)
    one_msg msg

let mk_make_order_msgs : ByStr20 -> Uint128 -> ByStr20 -> Uint128 ->
                          ByStr20 -> ByStr20 -> ByStr20 -> List Message =
  fun (token_sell_address : ByStr20) =>
  fun (sell_amount : Uint128) =>
  fun (token_buy_address : ByStr20) =>
  fun (buy_amount : Uint128) =>
  fun (this_address : ByStr20) =>
  fun (order_placer : ByStr20) =>
  fun (order_maker : ByStr20) =>
    (* Construct a Transfer messsage to transfer from exchange to maker *)
    let sell_msg = mk_transfer_msg false token_sell_address this_address order_maker sell_amount in
    (* Construct a TransferFrom messsage to transfer from maker to placer *)
    let buy_msg = mk_transfer_msg true token_buy_address order_maker order_placer buy_amount in
    (* Create a singleton list *)
    two_msgs sell_msg buy_msg


contract SimpleExchange
(
  (* Ensure that the initial admin is an address that is in use *)
  initial_admin : ByStr20 with end
)

(* Active admin. *)
field admin : ByStr20 with end = initial_admin

(* Tokens listed on the exchange. *)
(* We identify the token by its exchange code, and map it to the address     *)
(* of the contract implementing the token. The contract at that address must *)
(* contain an allowances field that we can remote read.                      *)
field listed_tokens :
  Map String (ByStr20 with contract
                             field allowances : Map ByStr20 (Map ByStr20 Uint128)
                      end)
  = Emp String (ByStr20 with contract
                               field allowances : Map ByStr20 (Map ByStr20 Uint128)
                        end)

(* Active orders, identified by the order number *)
field active_orders : Map Uint128 Order = Emp Uint128 Order

(* The order number to use when the next order is placed *)
field next_order_no : Uint128 = zero

procedure ThrowListingStatusException(
  token_code : String,
  expected_status : Bool,
  actual_status : Bool)
  e = { _exception : "UnexpectedListingStatus";
       token_code: token_code;
       expected : expected_status;
       actual : actual_status };
  throw e
end

procedure ThrowInsufficientAllowanceException(
  token : ByStr20,
  expected : Uint128,
  actual : Uint128)
  e = { _exception : "InsufficientAllowance";
       token: token;
       expected : expected;
       actual : actual };
  throw e
end

(* Check that _sender is the active admin.          *)
(* If not, throw an error and abort the transaction *)
procedure CheckSenderIsAdmin()
  current_admin <- admin;
  is_admin = builtin eq _sender current_admin;
  match is_admin with
  | True =>  (* Nothing to do *)
  | False =>
    (* Construct an exception object and throw it *)
    e = { _exception : "SenderIsNotAdmin" };
    throw e
  end
end

(* Change the active admin *)
transition SetAdmin(
  new_admin : ByStr20 with end
  )
  (* Only the former admin may appoint a new admin *)
  CheckSenderIsAdmin;
  admin := new_admin
end

(* Check that a given token code is not already listed. If it is, throw an error. *)
procedure CheckIsTokenUnlisted(
  token_code : String
  )
  (* Is the token code listed? *)
  token_code_is_listed <- exists listed_tokens[token_code];
  match token_code_is_listed with
  | True =>
    (* Incorrect listing status *)
    ThrowListingStatusException token_code false token_code_is_listed
  | False => (* Nothing to do *)
  end
end

(* List a new token on the exchange. Only the admin may list new tokens.  *)
(* If a token code is already in use, raise an error                      *)
transition ListToken(
  token_code : String,
  new_token : ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end
  )
  (* Only the admin may list new tokens.  *)
  CheckSenderIsAdmin;
  (* Only new token codes are allowed.  *)
  CheckIsTokenUnlisted token_code;
  (* Everything is ok. The token can be listed *)
  listed_tokens[token_code] := new_token
end

(* Check that the sender has allowed access to sufficient funds *)
procedure CheckAllowance(
  token : ByStr20 with contract field allowances : Map ByStr20 (Map ByStr20 Uint128) end,
  expected : Uint128
  )
  actual_opt <-& token.allowances[_sender][_this_address];
  (* Find actual allowance. Use 0 if None is given *)
  actual = match actual_opt with
           | Some x => x
           | None => zero
           end;
  is_sufficient = uint128_le expected actual;
  match is_sufficient with
  | True => (* Nothing to do *)
  | False =>
    ThrowInsufficientAllowanceException token expected actual
  end
end

procedure AddOrder(
  order : Order
  )
  (* Get the next order number *)
  order_no <- next_order_no;
  (* Add the order *)
  active_orders[order_no] := order;
  (* Update the next_order_no field *)
  new_order_no = builtin add order_no one;
  next_order_no := new_order_no
end

(* Place an order on the exchange *)
transition PlaceOrder(
  token_code_sell : String,
  sell_amount : Uint128,
  token_code_buy: String,
  buy_amount : Uint128
  )
  (* Check that the tokens are listed *)
  token_sell_opt <- listed_tokens[token_code_sell];
  token_buy_opt <- listed_tokens[token_code_buy];
  match token_sell_opt with
  | Some token_sell =>
    match token_buy_opt with
    | Some token_buy =>
      (* Check that the placer has allowed sufficient funds to be accessed *)
      CheckAllowance token_sell sell_amount;
      (* Transfer the sell tokens to the exchange for holding. Construct a TransferFrom message to the token contract. *)
      msg = mk_place_order_msg token_sell _sender _this_address sell_amount;
      (* Send message when the transition completes. *)
      send msg;
      (* Create order and add to list of active orders  *)
      order = Order _sender token_sell sell_amount token_buy buy_amount;
      AddOrder order
    | None =>
      (* Unlisted token *)
      ThrowListingStatusException token_code_buy true false
    end
  | None =>
    (* Unlisted token *)
    ThrowListingStatusException token_code_sell true false
  end
end

transition MatchOrder(
  order_id : Uint128)
  order <- active_orders[order_id];
  match order with
  | Some (Order order_placer sell_token sell_amount buy_token buy_amount) =>
    (* Check that the placer has allowed sufficient funds to be accessed *)
    CheckAllowance buy_token buy_amount;
    (* Create the two transfer messages and send them *)
    msgs = mk_make_order_msgs sell_token sell_amount buy_token buy_amount _this_address order_placer _sender;
    send msgs;
    (* Order has now been matched, so remove it *)
    delete active_orders[order_id]
  | None =>
    e = { _exception : "UnknownOrder";
         order_id : order_id };
    throw e
  end
end

procedure CheckInitiator(
  initiator : ByStr20)
  initiator_is_this = builtin eq initiator _this_address;
  match initiator_is_this with
  | True => (* Do nothing *)
  | False =>
    e = { _exception : "UnexpecedTransfer";
         token_address : _sender;
         initiator : initiator };
    throw e
  end
end

transition RecipientAcceptTransferFrom (
  initiator : ByStr20,
  sender : ByStr20,
  recipient : ByStr20,
  amount : Uint128)
  (* The exchange only accepts transfers that it itself has initiated.  *)
  CheckInitiator initiator
end

transition TransferFromSuccessCallBack (
  initiator : ByStr20,
  sender : ByStr20,
  recipient : ByStr20,
  amount : Uint128)
  (* The exchange only accepts transfers that it itself has initiated.  *)
  CheckInitiator initiator
end

transition TransferSuccessCallBack (
  initiator : ByStr20,
  sender : ByStr20,
  recipient : ByStr20,
  amount : Uint128)
  (* The exchange only accepts transfers that it itself has initiated.  *)
  CheckInitiator initiator
end

正如介绍中提到的，我们保持交流简单化，以保持对 Scilla 功能的关注。

为了进一步熟悉 Scilla，我们鼓励读者添加其他功能，例如取消代币上市、取消订单、有到期时间的订单、以便订单匹配器获得最佳交易的优先订单、订单的部分匹配、反对滥用的交易保护、交易所交易费用等。