Mai*_*tor 41 haskell functional-programming idris ethereum smartcontracts
我想知道在Haskell或Idris等类型语言中表达智能合约的最佳方式是什么(例如,您可以将其编译为在以太坊网络上运行).我主要担心的是:哪种类型可以捕获合同可以执行的所有操作?
一个天真的解决方案是将合同定义为EthIO
类型的成员.这种类型就像Haskell一样IO
,但它不是启用系统调用,而是包括区块链调用,即它可以读取和写入区块链的状态,调用其他合同,获取块数据等等.
-- incrementer.contract
main: EthIO
main = do
x <- SREAD 0x123456789ABCDEF
SSTORE (x + 1) 0x123456789ABCDEF
Run Code Online (Sandbox Code Playgroud)
这显然足以执行任何合同,但是:
太强大了.
特别是与以太坊区块链非常相关.
根据这个想法,合同将被定义为一系列行动的折叠:
type Contract action state = {
act : UserID -> action -> state -> state,
init : state
}
Run Code Online (Sandbox Code Playgroud)
所以,程序看起来像:
incrementer.contract
main : Contract
main = {
act _ _ state = state + 1,
init = 0
}
Run Code Online (Sandbox Code Playgroud)
也就是说,您可以定义初始状态,操作类型以及用户提交操作时该状态的更改方式.这将允许人们定义任何不涉及发送/接收资金的任意合同.大多数区块链都有某种货币,大多数有用的合约都是以某种方式涉及金钱,所以这种类型的限制性太强了.
我们可以通过将货币逻辑硬编码到上面的类型中来使上述类型知道货币.因此,我们得到类似的东西:
type Contract action state = {
act : UserID -> action -> state -> state,
init : state,
deposit : UserID -> Amount -> state -> state,
withdrawal : UserID -> Amount -> state -> Maybe state
}
Run Code Online (Sandbox Code Playgroud)
即,合同开发商需要明确定义如何处理货币存款和取款.这种类型足以定义任何可以与主机区块链的货币互动的自包含合约.可悲的是,这样的合同无法与其他合同互动.在实践中,合同经常相互影响.例如,Exchange需要与其交换的令牌合同进行通信以查询余额等.
那么,让我们退后一步,重写保守的解决方案:
type Contract = {
act : UserID -> Action -> Map ContractID State -> State,
init : State
}
Run Code Online (Sandbox Code Playgroud)
根据这个定义,该act
函数不仅可以访问合同本身的状态,还可以访问同一区块链上的每个其他合同的状态.由于每个合同都可以读取彼此的状态,因此可以在此基础上轻松实现通信协议,因此,这种类型足以实现任意交互的合同.此外,如果区块链的货币本身是作为合约实现的(可能使用包装器),那么该类型也足以处理货币,尽管没有对货币进行硬编码.但该解决方案有两个问题:
窥视另一个合同的状态看起来像是一种非常"hacky"的方式来实现沟通;
以这种方式定义的合同将无法与不了解该解决方案的现有合同进行交互.
现在我在黑暗中.我知道我对这个问题没有正确的抽象,但我不确定它会是什么.看起来问题的根源在于我无法正确捕捉交叉合同通信现象.什么具体类型更适合定义任意智能合约?
Ari*_*ham 23
在回答主要问题之前,我将尝试更准确地定义在 Haskell 或 Idris 中编写代码并将其编译为在类似以太坊的区块链上运行意味着什么。Idris 可能更适合这个,但我将使用 Haskell,因为那是我熟悉的。
概括地说,我可以设想两种使用 Haskell 代码为区块链虚拟机生成字节码的方法:
将 EVM 字节码构建为 Haskell 数据的库
从 Haskell 代码生成字节码的GHC后端
使用库方法,将为每个 EVM 字节码声明构造函数,并在其之上分层库代码以创建程序员友好的构造。这可能会被构建成一元结构,从而为定义这些字节码提供类似编程的感觉。然后将提供一个函数来将该数据类型编译为正确的 EVM 字节码,以部署到正确的区块链中。
这种方法的优点是不需要添加基础设施 - 编写 Haskell 代码,使用现有的 GHC 进行编译,然后运行它来生成字节码。
最大的缺点是,不容易重用库中现有的 Haskell 代码。所有代码都必须针对 EVM 库从头开始编写。
这就是GHC 后端发挥作用的地方。编译器插件(目前可能必须是 GHC 分支,就像 GHCJS 一样)会将 Haskell 编译为 EVM 字节码。这将对程序员隐藏单个操作码,因为它们确实太强大而无法直接使用,从而将它们降级为由编译器基于代码级构造发出。您可以将 EVM 视为不纯粹、不安全、有状态的平台,类似于 CPU,语言的工作是将其抽象出来。相反,您可以使用常规 Haskell 函数样式对此进行编写,并且在后端和自定义编写的运行时的限制内,现有的 Haskell 库将编译并可用。
还有混合方法的可能性,我将在本文末尾讨论其中一些方法。
在本文的其余部分中,我将使用 GHC 后端方法,我认为这是最有趣和最相关的。我确信核心思想将延续到图书馆方法中,也许经过一些修改。
然后,您需要决定如何针对 EVM 编写程序。当然,可以编写常规的纯代码并进行编译和计算,但还需要与区块链进行交互。EVM 是一个有状态的、命令式的平台,因此 monad 将是一个合适的选择。
我们将这个基础称为 monadEth
(尽管它不一定是特定于以太坊的),并为其配备一组适当的原语,以便以安全且实用的方式利用底层 VM 的全部功能。
我们稍后将讨论需要哪些原始操作,但现在有两种方法来定义这个 monad:
作为具有一组操作的内置原始数据类型
-- Not really a declaration but a compiler builtin
-- data Eth = ...
Run Code Online (Sandbox Code Playgroud)
由于 EVM 的大部分类似于普通计算机,主要是其内存模型,因此一种更偷偷摸摸的方法是将其别名为IO
:
type Eth = IO
Run Code Online (Sandbox Code Playgroud)
通过编译器和运行时的适当支持,这将允许现有的IO
基于 - 的功能(例如IORef
s)无需修改即可运行。当然,许多IO
功能(例如文件系统交互)将不受支持,并且base
必须提供没有这些功能的自定义包,以确保使用它们的代码不会编译。
需要定义一些内置值来支持区块链编程:
-- | Information about arbitrary accounts
balance :: Address -> Eth Wei
contract :: Address -> Eth (Maybe [Word8])
codeHash :: Address -> Eth Hash
-- | Manipulate memory; subsumed by 'IORef' if the 'IO' monad is used
newEthVar :: a -> Eth (EthVar a)
readEthVar :: EthVar a -> Eth a
writeEthVar :: EthVar -> a -> Eth ()
-- | Transfer Wei to a regular account
transfer :: Address -> Wei -> Eth ()
selfDestruct :: Eth ()
gasAvailable :: Eth Gas
Run Code Online (Sandbox Code Playgroud)
其他基本功能,包括函数调用,包括确定调用是常规(内部)函数调用、消息调用还是委托消息调用,将由编译器和运行时处理。
我们现在要回答最初的问题:智能合约合适的类型是什么?
type Contract = ???
Run Code Online (Sandbox Code Playgroud)
合同需要:
Eth
monad中返回一个操作Eth
我们稍后将定义一个操作来执行此操作。in
获取并返回类型为 的值out
因此,合适的类型可能是:
newtype Contract in out = Contract (Wei -> Env -> in -> Eth out)
Run Code Online (Sandbox Code Playgroud)
该Wei
参数仅供参考;实际转移发生在调用合约时,并且不能被合约修改。
关于环境信息,需要进行一些判断来决定什么应该作为参数传递以及什么应该作为原始Eth
操作可用。
可以使用合约调用原语来调用合约:
call :: Contract in out -> Wei -> in -> Eth out
Run Code Online (Sandbox Code Playgroud)
当然这是一种简化;例如,它不会柯里化输入类型。据推测,编译器将为每个可见合约生成独特的操作,类似于 Solidity。使这个原语可用甚至可能不合适。
另一细节:EVM 支持构造函数,EVM 代码将在合约创建时执行,以允许使用环境信息。因此,由程序员编写的合同类型将是:
main :: Eth (Contract in out)
main = return . Contract $ \wei env a -> do
...
Run Code Online (Sandbox Code Playgroud)
我省略了许多细节,例如错误处理、日志记录/事件、Solidity 互操作/FFI 和部署。尽管如此,我希望我已经对区块链智能合约环境下的函数式语言的编程模型进行了有用的概述。
这些想法并不是严格针对以太坊的。但是,请注意,以太坊使用基于帐户的模型,而比特币和卡尔达诺都使用未花费交易输出(UTxO)模型,因此许多细节会有所不同。比特币实际上并没有一个可用的智能合约平台,而卡尔达诺(其智能合约功能在撰写本文时正处于后期测试阶段)完全是用 Plutus 编程的,Plutus 是 Haskell 的变体。
可以设计其他更加用户友好的方法,而不是使用严格的基于库或后端的方法来生成 EVM 字节码。Cardano 区块链语言Plutus使用模板 Haskell 拼接将链上 Haskell 代码嵌入普通 Haskell 中,并在链下执行。然后该代码由 GHC 插件处理。
另一个有趣的想法是使用 Conal Eliot 的类别编译来提取和编译区块链的 Haskell 代码。这也使用了编译器插件,但必要的插件已经存在。所有这些都是定义相关类别理论类型类的实例所必需的,并且您可以免费获得 Haskell 到任意后端编译。
在写这篇文章时,我大量参考了以下参考资料:
其他有趣的资源:
一篇论文描述了在 Idris 中指定智能合约的更完整方案,利用依赖编程功能来强制执行重要的不变量
一篇描述使用函数式语言来指定区块链智能合约的论文,这是卡尔达诺普利拓斯技术的先驱
为那些对函数式编程和以太坊智能合约感兴趣的人提供的参考文献和 gitter 社区列表。
在Kindelia中,合约只是一个返回 IO 的函数,在网络上执行副作用操作,包括保存/加载持久状态、获取调用者名称和块高度以及调用其他 IO。因此,只需通过输入调用合约即可调用它们,然后它们就可以像普通程序一样执行所需的任何操作。五年后,我认为一定不会有一种不同的或奇特的方式来处理合同。下面是一个“计数器”示例:
// Creates a Counter function with 2 actions:
ctr {Inc} // action that increments the counter
ctr {Get} // action that returns the counter
fun (Counter action) {
// increments the counter
(Counter {Inc}) =
!take x // loads the state and assigns it to 'x'
!save (+ x #1) // overwrites the state as 'x + 1'
!done #0 // returns 0
// returns the counter
(Counter {Get}) =
!load x // loads the state
!done x // returns it
// initial state is 0
} with {
#0
}
Run Code Online (Sandbox Code Playgroud)
如果写成它的类型,则为Counter : CounterAction -> IO<U128>
. 请注意,合约必须具有依赖类型,因为它们返回的类型可能取决于调用者正在执行的操作的值。
当然,不同的网络可能有截然不同的类型,并有或多或少的限制,但它们至少必须满足两个基本需求:持久状态和与其他合约通信。
归档时间: |
|
查看次数: |
1227 次 |
最近记录: |