Simplicity
Speakers: Russell O’Connor
Date: October 15, 2019
Transcript By: Michael Folkson
Tags: Simplicity
Media: https://www.youtube.com/watch?v=Pn5rySgyTQ0
Slides: https://drive.google.com/file/d/1FivYGQzOYfM0JGl4SS3VR1UGKsyMn_L5/
Simplicity white paper: https://blockstream.com/simplicity.pdf
Intro
So Simplicity is a programming language that I have been working on at Blockstream. I call it an alternative or reimagination of Bitcoin Script as it would have been if I had invented Bitcoin. An alternative or new instruction set that is compatible with Bitcoin. It could be soft forked in. We’ve experimented with it on sidechains such as Elements or Liquid. First I think I should reflect a bit on Bitcoin Script. When I first got interested in Bitcoin I was very intrigued by this idea of programmable money. It had this little programming language called Bitcoin Script that you could program with. But Bitcoin Script has some problems. I think it is fair to say that Bitcoin Script in many ways failed to achieve its design goals the way it was implemented. To get a little bit technical for those who are familiar with Bitcoin Script. When you create a transaction in Bitcoin that you want to redeem there are two components to the Script, the scriptPubKey gets put into the UTXO. When you spend it you have this scriptSig and it has this really cool idea where you concatenate the two Scripts together and you execute it. It looks really beautiful and it was full of problems. OP_RETURN being the most severe where you can just bypass signature verification process entirely. It is sort of because this cool little symmetry idea doesn’t actually work very well because there is this asymmetry actually between the commitment time when you have to put all your logical conditions and spending time. At spending time you can just execute that spending portion of your scriptSig and produce its environment that the scriptPubKey runs in explicitly. Which is why today in Bitcoin the scriptPubKey is basically reduced to push operations only because that constructs the environment that the scriptPubKey gets run in. There are also many other problems with Bitcoin Script. By the time I showed up on the scene many of the opcodes had been disabled by Satoshi including things like multiplication of numbers. It had really been reduced to this miniature script core that just lets you do digital signature verification and hash preimages. Even the timelock mechanism that was originally proposed was broken and had to have soft forks to enable it so that you could do something like that. I have been thinking for a long time how we can achieve the original design ideas of programmable money? Despite all my criticism for Bitcoin Script it was also incredibly innovative I think. There were many, many good design features of Bitcoin Script including the fact that it has no loops which makes it easy to do stack analysis and understand the resource costs upfront before you execute it. The entire UTXO system which I will talk more about later.
Language Design
What would we do if we were to design it from the bottom up? Forget about Bitcoin Script and do something else. We want an expressive language that would allow you to create any functionality you want. Maybe not have such a limited set of hash functions or cryptographic primitives. Maybe you want to get into elliptic curve primitive operations so you can do fancy cryptographic protocols. We also want something that is easy to reason about. Something with simple and machine understandable semantics so that we don’t have semantics like in the original OP_LSHIFT where the semantics are in some cases your machine crashes. The language that we are designing for a blockchain is very different from your traditional programming language because we are operating in an adversarial environment. We want to be able to safely execute programs that you are receiving from the internet. You want to be resistant to denial of service attacks. This is very different from traditional programming languages where you are assumed to be cooperating with the compiler rather than being an adversary of the compiler. Different considerations have to be made. Also blockchain languages are of the form where you are potentially guarding hundreds of millions of dollars with a program that you expect to be executed once. There is a very different cost benefit trade-off compared to traditional programming language where you expect to run the program many times and maybe you can uncover bugs that way. Maybe you don’t have hundreds of millions of dollars at stake. Another design feature that I’d like is concise representation. This is something I talked about very early on about reducing transportation costs through sharing and pruning of subexpressions. Because any code that ends up not being executed in this one time that you execute your program that doesn’t actually have to put on the blockchain because it never gets executed. This is where the Merklized Abstract Syntax Tree (MAST) idea comes from.
Language Features
Simplicity is designed to be an extensible, low level, I want to emphasize low level, programming language that has access to a wide range of intrinsic functions. You would have direct access to elliptic curve operations. Schnorr signatures wouldn’t require a soft fork if Bitcoin was designed this way because you would have access to the elliptic curve math to implement Schnorr Signatures directly. Simplicity has features like transaction introspection and in particular output introspection. This implies this covenant feature. Bitcoin Script allows you to put conditions on who can spend it, whoever has access to the pubkey. With the not so recent soft forks we have access to when it can be spent through the various timelock mechanisms. The covenants tell you where it can be spent basically. It also allows for delegation which allows users to add posthoc spending conditions after the UTXO has been committed but before it has been redeemed. And the Merklized Abstract Syntax allows you to prune away unused branches.
Core Simplicity
I only put this slide up here to make things concrete. This is the core computational part of the Simplicity language. It is only nine combinators. Every Simplicity expression is a function from some type formed out of disjoint union types and product types to some type formed out of disjoint union types and product types. It is first order, there are no higher order functions. This is very, very low level and very simple and very generic. From these nine combinators you can basically produce any computable function at all. This is the syntax of the Simplicity core language. The computation and transaction introspection commands are extra blockchain specific combinators that are in addition to this core computational language. That will give you access to the transaction data to read from and produce sighashes.
Denotational Semantics
This is the formal functional semantics of the Simplicity language. I don’t expect you to read this necessarily but the idea is that it is very short. I made this joke about fitting it on a T shirt before so I now have to go round with my T shirt on showing that that in fact is true. The design of Simplicity is intended so that it is very hard to get the implementation a little wrong. Hopefully either your implementation of the language will be correct or it will be so wrong that it won’t even come close to working correctly. We want to reduce these corner cases and remove subtle bugs from the implementation. This is important for consensus because the interpreter of this language is consensus critical and we want to make those components as simple as possible. That’s why the name is Simplicity. When you make the language simple what you do is offload all of the complexity onto the developer or the programmer. I think that is the correct trade-off when it comes to consensus versus non-consensus critical components.
Example Simplicity
This is an example of how to implement a half-adder for those who took digital logic at university. We have two input bits and it produces a two output answer which is the sum of the two input bits. We don’t have to go over the code. The handwavey explanation is it does the case analysis on the first bit, if the first bit is zero then it produces an output which is zero followed by a copy of the second bit. If the first bit is one then it produces two bit outputs where the first bit is a copy of the second bit and the second bit is the inverse of the second bit. Then it becomes a mathematical theorem that what I just said about manipulating bits is in fact a description of the addition of two binary single bit numbers. Because we have formal semantics that is something that you can prove.
In Haskell you can write it this way. This is the domain specific language I used to generate Simplicity expressions. It gets compiled to a concise binary format. This is something you would transport over the network for your Simplicity program. When your node receives a Simplicity program over the network it reconstructs an internal memory representation of that Simplicity expression as a DAG. We can see some of the sharing that is going on here. Some of the nodes are referred to the same subexpression. This subexpression sharing allows us to make very sophisticated programs but keeping it very concise. This is the half-adder. The DAG representation in memory, a full-adder is composed of two half-adders. We can share that half-adder subexpression and then we can build a 8 bit adder out of a bunch of full-adders. Then we can build the SHA256 compression function and we just keep on going. We can build the Schnorr signature verification function all out of these nine combinators. You might that this produces a very large program. It sort of does. But computer science and programming is even more modular than you might think. The full Schnorr signature verification written in Simplicity includes SHA256 compression because that is part of the protocol for Schnorr signature verification. That only amounts to about 7000 nodes in the DAG because we have all that sharing that reuses various subroutines. If it weren’t for the sharing, unshared everything, it would end up being six trillion nodes. So we get this super exponential compression when you have sharing of subexpressions. It actually turns out very nice.
Bit Machine
To implement the Simplicity language we define this abstract machine that I call the Bit Machine. The Bit Machine is basically a specialized abstract machine designed for interpreting or evaluating Simplicity programs. All those data values, they are encoded as bit strings. We have this cute encoding so that substructures of your data structures are encoded so that those substructures are actually substrings of that data value which allows the Bit Machine to very easily dive into the substructures. The Bit Machine manipulates these two stacks of data while traversing this DAG that we saw over here. It has got this read data stack, the data stack that it reads from. And this other data stack that it writes to. The most important aspect of the Bit Machine is that it provides operational semantics. The denotational semantics tells you what the program does and the operational semantics tells you what are the costs associated with evaluation. We need to model these costs and we can use the Bit Machine to model the costs. Modeling the costs is important when it comes to preventing denial of service attacks against your node. We get a formal model of computational costs. We have a formal proof that these operational semantics defined by the Bit Machine matches the denotational functional semantics I showed you earlier. We can formally prove various static analysis of Bitcoin programs. We can correctly compute costs in time and costs in space. How much time and space, how much memory will be used by the evaluator.
Jets
Jets are an important aspect of the design here. Without it we would run into the problem that if we tried to interpret Schnorr signature verification just by interpreting Simplicity it would be far too expensive. Even though it runs pretty fast, it runs in like a few minutes. But what we do is because we have this Merklized Abstract Syntax we can recognize common subexpressions and then we ca modify the interpreter as an optimization step to say “I’m about perform a Schnorr signature verification so instead of running the Simplicity interpreter what we’re going to do is call into libsecp and run this Schnorr signature verification through there and come back.” This doesn’t change the semantics of the language but it does bring the operational costs down to a respectable level. We need to specify the behavior of the jets. The very cheap solution to specifying behavior of jets is to simply specify them by writing them in Simplicity. This removes any ambiguity that we have. Different implementations can agree on what the definition of these jets are. In the worst case when somebody implements it wrong we can determine who is wrong because we have a formal specification. In the best case what we can do is use formal methods to prove our implementation in C in fact correctly implements the jet. We have some work done on that line at least for the SHA256 compression function already. My opinion is the more jets the better. We should arithmetic jets, we should have elliptic curve operations, we should have all sorts of hash functions, digital signature verification, anything reasonable that we would want we should make a jet.
High Assurance
One of the goals here is high assurance. That is part of what we’re talking about today. We want to use software proof assistants to specify semantics and reason about Simplicity expressions. Not only for jets but also for the programs that people develop. If you are going to secure 100 million dollars worth of value by one of these programs maybe it is worth spending 100 thousand dollars or tens of thousands of dollars to verify it. It might be a good return on investment. I use the Coq proof assistant but Simplicity semantics are simple enough that you could probably define it in any popular software proof assistant. We have a verification of the SHA256 compression function that has been developed in Simplicity. We basically take the specification of SHA256 from Princeton’s verifiable C project where they verified OpenSSL’s implementation of SHA256. We grab that specification, prove that the Simplicity program produces the same result. We get a net result of a formal proof checked in Coq that the Simplicity program produces the same output that the OpenSSL implementation of SHA256 produces. That means that we can safely use the C interpreter to call into OpenSSL’s implementation of SHA256 and we know that we are not going to change the semantics that way. The idea would be to do this for all the various jets that we want to implement. In addition to that having a formal specification of Simplicity is great on one hand. But when you implement it in C and C becomes your consensus implementation then if your C code doesn’t match the formal description you’ve given of Simplicity it turns out your consensus critical C code is the actual definition of what you’re doing not whatever I put on a bunch of slides or a T shirt. Our proposed solution there is to use the verifiable C component of the verified software toolchain that has been developed at Princeton. I’d like to verify the C implementation of the Simplicity interpreter by proving it matches the Coq semantics that define the Coq language. Then we’ll have a very great story to tell of the correctness all the way from the implementation to the interpreter to the definition of the Simplicity language to the programs that people write in Simplicity. We can prove that those are going to be correctly executed by the C interpreter.
Simplicity Applications
Simplicity has a lot of applications. The way it is going to be deployed is right now I have just built a branch off the Elements project. Elements is a sidechain developed by Blockstream based on Bitcoin Core code. Now there is a branch where the Simplicity interpreter has been integrated. You can send regtest funds to a Simplicity contract and redeem them. That is very recent stuff. Then hopefully it will be deployed after more vetting and various other completed work into the Liquid sidechain and maybe other sidechains where people can experiment with it. You can build very interesting applications with Simplicity. For instance the vault construct where you want to force a two phase withdrawal of funds that are protected. The way it works is that you have this first phase of withdrawal that goes on the blockchain and then you are forced into some 24 hour or maybe week long time delay before sending it on to the ultimate destination. During that delay period you have this cancellation clause that you can invoke to recover the funds. That way the idea is that if your hot wallet private key is stolen in order to steal funds they have to post it on a blockchain and then they have to go through this week delay which you can detect. Then pull out some sort of recovery key from cold storage to recover it. Simplicity can be used for transaction rebinding. This is under consideration for Lightning’s new eltoo protocol. You wouldn’t need to add any soft forks, it would just work with Simplicity. You can add velocity limits to hot wallets using covenants to check the time delays on your spending transaction and then limit the amount you are spending to be proportional to the time period. We can do delegation of UTXOs. You can delegate to your administrator when you are going on vacation, control of your UTXO funds all without going onchain. You can even add side conditions to those delegations. You can add limits on the number of funds that you delegate or some velocity limit on that delegation you give to your administrator. We could do escrow for digitally signed proof of delivery. If UPS produces some sort of certificate saying that they delivered something you could automatically release things under those conditions. That sort of oracle model where you use an oracle to connect the real world to the blockchain. For multi-asset sidechains like we have in Liquid we can do automatic partial order fills. It is fairly easy to do an order with a transaction in Liquid. If that order is going to be partially filled that is a little bit more difficult. It requires a lot of interaction between the two participants to come up with a subset of the transaction. They all have to be online at the same time to sign things. But you can create a smart contract with Simplicity that is familiar with the ratio of the two assets that you are requesting. Then when somebody comes along they can partially fulfill the transaction and the remainder balance is automatically respent using a covenant mechanism back to the same script, the same Simplicity expression in order to be posted for other people to fulfill the remainder of your trade that you’re trying to do. The most important Simplicity applications are the ones that I haven’t thought of. That is where you guys come in. To find new and novel uses because the idea behind Simplicity is to provide that flexibility for people to design applications that I haven’t even thought of. I intend to enable those constructions.
Universal Sighash
One idea that I like here, on the Bitcoin mailing list there has been recent discussions about new sighash formats and stuff like that. Simplicity enables what I call universal sighash. This is a combination of delegation with introspection where basically you can specify any hash of the transaction data that you want and sign for that. If you want to only do the outputs or some subset of the outputs or some subset of the inputs, at signing time you can decide which subset you are going to do. You provide using the delegation mechanism a Simplicity expression that constructs the particular aspects of the transaction that you want to hash together. Then you sign the Merkle root of the Simplicity expression that generates it, that’s signing the sighash, plus signing the message hash as well.
Call to Action
So this is my call to action. In my implementation there is much consensus critical work to be done. Mostly about enabling limitations and preventing various denial of service attacks that haven’t been implemented yet. If you are interesting in using Simplicity to experiment with and you are not planning to DOS yourself then this is something you can start working on starting today. Are you a researcher that is doing novel smart contracts based on UTXO smart contracts but you need computation that is not available in Bitcoin? Now you can use Simplicity. The UTXO based model is actually very interesting. It has some advantages and some disadvantages. Some people will say a disadvantage is that you don’t have concurrent access to global state which is too bad. But it has some advantages as well. For instance there is no access to global mutable state. That makes things way more simple to reason about. A UTXO based system has this automatic ability where you have multiple concurrent solutions to a UTXO you are guaranteed that at most one will ever get committed to the blockchain which is very convenient. Do you need novel cryptographic primitives to work with? Are you working with blinded values? Do you need pairing based crypto? We can add jets for that. Are you interested in making tooling? Simplicity is a low level language, it is like writing in Assembly. I expect multiple higher level languages to be compiled to Simplicity. Are you interested in formal verifications of protocols, specifications and implementations and stuff like that? There is lots of work that could be done here.
More Possibilities
In closing I want to mention, although Simplicity is designed for this blockchain application Simplicity’s expressiveness turns out to be basically the same class as that of a boolean circuit. For instance a boolean circuit is just a special case of an arithmetic circuit. If you have gone to some of the other talks here what we can do is generate from Simplicity expressions a set of quadratic polynomial constraints that evaluate the Simplicity program as an algebraic concurrent constraint system. This is useful for various zero knowledge proof systems like bulletproofs and a whole host of other things. There could be some reuse here of taking verified Simplicity expressions to generate various succinct cryptographic proofs.
Where Simplicity
Where can you get more information? There is an introduction pdf link over here. We have a GitHub repository with code and a technical report and this prototype integrationis to the Elements sidechain. Don’t trust, verify. Thank you.
Q&A
Q - Is it sort of like a first order fragment of lambda calculus?
A - That is a fair characterization. It is more related to the sequent calculus than the lambda calculus but those things are closely connected to each other.
Q - You are primarily targeting this as a low level language that people will compile to rather than something that people will write in?
A - That’s correct.
Q - I have a question that might make you go home and cry. Obviously using a verified toolchain is much better but assuming we are going to use clang and LLVM to compile the rest of the consensus critical source code have you looked at taking Simplicity expressions and converting them to LLVM IR as a way to much more cheaply create jets under the same trust model of a compiler behaving correctly?
A - I haven’t looked into that. I think that is an entirely reasonable aspect to research but my time is limited. If somebody else wants to do that I think that would be a great thing to investigate.
Q - You mentioned you have a branch of the Elements project where we can use Simplicity, we can send coins to Simplicity programs and spend. What tooling exists to generate these programs in the first place?
A - At the moment the Simplicity programs are generated by some poorly documented Haskell code that is in the main Simplicity repository. There is really no tooling to integrate it with the transactions. The way I’ve done it is basically… in hex. I think that can be very quickly filled with tooling. Especially interested and motivated parties who might be interested in using Elements to vet their new idea.
Q - How does Simplicity relate to the idea of scriptPubKey and scriptSig. Is the program the scriptPubKey and then the scriptSig is an input?
A - It automatically combines the pay-to-script-hash idea into a single construct. What you do is you use the Merklized Abstract Syntax Tree to compute the Merkle root of your Simplicity expression. That is sort of equivalent to the scriptPubKey. That is where you put in your address that you send to. It is very concise. During redemption what you do is you provide the Simplicity program, this is where the pay-to-script-hash kind of works, and then as part of the consensus rules you have to recompute the commitment Merkle root of that program to make sure it matches. Then there is some other witness data that is hanging on the leaves of that program that is malleable. The scriptSig is not included in that commitment Merkle root calculation but is committed as part of the witness data.