Filecoin Filecoin Orbit, 23 Oct 2021

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: Exploring New Proving Systems

Description

Filecoin's cryptographic proofs currently use the Groth16 proving system, we are exploring new proof systems which would allow us to add new proof types without the need for a labor intensive trusted-setup as well as reduce the storage footprint of the proofs published by Filecoin storage providers. Our goal is to achieve these without sacrificing proving or verification time.

A

Hello, um my name is jake. I am a software developer software engineer at filecoin. I work on primarily on the cryptographic proofs and like the file coin proofs um that you may uh know about, um but today I'm going to be talking about what cryptographic proofs are, how they're used in filecoin uh some of the scaling limitations.

A

We've come across with the current proofs and potential solutions, and, namely the halo 2 proving system which is currently being developed by the electronic coin, like ecc and um in collaboration with us, and the ethereum foundation uh meant to try to get into a like a production, ready state where it can be deployed on like file coin and maybe with ethereum and zcash.

A

um So then what are cryptographic proofs? uh They are not what you would typically consider to be like a traditional mathematical proof um like, for example, like there will be a proof statement, a thing that you're proving and then you'll follow like a logical sequence of lines that, like have to be logically consistent with each other.

A

Until you get to a proof of the statement- um and that's not exactly what a cryptographic proof is, um but with these traditional proofs are they're secure like because they're logically consistent, there's no randomization in it like meaning they're, deterministic, um they're, non-interactive, so they're, just like static proofs that you just read, anyone can read, they involve no interaction and you just follow line by line, um but sometimes those can be cognitively complex.

A

There could be like a lot of a lot of um logic in each statement, basically and they're not super efficient and they're, more written linguistically for humans and not computers.

A

um That's not what a cryptographic proof is um a cryptographic proof or a cryptographic proof system, or just a proof system that I'll call there are protocols that will allow computation to be outsourced to someone else.

A

So if there's like some computation, just like some function with inputs and outputs, um a verifying party can say: okay, so I'm proving we want some proving party to run the function on this set of chosen inputs and then the prover has to uh prove that they run the computation correctly and they give you an output um and these cryptographic protocols they allow for provable computation and a very interesting thing about these cryptographic.

A

Proof systems is that you can verify proofs from them faster than actually doing the computation yourself, partly why that is that they're probabilistic, meaning that the verifier has access to some randomness which they can exploit to um for fast uh verification, but that also introduces a small probability of very small probability that false proofs will pass verification. uh This is one of the main differences with like a traditional mathematical proof is um traditional mathematical proofs.

A

They they're they're static, they're, deterministic, meaning that like, if you follow line by line, you will always get to whether the proof is true or false um cryptographic, proofs, uh they're probabilistic. So there is a small chance that uh verification doesn't hurt that false proofs verify.

A

um Partly how this is done is that, like all of the logical, consistencies or logical lines, that would be in a mathematical proof, they're just all compressed into like a single arithmetic or algebraic statements, or just like function, equality, sometimes or polynomial, or something, and then the verifier checks or like asserts that some condition on that algebraic statement is true generally using some source of randomness and um like an equality, will hold with some probability.

A

If the statement is true, um another part of what makes cryptographic proofs a little bit different than traditional proofs is that they're written for satisfaction problems rather than evaluation problems by evaluation problem. I would mean, given some inputs, follow these exact steps to compute the output, we're actually evaluating the function line by line a satisfaction problem is more along the lines of um given some function.

A

Given some inputs, I know I, the prover who's proving, like some computation, know some set of values that I could only know if I performed the computation correctly, um that set of values is they're private to the approver and they're called the witness.

A

um So for, like example, if um you have some value a maybe some input a and you want to prove that you know like it's multiplicative inverse like um you, would the prover would like witness some value w and show that a times w is equal to one, um instead of actually going through all the the arithmetic steps to compute the inverse of an integer, which would be an evaluation problem, um and you get the benefit that a lot of arithmetic computations are easier to verify than to actually compute themselves.

A

So, for example, like verifying a multiplicative inverse takes one multiplication, because you take some value, a some value b, you check if they they're they multiply together to get one, um that's a lot easier than actually computing a multiplicative inverse of an integer um and they have a property or satisfiability problem evaluation problems can always be transformed into like a corresponding satisfiability problem.

A

um So these cryptographic proofs they're not actually like evaluating things like line by line, as you maybe would see in like a computer program or something they uh there are these satisfiability problems where you show you know all the values to make the computation true.

A

um So kind of this is a high level diagram proofs for general computation uh cryptographic proofs. They can be computation specific or they can be for general computations, which um generally is any arithmetic computation, but there can be more operations um and generally how they work out, um and maybe it's not for every proof system as clearly delineated as this diagram. But you start with some general computation, like whatever that could be like computing, a hash function or you know inverting an integer or whatever arithmetic program.

A

You want like no saying that, like maybe I know the roots of some polynomial, um we start with some general computation f and then you transform it into an intermediary uh representation, which is interpretable by the proof system and usually a proof system will say, like okay, we're going to work in like this sort of hardware model, um because it's not like a compute like a computer, already has its hardware model, but like the proof system, in order to interpret computation, it has to have like its own model of how hardware works and usually that's like a set of instructions.

A

um For many, like arithmetic computations, the hardware model is, uh you have addition and multiplication are your arithmetic operations. Then you have like your integer type and uh those can be basically fed into each other inputs and outputs to um instructions, and that would be kind of like the hardware model um and then uh once you've kind of modeled. Your computation, using like this hardware like uh integers and additional multiplication or whatever else um you want to write your computation as a satisfiability problem, which is okay uh to do this computation.

A

Someone doing it correctly would have to know some subset of values throughout the computation, um as it runs um that would kind of be like if a program's running, maybe the person who runs it correctly, would always know like what certain registers in your processor would hold.

A

What certain values and processor would be um it'd kind of, be like that, um and then once you have a satisfiability problem and it's using like operations and integers or whatever type of numbers the proof system wants you to use, then you convert it into some sort of algebraic statement or algebraic form. um Here, for example, I have like a matrix times a vector, then a product of that with a matrix times a vector, and then you assert that that's equal to some other matrix times a vector w.

A

um That would be like one sort of algebraic form that you can put these in like matrix, vector multiplication, and then you assert some equality. Sometimes it has to do with polynomials, um but there's some algebraic form that these proof systems can that a certain proof system will operate on um and then the proof system itself it defines like how do you use this algebraic form to like prove and verify uh proofs, and then also cryptography is used to enforce that the prover has actually behaved and done the protocol correctly.

A

uh In reality, the proof system kind of sets some of these things. Sometimes it doesn't it's not just as clear-cut as the proof system gives you a proven verify function like sometimes it may say exactly what kind of satisfiability problems are allowed. What the hardware model is, um and usually it sets like what the algebraic statements are, that it ultimately will work on.

A

um So uh there are many different types of cryptographic: proof systems and one of the most common are called snarks and that stands for succinct, non-interactive arguments of knowledge. Succinct means you have fast verification. Non-Interactive means that the prover and verifier don't have to interact. The prover just can send the verifier a single message, the proof or just publish it publicly, and anyone can verify it or the verifier can verify it.

A

um Arguments of knowledgeable argument means that uh the proof system or the proof itself uh is secure against a cheating proverb unless, when the prover is computationally bounded like in modern cryptography, uh most cryptographic techniques are secure when you assume, like the there's, some bound on the provers or the cheaters, computational ability or resources on these an argument means the same thing. It's a proof system, that's sound.

A

Unless the prover has some like extraordinary, basically impossible, computational power or resources, then if knowledge means um you're proving a satisfiability problem, it means that the approver knows some secret values or some values that they could only know if they ran the computation correctly.

A

um So these snarks, these cryptographic proofs they can enable decentralized storage, which is what filecoin is falcoin, is a decentralized verifiable storage network, meaning like anyone, can join to be a storage provider um and they offer a service of storage, and they have to prove that they have the resources to offer the service and they have to prove that they're, storing people's files, um and they have to prove that they've, like maintained people's files.

A

And there's also a public ledger which basically keeps the state of the network. It says, like what uh storage providers are currently providing, what storage to what clients and how much resources that they they have available, um but what's nice about snarks and why there can be used in filecoin is that snarks have small proofs and efficient verification, uh non-interactive proofs, meaning like the verifier improver, don't have to communicate, which is really useful in a like public ledger type system and um the verifier improver.

A

They don't have much additional overhead because of these proof, systems like the prover celeste do like the computation that they're proving, but um the proof system doesn't add much onto that and uh fast verification uh yeah. It just helps for people who are verifying the the proofs that are generated by storage providers.

A

uh This meme, uh it shows trach, on the left hand, side saying uh in a decentralized system. I don't want people like living in the data center basement, uh maintaining like a state of the network like we don't necessarily want. We want maybe to automate these processes.

A

um If you have like storage providers constantly coming on and offline, um it would be kind of a pain to have like someone living in the basement of everyone's data center, uh like ensuring that there's like a certain amount of storage available, and uh it would just be hard to do that in human space.

A

But you can use snarks to automate a lot of that process and that's a lot of what filecoin has done figuring out how to use snarks to automate these uh processes.

A

um So drake is saying yes, snarks know some guy living in the basement of your data center monitoring your resources, um but there are many snark systems. um There's I mean really. Over the past decade, there has been what many people call an explosion of snarks.

A

Improving systems um like some of the most common ones are like pinocchio was like an original that really laid the groundwork for a lot of these um grot 16 is a very popular one today, because it has succinctness and fast verification and low prover overhead um there's just a lot and they keep more and more developed every single day, um but some of the properties that you might at least have filecoin looked at and that you would look at if you were trying to choose.

A

One of these proving systems is like proof, size, verification time which usually are highly correlated um does the prove system add like require a lot of resources from the prover. On top of the computation that they're proving uh what sort of like mathematical operations does the proof system require improving verifying, um because some mathematical operations are really expensive.

A

So, even if there's a small number of of these operations that could still be really really expensive, um and that would be like something like ffts, which would like multiply, polynomials or you just basically use for multiplication, um but also certain like elliptic curve operations are really expensive. um So you basically have to weigh out the cost of like those the types of operations you're doing and the numbers of them would factor into your own.

A

Your overheads on the proven verifier side, um but also you can look at potential optimizations for those operations, which is something that falcon engineers have done a lot of like. How do you optimize these proof systems um beyond like in practice? uh Many cryptographic, proof systems and snarks? Specifically, they have some setup procedure.

A

Sometimes the setups are specific to the computation being proven. Sometimes there's one set up for all computations that will be approved.

A

Sometimes you can have just like you, can keep updating the setup as you go like, maybe to insured security or to add on to it um or then there are transparent, snarks which are relatively new, but they don't require the setup procedure um in certain ways they may be less efficient than current snarks, but um but yeah I'll get to that a little bit.

A

But they are very interesting and they don't require this like big, costly setup procedure, which is usually called trusted, setup um yeah and it allows you more uh flexibility in what kind of things you're gonna be proving, because maybe you don't have to do a setup for every single like proof that you're doing and sometimes, if you're doing a computation, specific proof or like you have your proof system is computation specific or um you.

A

You may be limited by the size of computations that you're allowed to prove because like if you have run trusted setup for whatever like uh proofs with like a hundred multiplications and then you come say, I want to actually prove something with like 200 multiplications. Well, you can't do it. You have to do another one of these very costly setup procedures, so that's where transparent snark systems would be really helpful.

A

um Then, when you're choosing a snark uh or cryptographic proof system, you want to think about its hardware model or how it internally or how you represent just a general computation using like the operations uh that the proof system like allows you. uh So, for example, like I guess, if you have a computation, that's using, like maybe bits like if you were doing like a shaw, hash or something, and you want to prove something about that, but your proof system it uses like integers and doesn't have like bitwise operations or binary operations or boolean logic.

A

Well, the transition from bits to integers and like arithmetic operations, improve systems hardware model- uh you may get a big blow up and it may not be the right, snark or proof system for you um also. You might want to consider what is the aggregate ability I'll talk more about this later with proof systems, but it basically allows you to um to batch together proofs.

A

Maybe you can prove multiple proofs in a single one or in a single proof, or maybe you can verify in batches um and then I guess, existing developer tooling is also really important around the snarks, um like there's only a handful of these that have actually been done in practice and have like support from like communities or companies and um they're pretty complicated.

A

So having like a community with like programming, language support and like libraries uh that are usable is also a big factor in like choosing a snark, because it'd be it's a lot of work to uh try to create a library that does all of the things necessary from scratch um and filecoin chose to use the grot16 proving system, which is one of the most popular snarks right now, and it's it's popular because it has small proofs, which means very fast verification and loop, low prover overhead, and um he has a lot of developer tooling.

A

A lot of people use it. um I think I'm running low on time, but the way filocoin proves is uh it's. A decentralized storage network is basically have a client that says I need file, storage, a approver or storage data center person says I'll, store your file, and then they have to prove that there's the approver has to prove that they're storing the file, then the client says like it needs some proof that they will that the file has been maintained uh on in the data center.

A

Those are called pull rep proof that, like a file, has been stored and proof of space time proof that the file has been stored over time.

A

um Filecoin's been producing many proofs, I'm not going to go through all these metrics, but um we create a lot of proofs is essentially the uh the big takeaway um limitations of the current snark system in falcon is that there are a large number of proofs and that creates a bottleneck, because every proof has to be validated before it's included in the public ledger and that's a bottleneck on the network and like growth and onboarding storage, because it takes a little bit of time to verify these and if you're creating a ton of proofs, then it may take too long like it will slow how fast things can be included in the public ledger.

A

Also, you have these per statement trusted setups with grad 16, and that limits you to what computations you can do in size of computations.

A

um So the solution that I am most familiar with, that we've been working with and we've been working with, the like ethereum foundation and ecc zcash developers is um the halo, 2 proof system.

A

uh We've have many solutions to like some of the like some of these snark scaling issues, um but halo 2 is the one that I've really been looking at and it's a new proof system, not grout 16, but it has a transparent setup, which means that you don't have a trusted setup or setup. So you can prove any statement that you want. um You can prove like anything.

A

You want you're, not restricted to like one or two things that you're proving without a trusted setup uh and you get what's called proof recursion, and this is going to factor really highly into the potential scaling solutions in the future, um at least for snarks, and it means that you can create proofs that verify other proofs that have been proven.

A

So if um so, you could create one proof that maybe verifies like a thousand other proofs and then just post, that to the public ledger and um it essentially kind of makes a tree structure to my understanding of the so far. uh Zcash is currently like implementing this and getting it down, but there are papers and stuff about it. um Halo 2 also has weaker security assumptions, meaning it doesn't assume as much as like our current proving systems like route 16 like it has um yeah, it assumes less about the environment.

A

Usually that means there's more security or you they're a little bit more realistic. Maybe if you have weaker security assumptions and um you get some new arithmetic operations, you can do like within the hardware model of the proof system um like, namely you have like lookup tables like you can basically do like dictionary lookups or like hash map lookups, which is pretty cool, and that's not something that I know of in other snarks, um and you have other arithmetic operations like you can do.

A

You can define like your own arithmetic operations for computing, specific polynomials, which is interesting um but yeah, and the main thing that we're really interested in is this proof recursion, where you can offload uh storage of, like maybe thousands, maybe unlimited number of proofs to into a single proof via proofs that verify other proofs.

A

um This is currently in developments and yeah working with ecc and the ethereum foundation on it. um Yeah zcash has done a lot of work. They have papers on it, they are leading the developments of the libraries in rust, but everyone is really excited to get it fully developed and production ready and deployed, possibly in in various public ledger type systems.

A

um uh Yeah. That's that's it for me.

A