R1CS output schema

[sga001]

I'd like to help write a parser/serializer for the outputted R1CS, but I need to understand the schema (i.e., the format of the output). I tried looking around to see if I could find some function/document/readme that describes this output format, but couldn't find anything.

Any help would be appreciated! I tried reading the code but I don't know haskell :(

Is this output consumed directly by libsnark? if so, is it 3 matrices (A, B, C) concatenated?

[elefthei]

int add(int a, int b) {
   return a + b;
}

Becomes in json with no-overflows;

{
   "constraints":[
      [
         {
            "0":"1",
            "1":"1",
            "2":"-1",
            "3":"-1"
         },
         {
            "4":"1"
         },
         {
            "0":"1"
         }
      ],
      [
         {
            
         },
         {
            
         },
         {
            "1":"1",
            "2":"-1",
            "3":"-1"
         }
      ]
   ],
   "signals":[
      {
         "names":[
            "one"
         ]
      },
      {
         "names":[
            "\"f0_add__return\""
         ]
      },
      {
         "names":[
            "\"f0_add_lex0__a_v0\""
         ]
      },
      {
         "names":[
            "\"f0_add_lex0__b_v0\""
         ]
      },
      {
         "names":[
            "\"inv_v1\""
         ]
      }
   ]
}

So all we need to do is mentally map that into A*B - C = 0 and we're good

[alex-ozdemir]

This is a great idea!

Ultimately, this function defines the current textual format: https://github.com/mlfbrown/compiler/blob/master/libsnark-frontend/src/main.cpp#L87.

[sga001]

Thanks, that code is super helpful (finally some code I can read!). I'll try to integrate things with Spartan so we can get rid of libsnark entirely.

What would be better: (1) output a flatbuffer serialized object with some sensible schema (this requires changing the Haskell code that produces the output). (2) keep the current format and just write a parser that takes the current output file as input.

I'm leaning towards (1), but my lack of Haskell knowledge limits my ability to contribute. I can write the Spartan plugin that consumes the flatbuffer and instantiates the R1CS instance since that's in Rust.

[elefthei]

I can help with 1

[mlfbrown]

I vote (1) so that we don't start accumulating non-standard dependencies, but (2) works in a pinch!

[alex-ozdemir]

I agree that (1) is the way to go. The current format has 0 thought put into it; any improvement would be welcome.

Pointer to Haskell code that writes the format: https://github.com/circify/compiler/blob/master/src/IR/R1cs.hs#L365.

[sga001]

Okay. I'll put together a schema that makes sense in the next few days and we'll go from there.

Note that SIEVE IR folks are still working on standardizing the schema. They have a standard for arithmetic circuits (called IR0) but not for R1CS (kind of baffling but c'est la vie). Nevertheless, I expect that the standardized format for R1CS will look very similar, so I'll try to adopt as many aspects of IR0 as I can (e.g., header information that defines #variables, #constraints, version, etc.).

Once we have the flatbuffer schema, we can just use Haskell's flatbuffer implementation (Lef confirmed that one such library already exists) to output the R1CS. This will also mean that when DARPA releases IR1 which includes R1CS, in the best case we'll be done, and in the worst case we'll have to patch up the schema a little bit (but can reuse all existing code/architecture).

[sga001]

As per SIEVE IR discussion today, there are no plans to standardize an R1CS IR. The SIEVE IR will likely remain arithmetic circuits for now (unless we want to put in the work of doing the standardization ourselves).

ZKInterface team is creating a converter from R1CS to SIEVE IR0.

Proposal: output ZKInterface R1CS flatbuffer format. See spec here: https://github.com/QED-it/zkinterface/blob/master/zkInterface.pdf. See schema: https://github.com/QED-it/zkinterface/blob/master/zkinterface.fbs. There is already a parser for that schema in Rust that we can integrate into Spartan fairly easily.

There are some details that need to be fleshed out, particularly how to interface with ZKInterface itself (or if we can avoid that altogether by saving the "messages" into a .zkif file, and then parsing that file in Spartan).

Then, if DARPA asks: "But we want SIEVE IR0 to test your compiler with some other backend", we can just use the converter.

Thoughts? @kwantam , @alex-ozdemir .

[kwantam]

I think keeping things as R1CS internally is best, because it's a more powerful representation: the R1CS->AC direction is a potentially lossy conversion (in the sense that we expect an R1CS->AC->R1CS roundtrip to blow up the constraint set, at least absent some optimizations to squash addition gates).

As you say, Sebastian, I'm sure it will be easy to add the ability to generate whatever format is necessary. We could also output our own, richer format containing a superset of the circuit information (e.g., also containing cached results from compilation that make solving easier), and then convert that lossily to ZKIF or whatever.

[alex-ozdemir]

Emitting ZKIF R1CS sounds like a great idea to me.