Proposal: Low budget gadgets (in C)

[elefthei]

I proposed a plan to Sebastian in order to start writing gadgets as soon as possible, since we are behind where we thought we would be at this point. If it makes sense to you I'd like to prioritize this, and it should be quick and extensible.

We should write gadgets in C, not in the compiler, then import them.

Here's how it would work by example. Let's take a function that inverses an int

int inv(int a) {
  if (a != 0) {
     return 1/ a;
  }
}

My suggestion was to leverage a new __GADGET_rewrite() intrinsic to pass the constraints we want as C propositions. Then, the compiler will throw away the AST and plug in the given equation hints.

int inv(int a) {
   int result;
   if (a != 0) {
     result = 1/ a;
  }
  // It will return `result` for the prover and expect it as a witness for the verifier
  return __GADGET_rewrite(result, result * a == 1);
}

The contents of __VERIFY_assert() should be translated to SMT and replace inv(a) in the SMT layer. This is fairly terrible UI but should work, it would be great if we can find ways to make it better for the user.

[elefthei]

@sga001 @kwantam

[kwantam]

Thanks! I will think about this more carefully and give feedback (if any) asap

[alex-ozdemir]

It seems like you want to head in the direction of what I would call user visible gadgets, in which the gadget is written in a high-level language and potentially explicitly invoked.

There is good use for such things, and I want the compiler should support them. The approach that you suggest sort of works, with a few details to patch up related to how this all interacts with variable versioning and witness computation.

BEGIN DIGRESSION One danger to keep in mind when pursuing this approach is that some gadgets shouldn't really be implemented in the C language because either (a) C semantics make expressing them inefficient or impossible or (b) the gadgets are applicable more broadly than just to C, and implementing them in C may artificially bind them to C. In some sense, the inv toy example illustrates both these drawbacks: it should generalize to more than C, and C fails to express the gadget correctly anyway. This gadget really belongs in the SMT-to-R1CS translation pass. Of course, this is just a toy example. There are likely gadgets that do belong in C. END DIGRESSION

At any rate, if you're interested in going in this direction, I think that's fine, and as you observe, it's quite easy to get the compiler to support it, and I'm happy to advise/review PRs.

[mlfbrown]

With Alex. One place to look for perspectives here may be the verification literature (e.g., the argument over inline assertions vs external DSL based approaches). Overall, though, in the very short term (before Nov 20) I don't see an issue with this.

[sga001]

After thinking about this some more, we do not think it is sufficient to handle user-defined gadgets. The reason is that the code needs to be run somewhere.

We think a different architecture is as follows.

We implement an RPC layer where the compiler (in compile + solve mode) can perform RPCs to the external world by perhaps spawning programs in a specific subfolder. Before compiling the code with our R1CS compiler, we use a separate C compiler to build x86 programs that are then placed in the subfolder and take care of receiving requests from R1CS compiler and providing responses (which are then used to assign values to variables during solving).

I think this architecture is morally similar to Pequin's (@kwantam can comment on this). With it, we can support gadgets written as Lef did above, where the C compiler ignores the assert, and the R1CS compiler only cares about the assert when creating constraints. Furthermore, it also supports gadgets that require interacting with the external world, such as accessing a storage server, etc.

This is just a preliminary proposal. The goal was to preserve the sanctity of the existing R1CS compiler so that it never has to know anything about LLVM, x86, and doesn't have to implement some kind of interpreter to run our user-defined code. We would then implement a script that first calls clang and then the R1CS compiler.

We welcome your comments: @mlfbrown, @alex-ozdemir, @kwantam.

[kwantam]

It probably make sense to implement something like pequin's exo_compute() (which I think is what you've described here) as a backstop.

My guess, however, is that this is not the right approach for most cases. For one thing, it's very unwieldy, and seems to be ridiculous overkill for things like multiplicative inverse. For another, depending on how closely we follow exo_compute, it could mean that the programmer has to put the widget into the high-level representation, which really shouldn't be necessary most of the time.

I do agree that we'll probably want some kind of flexible plugin-style infrastructure for specifying widgets, and that infrastructure will probably want to be able to do things like interact with a database (e.g., for things like supplying hash preimages). But the hope is that these will mostly (though maybe not always) look a lot like user-specified optimization passes, with an API that makes writing this kind of thing nice. And if those optimization passes want to do things like call external programs or make remote procedure calls, that's fine, because they'll be written in a full-fledged programming language (Haskell or potentially even a different language via FFI).

I am sure that @mlfbrown has some thoughts on this, since my guess is these passes will bear at least a vague similarity to static checkers.

---

EDIT: by the way, to me the stuff about compiling a C program or whatever is a build system detail. I certainly hope that we won't attempt to reinvent the wheel here, and in any case we definitely should not be hard-coding in things like "compile these C programs, put them in this directory, etc." Yes, that is the way that exo_compute works---and that in itself is probably enough reason to believe that it's a bad idea :)

[sga001]

@mlfbrown: Is there support for such "user-specified optimization passes"? If so, what does it look like. Ideally, the user doesn't have to know Haskell to write a widget, and it can instead be written in some simpler language.

FFI as a way for compiler and widget programs to communicate with each other seems fine.

@elefthei, any thoughts?

[elefthei]

I agree with Sebastian, when I proposed this I had no plan to run x86 code in the prover, in fact I was proposing of throwing the AST body of a gadget away, while using the user-provided assertion for the verifier circuit. But it makes a lot of sense to think about how the prover will run the code now, rather than later.

I was wondering how the existing implementation (“compile & solve”) generates a solution to the R1CS system. Maybe @alex-ozdemir can help.

EDIT: Also, with regards to gadgets = optimization passes Vs gadgets = library functions, I think there’s good reasons to have both eventually, as Alex said in his first comment, and through maybe two completely different pipelines. However, I don’t think “user-defined optimization passes” for both is the way to go. Here’s some counter arguments.

1. Users will need a Haskell API in the compiler which can get very complicated. One such complication is dependencies between gadgets and how to handle them. Configuration as well. LLVM has the most pluggable optimization passes system I’ve seen and it’s still pretty terrible.

2. Who maintains the user defined gadgets DB? Is it through PRs to the compiler repo? Can I have different plugins installed than somebody else?

3. Gadget external dependencies; gadget A depends on MySQL for its FFI, gadget B depends on MongoDB, gadget C depends on BLAS. Does the compiler pull in and link all that stuff?

[kwantam]

Ideally, the user doesn't have to know Haskell to write a widget, and it can instead be written in some simpler language.

Please, let's not complicate things by introducing more programming languages. Once there is support in Haskell, we can add support for other languages via FFI if/when that becomes necessary. I am pretty strongly against making the compiler a mishmash of different languages.

[kwantam]

Quick thoughts on the questions @elefthei asks:

• Users will need a Haskell API in the compiler which can get very complicated. One such complication is dependencies between gadgets and how to handle them. LLVM has the most pluggable optimization passes system I’ve seen and it’s still pretty terrible.

This doesn't seem like a Haskell problem, it seems like an extensibility problem generally. This claim appears to be supported by your LLVM point, for example.

• Who maintains the user defined gadgets DB? Is it through PRs to the compiler repo? Can I have different plugins installed than somebody else?

This seems to be the same question as for any other pluggable infrastructure. exo_compute-style widgets (not gadget, widget) also require carrying around extra code, namely, to implement the external computation.

• Gadget dependencies; DB gadget A depends on MySQL, DB gadget B depends on MongoDB, gadget C depends on BLAS. Does the compiler pull in and link all that stuff?

This seems to be a question about how compilation gets handled, which is certainly something we'll have to consider, but I don't think it really exerts much influence on the design of the API.

With a Haskell API, presumably one can use existing bindings to libraries like the ones you list above. Or Haskell would let you implement an RPC interface like the one discussed above, in which case the binary that is called remotely would presumably link against the requisite library. Or, if we want to get fancy, we could implement, in Haskell, a shim layer that loads a dynamic library (i.e., a .so file) and calls functions that it exposes---and the .so file could then presumably be written in any language.

[elefthei]

@kwantam I’m using LLVM as a counter-example. I think it was an unsuccessful attempt at user-defined passes. Evidence is all the literal billions of dollars it takes to maintain a huge tree of, what was once user defined passes, adopted in the main repo because it’s impossible to maintain them out of tree when the LLVM API changes. But I agree it’s an extensibility point not a Haskell point. I think whatever the decision is, extensibility should be the main goal.

[sga001]

@elefthei, @kwantam :

I think it is totally fine to implement the general framework using user-defined optimization passes. Since the first (and maybe only) such user-defined optimization pass that we would implement is one that implements, in Haskell, RPCs to our external service. We would then be able to run whatever programs we want on our end and the compiler will happily talk to them without issue.

Then, other widgets that are not application-specific can be implemented as separate user-defined optimization passes, or hardcoded in the way that inverses and bit-decompositions are hardcoded. But that's not what I care about at the moment. What I want is to be in a position where a user (or we) doesn't (don't) need to talk to anybody to implement a new widget (e.g., submit a PR).

Would the above be a reasonable starting point. Once we have widgets that have been proven to be general enough, we can always reconsider merging them in the compiler and making them standard by hardcoding them or through their own user-defined optimization pass.

It would be good to get some consensus relatively soon, since this is our most pressing issue at the moment.

[kwantam]

I’m using LLVM as a counter-example. I think it was an unsuccessful attempt at user-defined passes.

Right, I agree that LLVM is bad. But what you wrote was that a Haskell API implies complexity / badness. LLVM is written in C++ and it is also bad. Therefore, as I said, Haskell does not appear to be the problem.

Extensibility is hard! but there does not appear to be a way around this --- what we want is precisely to be able to extend the compiler with new functionality (i.e., widgets), so we will have to solve this problem no matter what language we use.

[kwantam]

Since the first (and maybe only) such user-defined optimization pass that we would implement is one that implements, in Haskell, RPCs to our external service. We would then be able to run whatever programs we want on our end and the compiler will happily talk to them without issue.

That's fine, but we still need to design the API itself, and I don't see how the RPC design you've described actually achieves the goal of replacing an expensive set of constraints with a cheaper one. It seems like the RPC part is only useful once you've actually done that replacement and now need to solve for the correct wire values.

[elefthei]

I’m using LLVM as a counter-example. I think it was an unsuccessful attempt at user-defined passes.

Right, I agree that LLVM is bad. But what you wrote was that a Haskell API implies complexity / badness. LLVM is written in C++ and it is also bad. Therefore, as I said, Haskell does not appear to be the problem.

I see now the confusion is because I wasn't clear on where I perceived a cause of complexity. I wasn't making a judgement on the language (Haskell), I was making a judgement on having an internal API in the compiler Vs an external API for marshaling gadgets. I think any internal API for registering gadgets will be similar in complexity to LLVM (independent of the language), which is bad.

If we write an external API, like the RPC service proposed and some Makefiles that call the compiler, that puts the gadget marshalling complexity to the user which is easier for us to implement.

That's fine, but we still need to design the API itself, and I don't see how the RPC design you've described actually achieves > the goal of replacing an expensive set of constraints with a cheaper one. It seems like the RPC part is only useful once you've actually done that replacement and now need to solve for the correct wire values.

Yeah that part should be the same as my initial proposal and orthogonal to everything else, except maybe use a different intrinsic that __VERIFY_assert. Maybe __GADGET_rewrite is a better name.

[kwantam]

An example of an external API would be ie: a Makefile and an RPC service that assembles programs from gadgets by calling the compiler.

With respect, this is not an API, it's a hack. I implemented this (in the form of exo_compute) in pequin because it was a hack that took an hour to implement. For this project, we should set our sights higher.

[sga001]

To follow on what Lef said:

There are 3 parts to our proposal:

(1) A compiler intrinsic: this intrinsic will allow the widget developer to express to the optimization pass the optimized constraint set. In addition, this intrinsic will also communicate things like variable names and how to recover the value of each variable from the outputs of the RPC server. It will also communicate to the optimization pass how to access the RPC server (see below).

(2) The user-defined optimization pass itself (which is not actually user defined at all. It's just that we'll implement it once via the user-defined optimization pass infrastructure that already exists in the compiler). This code will look for the compiler intrinsics and rewrite/add R1CS as needed. It will also talk to the RPC server following some API. In one extreme case, we could imagine the compiler intrinsic providing an IP/port, and this optimization pass will open a network socket to that service. This is probably the most general instantiation of widgets. We can of course think of other approaches.

(3) The actual RPC server that will be listening on an IP/port (or something else), and will await requests and provide responses.

With this infrastructure, we can naturally support: (1) database queries, (2) passing preimages for hash functions, (3) user-defined widgets in any language that implement the RPC schema. And the compiler stays relatively untouched.

When the compiler is used in "compile" mode, all of the RPC stuff is ignored. When the compiler is used in "compile + solve" mode, it will interact with the RPC server. Hell, maybe the RPC servers are really just lambdas running on AWS spawned on demand as needed. The compiler intrinsic just communicates "lambda handler" to the compiler.

Which of the above are you concerned with ("hacks")? All 3, or some subset in particular?

[kwantam]

Sebastian, what you are describing is exo_compute with fancy terminology thrown in. exo_compute is undeniably a hack. The proposal to implement it as a ratsnest of Makefiles and network daemons does nothing to improve this assessment.

Specific concerns:

• RPC is an implementation detail. This is not the level of detail at which problem currently need to be solved.

• The description you (Sebastian) give in step (2) does not actually correspond to how the compiler works (in particular, there is no direct translation from C to R1CS, so the idea of translating C intrinsics to R1CS just doesn't make any sense as stated). It could be that you're being imprecise, but that also makes me worry: it seems like you're glossing over the part that actually needs thought and giving tons of detail on the part that doesn't, which implies to me that you have only thought about how this integrates with the compiler in an extremely superficial way.

• Similarly, the statements upthread to the effect that the current workings of the compiler are a mystery do not inspire confidence in the proposed changes.

• Finally, zooming out: the proposal is Rube-Goldbergian. Sadly, I am guilty of building many "better" mousetraps in my life; the upside is that it gives me the ability to recognize them.

I understand that designing a real API for optimization passes is more difficult than what you are proposing, and I'm guessing that your priority is speed. Totally fair. But I think we should all be clear that this is not a serious attempt at designing a widget API for the compiler---it's just a way of sidestepping the compiler and having the programmer insert the widgets themselves.

[sga001]

The purpose of this Proposal (see title of github issue), is to have a way to define user-specific widgets. These are widgets that are only applicable to a particular computation (i.e., the current computation). They may or may not generalize, but we don't care about generalization, and hence we don't need them to be part of the compiler in any way, shape or form. Right now there is no way to do that, which means that we cannot express any computation that requires "existential variables" or "hints". This is a major blocking issue for us at the moment.

Do you have a concrete suggestion?

[kwantam]

As I said above, my suggestion is that you need to think more about how this interacts with the compiler, because the details you have provided so far don't really work.

See my previous comment (bullet 2) and Alex's first comment in the thread for examples of issues that you will need to solve.

[elefthei]

Merged in our repo.