资源描述：
Simplicity A New Language for BlockchainsRussell O’C2017-10-30AbstractSimplicity is a typed, combinator-based, functional language withoutloops and recursion, designed to be used for crypto-currencies and block-chain applications. It aims to improve upon existing crypto-currency lan-guages, such as Bitcoin Script and Ethereum’s EVM, while avoiding someof the problems they face. Simplicity comes with al denotationalsemantics de ned in Coq, a popular, general purpose software proof as-sistant. Simplicity also includes operational semantics that are de nedwith an abstract machine that we call the Bit Machine. The Bit Ma-chine is used as a tool for measuring the computational space and timeresources needed to uate Simplicity programs. Owing to its Turingincompleteness, Simplicity is amenable to static analysis that can be usedto derive upper bounds on the computational resources needed, prior tocution. While Turing incomplete, Simplicity can express any nitaryfunction, which we believe is enough to build useful \smart contracts“ forblockchain applications.0 LicenseThis work is licensed under a Creative Com-mons \Attribution 4.0 International“ license.〈https//creativecommons.org/licenses/by/4.0/deed.en〉1 IntroductionBlockchain and distributed ledger technologies de ne protocols that allow large,ad-hoc, groups of users to transfer value between themselves without needingto trust each other or any central authority. Using public-key cryptography,users can sign transactions that transfer ownership of funds to other users. Toprevent transactions from con icting with each other, for example when oneuser attempts to transfer the same funds to multiple di erent users at the sametime, a consistent sequence of blocks of transactions is committed using a proofof work scheme. This proof of work is created by participants called miners.Each user veri es every block of transactions; among multiple sequences of validblocks, the sequence with the most proof of work is declared to be authoritative.1Bitcoin [20] was the rst protocol to use this blockchain technology to createa secure and permissionless crypto-currency. It comes with a built-in program-ming language, called Bitcoin Script [6, 22], which determines if a transactionis authorized to transfer funds. Rather than sending funds to a speci c party,users send funds to a speci c Bitcoin Script program. This program guards thefunds and only allows them to be redeemed by a transaction that causesthe program to return successfully. Every peer in the Bitcoin network must -cute each of these programs with the provided by the transaction data andall these programs must return successfully in order for the given transaction tobe considered valid.A typical program speci es a public key and simply requires that a validdigital signature of the transaction for that key be provided. Only someonewith knowledge of the corresponding private key can create such a signature.Funds can be guarded by more complex programs. Examples range fromsimpler programs that require signatures from multiple parties, permitting es-crow services [14], to more complex programs that allow for zero-knowledgecontingent payments [19], allowing for trustless and atomic purchases of digitaldata. This last example illustrates how Bitcoin Script can be used to buildsmart contracts, which allow parties to create conditional transactions that areenforced by the protocol itself.Because of its Script language, Bitcoin is sometimes described as pro-grammable money.1.1 Bitcoin ScriptBitcoin Script is a stack-based language similar to Forth. A program in BitcoinScript is a sequence of operations for its stack machine. Bitcoin Script hasconditionals but no loops, thus all programs halt and the language is not Turingcomplete.Originally, these programs were committed as part of the output eld of aBitcoin transaction. The program from the output being redeemed is cutedstarting with the initial stack provided by the redeeming it. The programis successful if it completes without crashing and leaves a non-zero value on thetop of stack.Later, a new option called pay to script hash P2SH [1] was added to Bitcoin.Using this option, programs are committed by specifying a hash of the sourcecode as part of the output eld of a Bitcoin transaction. The eld of aredeeming Bitcoin transaction then provides both the program and the initialstack for the program. The transaction is valid if the hash of the providedprogram matches the hash speci ed in the output being redeemed, and if thatprogram cutes successfully with the provided , as before. The maine ect here is moving the cost of large programs from the person sending fundsto the person redeeming funds.Bitcoin Script has some drawbacks. Many operations were disabled by Bit-coin’s creator, Satoshi Nakamoto [21]. This has left Bitcoin Script with a fewarithmetic multiplication was disabled, conditional, stack manipulation, hash-2ing, and digital-signature veri cation operations. In practice, almost all pro-grams found in Bitcoin follow a small set of simple templates to per digitalsignature veri cation.However, Bitcoin Script also has some desirable properties. All BitcoinScript operations are pure functions of the machine state expect for thesignature-veri cation operations. These signature-veri cation operations re-quire a hash of some of the transaction data. Together, this means the pro-gram’s success or failure is purely a function of the transaction data. Therefore,the person creating a transaction can know whether the transaction they havecreated is valid or not.Bitcoin Script is also amenable to static analysis, which is another desirableproperty. The digital-signature veri cation operations are the most expensiveoperations. Prior to cution, Bitcoin counts the number of occurrences ofthese operations to compute an upper bound on the number of expensive callsthat may occur. Programs whose count exceeds a certain threshold are invalid.This is a of static analysis that ensures the amount of computation thatwill be done isn’t excessive. Moreover, before committing a program to anoutput, the creator of the program can ensure that the amount of computationthat will be done will not be excessive.1.2 Ethereum and the EVMEthereum [31] is another crypto-currency with programmable transactions. Itde nes a language called EVM for its transactions. While more expressive andexible than Bitcoin Script, the design of Ethereum and the EVM has severalissues.The EVM is a Turing-complete programming language with a stack, randomaccess memory, and persistent storage. To prevent in nite loops, cution islimited by a counter called gas, which is paid for in Ethereum’s unit of account,Ether, to the miner of the block containing the transaction. Static analysis isn’tpractical with a Turing-complete language. Therefore, when a program runsout of gas, the transaction is nulli ed but the gas is still paid to the miner toensure they are compensated for their computation e orts.Because of direct access to persistent storage, EVM programs are a functionof both the transaction and the state of the blockchain at the point the transac-tion is inserted into the blockchain. This means users cannot necessarily knowwhat the result of their transaction will be when they create it, nor can theynecessarily know how much gas will be consumed. Users must provide enoughgas to cover the worst-case use scenario and there is no general purpose algo-rithm that can compute that bound. In particular, there is no practical generalpurpose way to tell if any given program will run out of gas in some contexteither at redemption time or creation time. There have been some e orts toper static analysis on a subset of the EVM language [5], but these tools arelimited e.g. they do not support programs with loops.Unlike Bitcoin, there are many instances of ad-hoc, one-o , special purposeprograms in Ethereum. These programs are usually written in a language called3Solidity [12] and compiled to the EVM. These ad-hoc programs are regularlybroken owing to the complex semantics of both Solidity and the EVM; themost famous of these failures were the DAO [8] and Parity’s multiple signaturidation program [26].1.3 A New LanguageIn this paper, we propose a new language that maintains or enhances the desir-able properties that Bitcoin Script has while adding expressiveness. Our designgoals are Create an expressive language that provides users with the tools neededto build novel programs and smart contracts. Enable static analysis that provides useful upper bounds on the amountof computation required. Minimize bandwidth and storage requirements and enhance privacy byremoving unused code at redemption time. Maintain Bitcoin’s design of self-contained transactions whereby programsdo not have access to any ination outside the transaction. Provide al semantics that facilitate easy reasoning about programsusing existing o -the-shelf proof-assistant software.A few of these goals deserve additional explanationStatic analysis allows the protocol to place limits on the amount of compu-tation a transaction can have, so that nodes running the protocol are not overlyburdened. Furthermore, the static analysis can provide program creators witha general purpose tool for verifying that the programs they build will alwayst within these limits. Additionally, it is easy for the other participants in acontract to check the bounds on smart contract’s programs themselves.Self-contained transactions ensure that cution does not depend on theglobal state of the blockchain. Once a transaction’s programs have been vali-dated, that fact can be cached. This is particularly useful when transactionsare being passed around the network before inclusion in the blockchain; onceincluded in the blockchain, the programs do not need to be cuted again.Finally, al semantics that work with proof-assistant software providethe opportunity for contract developers to reason about their programs to ruleout logical errors and to help avoid scenarios like the DAO and Parity’s multi-signature program failure.Like Bitcoin Script and the EVM, our language is designed as low-level lan-guage for cuting smart contracts, rather than as a language for programmerswrite directly. As such, we expect it to be a target for other, higher-level, lan-guages to be complied to.We call our new language Simplicity.4iden A‘As A‘B t B‘Ccompst A‘Cunit A‘1t A‘Binjlt A‘B Ct A‘Cinjrt A‘B Cs A C‘D t B C‘Dcasest AB C‘Ds A‘B t A‘Cpairst A‘B Ct A‘Ctaket A B‘Ct B‘Cdropt A B‘CFigure 1 Typing rules for the terms of core Simplicity.2 Core SimplicitySimplicity is a typed combinator language. Each well-typed Simplicity expres-sion is associated with two types, an type and an output type. Everyexpression denotes a function from its type to its output type.2.1 Types in SimplicityTypes in Simplicity come in three avors. The unit type, written as 1, is the type with one element. A sum type, written as A B, contains the tagged union of values fromeither the left type A or the right type B. A product type, written as A B, contains pairs of elements with the rstone from the type A and the second one from the type B.There are no recursive types in Simplicity. Every type in Simplicity onlycontains a nite number of values; the number of possible values a type containscan be computed by interpreting the type as an arithmetic expression.2.2 Terms in SimplicityThe term language for Simplicity is based on Gentzen’s sequent calculus [13]. Wewrite a type-annotated Simplicity expression as t A‘B where t a Simplicityexpression, A is the expression’s type, and B is the expression’s outputtype.5The core of Simplicity consists of nine combinators for building expressions.They capture the fundamental operations for the three avors of types in Sim-plicity. The typing rules for these nine combinators is given in Figure 1.We can classify the combinators based on the avor of types they support. The unit term returns the singular value of the unit type and ignores itsargument. The injl and injr combinators create tagged values, while the case com-binator, Simplicity’s branching operation, uates one of its two sub-expressions based on the tag of the rst component of its . The pair combinator creates pairs, while the take and drop combinatorsaccess rst and second components of a pair respectively. The iden and comp combinators are not speci c to any avor of type.The iden term represents the identity function for any type and the compcombinator provides function composition.Simplicity expressions an abstract syntax tree. The leaves of this tree areeither iden or unit terms. The nodes are one of the other seven combinators.Each node has one or two children depending on which combinator the noderepresents.Precise semantics are given in the next section. Extensions to this core setof combinators is given in Section 4.2.3 Denotational Semantics of SimplicityBefore giving the semantics of Simplicity terms, we need notations for the valuesof Simplicity types. We write hi 1 for the singular value of the unit type. We write La AB when a A for left-tagged values of the sum type. We write Rb A B when b B for right-tagged values of the sumtype. We write ha;bi A B when a A and b B for values of the pair type.We emphasize that these values are not directly representable in Simplicitybecause Simplicity expressions can only denote functions; we use these valuesonly to de ne the functional semantics of Simplicity.Simplicity’s denotational semantics are recursively de ned. For an expres-sion t A‘B, we de ne its semantics JtK AB as follows.6JidenKa aJcompstKa JtKJsKaJunitKa hiJinjltKa LJtKaJinjrtKa RJtKaJcasestKh La;ci JsKha;ciJcasestKh Rb;ci JtKhb;ciJpairstKa hJsKa;JtKaiJtaketKha;bi JtKaJdroptKha;bi JtKbWe have alized the language and semantics of core Simplicity in the Coqproof assistant [29]. The al semantics in Coq are the o cial semantics ofSimplicity, and for core Simplicity, it is short enough that it ts in Appendix Aof this paper. Having semantics in a general purpose proof assistant allowsus to ally reason both about programs written in Simplicity and aboutalgorithms that analyze Simplicity programs.2.4 CompletenessSimplicity cannot express general computation. It can only express nitary func-tions, because each Simplicity type contains only nitely many values. However,within this domain, Simplicity’s set of combinators is complete any functionbetween Simplicity’s types can be expressed.Theorem 2.1 Finitary Completeness Let A and B be Simplicity types.Let f AB be any function between these types. Then ther
展开阅读全文