Simplicity: Going Beyond Miniscript
Speakers: Christian Lewe
Date: March 1, 2023
Transcript By: aphilg via review.btctranscripts.com
Tags: Simplicity
Category: Conference
Media: https://www.youtube.com/watch?v=abUF4MQ7j1w
Can we welcome Christian to the stage? I think I don’t have any computer yet. Oh.. It’s just okay. All right, I just, I just just read. There’s a pointer, okay, great great. I was a bit confused for a second. Can I start? great, so welcome, I’m Christian Lewe. I work for Blockstream to research where I mainly work on Simplicity and Miniscript and it’s great that we just had a talk on Miniscript so you all know why Miniscript is great, why you should use Miniscript, and in my talk I want to go beyond that. So let’s do a very short introduction. Could you remove like the mouse or something? Like people in the back… great… that confused me so. We just saw that Bitcoin Script is complicated. I, you know, the previous presenter did a way better job of explaining that, doing this nice quiz. That was great. I just have one slide on it, which is a very common smart contract. It’s used in lightning and even though it’s ubiquitous and it’s not so hard, like it’s what the script does is not so complicated, It looks complicated and there are many foot guns so turns out that this is represented with this very short Miniscript. It’s the same.
Miniscript vs Bitcoin Script
Miniscript is Bitcoin script with structure and in particular humans, but also machines can reason about this way more easily. It has a street structure. We can see an or an and, we can see some public keys. Some hash pre images. This is much better for the eyes and much better for machines to reason about. I will just go very quickly about benefits of this. So benefits of structure, we can make sure that our scripts are correct so the intended spending paths that we want are there and unintended spending paths are not there so hackers cannot spend our coins. The scripts are non-malleable so no one can take my transaction and fiddle with the witness in a funky way to bump the fees or something. Scripts are composable like we heard in the previous talk so I can take two scripts from different sources combine them into a larger script Those two sources don’t need to talk to each other and I can reason about the resulting script. I can try to find a witness for this resulting script which is great for interoperability. I can analyze the script statically by just looking at the script so I can see what are the fees, what fees do I expect? Do I hit any consenus bounds that will prevent me from spending my coins and all in all the scripts are machine readable so I can use my my scripts in third-party tools to reason about them but also in tools that merkleize my scripts that you know, I can use them in zero knowledge proofs and all these kinds of things so that’s great also for the future.
Simplicity
So what am I talking about today? I’m talking about Simplicity which is a new blockchain language and it has all these benefits that I just talked about. It is structured. What it brings to the table is, it has arbitrary computation and I will talk about what that means and it’s formally verifiable in a stronger sense than Miniscript so that’s exciting. Let’s let’s dig in. So what do I mean by arbitrary computation which seems a bit opaque? One way to put it is if, I can compute every finitary function, which is a function from n bits to M bits and maybe you have some idea what this might mean but maybe this is still kind of very theoretical. Maybe you don’t understand what this means. So another try. Every function eventually halts so with Simplicity I cannot write a Turing machine that will loop forever, I cannot write any infinite loops. We don’t want that, right? It’s, this will be an anti-feature. I want to have a finitary function. But still What does that even mean? I don’t know. Third try, every function that you care about and even though this doesn’t really help in a way it at least reveals a goal that we have a Simplicity. We want to enable every function that you might want to have on the on the blockchain which does not DDoS the blockchain, which does not have infinite loops. All of these things you can do with Simplicity. You might not know what this means but I will go into three concrete cases that are enabled with Simplicity that we cannot do right now.
Computation Model
So, well, first the computation model, so because Simplicity seems complicated. It’s actually not. It’s actually simple as the name implies So we have a witness when we spend the script the program. We call it a program. There were some signatures and pre images. We have the transaction which contains the log time sequence and all the transaction data and the Simplicity program tells you spent are not spent. That’s what it does. There is no state. There’s nothing of that sort going on The programs always terminate and there is no expensive introspection so we do not need expensive index structures, anything of that sort so they’re actually fast to execute even though there they are so powerful.
Universal Sighashes
One concrete thing we can do is universal sighashes which are pretty cool. We wrote a blog post about it a while ago So maybe you know the sig hash modes when I have a signature in Bitcoin I sign certain parts of the transaction and I commit to these parts we say. And this means if I change these parts the signature becomes invalid because I committed them. But on the other hand, if I change the other parts that didn’t sign, that’s fine. The transaction is still valid and this is really important for lightning and other schemes so the uncommitted paths are malleable and in Bitcoin script we have like six modes we can use. But six is not, that’s not a lot we can we can do much better and we can do much more with Simplicity. So one thing we can do, we can, we can write basically a Simplicity program that influences the hash. One thing we can do is, we can have a conditional that says I sign that the time lock is greater than a threshold. We cannot do that right now with Bitcoin script. I can sign a ratio so I can say I don’t care about the amounts, say if we have an asset like on Liquid, I don’t, I don’t care about how many units of the asset I have and how much I spent, how much I spend for this. I only care about the ratio which is the price. So I only want to buy this asset for this much but you can malleate it, you can change how much I buy because I just want to buy for this price. I don’t care how many units you give me. I can sign a covenant, so that’s pretty cool. I can sign that the covenant is being upheld. This I sign and all of, many of, these things rely on delegation aspects so I can actually plug in the sighash mode I want to use at signing time and you can also restrict which parts you can plug in and which you don’t allow to be plugged in and what we can do is we can say in the sighash mode I don’t actually sign at all I just give my keys to another party. I can control which party that is and then they can spend so I can transform a sighash for a signature for my key to a signature from to someone else’s key, which is pretty cool. And this is much much more powerful than any old hash function because we can compute the hash at spending time.
ZKP Verifier
Something else is ZKP. Very popular these days and the problem with ZKP is we need a softfork usually. With Simplicity because we can compute any function which in any find every function which includes ZKP verifiers We can build this in Simplicity without a softfork, we can try it out and in the previous talk we had confidential transactions for privacy so they use something called bulletproofs to hide the amounts and this uses the zero-knowledge property of bulletproofs and zero-knowledge proofs. And we can do roll-ups with Simplicity so we can implement a snark and use the succintness property, which means that we can compress the computation and make the proof very short, logarithmically long, and make the verification time very short, also logarithmic, which is great for scaling. We can write all of this in Simplicity and try it out.
Custom Crypto
And in general we can do also custom crypto so if you want you can implement Pairing, you can implement a different curve and do BLS signatures. We can do SHA3 if you want. You can implement that We actually implemented SHA2 to in Simplicity so that’s possible we can do SHA3 we can do identity based encryption, which not many people know about these days, but it’s pretty cool and infinitely many more things so it’s all about trying out new things without needing a soft fork. These things might be expensive but you can still try them out on your local machine And if the community is excited they can decide to speed this up and I will talk about what this means.
Common Misconceptions
Expressiveness: Simplicity vs Bitcoin Script
I want to talk a little bit about common misconceptions. So one thing you might think is Bitcoin script was already sufficiently expressive. Because someone managed to convince me that Bitcoin script can do much more than people might think using very impractical ways to use the script and using bit strings. So I, I’m pretty convinced you can compute everything that Simplicity can compute. But the problem is these constructions are like I said impractical. They’re huge because Bitcoin Script is not meant to have arbitrary computation whereas Simplicity is. So Simplicity is much more elegant, much shorter. It’s meant to have arbitrary computation. Bitcoin script on the other hand is not. So this is technically true, but actually it’s not.
Structure: Simplicity vs Miniscript
I want to talk a little about the structure because Simplicity is new but it’s still very similar to Miniscript actually. So we have a tree structure and they use the so-called combinators and they’re like puzzle pieces you put together in a tree kind of way, in a recursive kind of way, you can see that these combinators take a different number of arguments, so we have ones that take no arguments, these take one argument, and these take two arguments. You just plug them in like in Scratch and this is your program and all of these have a meaning that I will not talk about. So, and it’s no coincidence that this looks very similar to the BDK playground where I took this from because, like I said, Miniscript is very similar. It has a tree structure like Simplicity. The only difference maybe is that here these puzzle pieces have a more high level meaning whereas in Simplicity, Simplicity is more like a, more like an assembly like language so it’s much more low level. The puzzle pieces do very specific things where these ones do high level things.
Example Simplicity Code
I want to show you very quickly some simplicity program so you can go home and say you saw some some Simplicity today. I will not go into like the details because there’s no time for that, but this is a key lock. So you can see you have a public key of some sighash. You have a signature which is in witness data and you have some schnorr verification in some kind of tree structure. You can do a hash lock so there is some hard-coded image that is your target. You have the witness data, which is a preimage, some hashing, and some equality check. And you can do a time lock so you have some threshold, you have the lock time that is read from the transaction, and you check if for less equal. So Simplicity programs are tree shaped you can represent all functions, determinate or find every functions, and we call this core Simplicity. So core Simplicity is all the programs that we can represent using the combinators and we prove that this is complete so we can actually represent all these functions that I claim we can represent. But obvious downside is some of these programs are large, especially things like a schnorr verification. We wrote this in Simplicity. It’s rather large. So we need some shortcuts and we call them jets. So for some of these programs that compute useful things we decide, I care about this or the community decides I care about this, put this into a jet. I make it a jet. Speed this up. I write some C code that speeds us up. I define a jet and this is a subset therefore of core Simplicity and what this also means is that suddenly I have this design space for a new opcode. So, because simplicity can compute everything we might want on Bitcoin eventually we already know, in a way, all possible opcodes that we could ever invent and what this means is, if we ever, if we merge Simplicity or if we think in terms of Simplicity a new opcode is a new Jet and it’s part of, it’s somewhere in this core bubble. We have a way of talking about a new opcode in a structured way and we can also verify that the opcode does what it was intended to do and I will talk about that shortly.
Consensus Limits
Another misconception, Simplicity cannot be almighty because of consensus limits. Of course, so even though we can do all functions, we can compute all functions, actually some functions take a long time to compute and we do not want to DDoS the blockchain so there are consensus limits, but this is true a bit for Bitcoin script too. And the solution I just outlined, so everything we care about that, we want to be want to be fast, we create a jet for it which will speed things up, so this is not a problem.
Formal Verification
Formal verification. A scary word I know. I want to talk a little bit about that. So this picture is maybe helpful. So on the left hand side we have the Simplicity stack, on the right hand side we have this Miniscript stack and we have a Simplicity program which has some formal semantics. So we actually know what this means in a mathematical sense. And this is executed on the Simplicity runtime, which again has a formal representation so we know what it is and we have some jets which are written in C code and we actually write this in verifiable C, which is a subset of C, and this also has mathematical semantics. And all of this is executed on the verified C compiler, which is proven to be correct so we have some guarantees for the binary as well, which is important, right? We don’t just prove mathematical theories on paper they actually hold for the binary as well. This is much more solid than Miniscript, which itself, it has a formal semantics and it’s great but we really had to fight to get this whereas on, underneath it, it’s much less formal. We have the Bitcoin script which arguably is formal in a way it has some C code. It’s based on the C++ standard which has a definition, but it was never meant for formal analysis and it has some really funky semantics which might surprise people. It’s very hard to do. It’s how very hard to verify things with Bitcoin script.
What Simplicity Enables
Let’s talk about things we can do with Simplicity now that we cannot do maybe with Miniscript because we can prove more things with Simplicity. I made some, some figures to illustrate this.
Correct Subroutines
So one of the applications is subroutines we have, I talked about how we can write all these funky math gadgets like a SHA3, a ZKP verify, those are complicated programs. How do I actually know that they’re correct and especially, and this is even more problematic when these programs become really large and nest them and there’s programs and programs, I need to keep an overview of things. So I need, I need to know that the math gadgets produce correct outputs and what what I do? I write a formal specification, this can be an exact spec on another language, and this specification has some formal representation, which is this funky Spiral or whatever the shape is called. There’s a mathematical object and I have some Simplicity program. So this could be the SHA3 program, something I write, and because it’s Simplicity we have a way of putting this into the mathematical realm, which is this other spiral. And what I can do is, I can use a proof assistant and show that these are the same. And maybe they don’t look the same but when I look at first glance but when I do the math they turn out to be the same and then I can be sure that the program implements a spec so that I verify the program. Which is great and we should do this much more when so much money is involved.
Specified and Verified Opcodes
Something else is opcodes, so, and this, Jonas Nick talked about this at TABConf, about provably bug-free BIPs, which is really cool. So when you read BIPs you often, that specify a new opcode, you read something like this opcode fails if any of these things are satisfied or it does nothing otherwise. And this is an informal specification. And if you look at the Taproot BIPs they have some pseudocode, maybe some Python code, that helps. This is also an informal specification. We can do better than that so we can write things formally like an exact spec and the BIP for half aggregation is written in exact spec I hear, which is cool. And what this means is the spec has again some mathematical formal structure that we can extract so we can clearly communicate what we actually mean. There is no ambiguity in our words because math doesn’t allow that which is what why we do this in the first place. And we can also execute some unit tests on on the spec and verify it and what this means is, in the case of Simplicity, an opcode is a jet. It’s some jet C code and we write this in verifiable C, which again has some, we have a way to extract the mathematical object. So the function that this code computes and again, we can prove that the jet implements the spec or it, yeah, it implements the spec by proving that these representations are the same. The spec and the implementation have the same mathematical representation and this will make our opcodes much more fault resistant. In theory bug free, but this is obviously difficult. The spec has limits, but it’s, even just writing the spec, not just, even if we skip the step, writing this spec will be a huge improvement. And Simplicity enables that and also enables us to verify the opcodes if we wish to verify them. And you can do much, much more than that but I will limit myself to these examples.
Script Verification
In a way Bitcoin Script was already verifiable. We can do manual audits. We can go line by line and check this this code does what I, what I want it to do. We can keep track of the state of the contract and we did this in a way in the Miniscript talk to find out why the scripts are wrong. But this is kind of tedious and it was never really meant to be done this way. With Simplicity we try to make it easier to verify and we will also try to build, to give you some building blocks, some ready programs that already have a lot of theorems, a lot of guarantees that go along with them and you can combine them in this plug and play fashion to write larger programs that are correct. That you can prove relative easily to be correct. So you have this verification toolkit, which we try, Simplicity is meant to be verified whereas Bitcoin Script can be verified but it’s not explicitly designed to be verified.
From Miniscript to Simplicity
We go beyond Miniscript, so let’s talk about how we can actually map Miniscript into Simplicity because they are so similar that we can do this very easily.
Recursive Conversion
They’re both tree structures and so what we can do is, we can do a recursive conversion. We can convert the nodes so a signature becomes a signature pre image becomes a pre image and so on and then recursively we map all the, all these children. So in the end a Miniscript tree becomes a Simplicity tree using this recursive conversion. And we can always look at the Simplicity program and say oh this came from this Miniscript source. So it’s not, it’s not nearly as complicated as the Miniscript compiler. It’s much much more straightforward It’s by ejection as far as I know and we are working on a tool that lets you do that so, it’s, I think we call it the Miniscript Simplicity bridge so you give it a Miniscript hex, a Bitcoin Script hex and it gives you an equivalent Simplicity program and we are also working on other tools that will help you visualize the program, the tree structure, and many other things. So that’s exciting and yeah, stay up to date for an upcoming blog post on that. And This was a semantic side. We can also talk about the, no sorry this was a syntactic side, and we can also have the semantic side.
Semantic Representation
So we have a Miniscript script and thats syntax and it has some meaning. So this is a semantics and we have a Simplicity program and it also has some meaning, it’s meaning is the spending conditions that it implements so when can you spend the coins? When can you not spend the coins? And I talked about how Miniscript is weaker than Simplicity and how we can convert Miniscript to Simplicity. This is this arrow. Well, we can, what we can also do is, the semantics of Miniscript is also weaker than the semantics of Simplicity. The semantics of Simplicity is in a way richer. It’s more complete. It’s a more complete picture so we can embed these semantics into these semantics which, by a process which we call lifting. The exciting thing we can do is we can take a Miniscript, we can take a Simplicity program and we can check that they are equivalent in a way even though they are written in different languages, very different syntax, we can say actually, they implement the same the same checksig or something, the same key lock or the same time lock and many more complicated things too. So that’s cool. And we are also working on that.
Integration into Bitcoin
Very briefly I will talk about how we could put Simplicity, integrate Simplicity, into Bitcoin. This will be a very long process. Of course, this is like five, ten years to the future.
Taproot
But in general, we will implement, we will integrate this into Taproot. So this will be a new Taproot leaf version because you know Taproot has versions. It’s meant to be extendable in the future at some point. Maybe Simplicity will have a tap leaf version number. I just picked any number and you have the tap tree which is used for the script path spent and you have a lot of leaves and many of them in this case have like the old, so they’re standard Taproot leaves, and they have some Bitcoin Script or some Bitcoin Script that is actually Miniscript. But you could also have a new leaf which has version c2 in this case and this means it’s a Simplicity leaf and this means this binary, these bytes are actually a Simplicity program. So when, when we spend this, we use the Simplicity deserializer to deserialize and we use a Simplicity runtime to run this. But this will coexist. Simplicity will coexist with Bitcoin script and Miniscript inside these tap trees.
Liquid Network
This is what we are targeting and currently, we’re working on Liquid. So we have the Simplicity branch for Elements. We’re working with the Elements team to integrate Simplicity into Liquid even though we know what we’re doing even though we put in the hours and make sure and we actually prove many of the things we claim we know. There’s theory and there’s practice so we must test this, test these features on the sidechain. Get some feedback, learn. We’re currently working on on the jets. Try to see how long the jets take and assign some weights. So this will be the next big step in Simplicity.
Conclusion
To conclude I talked about structured programs, the previous talk talked about structured programs, I talk about structured programs. So structure programs are good programs. Simplicity is a successor of Miniscript in many ways, in what it tries to achieve and in the way that it looks. It’s a tree structure. It gives has all the benefits of structure. But it goes beyond that So we have much more functionality. we can compute many more functions than that. We have verifiability so we can prove, we can do whatever what we might want to do and we can also prove whatever we might want to prove. So let’s hope this will lead to maximum adoption. It’s up to you. It’s certainly exciting. It’s a very exciting proposal and I hope that more people will be interested in this and I hope that more people can get to know this in the future. The next step is the Liquid integration. So I talked about, can you, I talk about a new blockchain language. So this is scary. Maybe to some of you this seemed like Pandora’s box. It will destroy Bitcoin and I hope I could convince you of the opposite. I hope I can convince you that even though it is powerful, first of all, we need this power. So Bitcoin needs to be future proof even though this will be a slow and very careful process but at the same time we can verify that our programs are correct given that power and we have consensus limits so we do not have any DDoS. So this will not destroy Bitcoin, but it will help Bitcoin. So, thank you.