Scilla深度解析¶

Scilla 合约结构¶

Scilla 合约的一般结构在下面的代码片段中给出：

合约以 scilla_version 的声明开始，它指明合约使用的 Scilla 主版本号。
然后是一个包含纯数学函数的 library 声明，例如，一个计算两位布尔 AND 的函数，或一个计算给定自然数阶乘的函数。
然后是遵循使用关键字 contract 声明的实际合约定义。
在合约中，有四个不同的部分：
1. 第一部分声明了合约的不可变参数。
2. 第二部分描述了合约的约束，约束指明在部署合约时必须是有效的。
3. 第三部分声明了可变字段。
4. 第四部分包含所有 transition 和 procedure 定义。

(* Scilla contract structure *)

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

scilla_version 1

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

library MyContractLib


(* Library code block follows *)



(***************************************************)
(*             Contract definition                 *)
(***************************************************)

contract MyContract

(* Immutable contract parameters declaration *)

(vname_1 : vtype_1,
 vname_2 : vtype_2)

(* Contract constraint *)
with
  (* Constraint expression *)
=>

(* Mutable fields declaration *)

field vname_1 : vtype_1 = init_val_1
field vname_2 : vtype_2 = init_val_2

(* Transitions and procedures *)


(* Procedure signature *)
procedure firstProcedure (param_1 : type_1, param_2 : type_2)
  (* Procedure body *)

end

(* Transition signature *)
transition firstTransition (param_1 : type_1, param_2 : type_2)
  (* Transition body *)

end

(* Procedure signature *)
procedure secondProcedure (param_1 : type_1, param_2 : type_2)
  (* Procedure body *)

end

transition secondTransition (param_1: type_1)
  (* Transition body *)

end

不可变合约参数¶

不可变参数是合约的初始参数，其值在合约部署时定义，之后无法修改。

不可变参数使用以下语法声明：

(vname_1 : vtype_1,
 vname_2 : vtype_2,
  ...  )

每个声明都包含一个参数名称（一个标识符），后跟它的类型，用 : 分隔。多个参数声明由 , 分隔。参数的初始化值将在部署合约时指定。

注解

除了显式声明的不可变参数外，Scilla 合约还具有以下隐式声明的不可变合约参数

1. _this_address of type ByStr20, which is initialised to the address of the contract when the contract is deployed.

2. _creation_block of type BNum, which is initialized to the block number at which the contract is / was deployed.

这些参数可以在实现中自由读取，而不必使用 <- 来取消它的引用调用，并且不能使用 := 修改。

合约约束¶

合约约束是对合约不可变参数的要求。合约约束提供了一种在合约部署后立即建立合约不变性的方法，从而防止合约使用无意义的参数进行部署。

使用以下语法声明合约约束：

with
  ...
=>

约束必须是 Bool 类型的表达式。

在部署合约时检查约束。仅当约束判定为 True 时，合同部署才会成功。如果判定结果为 False ，则部署失败。

下面是一个简单的例子，它使用合约约束来确保在该期限之后不会部署具有有限功能期限的合约：

contract Mortal(end_of_life : BNum)
with
  builtin blt _creation_block end_of_life
=>

上面的代码片段使用了不可变合约参数中描述的隐式合约参数 _creation_block 。

注解

声明合同约束是可选的。如果未声明约束，则假定该约束被简单地默认为 True 。

可变字段¶

可变字段代表合约的可变状态（可变变量）。它们在不可变参数之后声明，每个声明都以关键字 field 为前缀。

field vname_1 : vtype_1 = expr_1
field vname_2 : vtype_2 = expr_2
...

这里的每个表达式都是相关字段的初始值设定项。这些定义在创建时完成了合约的初始状态。当合约执行 transition 时，这些字段的值会被修改。

注解

除了显式声明的可变字段之外，Scilla 合约还有一个隐式声明的 Uint128 类型的可变字段 _balance ，在部署合约时将其初始化为 0。 _balance 字段保存合约持有的资金量，以 QA 衡量（1 ZIL = 1,000,000,000,000 QA）。该字段可以在实现中自由读取，但只能通过明确地将资金转移到其他帐户（使用 send ）或通过接收来自传入消息的资金（使用 accept ）来修改。

注解

可变字段和不可变参数都必须是可存储类型：

消息、事件和特殊 Unit 类型不可存储。所有其他原始类型（如整数和字符串）都是可存储的。
函数类型不可存储。
涉及未实例化类型变量的复杂类型不可存储。
如果映射和 ADT 的子值类型是可存储的，则它们是可存储的。对于映射，这意味着键类型和值类型都必须是可存储的，对于 ADT，这意味着每个构造函数参数的类型都必须是可存储的。

单位¶

Zilliqa 协议支持三种基本的代币单元——ZIL、LI (10^-6 ZIL) 和 QA (10^-12 ZIL)。

Scilla 智能合约中使用的基本单位是 QA。因此，在使用货币变量时，重要的是需要明确表明最后有多少个0附加在 QA 中。

(* fee is 1 QA *)
let fee = Uint128 1

(* fee is 1 LI *)
let fee = Uint128 1000000

(* fee is 1 ZIL *)
let fee = Uint128 1000000000000

Transitions¶

transition 是一种定义合约状态如何改变的方式。合约的 transition 定义了合约的公共接口，因为可以通过向合约发送消息来调用 transition。

transition 是用关键字 transition 定义的，后跟要传递的参数。定义以 end 关键字结束。

transition foo (vname_1 : vtype_1, vname_2 : vtype_2, ...)
  ...
end

其中 vname : vtype 指定每个参数的名称和类型，多个参数之间用 , 分隔。

注解

除了定义中显式声明的参数外，每个 transition 都有以下隐式参数：

_amount : Uint128 : 发送方发送的传入金额，在 QA 中（请参阅上面有关单位的部分）。要将钱从发送方转移到合约，transition 必须使用 accept 指令明确接受资金。如果 transition 不执行 accept ，则不会发生汇款。
_sender : ByStr20 with end : 触发此 transition 的帐户地址。如果 transition 是由合约账户而不是用户账户调用的，则 _sender 是调用此 transition 的合约的地址。在链式调用中，这是发送调用当前 transition 的消息的合约。
_origin : ByStr20 with end : 发起当前交易的账户地址（可能是链式调用）。这始终是用户地址，因为合约永远无法发起交易。

ByStr20 with end 的类型是地址类型。地址类型在地址部分有详细说明。

注解

transition 的参数必须是可序列化的类型：

消息、事件和特殊 Unit 类型不可序列化。
字节字符串是可序列化的。地址只能作为 ByStr20 值进行序列化。所有其他原始类型（如整数和字符串）都是可序列化的。
函数类型和映射类型不可序列化。
涉及未实例化类型变量的复杂类型不可序列化。
如果 ADT 的子值的类型是可序列化的，则 ADT 是可序列化的。这意味着每个构造函数参数的类型都必须是可序列化的。

Procedures¶

procedure 是另一种定义合约状态的方法，现在合约的状态可能会改变，但与 transition 相反，procedure 不是合约公共接口的一部分，并且不能通过向合约发送消息来调用。调用 procedure 的唯一方法是从 transition 或从另一个 procedure 调用它。

procedure 是用关键字 procedure 定义的，后跟要传递的参数。定义以 end 关键字结束。

procedure foo (vname_1 : vtype_1, vname_2 : vtype_2, ...)
  ...
end

其中 vname : vtype 指定每个参数的名称和类型，多个参数之间用 , 分隔。

一旦定义了 procedure，就可以从合约文件其余部分的 transition 和 procedure 中调用它。但是不能从合约中之前定义的 transition 或 procedure 中调用它，procedure 也不能递归调用自身。

使用 procedure 名称后跟 procedure 的实际参数来调用 procedure：

v1 = ...;
v2 = ...;
foo v1 v2;

调用 procedure 时必须提供所有参数。 procedure 不返回结果。

注解

隐式 transition 参数 _sender 、_origin 和 _amount 被隐式传递给 transition 调用的所有 procedure。因此，在定义 procedure 时无需显式声明这些参数。

注解

procedure 参数不能是（或包含）映射。如果一个 procedure 需要访问一个映射，就必须让该 procedure 直接访问包含该映射的合约字段，或者使用库函数在映射上执行必要的计算。

表达式¶

表达式处理纯操作。 Scilla 包含以下类型的表达式：

let x = f ：在合约中把 f 命名为 x。 x 到 f 的绑定是全局的，并延伸到合约结束。以下代码片段定义了一个常量 one ，其值在整个合约中都是 Int32 类型的 1 。
```
let one = Int32 1
```
let x = f in expr ：将 f 绑定到表达式 expr 中的名称 x 。这里的绑定对 expr 来说仅仅是 local 。以下示例将 Int32 类型的 1 的值绑定到 one 以及将 Int32 类型的 2 的值绑定到 two 并使用内置表达式 builtin add one two 计算，该表达式将 1 与 2 相加，因此计算结果为 Int32 类型的 3。
```
let sum =
  let one = Int32 1 in
  let two = Int32 2 in
  builtin add one two
```
{ <entry>_1 ; <entry>_2 ... } ：消息或事件表达式，其中每个条目具有以下形式： b : x 。这里 b 是一个标识符， x 是一个变量，其值绑定到消息中的标识符。
fun (x : T) => expr ：一个函数，它接受类型为 T 的输入 x 并返回表达式 expr 求值结果。
f x ：将函数 f 应用于参数 x 。
tfun 'T => expr ：一个类型函数，它将 'T 作为参数类型并返回表达式 expr 求值结果。这些通常用于构建库函数。有关示例，请参阅 fst 的实现。

注解

当前不允许隐藏类型变量。例如。 tfun 'T => tfun 'T => expr 不是有效的表达式。
@x T ：将类型函数 x 应用于类型 T 。这通过将 x 的第一个类型变量实例化为 T 来专门化类型函数 x 。类型应用程序通常在即将应用库函数时使用。有关示例，请参阅 fst 的示例应用程序。
builtin f x ：在 x 上应用内置函数 f 。
match 表达式：将绑定变量与模式匹配并判断该子句中的表达式。 match 表达式类似于 OCaml 中的 match 表达式。要匹配的模式可以是带有子模式、变量或通配符 _ 的 ADT 构造函数（请参阅 ADTs ）。如果子模式匹配相应的子值，则 ADT 构造函数模式匹配使用相同构造函数构造的值。变量匹配任何内容，并将变量绑定到它在该子句的表达式中匹配的值。通配符匹配任何内容，但随后会忽略该值。
```
match x with
| pattern_1 =>
  expression_1 ...
| pattern_2 =>
  expression_2 ...
| _ => (*Wildcard*)
  expression ...
end
```
注解

模式匹配必须是详尽的，即 x 的每个合法（类型安全）值都必须与模式匹配。此外，每个模式都必须是可达的，即对于每个模式，必须有一个合法（类型安全）的 x 值与该模式匹配，并且不匹配它之前的任何模式。

语句¶

Scilla 中的语句是有效的运算，因此不是纯粹的数学运算。 Scilla 包含以下类型的语句：

x <- f ：获取合约字段 f 的值，并将其存储到局部变量 x 中。
f := x ：用 x 的值更新可变合约字段 f 。 x 可能是一个局部变量，或另一个合约字段。
x <- & BLOCKNUMBER ：获取区块链状态变量 BLOCKNUMBER 的值，并将其存储到局部变量 x 中。
x <- & c.f ：远程获取。获取地址 c 处的合约字段 f 的值，并将其存储到局部变量 x 中。请注意， c 的类型必须是包含字段 f 的地址类型。有关地址类型的详细信息，请参阅地址部分。
v = e ：计算表达式 e ，并将值赋给局部变量 v 。
p x y z ：使用参数 x、y 和 z 调用 procedure p。提供的参数数量必须与 procedure 采用的参数数量相对应。
forall ls p ：为列表 ls 中的每个元素调用 procedure p。 p 应该被定义为只接受一个类型等于列表 ls 元素的参数。

match ：语句级别的模式匹配：

match x with
| pattern_1 =>
  statement_11;
  statement_12;
  ...
| pattern_2 =>
  statement_21;
  statement_22;
  ...
| _ => (*Wildcard*)
  statement_n1;
  statement_n2;
  ...
end

accept ：接受调用 transition 的消息的 QA。该金额会自动添加到合约的 _balance 字段中。如果消息包含 QA，但调用的 transition 不接受这笔钱，则将钱转回给消息的发送者。不接受传入金额（当它非零时）不是错误。
send 和 event：与区块链的通信。有关详细信息，请参阅下一节。
原位映射操作：对 Map 类型的合约字段的操作。有关详细信息，请参阅 Maps 部分。

语句序列必须用分号分隔 ;：

transition T ()
  statement_1;
  statement_2;
  ...
  statement_n
end

请注意，最后的语句没有尾随 ;，因为 ; 用于分隔语句而不是终止它们。

通信¶

一个合约可以通过 send 指令与其他合约和用户账户进行通信：

send msgs：发送 msgs 消息列表。

以下代码片段定义了一条 msg，其中包含四个条目 _tag、_recipient、_amount 和 param。

(*Assume contractAddress is the address of the contract being called and the contract contains the transition setHello*)
msg = { _tag : "setHello"; _recipient : contractAddress; _amount : Uint128 0; param : Uint32 0 };

传递给 send 的消息必须包含必填字段 _tag、_recipient 和 _amount。

_recipient 字段（ByStr20 类型）是消息要发送到的区块链地址，_amount 字段（Uint128 类型）是要转移到该帐户的 QA 数量。

_tag 字段（String 类型）仅在 _recipient 字段的值为合约地址时使用。在这种情况下，_tag 字段的值是要在接收方合约上调用的 transition 的名称。如果收件人是用户帐户，则忽略 _tag 字段。

注解

为了能够将资金从合约转移到合约和用户账户，请使用 ZRC-5 中的标准 transition 名称，即 AddFunds。请务必检查您打算向其发送资金的合约是否符合 ZRC-5 公约。

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

这是一个发送多条消息的示例。

msg1 = { _tag : "setFoo"; _recipient : contractAddress1; _amount : Uint128 0; foo : Uint32 101 };
msg2 = { _tag : "setBar"; _recipient : contractAddress2; _amount : Uint128 0; bar : Uint32 100 };
msgs =
  let nil = Nil {Message} in
  let m1 = Cons {Message} msg1 nil in
  Cons msg2 m1
  ;
send msgs

注解

transition 可以在执行期间的任何时候执行 ``send``（包括在它调用的 procedure 的执行期间），但是直到 transition 完成后才会继续发送消息。更多细节可以在链式调用部分找到。

合约还可以通过发出事件与外界进行通信。事件是存储在区块链上供所有人查看的信号。如果用户使用客户端应用程序调用合约上的 transition，则客户端应用程序可以侦听合约可能发出的事件，并提醒用户。

event e：将消息 e 作为事件发出。以下代码发出一个名为 e_name 的事件。

e = { _eventname : "e_name"; <entry>_2 ; <entry>_3 };
event e

发出的事件必须包含强制字段 _eventname （String 类型），并且还可以包含其他条目。 _eventname 条目的值必须是字符串文字。所有具有相同名称的事件必须具有相同的条目名称和类型。

注解

与发送消息一样，transition 可以在执行期间的任何时候（包括在它调用的过程的执行期间）发出事件，但在 transition 完成之前，该事件在区块链上是不可见的。更多细节可以在链式调用部分找到。

运行时错误¶

transition 在执行过程中可能会遇到运行时错误，例如 out-of-gas 错误、整数溢出或故意抛出的异常。运行时错误会导致 transition 突然终止，并中止整个事务。但是gas费用仍旧会被扣除，直到出现错误为止。

抛出异常的语法类似于事件和消息的语法。

e = { _exception : "InvalidInput"; <entry>_2; <entry>_3 };
throw e

与 event 或 send 不同， throw 的参数是可选的，可以省略。不带参数的抛出异常将导致错误，该错误只会展示发生 throw 的位置而没有更多信息。

注解

如果在执行 transition 期间发生运行时错误，则整个交易将被中止，并且当前合约和其他合约中的任何状态更改都将回滚。（其他合约的状态可能因链式调用而发生变化）。

特别是：

即使在错误发生之前执行了 accept，所有转移的资金都会返回给各自的发送者。
消息队列被清除，因此即使在错误之前执行了 send，也不会再继续发送尚未处理的消息。
事件列表被清除，因此即使在错误之前执行了 event，也不会发出任何事件。

在发生运行时错误之前，仍会为交易收取 Gas 费用。

注解

Scilla 没有异常处理程序。抛出异常总是会中止整个事务。

Scilla 的 Gas 消耗量¶

部署合约并在其中执行 transition 会消耗 gas。这里解释了详细的成本机制。

Nucleus 钱包页面可用于估算某些交易的 gas 成本。

原始数据类型和操作¶

整数类型¶

Scilla 定义了 32、64、128 和 256 位的有符号和无符号整数类型。这些整数类型可以用关键字 IntX 和 UintX 指定，其中 X 可以是 32、64、128 或 256。例如，32 位无符号整数的类型是 Uint32。

以下代码片段声明了一个 Uint32 类型的变量：

let x = Uint32 43

Scilla 支持以下内置的整数运算。每个操作都采用两个整数 IntX / UintX （相同类型）作为参数。有两个除外，即 pow 的第二个参数始终是 Uint32 以及 isqrt 接受单个 UintX 参数。

builtin eq i1 i2 ：判断 i1 是否等于 i2。返回 Bool。
builtin add i1 i2：整数值 i1 和 i2 相加。返回相同类型的整数。
builtin sub i1 i2：从 i1 中减去 i2。返回相同类型的整数。
builtin mul i1 i2：i1 和 i2 的整数乘积。返回相同类型的整数。
builtin div i1 i2：i1 除以 i2 的整数。返回相同类型的整数。
builtin rem i1 i2：i1 除以 i2 的整数余数。返回相同类型的整数。
builtin lt i1 i2：i1 是否小于 i2，返回 Bool。
builtin pow i1 i2：i1 提升到 i2 的幂运算。返回与 i1 类型相同的整数。
builtin isqrt i：计算 i 的整数平方根，即最大整数 j 使得 j * j <= i。返回与 i 类型相同的整数。
builtin to_nat i1：将 Uint32 类型的值转换为 Nat 类型的等效值。
builtin to_(u)int32/64/128/256：将 UintX / IntX 或 String （表示十进制数）值转换为 Option UintX 或 Option IntX 类型的结果。如果转换成功，则返回 Some res，否则返回 None。转换可能会在下面这些情况下失败
- 没有足够的位来表示结果；
- 将负整数（或表示负整数的字符串）转换为无符号类型的值时；
- 输入字符串不能解析为整数。
以下是具体转换内置函数列表：to_int32、to_int64、to_int128、to_int256、to_uint32、to_uint64、to_uint128、to_uint256。

加法、减法、乘法、幂、除法和余数运算可能会引发整数溢出、下溢和除零错误。这会中止当前 transition 的执行并还原迄今为止所做的所有状态更改。

注解

与区块链货币相关的变量，例如消息的 _amount 条目或合约的 _balance 字段，属于 Uint128 类型。

字符串¶

Scilla 中的 String 文字使用双引号括起来的字符序列表示。可以通过使用关键字 String 指定来声明变量。

以下代码片段声明了一个 String 类型的变量：

let x = "Hello"

Scilla 支持以下对字符串的内置操作：

builtin eq s1 s2 ： s1 是否等于 s2。返回 Bool。 s1 和 s2 必须都是字符串类型。
builtin concat s1 s2 ：将字符串 s1 与字符串 s2 连接起来。返回一个 String。
builtin substr s idx len ：从位置 idx 开始提取长度为 len 的 s 子串。 idx 和 len 必须是 Uint32 类型。字符串中的字符索引从 0 开始。如果输入参数的组合导致无效的子字符串，则返回 String 或失败并显示运行时错误。
builtin to_string x：将 x 转换为字符串文字。 x 的有效类型是 IntX、UintX、ByStrX 和 ByStr。返回一个 String。字节字符串被转换为文本十六进制表示。
builtin strlen s ：计算 s （String 类型）的长度。返回一个 Uint32。
builtin strrev s ：返回字符串 s 的反转。
builtin to_ascii h ：将字节字符串（ByStr 或 ByStrX）重新解释为可打印的 ASCII 字符串并返回等效的 String 值。如果字节字符串包含任何不可打印的字符，则会引发运行时错误。

字节字符串¶

Scilla 中的字节字符串使用 ByStr 和 ByStrX 类型表示，其中 X 是一个数字。 ByStr 是指任意长度的字节串，从而对应于任意 X，ByStrX 是指固定长度 X 的字节串。例如，ByStr20 是长度为20的字节串类型，ByStr32 是长度为32的字节串类型，等等。

Scilla 中的字节字符串文字是使用以 0x 为前缀的十六进制字符编写的。请注意，指定 1 个字节需要 2 个十六进制字符，因此 ByStrX 文字需要 2 * X 个十六进制字符。以下代码片段声明了一个 ByStr32 类型的变量：

let x = 0x123456789012345678901234567890123456789012345678901234567890abff

Scilla 支持以下用于计算和转换字节字符串类型的内置操作：

builtin to_bystr h ：将 ByStrX 类型的值 h （对于某些已知的 X）转换为 ByStr 类型的任意长度之一。
builtin to_bystrX h :（请注意，这里的 X 是数字参数，而不是内置名称的一部分，请参见下面的示例）
- 如果参数 h 的类型为 ByStr：将任意大小的字节字符串值 h （类型为 ByStr）转换为固定大小的 ByStrX 类型的字节字符串，长度为 X。在这种情况下，结果为 Option ByStrX 类型：如果参数的长度等于 X，内置函数返回 Some res ，否则为 None 。例如，如果 bs 的长度为 42，则 builtin to_bystr42 bs 返回 Some bs'。
- 如果参数 h 是 Uint(32/64/128/256) 类型：将无符号整数转换为它们的大端字节表示，返回一个 ByStr(4/8/16/32) 值（注意在这个情况下它不是一个可选类型）。例如，builtin to_bystr4 x （仅在 x 的类型为 Uint32 时进行类型检查）或 builtin to_bystr16 x （仅在 x 的类型为 Uint128 时进行类型检查）。
builtin to_uint(32/64/128/256) h ：将固定大小的字节字符串值 h 转换为 Uint(32/64/128/256) 类型的等效值。对于一些小于或等于 (4/8/16/32) 的已知 X，h 必须是 ByStrX 类型。假设采用大端表示。
builtin concat h1 h2：连接字节字符串 h1 和 h2。
- 如果 h1 的类型为 ByStrX 而 h2 的类型为 ByStrY，则结果的类型为 ByStr(X+Y)。
- 如果参数是 ByStr 类型，则结果也是 ByStr 类型。
builtin strlen h：字节串 (ByStr) h 的长度。返回 Uint32。
eq a1 a2: a1 是否等于 a2 ，返回一个 Bool。

地址¶

Zilliqa 网络上的地址是 20 字节的字符串，因此原始地址由 ByStr20 类型的值表示。

此外，Scilla 支持结构化地址类型，即等价于 ByStr20 的类型，但当被解释为网络上的地址时，会提供有关该地址内容的附加信息。地址类型使用形式为 ByStr20 with <address contents> end，其中 <address contents> 指地址包含的内容。

地址类型的层次结构如下：

ByStr20：长度为 20 的原始字节字符串。该类型不提供任何关于地址处的内容的保证。（通常，ByStr20 不被视为地址类型，因为它可以引用任何长度为 20 的字节串，无论它是否表示地址。）
ByStr20 with end：一个 ByStr20，当解释为网络地址时，指的是一个正在使用的地址。如果地址包含合约，或者地址的余额或随机数大于 0，则该地址正在使用中。（地址余额是地址帐户持有的 Qa 数量。地址的随机数是从该地址发起的交易数量）。
ByStr20 with contract end：一个 ByStr20，当解释为网络地址时，指的是合约的地址。
ByStr20 with contract field f1 : t1, field f2 : t2, ... end: 一个 ByStr20，当解释为网络地址时，指的是包含类型为 t1 的可变字段 f1 、类型为 t2 的可变字段 f2 的合约地址，等等。有一个问题是合约可以定义比类型中指定的更多的字段，但类型中指定的字段必须在合约中定义。

注解

所有使用中的地址，以及因此通过扩展的所有合约地址，都隐式定义了一个可变字段 _balance : Uint128。对于用户帐户，_balance 字段是指帐户余额。

注解

不支持指定不可变参数或合约 transition 的地址类型。

地址子类型¶

地址类型的层次结构定义了一个子类型关系：

任何 ByStr20 with ... end 的地址类型都是 ByStr20 的子类型。这意味着可以使用任何地址类型代替 ByStr20，例如，使用 builtin eq 比较相等性，或作为消息的 _recipient 值。
任何 ByStr20 with contract ... end 的合约地址类型都是 ByStr20 with end 的子类型。
任何指定显式字段 `ByStr20 with contract field f1: t11, field f2: t12, ... end 的合约地址类型都是指定这些字段的子集 ByStr20 with contract field f1: t21, field f2: t22 , ... end 的合约地址类型的子类型，前提是 t11 是 t21 的子类型， t12 是 t22 的子类型，两种合同类型中指定的每个字段都依此类推。
对于带有 List 或 Option 等类型参数的 ADT，如果 T 与 S 相同，并且 t1 是 s1 的子类型，t2 是 s2 的子类型，那么 T t1 t2 ... 是 S s1 s2 ... 的子类型，以此类推。
如果 kt1 是 kt2 的子类型且 vt1 是 vt2 的子类型，则具有键类型 kt1 和值类型 vt1 的映射是具有键类型 kt2 和值类型 vt2 的另一个映射的子类型。

地址的动态类型检查¶

通常，Scilla 检查器不能完全静态地对地址类型进行类型检查。例如下面的情况就可能会发生，由于字节字符串是一个 transition 参数，因此不能静态地知道它的值，或者因为字节字符串指的是当前不包含合约但将来可能包含合约的地址。

出于这个原因，只有当实际字节字符串已知时，不可变参数（即部署合约时提供的合约参数）和地址类型的 transition 参数才可以进行动态类型检查。

例如，合约可能会指定一个如下所示的不可变字段 init_owner ：

contract MyContract (init_owner : ByStr20 with end)

当合约被部署时，作为 init_owner 提供的字节字符串被查找为区块链上的地址，如果该地址的内容与地址类型匹配（在地址被用户或合约使用的情况下），那么继续部署，并且 init_owner 可以在整个合约中被视为一个 ByStr20 with end。

类似地，transition 可能指定如下的参数 token_contract：

transition Transfer (
    token_contract : ByStr20 with contract
                                    field balances : Map ByStr20 Uint128
                             end
    )

当 transition 被调用时，作为 token_contract 参数提供的字节字符串被查找为区块链上的地址，如果该地址的内容与地址类型匹配（在地址包含一个具有 Map ByStr20 Uint128 类型的字段 balances 的合约的情况下），那么 transition 参数成功初始化，并且 token_contract 可以在整个转换调用中被视为 ByStr20 with contract field balances : Map ByStr20 Uint128 end。

在任何一种情况下，如果地址的内容与指定的类型不匹配，则动态类型检查不成功，同时会导致部署（对于失败的不可变参数）或 transition 调用（对于 transition 参数）失败。失败的动态类型检查被视为运行时错误，同时会导致当前事务中止。（出于对不可变字段的动态类型检查的目的，合约的部署被视为交易）。

注解

无法指定 ByStr20 文字并将其解释为地址。换句话说，以下代码片段将导致静态类型错误：

let x : ByStr20 with end = 0x1234567890123456789012345678901234567890

针对地址类型验证字节字符串的唯一方法是将其作为不可变字段的值或作为适当类型的 transition 参数传递。

远程获取¶

要执行远程获取 x <- & c.f，c 的类型必须是某种声明字段 f 的地址类型。例如，如果 c 的类型为 ByStr20 with contract field paused : Bool end，则可以使用语句 x <- & c.paused 获取在地址 c 处 paused 字段的值，而无法获取 c 中未声明字段的值（例如，admin），即使地址 c 的合约确实包含字段 admin。为了能够获取 admin 字段的值，c 的类型也必须包含 admin 字段，例如，ByStr20 with contract field paused : Bool, field admin : ByStr20 end

可以使用与本地声明的地图字段相同的方式使用就地操作执行映射字段的远程获取，即 x <- & cm[key]，x <- & cm[key1][key2]，x <- & exists m[key] 等。与远程获取映射字段一样，远程映射字段必须以 c 类型声明，例如，ByStr20 with contract field m : Map Uint128 (Map Uint32 Bool) end。

不允许写入远程字段。

加密内置插件¶

Scilla 中的散列是使用数据类型 ByStr32 声明的。一个 ByStr32 代表一个 32 字节（64 个十六进制字符）的十六进制字节串。 ByStr32 文字以 0x 为前缀。

Scilla 支持以下对哈希和其他加密原语（包括字节序列）的内置操作。在下面的描述中，Any 可以是 IntX、UintX、String、ByStr20 或 ByStr32 类型。

builtin eq h1 h2：h1 是否等于 h2？两个输入都是相同类型的 ByStrX （或者都是 ByStr 类型）。返回一个布尔值。
builtin sha256hash x ：将 Any 类型的 x 转换为其 SHA256 哈希。返回一个 ByStr32。
builtin keccak256hash x：将 Any 类型的 x 转换为其 Keccak256 哈希。返回一个 ByStr32。
builtin ripemd160hash x：将 Any 类型的 x 转换为其 RIPEMD-160 哈希。返回一个 ByStr20。
builtin substr h idx len ：从位置 idx 开始提取长度为 len 的 h 的子字节串。 idx 和 len 必须是 Uint32 类型。字节字符串中的字符索引从 0 开始。返回 ByStr 或失败（导致运行时错误）。
builtin strrev h ：反向字节字符串（ByStr 或 ByStrX）。返回与参数类型相同的值。
builtin schnorr_verify pubk data sig ：使用类型为 ByStr33 的 Schnorr 公钥 pubk 对类型为 ByStr 的字节字符串 data 验证类型为 ByStr64 的签名 sig。
builtin schnorr_get_address pubk：给定一个 ByStr33 类型的公钥，返回与该公钥对应的 ByStr20 Zilliqa 地址。
builtin ecdsa_verify pubk data sig ：使用类型为 ByStr33 的 ECDSA 公钥 pubk 验证类型为 ByStr64 的签名 sig 与类型为 ByStr 的字节字符串 data。
builtin ecdsa_recover_pk data sig recid ：恢复 data （ByStr 类型），同时具有签名 sig （ByStr64 类型）和 Uint32 类型的恢复整数 recid，其值限制为 0、1、2 或 3，未压缩的公钥，返回一个 ByStr65 的值。
builtin bech32_to_bystr20 prefix addr。内置函数采用 String 类型的网络特定前缀（"zil" / "tzil"）和输入 bech32 字符串（String 类型），如果输入有效，则将其转换为原始字节地址 (ByStr20)。返回类型是 Option ByStr20。成功时，返回 Some addr ，输入无效时返回 None。
builtin bystr20_to_bech32 prefix addr。内置函数采用 String 类型的网络特定前缀（"zil" / "tzil" ）和输入 ByStr20 地址，如果输入有效，则将其转换为 bech32 地址。返回类型是 Option String。成功时，返回 Some addr ，无效输入返回 ``None`。
builtin alt_bn128_G1_add p1 p2。内置函数在 alt_bn128 曲线上取两个点 p1、p2，并返回基础组 G1 中的点的总和。输入点和结果点都是一个 Pair {Bystr32 ByStr32}。一个点的每个标量分量 ByStr32 都是一个大端编码的数字。另见 https://github.com/ethereum/EIPs/blob/master/EIPS/eip-196.md
builtin alt_bn128_G1_mul p s。内置函数取 alt_bn128 曲线上的一个点 p （如前所述）和一个标量 ByStr32 的值 s 并返回点 p 取 s 次的总和。结果是曲线上的一个点。
builtin alt_bn128_pairing_product pairs。这个内置函数接受一对点的 pairs 的列表。每对由 G1 组中的一个点（Pair {Bystr32 ByStr32}）作为第一个分量和 G2 组中的一个点（Pair {Bystr64 ByStr64}）作为第二个分量。因此，参数的类型为 List {(Pair (Pair ByStr32 ByStr32) (Pair ByStr64 ByStr64)) }。该函数在每个点上应用一个配对函数来检查是否相等，并根据配对检查是成功还是失败返回 True 或 False。另见 https://github.com/ethereum/EIPs/blob/master/EIPS/eip-197.md

映射¶

Map kt vt 类型的值提供了一个键值存储，其中 kt 是键的类型，vt 是值的类型（在其他一些编程语言中，像 Scilla 的 Map 这样的数据类型被称为关联数组、符号表或字典）。映射键 kt 的类型可以是以下基元类型中的任意一种：String、IntX、UintX、ByStrX、ByStr 或 BNum。值 vt 的类型可以是除函数类型之外的任何类型，这包括内置和用户定义的代数数据类型。

由于不支持复合类型作为映射键类型，因此建模的方式是通过使用诸如一对值与另一个值的关联的嵌套映射实现的。例如，如果一个帐户要与一个特定的受信任用户相关联，同时允许受信任用户代表该帐户花费一定的资金限制，可以使用以下嵌套映射：

field operators: Map ByStr20 (Map ByStr20 Uint128)
  = Emp ByStr20 (Map ByStr20 Unit)

第一个和第二个键是 ByStr20 类型的，分别代表账户和可信用户。我们用 Uint128 类型表示资金限制。

Scilla 支持多种映射操作，可以归纳为

就地操作修改字段映射而不制作任何副本，因此它们属于 Scilla 的命令式片段。这些操作是非常有效的，建议在所有情况下都使用；
函数映射操作旨在用于纯函数，例如，在设计 Scilla 库时，因为它们从不修改调用它们的原始映射。这些操作可能会导致显着的性能开销，因为其中一些操作会创建输入映射的新（修改）副本。在语法上，复制操作都以 builtin 关键字为前缀（见下文）。请注意，要在字段映射上调用函数内置函数，首先需要使用如下命令复制字段映射：map_copy <- field_map，这会导致 gas 消耗与 field_map 的大小成正比。

就地映射操作¶

m[k] := v: 就地插入。将绑定到值 v 的键 k 插入到映射 m 中。如果 m 已经包含键 k，则绑定到 k 的旧值将被映射中的 v 替换。 m 必须引用当前合约中的可变字段。使用语法 m[k1][k2][...] := v 支持插入嵌套映射。如果嵌套映射中不存在中间键，则将它们连同与其关联的映射值一起重新创建。
x <- m[k]：就地本地获取。获取与映射 m 中的键 k 关联的值。 m 必须引用当前合约中的可变字段。如果 k 在 m 中具有关联值 v，则获取的结果为 Some v （请参阅下面的 Option 类型），否则结果为 None。在获取之后，结果被绑定到局部变量 x。使用语法 x <- m[k1][k2][...] 支持从嵌套映射中获取。如果对应的映射中不存在一个或多个中间键，则获取的结果为 None。
x <- & c.m[k]：就地远程获取。除了 m 必须引用地址 c 处合约中的可变字段，其他以与本地获取操作相同的方式工作。
x <- exists m[k]：就地本地密钥存在检查。 m 必须引用当前合约中的可变字段。如果 k 在映射 m 中具有关联值，则检查的结果（Bool 类型）为 True，否则结果为 False。检查后，结果绑定到局部变量 x。语法 x <- exists m[k1][k2][...] 支持通过嵌套映射进行存在检查。如果对应的映射中不存在一个或多个中间键，则结果为 False。
b <- & exists c.m[k]：就地远程密钥存在检查。除了 m 必须引用地址 c 处合约中的可变字段，其他以与本地密钥存在性检查相同的方式工作。
delete m[k]：就地删除。从映射 m 中删除键 k 及其关联值。标识符 m 必须引用当前合约中的可变字段。使用语法 delete m[k1][k2][...] 支持从嵌套映射中删除。如果对应的映射中不存在一个或多个中间键，则该操作无效。请注意，在嵌套删除 delete m[k1][...][kn-1][kn] 的情况下，仅删除 kn 的键值关联。 k1 到 kn-1 的键值绑定将保留在映射中。

函数式映射操作¶

builtin put m k v：将绑定到值 v 的键 k 插入到映射 m 中。返回一个新映射，它是 m 的副本，但 k 与 v 关联。如果 m 已经包含键 k，则绑定到 k 的旧值在结果映射中被 v 替换。 m 的值不变。 put 函数通常用于库函数中。请注意， put 在插入键值对之前制作了 m 的副本。
builtin get m k：获取映射 m 中与键 k 关联的值。返回一个可选值（参见下面的 Option 类型）——如果 k 在 m 中有一个关联值 v，那么结果是 Some v，否则结果是 None。 get 函数通常用于库函数中。
builtin contains m k：键 k 是否与映射 m 中的值相关联？返回一个 Bool 值。 contains 函数通常用于库函数中。
builtin remove m k：从映射 m 中删除键 k 及其关联值。返回一个新映射，它是 m 的副本，但 k 与值无关。 m 的值不变。如果 m 不包含键 k，则 remove 函数仅返回 m 的副本，而不会指示缺少 k。 remove 函数通常用于库函数中。请注意，在删除键值对之前，remove 会复制 m。
builtin to_list m：将映射 m 转换为 List (Pair kt vt)，其中 kt 和 vt 分别是键和值类型（参见下面的 List 类型）。
builtin size m：返回映射 m 中的绑定数。结果类型为 Uint32。调用这个内置函数会消耗少量恒定的 gas 费用。但是不支持直接在字段映射上调用它，这意味着在避免昂贵的复制的同时获取字段映射的大小需要更多的脚手架，你可以在字段映射大小部分找到相关信息。

注解

内置函数 put 和 remove 返回一个新映射，它可能是原始映射的修改副本。这可能会影响性能！

注解

可以使用 Emp 关键字构造空映射，指定键和值类型作为其参数。这是将 Map 字段初始化为空的方法。例如 field foomap : Map Uint128 String = Emp Uint128 String 声明一个 Map 字段，其键是 Uint128 类型，值是 String 类型，它被初始化为空映射。

区块高度¶

区块高度在 Scilla 中有一个专用类型 BNum。这种类型的变量用关键字 BNum 指定，后跟一个整数值（例如 BNum 101）。

Scilla 支持以下对区块高度的内置操作：

eq b1 b2: b1 是否等于 b2？返回一个 Bool 值。
blt b1 b2：b1 是否小于 b2？返回一个 Bool 值。
badd b1 i1：将 UintX 类型的 i1 添加到 BNum 类型的 b1。返回一个 BNum。
bsub b1 b2：b1 减去 b2，均为 BNum 类型。返回一个 Int256。

代数数据类型¶

代数数据类型 (ADT) 是函数式编程中常用的复合类型。每个 ADT 被定义为一组 构造函数。每个构造函数都接受一组特定类型的参数。

Scilla 配备了许多内置 ADT，如下所述。此外，Scilla 允许用户定义他们自己的 ADT。

布尔值¶

布尔值使用 Bool 类型指定。 Bool ADT 有两个构造函数 True 和 False，它们都不带任何参数。因此，以下代码片段使用构造函数 True 构造了一个 Bool 类型的值：

x = True

可选值¶

可选值使用类型 Option t 指定，其中 t 是某种类型。 Option ADT 有两个构造函数：

Some 代表一个值的存在。 Some 构造函数接受一个参数（t 类型的值）。

None 表示没有值。 None 构造函数不接受任何参数。

以下代码片段构造了两个可选值。第一个值是一个不存在的字符串类型的值，使用 None 构造。第二个值是 Int32 类型的值 10，因为该值存在，所以使用 Some 构造：

let none_value = None {String}

let some_value =
  let ten = Int32 10 in
  Some {Int32} ten

可选值对于初始化值未知的字段非常有用：

field empty_bool : Option Bool = None {Bool}

可选值对于可能没有结果的函数也非常有用，例如映射的 get 函数：

getValue = builtin get m _sender;
match getValue with
| Some v =>
  (* _sender was associated with v in m *)
  v = v + v;
  ...
| None =>
  (* _sender was not associated with a value in m *)
  ...
end

列表¶

使用 List t 类型指定值列表，其中 t 是某种类型。 List ADT 有两个构造函数：

Nil 表示一个空列表。 Nil 构造函数不接受任何参数。

Cons 代表一个非空列表。 Cons 构造函数接受两个参数：列表的第一个元素（t 类型），以及另一个表示列表其余部分的列表（List t 类型）。

列表中的所有元素都必须属于同一类型 t。换句话说，不能将两个不同类型的值添加到同一个列表中。

以下示例显示如何构建 Int32 值列表。首先，我们使用 Nil 构造函数创建一个空列表。然后我们使用 Cons 构造函数一一添加其他四个值。注意列表是如何通过添加最后一个元素，然后是倒数第二个元素，依此类推向后构造的，因此最终列表是 [11; 10; 2; 1]：

let one = Int32 1 in
let two = Int32 2 in
let ten = Int32 10 in
let eleven = Int32 11 in

let nil = Nil {Int32} in
let l1 = Cons {Int32} one nil in
let l2 = Cons {Int32} two l1 in
let l3 = Cons {Int32} ten l2 in
  Cons {Int32} eleven l3

Scilla 为列表提供了三种结构递归原语，可用于遍历任意列表的所有元素：

list_foldl: ('B -> 'A -> 'B) -> 'B -> (List 'A) -> 'B ：从前到后递归处理列表中的元素，同时跟踪 累加器 （可以认为是一个累计）。 list_foldl 接受三个参数，它们都依赖于两个类型变量 'A 和 'B：
- 处理元素的函数。这个函数有两个参数。第一个参数是累加器（'B 类型）的当前值。第二个参数是要处理的下一个列表元素（类型为``’A``）。该函数的结果是累加器的下一个值（'B 类型）。
- 累加器的初始值（'B 类型）。
- 要处理的元素列表（类型 (List 'A)）。
应用 list_foldl 的结果是所有列表元素都被处理后的累加器（'B 类型）的值。
list_foldr: ('A -> 'B -> 'B) -> 'B -> (List 'A) -> 'B : 与 list_foldl 类似，只是列表元素是从后向前处理的。另请注意，处理函数以与 list_foldl 中的顺序相反的顺序获取列表元素和累加器。
list_foldk: ('B -> 'A -> ('B -> 'B) -> 'B) -> 'B -> (List 'A) -> 'B ：根据 折叠函数 递归处理列表中的元素，同时跟踪 累加器。 list_foldk 是左右折叠的更通用版本，顺便说一下，这两个折叠都可以通过它来实现。 list_foldk 接受三个参数，它们都依赖于两个类型变量 'A 和 'B：
- 描述折叠步骤的函数。这个函数接受三个参数。第一个参数是累加器（'B 类型）的当前值。第二个参数是要处理的下一个列表元素（类型为 'A）。第三个参数表示延迟的递归调用（类型 'B -> 'B）。该函数的结果是累加器的下一个值（'B 类型）。如果开发者不调用延迟的递归调用，则计算终止。这是 list_foldk 和左右折叠之间的主要区别，左右折叠无条件地从头到尾处理它们的输入列表。
- 累加器 z 的初始值（'B 类型）。
- 要处理的元素列表（类型 List 'A）。

注解

当 ADT 接受类型参数（例如 List 'A），并出现在更大的类型（例如 list_foldl 的类型）中时，必须使用括号将 ADT 及其参数分组 ( )。即使当 ADT 作为另一个 ADT 的唯一参数出现时也是如此。例如，当构造类型为 Int32 的可选值的空列表时，必须使用语法 Nil {(Option Int32)} 来实例化列表类型。

为了进一步说明 Scilla 中的 List 类型，我们展示了一个使用 list_foldl 来计算列表中元素数量的小例子。有关 list_foldk 的示例，请参阅 list_find。

let list_length : forall 'A. List 'A -> Uint32 =
   tfun 'A =>
   fun (l : List 'A) =>
   let foldl = @list_foldl 'A Uint32 in
   let init = Uint32 0 in
   let one = Uint32 1 in
   let iter =
     fun (z : Uint32) =>
     fun (h : 'A) =>
       builtin add one z
   in
     foldl iter init l

list_length 定义了一个函数，它接受一个类型参数 'A 和一个 List 'A 类型的普通（值）参数 l。

'A 是一个类型变量，必须由打算使用 list_length 的代码实例化。类型变量在第 2 行中指定。

在第 4 行，我们实例化 list_foldl 的类型。由于我们正在遍历类型为 'A 的值的列表，我们将 'A 作为第一个类型参数传递给 list_foldl，并且由于我们正在计算列表的长度（一个非负整数），我们将 Uint32 作为累加器类型传递。

在第 5 行中，我们定义了累加器的初始值。由于空列表的长度为 0，因此累加器的初始值为 0（类型为 Uint32，以匹配累加器类型）。

在第 6-10 行，我们指定了处理函数 iter，它接受当前累加器值 z 和当前列表元素 h。在这种情况下，处理函数会忽略列表元素，并将累加器加 1。当列表中的所有元素都被处理后，累加器将增加与列表中元素一样多的次数，因此累加器的最终值将等于列表的长度。

在第 12 行，我们将第 4 行的 list_foldl 的类型实例化版本应用于处理函数、初始累加器和值列表。

作为 Scilla 标准库分发的一部分，ListUtils 库中提供了 List 类型（包括 list_length）的常用实用程序。

Pair¶

值 Pairs 使用类型 Pair t1 t2 指定，其中 t1 和 t2 是类型。 Pair ADT 有一个构造函数：

Pair 代表一对值。 Pair 构造函数接受两个参数，即 pair 的两个值，分别是 t1 和 t2 类型。

注解

Pair 既是类型的名称，也是该类型构造函数的名称。 ADT 和构造函数通常仅在构造函数是 ADT 的唯一构造函数时共享它们的名称。

Pair 值可能包含不同类型的值。换句话说，t1 和 t2 不需要是相同的类型。

下面是一个例子，我们声明了一个 Pair String Uint32 类型的字段 pp，然后我们通过构造一个由 String 类型的值和 Uint32 类型的值组成的 pair 来初始化它：

field pp: Pair String Uint32 =
              let s1 = "Hello" in
              let num = Uint32 2 in
              Pair {String Uint32} s1 num

请注意我们如何将字段类型指定为 Pair A' B' 以及如何将提供给构造函数的值类型指定为 Pair { A' B' } 的不同。

我们现在说明如何使用模式匹配从 Pair 中提取第一个元素。下面显示的函数 fst 是在 Scilla 标准库的 PairUtils 库中定义的。

let fst =
  tfun 'A =>
  tfun 'B =>
  fun (p : Pair ('A) ('B)) =>
    match p with
    | Pair a b => a
    end

要应用 fst ，则必须首先实例化类型变量 'A 和 'B，具体操作如下：

p <- pp;
fst_specialised = @fst String Uint32;
p_fst = fst_specialised p

与标识符 p_fst 关联的值将是字符串 "Hello"。

注解

通常不鼓励使用 Pair。相反，开发者应该定义一个专门用于特定用例中所需的特定类型 pair 的 ADT。请参阅下面有关 User-defined ADTs 的部分。

Nat¶

Peano 数字使用 Nat 类型指定。 Nat ADT 有两个构造函数：

Zero 代表数字 0。Zero 构造函数不接受任何参数。

Succ 代表另一个 Peano 数的后继者。 Succ 构造函数接受一个参数（Nat 类型），它表示比当前数小 1 的 Peano 数。

下面的代码展示了如何构建对应于整数 3 的 Peano 数：

let three =
  let zero = Zero in
  let one  = Succ zero in
  let two  = Succ one in
  Succ two

Scilla 为 Peano 数提供了两种结构递归原语，可用于遍历从给定 Nat 到 Zero 的所有 Peano 数：

nat_fold: ('A -> Nat -> 'A) -> 'A -> Nat -> 'A：递归处理从 Nat 到 Zero 的数字序列，同时跟踪累加器。 nat_fold 接受三个参数，其中两个取决于类型变量 'A：
- 处理数字的函数。这个函数有两个参数。第一个参数是累加器（'A 类型）的当前值。第二个参数是下一个要处理的 Peano 数（类型为 Nat）。顺便说一下，下一个要处理的数字是当前正在处理的数字的前身。该函数的结果是累加器的下一个值（'A 类型）。
- 累加器的初始值（'A 类型）。
- 要处理的第一个 Peano 数（Nat 类型）。
应用 nat_fold 的结果是累加器（'A 类型）的值，当所有 Peano 数都被处理到 Zero 时。
nat_foldk: ('A -> Nat -> ('A ->'A) ->'A) ->'A -> Nat ->'A：根据 折叠函数 递归处理 Peano 数到零，同时跟踪 累加器。 nat_foldk 是左折叠的更通用版本，允许提前终止。它需要三个参数，两个取决于类型变量 'A。
- 描述折叠步骤的函数。这个函数接受三个参数。第一个参数是累加器（'A 类型）的当前值。第二个参数是正在处理的 Peano 数的前身（Nat 类型）。第三个参数表示延迟的递归调用（类型 'A -> 'A）。该函数的结果是累加器的下一个值（'A 类型）。如果开发者不调用延迟的递归调用，则计算终止。左折叠必须处理整个列表，而 nat_foldk 在这方面可能有所不同。
- 累加器 z 的初始值（'A 类型）。
- 要处理的 Peano 数（Nat 类型）。

为了更好地理解 nat_foldk，我们解释了 nat_eq 的工作原理。 nat_eq 检查两个 Peano 数是否相等。下面是带有行号和解释的具体程序。

let nat_eq : Nat -> Nat -> Bool =
fun (n : Nat) => fun (m : Nat) =>
  let foldk = @nat_foldk Nat in
  let iter =
    fun (n : Nat) => fun (ignore : Nat) => fun (recurse : Nat -> Nat) =>
      match n with
      | Succ n_pred => recurse n_pred
      | Zero => m   (* m is not zero in this context *)
      end in
  let remaining = foldk iter n m in
  match remaining with
  | Zero => True
  |   _ => False
  end

第 2 行指定我们采用两个 Peano 数 m 和 n。第 3 行实例化了 nat_foldk 的类型，因为我们将传递一个 Nat 值作为折叠累加器，所以我们给它 Nat。

第 4 到 8 行指定了折叠描述，这是 nat_foldk 通常采用的第一个参数，类型为 'A -> Nat -> ('A -> 'A) -> 'A，但我们在这种情况下指定了 'A 是 Nat。我们的函数采用累加器 n 并且 ignore : Nat 是正在处理的数字的前身，在这种特殊情况下我们不关心它。

本质上，我们从 n 开始累积最终结果并最多迭代 m 次（参见第 10 行），在每个递归步骤（第 4 - 9 行）递减 n 和 m。 m 变量隐式递减，因为这就是 nat_foldk 在幕后工作的方式。我们使用模式匹配（第 6、7 行）显式地递减 n。为了继续迭代递减 m 和 n，我们在第 7 行使用 recurse。如果两个输入数字相等，我们最终将得到等于 0 的累加器 (n)。我们在第 10 行调用累加器的 remaining 来获取最终值。最后，我们将检查我们的累加器是否最终为 Zero，以判断输入数字是否相等。如上所述，在最后几行，当折叠结果为 Zero 时返回 True，否则返回 False。

在累加器 n 达到零（第 8 行）而 m 仍未完全处理的情况下，我们停止迭代（因此该行没有 recurse）并返回一个非零自然数以表示不等式。任何数字（例如 Succ Zero）都可以，但为了使代码简洁，我们返回原始输入数字 m，因为我们知道只有当 m 不为零时才会在 m 上调用 iter。

因为 remaining 得到 n 的最终值，所以在 m 达到零而累加器 n 仍然严格为正的对称情况下，我们表示不等式。

用户自定义 ADT¶

除了上述内置的 ADT 之外，Scilla 还支持用户自定义 ADT。

ADT 定义可能只出现在程序的库部分：要么出现在合约的库部分，要么出现在导入的库中。 ADT 定义在定义它的整个库的范围内，除了 ADT 定义引用之前在同一库或导入库中定义的其他 ADT 定义。特别是，ADT 定义可能不会以归纳/递归方式引用自身。

每个 ADT 定义了一组构造函数。每个构造函数都指定了许多类型，这些类型对应于构造函数采用的参数的数量和类型。构造函数可以指定为不带参数。

一个合约的 ADT 必须有不同的名称，合约中所有 ADT 的所有构造函数的集合也必须有不同的名称。 ADT 和构造函数名称都必须以大写字母开头（‘A’ - ‘Z’）。但是，构造函数和 ADT 可能具有相同的名称，就像 Pair 类型的情况一样，它的唯一构造函数也称为 Pair。

作为用户定义的 ADT 的示例，请考虑来自实现名为 Shogi 或 Japanese Chess (https://en.wikipedia.org/wiki/Shogi) 的类象棋游戏的合约中的以下类型声明。当轮到你时，玩家可以选择移动他的一个棋子，将先前捕获的棋子放回棋盘上，或者弃权并将胜利授予对手。

可以使用以下类型 Piece 定义游戏的棋子：

type Piece =
| King
| GoldGeneral
| SilverGeneral
| Knight
| Lance
| Pawn
| Rook
| Bishop

每个构造函数都代表游戏中的一种棋子。每个构造函数都不接受任何参数。

棋盘表示为一组方块，其中每个方块有两个坐标：

type Square =
| Square of Uint32 Uint32

类型 Square 是一个类型的示例，其中构造函数与类型具有相同的名称。这通常发生在一个类型只有一个构造函数时。构造函数 Square 接受两个参数，都是 Uint32 类型，它们是棋盘上正方形的坐标（行和列）。

与类型 Piece 的定义类似，我们可以使用构造函数为每个合法方向定义运动方向的类型，如下所示：

type Direction =
| East
| SouthEast
| South
| SouthWest
| West
| NorthWest
| North
| NorthEast

我们现在可以定义用户在以下情况下可以选择执行的可能操作类型：

type Action =
| Move of Square Direction Uint32 Bool
| Place of Piece Square
| Resign

如果玩家选择移动一个棋子，她应该使用构造函数 Move，并提供四个参数：

Square 类型的参数，指示她要移动的棋子的当前位置。
Direction 类型的参数，指示移动的方向。
Uint32 类型的参数，指示棋子应移动的距离。
Bool 类型的参数，指示被移动的棋子在被移动后是否应该被提升。

相反，如果玩家选择将先前捕获的棋子放回棋盘上，她应该使用构造函数 Place，并提供两个参数：

Piece 类型的参数，指示将哪一块放置在板上。
Square 类型的参数，指示棋子应放置的位置。

最后，如果玩家选择弃权并将胜利授予她的对手，她应该使用构造函数 Resign。由于 Resign 不接受任何参数，因此不应提供任何参数。

要检查玩家选择了哪个动作，我们使用 match 语句或 match 表达式：

transition PlayerAction (action : Action)
  ...
  match action with
  | Resign =>
    ...
  | Place piece square =>
    ...
  | Move square direction distance promote =>
    ...
  end;
  ...
end

用户自定义 ADT 的类型标识¶

注解

由于 Scilla 实现中的错误，本节中的信息仅适用于 Scilla 0.10.0 及更高版本。使用 0.10.0 之前的 Scilla 版本编写并发现此错误的合约必须重新编写和重新部署，因为它们将不再适用于 0.10.0 及更高版本。

每个类型声明定义了一个唯一的类型。特别需要注意的是，这意味着即使两个库都定义了相同的类型，这些类型也被认为是不同的。

例如，思考以下两个合约：

library C1Lib

type T =
| C1 of Uint32
| C2 of Bool

contract Contract1()

field contract2_address : ByStr20 = 0x1234567890123456789012345678901234567890

transition Sending ()
  c2 <- contract2_address;
  x = Uint32 0;
  out = C1 x;
  msg = { _tag : "Receiving" ; _recipient : c2 ; _amount : Uint128 0 ;
         param : out };
  no_msg = Nil {Message};
  msgs = Cons {Message} msg no_msg;
  send msgs
end

(* ******************************* *)

(* Contract2 is deployed at address 0x1234567890123456789012345678901234567890 *)
library C2Lib

type T =
| C1 of Uint32
| C2 of Bool

contract Contract2()

transition Receiving (param : T)
  match param with
  | C1 v =>
  | C2 b =>
  end
end

尽管两个合约都定义了相同的类型 T，但这两种类型在 Scilla 中被认为是不同的。特别是，这意味着从 Contract1 发送到 Contract2 的消息不会触发 transition Receiving，因为作为 param 消息字段发送的值具有来自 Contract1 的类型 T，而真正需要的是来自 Contract2 的类型 T。

为了将用户自定义 ADT 的值作为参数传递给 transition，必须在用户定义的库中定义类型，发送和接收合约都必须导入：

library MutualLib

type T =
| C1 of Uint32
| C2 of Bool

(* ******************************* *)

import MutualLib

library C1Lib

contract Contract1()

field contract2_address : ByStr20 = 0x1234567890123456789012345678901234567890

transition Sending ()
  c2 <- contract2_address;
  x = Uint32 0;
  out = C1 x;
  msg = { _tag : "Receiving" ; _recipient : c2 ; _amount : Uint128 0 ;
         param : out };
  no_msg = Nil {Message};
  msgs = Cons {Message} msg no_msg;
  send msgs
end

(* ******************************* *)

(* Contract2 is deployed at address 0x1234567890123456789012345678901234567890 *)

scilla_version 0

import MutualLib

library C2Lib

contract Contract2()

transition Receiving (param : T)
  match param with
  | C1 v =>
  | C2 b =>
  end
end

用户自定义库部分提供了有关如何定义和使用库的更多信息。

标准库¶

Scilla 标准库在 Scilla 标准库中单独记录。

用户自定义库¶

除了 Scilla 提供的标准库，用户还可以在区块链上部署库代码。库文件只允许包含纯 Scilla 代码（这与合约库代码的限制相同）。库文件必须使用 .scillib 文件扩展名。

下面是一个用户自定义库的示例，它定义了一个函数 add_if_equal，如果它们相等，则添加到 Uint128 值，否则返回 0。

import IntUtils

library ExampleLib

let add_if_equal =
  fun (a : Uint128) => fun (b : Uint128) =>
  let eq = uint128_eq a b in
  match eq with
  | True => builtin add a b
  | False => Uint128 0

库文件的结构类似于 Scilla 合约的库部分的结构。库文件包含变量和纯库函数的定义，但不包含带有参数、字段、transition 等的实际合约定义。

特别重要的是库不能声明字段。因此，所有库都是无状态的，只能包含纯代码。

与合约导入库的方式类似，库也可以导入其他库（包括用户自定义库）。导入库中变量的范围仅限于直接导入者。因此，如果 X 导入库 Y 而后者又导入库 Z，则 Z 中的名称不在 X 的范围内，而仅在 Y 中。导入中的循环依赖项是不允许的，并在检查阶段标记为错误。

使用用户自定义库进行本地开发¶

要使用在外部（用户定义）库模块中声明的变量和函数，Scilla 可执行文件的命令行参数必须包含 -libdir 选项，以及作为参数的目录列表。如果 Scilla 文件导入库 ALib，则 Scilla 可执行文件将在提供的目录中搜索名为 ALib.scillib 的库文件。如果多个目录包含具有正确名称的文件，则这些目录的优先级与它们提供给 Scilla 可执行文件的顺序相同。或者，可以将环境变量 SCILLA_STDLIB_PATH 设置为库目录列表。

scilla-checker 以与合约模块相同的方式检查库模块。同样， scilla-runner 可以部署库。请注意， scilla-runner 将 blockhain.json 作为参数（它是合约创建所使用的方式）作为与合约创建兼容的命令行参数。

区块链上的用户自定义库¶

虽然 Zilliqa 区块链旨在为执行合约提供标准 Scilla 库，但必须为其提供额外信息以支持用户自定义库。

库的 init.json 必须包含一个名为 _library 的 Bool 条目，设置为 True。此外，导入用户自定义库的合约或库必须在其 init.json 中包含一个名为 _extlibs 的条目，属于 Scilla 类型 List (Pair String ByStr20)。列表中的每个条目都将导入的库名称映射到其在区块链中的地址。

继续上一个示例，导入 Examplelib 的合约或库应在其 init.json 中包含以下条目：

[
  ...,
  {
      "vname" : "_library",
      "type" : "Bool",
      "value": { "constructor": "True", "argtypes": [], "arguments": [] }
  }
  {
    "vname" : "_extlibs",
    "type" : "List(Pair String ByStr20)",
    "value" : [
        {
            "constructor" : "Pair",
            "argtypes" : ["String", "ByStr20"],
            "arguments" : ["ExampleLib", "0x986556789012345678901234567890123456abcd"]
        },
        ...
    ]
  }
]

命名空间¶

导入语句可用于为导入的名称定义单独的命名空间。要将名称从库 Foo 推送到命名空间 Bar，请使用语句 import Foo as Bar。现在必须使用限定名称 Bar.v 来访问 Foo 中的变量 v。这在导入多个定义相同名称的库时很有用。

同一个变量名不能在同一个命名空间中定义多次，因此如果多个导入的库定义了相同的名称，那么最多一个库可以驻留在默认（非限定）命名空间中。所有其他冲突的库必须推送到单独的命名空间。

扩展我们之前的示例，如下所示是一个为了使用函数 add_if_equal 而在命名空间 Bar 中导入 ExampleLib 的合约。

scilla_version 0

import ExampleLib as Bar

library MyContract

let adder = fun (a : Uint128) => fun (b : Uint128) =>
  Bar.add_if_equal a b

contract MyContract ()
...

Scilla 版本¶

主要和次要版本¶

Scilla 版本有一个主要版本、次要版本和补丁号，表示为 X.Y.Z，其中 X 是主要版本，Y 是次要版本，Z 是补丁号。

补丁通常是不影响现有合约行为的错误修复。补丁向后兼容。
次要版本通常包括不影响现有合约行为的性能改进和功能添加。次要版本向后兼容，直到最新的主要版本。
主要版本不向后兼容。我们希望矿工可以访问 Scilla 的每个主要版本的实现，以运行设置为该主要版本的合约。

在主要版本中，建议矿工使用最新的小版本。

命令 scilla-runner -version 将打印被调用的解释器的主要、次要和补丁版本。

合约语法¶

每个 Scilla 合约都必须以主要版本声明开始。语法如下所示：

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

scilla_version 0

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

library MyContractLib

...

(***************************************************)
(*             Contract definition                 *)
(***************************************************)

contract MyContract

...

部署合约时，解释器的输出包含字段 scilla_version : X.Y.Z，区块链代码将使用该字段来跟踪合约的版本。同样， scilla-checker 也会在检查成功时报告合约的版本。

`init.json` 文件¶

除了合约源代码中指定的版本外，还要求合约的 init.json 在部署合约和调用合约 transition 时指定相同的版本。这简化了区块链代码决定调用哪个解释器的过程。

init.json 和源代码中指定的版本不匹配将导致解释器产生 gas-charged 错误。

init.json 示例：

[
   {
      "vname" : "_creation_block",
      "type" : "BNum",
      "value" : "1"
   },
   {
      "vname" : "_scilla_version",
      "type" : "Uint32",
      "value" : "1",
   }
 ]

链式调用¶

当用户通过发送以合约地址作为接收者的消息来调用合约的 transition 时，那么该 transition 可能会继续发送一条或多条消息，也可能会调用其他合约的其他 transition。由此产生的消息、资金转移、transition 调用和合约状态更改的集合称为交易。

发送消息调用另一个 transition （通常在另一个合约上）的 transition 称为 链式调用。

在交易期间，维护未处理消息的 LIFO 队列（即堆栈）。最初，消息队列仅包含原始用户发送的单个消息，但当 transition 执行链式调用时，可能会向队列中添加其他消息。

当 transition 完成时，它的传出消息被添加到消息队列中。然后从队列中删除队列中的第一条消息以进行处理。如果没有消息要处理，则交易完成，所有状态更改和资金转移都提交到区块链。

当 transition 发送多条消息时，消息按以下顺序添加到队列中：

如果执行多条 send 语句，则最后一次 send 的消息最先添加。这意味着首先处理第一次 send 的消息。
如果给 send 语句提供了一个包含多条消息的列表，则在添加列表尾部的消息之前，将列表的头部添加到队列中。这意味着列表中的最后一条消息（首先添加到列表中的消息）首先得到处理。

交易执行期间的任何运行时故障都会导致整个交易中止，不再执行进一步的语句，不再处理进一步的消息，回滚所有状态更改，并将所有转移的资金返还给各自的发送者。然而，直到故障点为止，仍然会为交易收取 gas 费用。

单笔交易可以发送的消息总数目前设置为 10。该数字将来可能会进行修订。

不同 Scilla 版本的合约可能会相互调用 transition。合约之间消息传递的语义保证在主要版本之间向后兼容。

Accounting¶

对于原生 ZIL 资金的转移，Scilla 遵循接受语义。要进行转账，接收方必须通过执行 accept 语句明确接受资金——仅发送方执行 send 语句是不够的。

当合约执行 accept 语句时，传入消息的 _amount 被添加到合约的 _balance 字段中。同时，_amount 从发送方的余额中扣除（如果发送方是合约，则是 _balance 字段，或者如果发送方是用户，则从用户账户余额中扣除）。

相反，当合约执行 send 语句时，外发消息的 _amount 值不会从 _balance 字段中扣除，因为外发资金尚未被接收者接受。

注解

用户帐户（即不持有合约的地址）隐式接受所有传入资金，但在携带资金的消息被处理之前不会这样做。

使用接受语义进行转账意味着转换有可能发送比其合约当前的 _balance 多的资金。只有在一个或多个接收者不接受资金，或者如果多个传出消息中的一个（它会导致当前合约接收（和接受）额外资金来支付尚未处理的消息的传出）导致一系列链式调用时，才必须注意要这样做。

如果在交易过程中的任何时候，接收者接受的资金多于发送者余额中的可用资金，则会发生运行时错误，整个交易将被中止。换句话说，在交易期间的任何时候，账户余额都不会低于 0。