Russell O'Connor
ABSTRACT
Simplicity is a typed, combinator-based, functional language without loops and recursion, designed to be used for crypto-currencies and blockchain applications. It aims to improve upon existing crypto-currency languages, such as Bitcoin Script and Ethereum's EVM, while avoiding some of the problems they face. Simplicity comes with formal denotational semantics defined in Coq, a popular, general purpose software proof assistant. Simplicity also includes operational semantics that are defined with an abstract machine that we call the Bit Machine. The Bit Machine is used as a tool for measuring the computational space and time resources needed to evaluate Simplicity programs. Owing to its Turing incompleteness, Simplicity is amenable to static analysis that can be used to derive upper bounds on the computational resources needed, prior to execution. While Turing incomplete, Simplicity can express any finitary function, which we believe is enough to build useful ``smart contracts'' for blockchain applications.
- G. Andresen. 2012. BIP16: Pay to Script Hash. Bitcoin Improvement Proposal. (2012). shownotehttps://github.com/bitcoin/bips/blob/master/bip-0016.mediawiki.Google Scholar
- A. W. Appel. 2015. Verification of a Cryptographic Primitive: `-256. ACM Trans. Program. Lang. Syst. Vol. 37, 2, Article bibinfoarticleno7 (April 2015), bibinfonumpages31 pages.1007/978--1--4471--3215--8_12Google ScholarDigital Library
- J. Lau 2016. BIP114: Merkelized Abstract Syntax Tree. Bitcoin Improvement Proposal. (2016). shownotehttps://github.com/bitcoin/bips/blob/master/bip-0114.mediawiki.Google Scholar
- X. Leroy 2009. Formal verification of a realistic compiler. Commun. ACM Vol. 52, 7 (2009), 107--115. showURL%http://gallium.inria.fr/ xleroy/publi/compcert-CACM.pdf Google ScholarDigital Library
- G. Maxwell. 2011. Zero-Knowledge Contingent Payment. (2011). shownotehttps://en.bitcoin.it/wiki/Zero_Knowledge_Contingent_Payment.Google Scholar
- S. Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. http://bitcoin.org/bitcoin.pdf. (Nov. 2008).Google Scholar
- S. Nakamoto. 2010natexlaba. misc changes. https://github.com/bitcoin/bitcoin/commit/4bd188c4383d6e614e18f79dc337fbabe8464c82. (Aug. 2010). shownotehttps://bitcoin.svn.sourceforge.net/svnroot/bitcoin/trunk@131.Google Scholar
- S. Nakamoto. 2010natexlabb. Re: Transactions and Scripts: DUP HASH160 ... EQUALVERIFY CHECKSIG. https://bitcointalk.org/index.php?topic=195.msg1611#msg1611. (June 2010).Google Scholar
- National institute of standards and technology 2013. FIPS Pub 186--4 Federal Information Processing Standards Publication Digital Signature Standard (DSS). (2013). showURL%http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.362.5590Google Scholar
- National institute of standards and technology 2015. FIPS 180--4, Secure Hash Standard, Federal Information Processing Standard (FIPS), Publication 180--4. bibinfotypeTechnical Report. bibinfoinstitutionDEPARTMENT OF COMMERCE. showURL%http://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180--4.pdfGoogle Scholar
- R. O»Connor. 2016. Covenants in Elements Alpha. (2016). shownoteBlog post, https://blockstream.com/2016/11/02/covenants-in-elements-alpha.html.Google Scholar
- Parity 2017. The Multi-sig Hack: A Postmortem. (July 2017). shownotehttps://blog.parity.io/the-multi-sig-hack-a-postmortem/.Google Scholar
- M. S. Paterson and M. N. Wegman 1978. Linear unification. J. Comput. System Sci. Vol. 16, 2 (1978), 158 -- 167. showISSN0022-0000 https://doi.org/10.1016/0022-0000(78)90043-0Google ScholarCross Ref
- C. P. Schnorr. 1989. Efficient Identification and Signatures for Smart Cards Proceedings of CRYPTO »89.Google Scholar
- The Coq Development Team. 2016. The Coq Proof Assistant Reference Manual: Version 8.6. https://coq.inria.fr/refman/. (2016).Google Scholar
- P. Todd 2014. BIP65: OP_CHECKLOCKTIMEVERIFY. Bitcoin Improvement Proposal. (2014). shownotehttps://github.com/bitcoin/bips/blob/master/bip-0065.mediawiki.Google Scholar
- G. Wood 2014. Ethereum: A Secure Decentralised Generalised Transaction Ledger. (2014). shownotehttp://gavwood.com/paper.pdf.Google Scholar
- C. Yarvin, P. Monk, A. Dyudin, and R. Pasco. 2016. Urbit: A Solid-State Interpreter. (May 2016). shownotehttp://media.urbit.org/whitepaper.pdf. endthebibliographyGoogle Scholar
Index Terms
- Simplicity: A New Language for Blockchains
Recommendations
Towards Adding Variety to Simplicity
Leveraging Applications of Formal Methods, Verification and Validation. Industrial PracticeAbstractSimplicity is a Turing-incomplete typed combinator language for smart contracts with a formal semantics. The design of Simplicity makes it possible to statically estimate the resources (e.g., memory) required to execute contracts. Such a feature ...
Introduction to Bitcoins, Blockchains and Smart Contracts
SIGCSE '20: Proceedings of the 51st ACM Technical Symposium on Computer Science EducationThis workshop introduces participants to bitcoins, blockchains and programming smart contracts using Ethereum Blockchains and the Solidity programming language. Cryptocurrencies such as Bitcoins use Blockchains and Smart Contracts to enforce ...
Establishing security of Bitcoins using elliptic-curve cryptography-based protocol
It is undeniable that the growth of the computer and network security is repeatedly increased since the past 40 years. In 1985-1986 encryption was applied as a primary technique for providing security. Network security technology includes authentication ...
Comments