2022-04-22
bip119 CTV workshop
previous workshop:
# Introduction
I'll give a menu of options for what to cover. We could do a more architectural review of Sapio. We have some content on what miniscript is, as well. Then, we have a rust programming guide. We also have a tutorial for getting setup with sapio. I was thinking we'd end with the tutorial on getting setup unless anyone feels strongly that they want to play around in Sapio sooner.
All of the slides are in the company folder at the end the last slide has a link tree of sorts... Buck is going to rename all of those to the appropriate name so that it's less confusing which one to click on, thank you for your service Buck.
We're going to start with as I said someone wanted an overview of Sapio so we will talk about the architecture of Sapio under the hood a little bit and this theoretical calculus of covenants thing. Then we will go into what's actually ACTV in this context. Following that, we will do some content on what miniscript is and how you can use that and we will play around with that a little bit. Lastly we will do a primer on... who here has done any rust programming ever? Some people have played around with it. We're going to do a little bit of a primer that is just building some intuition for rust and avoid common pitfall. That should hopefully help when you're looking at some of these samples of code about how to get the compiler to stop fighting you. Then we will dwelve into setting up sapio, and hopefully people will be able to attempt a small challenge that I setup but we might run out of town.
# Sapio architecture
What is Sapio? It's just like Solidity... not really. It's kind of similar. It's a high level language for writing smart contracts. It has some nice tooling and you can do a lot, but it's not targeting EVM, it's targeting bitcoin. The bitcoin VM is this concept that I made up but actually Satoshi made it up. There's no strong formal model for what this bitcoin VM is, it's just that there are transactions, there are scripts. But maybe we can think about this in a new theoretical way and it will yield better mental models to think about smart contracts.
A common misconception is that Sapio is uniquely for CTV. This is a misunderstanding because Sapio is really trying to target any arbitrary transaction graph. If you can target an arbitrary transaction graph, then you can target any type of covenant. Inside of Sapio, because OP\_CHECKTEMPLATEVERIFY is a concrete defined thing... we can add support for what other covenants do into the Sapio framework if there were others. If people on Liquid wanted to make Liquid to be Sapio-compatible, then it's possible.
Q: When you say concrete and well-defined, are you referring to anything in particular like characteristics of smart contract?
A: Well, there is code for it, and the code has been tested pretty thoroughly and there are tools that you can use to work with it in terms of miniscript and other things. It's not just like here's an opcode, figure out how to use it. It's kind of well formed, and we will talk about the theoretical properties over the next two presentations.
Lightning can be thought of as a smart contract... or multisig smart contracts. If we had ANYPREVOUT, you could implement eltoo inside of Sapio. We don't have ANYPREVOUT, so it doesn't exist actually, but Sapio has one of the anyprevout like eltoo-like lightning implementations because you can model that kind of state transition system. It's kind of cool, I might not use it in production but it exists.
It's not quite a standard, but it's a standard for making bitcoin transaction flows. One day maybe Sapio will become mature and there will be a standards body around it so that I don't get to rugpull people when I get a crazy new idea, but instead something that users can rely on the formal semantics on how these things should work and maybe we'd get more tooling around it or other metadata protocols and things like that.
There's a lot of stuff that I showed you today. Here's the architecture diagram. Say you have a Sapio Application like a vault or a NFT. It's a compiled module that you can interact with and see it. Then underneath that there's Sapio-studio react GUI frontend, and then Sapio-studio electron which is the backend code for running the application itself. The electron application is using command line tools called Sapio CLI. It also uses bitcoind. Any flow that you're doing or might want to automate one day, it's not like there's some special magical thing happening in some mess of javascript and typescript. It's mostly just shelling out to a command line interface and you can reimplement using that, maybe with relative ease. It's still slightly difficult, but it's doable, if you have a separate tool managing it.
Then there's the sapio language itself which is a big block of complex topics like compiler logic, and it's built on top of rust-bitcoin which is one of the main ecosystem libraries, and it includes things like rust-miniscript. Then there's wasmer, which is a webassembly runtime in rust. wasmer uses llvm for running webassembly but I don't really fully understand that. I don't know how crane lift works. In theory it's deterministic-ish. After that, you have the turtles that all of this is based on anyway. Does anyone have any questions about this architecture diagram overall?
sapio-react is not a library, it's more of an application with a graphical user interface. There's a lot of things it handles in terms of like being able to click on things and generate state transitions, all of this can happen in a backend context. It just happens to be doing the things you need it to do, in an interactive form.
Is anyone more confused now?
# How do I use sapio?
At the end of the day, what you need to know is that you write smart contracts in a rust-based language for smart contracts called Sapio. Tensorflow is a little bit of a language itself, and then it compiles a neural network for you, but tensorflow itself is not that neural network. Sapio is like that; it's a library ultimately, but it's a language for describing flows of bitcoin. When you write a sapio program it's really making itself a little compiler that you can then pass a language in, and a language is a set of arguments, into it and it will generate an actual concrete program for you. The sapio module that you're running is not the actual transactions; the transactions are the compiled output. Sapio is the thing that compiles and generates those transactions. Those modules that you compile are compiled into webassembly, that's probably something where I could do some improvement. Some people are working on specs for very very deterministic webassembly because webassembly has a few holes about how it is setup, floating points are unspecified but it is defined or something so you can get some weird things... but generally webassembly is deterministic, if you run a contract once, you will get the same result next time. You can ask it questions like, what type are you? It will return json and you can use json-schema to figure out hwat types can you send into it, and so on. It's a self-describing webassembly model. Then you load the module into Sapio Studio, and then you can use it. You can play around with the transactions, build your contract, save to disk, you could have a covenant or a vault or whatever you're using. That's the user story at the end of the day.
# Mutable transaction graph
It generates a mutable transaction graph. What is a mutable transaction graph? Let's start with the idea of a contract called "pay my friends". In PMF, Alice wants to pay Bob and Carol the same amount and then put the change back into the contract. So Say there's a contract PayMyFrenz, the first step would be to generate a transaction graph that does that. Sapio allows us to finish a computation and then later pick-up where we left off, and resume that computation. In this example, Alice is paying an amount to Bob and to Carol, and the rest to the same contract PayMyFrenz. So we could apply that recursively, and Sapio is a toolkit for being able to deterministically re-generate -- this is like an effect type system where you can inject and resume transactions in this graph of things. You can generate the same graph, and you could continue....
Sapio supports CTV as a first-class citizen. It can support other things, as well. In particular, the emulation of CTV would work for ... I think there might be some issues with re-compilation but those signatures that the oracle is supposed to serve is deterministic, and you could cache them once you generate them. When you see these continuations, you left the purview of emulating CTV and now you're doing something else. CTV is just one of the things; emulating CTV is one of the facets of how CTV works. Covenants are just like a construct of something that can be enforced as a restriction on transfers, which also encapsulates things like multisig.
# What enforces the contract?
It could be CTV, but it could be multisig or even future covenant opcodes. Sapio helps us with tooling infrastructure around it. It could support a bunch of different things... but those things, Sapio is happy to do it, but those things need to be well-formed.
So how we should think about the shape of what is a covenant? I have a post on the bitcoin-dev mailing list that has a better formal treatment of this. This is a high level of what you would need to understand: a "covenanty" smart contract in bitcoin, needs (1) an intent generator that says something like "I want to sell my NFT via this transaction T", and then you have (2) an authorization verifier (something that checks whether the transfer is signed by some key, for example), and then (3) some authorization prover that says the transaction is valid because I generated a signature with the key. Then there's a meta-component: (4) what is the set of all possible conditions and are all these conditions desirable? Have we excluded all undesirable conditions and have we included all the desirable conditions? This can also be thought of in the recursive context as well.
Q: Why do we need that list? What does that list of requirements give us to think about covenants?
A: Basically, this is the set of things... there's a few ways of thinking about it. This is the set of things you would need to have to formally prove properties of a covenant's possible state transitions. If you don't have these things, I'm pretty sure you couldn't prove that a covenant is correct. These also happen to coincide with the things you would need to implement a piece of code for, in order to be able to integrate this into Sapio. There's an impetus match of like, these properties of formally proving it are the same pieces of code you would need to write, or you need to at least prove that the code could be written in a reasonable way, and if you can't then the thing might be difficult to use and maybe shouldn't be done. If you can't prove the entire set of intents that are provable under the verifier you generate, then maybe there are bad state transitions. If you can't generate a verifier, then how will you translate into script? If you can't do a prover, then how will you play these things out? Expressing these things- generally people want to live at the levels of intents and then you want the authorizer and prover to be automatically generated for you, that's the intution you should probably want. You don't want to spend your time writing a verifier or prover. You want to find the set of intents that are valid, automatically derive them, and then have a proof that it is total and that you have full coverage.
# Super simple vault
Say I have a vault V with a UTXO with 10 coins. If I want to move it, then I need to wait for 10 days after I say that I want to move it. If I say my distress word, then my funds get sent to my mom. Who wants this kind of vault? Okay, it looks like some people don't trust their moms with their coins.
Let's map it back to intent. So the tx1 intent is begin to withdraw funds, but allow time for the below transactions. tx send to mom: the intent is to send funds to mom. Tx move after maturity: the intent is to allow any transactions afterwards.
What about authorization? Well on tx1, authorization is done by CTV pre-committed in script. Then tx send-to-mom, then the authorization is done by CTV pre-committed in script. Then the tx maturity at the end is done by timelock plus keysign. It's an open-ended covenant for the tx maturity spend.
The verifier now. For tx1, the verifier just has to match that the txn hash matches. For send-to-mom tx, it's the same, check the txn hash. Then for the maturity movement tx, then it's just check the timelock and check the signature.
So now we have expressed the three facets of the intent, authorizer, and the verifier logic. All covenants look like this when you zoom in. You have some sort of way of generating state transitions that you want, you need to prove the state transition is correct, and you generate a verifier that only accepts the state transitions for you want. If you can't do that, then you don't have a covenant. I don't see how what you're doing would be a covenant if you were missing any prong of these 3 things, or maybe it is a covenant but would not be well-formed.
...
Multisig: it's easy, as long as you define a good federation for the multisignature and if the majority of those are running the same Sapio code then they will be verifying state transitions by seeing that they were constructable through the Sapio code themselves. So we are subverting having any of this happening as a consensus-level authorizer or verifier because we're doing client-side validation. When we jump into consensus, it's easy because Sapio is already doing the intent generator, prover and authorizer, if we were to write our covenant in a way that we were happy with all the state transitions that we were happy with.
# Why not something else other than CTV
Some people don't like CTV. Some people do like it. My challenge for people who don't like it, then extend Sapio to implement and extend your other covenant. Implement it, and then people can use it. It might be a high bar but the reality is that for me to argue in favor of CTV, I built all of Sapio but I am just asking you to build a plugin into Sapio for your opcode- it doesn't need to be all use cases for your opcode, but just at least one thing that it can do in the one well-formed thing and then we can write applications around it. If you can't do that, then probably whatever you're doing is an immature concept because we don't know how to write the three prongs for what you need to do a covenant. If it was usable, then we would know how to write those things. You don't have to use Sapio, but it would be easier to use this kind of tooling.
I think sapio is good because rust is a real programming language, and minx is more of a hobby language and if you were doing some real computation and figure out what your covenants do, it might be harder to do in minx because it doesn't have all the libraries you might expect.
Outside of sapio... an intent generator would be to be something like "I would like to sort this list". An authorizer prover would be "I sorted the list", and the verifier would be "I scanned over the list and checked that all the elements are in order". Those might seem like the same thing, but they are very different things in general. For a transaction in particular, your intent generator could be "I would like to only send to transactions which have every other input be the prime factorization value of like the next one or something like that". Then the authorization verifier would be, "look at them in this order". If you don't know the order, then it's probably not correct, it's probably an NP-hard problem. The verifier just looks in that order. It's three separate properties. The verifier is what goes into bitcoin consensus. The prover goes into your wallet. The intent generator is kind of also in your wallet, but it's the literal transactions that get played. You have to prove that this is what you actually want, prove to yourself.
With pre-signed transactions, don't you need to prove you deleted the key? In the mailing list post, there were 7 characteristics actually. A string of multisig could be viewed as a covenant but it's a little bit more difficult to get the same guarantees. Whether multisig is or isn't a covenant, it's in the category of thing that can be described by the Sapio framework which can also describe covenants. Timelocks are a covenant. It's an additional restriction on how the coins can be spent, beyond just the authorizers. I don't consider just authorizers without explicit instructions on what to do to be a covenant, but maybe it can be modeled as a covenant with no restriction on how it can be spent. Useful covenants are the ones where we can bound the set of outcomes. That's what we know about formal models: there's always things that you can't prove in them, there are things you might want to prove, but also that generally you can prove quite a lot of them but it's a framework for comparing. It's not whether you can describe something in a weird way this way, but rather that you can compare two different things and then compare the properties against them.
What's going on and what is... this is a calculus of covenants. It's a generic idea, it's that book in the sky.. what does this look like for Sapio? Get a rust struct that has Deserialize implemented on it, and probably Serialize, but I think you just formally need Deserialize. Read it from somewhere- you read the data in, and then you have some piece of logic for CTV enforcement or multisig enforcement of the set of intents. You add them to the contract; you bind it to wasm, and then you use it, and then you party. That's all you really need to know in order to do this thing. That's not the full theoretical framework but generally Sapio is not trying to cover all possible covenants. It's just trying to cover the ones that you will probably need to use to do something meaningful, and some other things might be out of scope. But is this solving a real critical business infrastructure thing? If not, then I don't think we should add 10,000 lines of code to support that niche business use case.
```rust
impl Contract for Vault {
declare! {updatable