RFC 7: An ASM-like language for kimchi

[mimoo]

This RFC proposes a syntax that can be used to debug kimchi circuits

Not an intermediate representation (IR)

Currently we think about the snarky-kimchi stack as either:

• some code written using the snarky library
• some kimchi gates using the types defined in kimchi (obtained by compiling the previous item)

at no point do we use an intermediate representation (IR). An IR would be interesting because:

• snarky supporting an IR would allow us to compile snarky programs to other backends (that support the same IR)
• kimchi supporting an IR would allow different frontends (that support the same IR) to compile to kimchi

I think there's some interesting developments with both VampIR (Anoma) and ACIR (Aztec Network) that we should investigate.

Anyway, this RFC is not about an IR! This RFC is about an assembly-like language (ASM) for Kimchi. In other words, for a human-readable encoding of kimchi gates.

Is it actually useful?

Low-level programmers need a way to reach out for the actual output produced by the circuits they write using a higher-level abstraction (like snarky), this is what ASM languages are for.

More generally, it seems like this could also be useful to users of snarkyjs to understand how code you write translates to kimchi gates, and how costly some of your lines of code can be. (Starknet has a cool product that allow users to submit gadgets and observe the computational efficiency of their solutions, it could be cool if we had something similar that would show you how some code translate to some kimchi gates.)

I've been successfully using such an ASM language for kimchi for my side project noname. In the repo, the folder examples/ contains circuits (in .no format) as well as their associated asm encoding of the compiled circuit (in .asm format).

Tests will compile every .no files, and check that they match their associated .asm file. Not only did I caught a number of bugs by being able to read through the ASM-encoded circuit, but bugs can also be caught in PRs as you can clearly see how changes impact the compilation of existing circuits we have. For example zksecurity/noname@fd60e81

The proposal

The ASM-language I use in noname looks like this:

@ noname.0.7.0

c0 = -7792942617772573725741879823703654500237496169155240735183726605099215774906
// (truncated)
c164 = 10888828634279127981352133512429657747610298502219125571406085952954136470354
DoubleGeneric<1>
DoubleGeneric<1,0,0,0,0>
Poseidon<c0,c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14>
Poseidon<c15,c16,c17,c18,c19,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29>
Poseidon<c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c40,c41,c42,c43,c44>
Poseidon<c45,c46,c47,c48,c49,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59>
Poseidon<c60,c61,c62,c63,c64,c65,c66,c67,c68,c69,c70,c71,c72,c73,c74>
Poseidon<c75,c76,c77,c78,c79,c80,c81,c82,c83,c84,c85,c86,c87,c88,c89>
Poseidon<c90,c91,c92,c93,c94,c95,c96,c97,c98,c99,c100,c101,c102,c103,c104>
Poseidon<c105,c106,c107,c108,c109,c110,c111,c112,c113,c114,c115,c116,c117,c118,c119>
Poseidon<c120,c121,c122,c123,c124,c125,c126,c127,c128,c129,c130,c131,c132,c133,c134>
Poseidon<c135,c136,c137,c138,c139,c140,c141,c142,c143,c144,c145,c146,c147,c148,c149>
Poseidon<c150,c151,c152,c153,c154,c155,c156,c157,c158,c159,c160,c161,c162,c163,c164>
DoubleGeneric<>
DoubleGeneric<1,-1>
(0,0) -> (14,1)
(1,0) -> (2,2)
(13,0) -> (14,0)

It basically has 4 sections:

• a version (@ noname.0.7.0)
• a number of constants (e.g. ci = ) that are too large to be displayed inline
• a number of gates (e.g. GateName<coefficients>)
• wirings (e.g. (row, col) -> (other_row, other_col))

The encoding has been optimized essentially to what I found useful at the time when I was debugging.

Note: numbers are displayed as negative numbers when we reach the middle of the field

I've iterated on this process and proposed something a bit different for kimchi in #831

The differences:

• it adds a pub keyword to the public rows, this is actually needed to differentiate different circuits with different public input size (and I need to fix this in noname)
• it displays the row number in front of each gate (e.g. row0.)
• the wiring is displayed right after the gate itself
• it handles the generic gate differently:
  • the coefficients are split in two if two generic gates are used (e.g. row2.Generic<-1,0,0,1,0><-1,0,0,1,0>)
  • the wiring is written differently by addressing directly l1, r1, o1, or l2, r2, o2

These changes were made so that I could read the tests I was writing for snarky more quickly (see MinaProtocol/mina#12125 and MinaProtocol/mina#12128)

Here's an example using the generic gate more heavily:

row0.pub.Generic<1,0,0,0,0>
.l1 -> row4.l1

row1.pub.Generic<1,0,0,0,0>
.l1 -> row2.l1

row2.Generic<-1,0,0,1,0><-1,0,0,1,0>
.l1 -> row4.r1, .r1 -> row1.l1
.l2 -> row0.l1, .r2 -> row2.l2

row3.Generic<-1,0,0,1,0><-1,0,0,1,0>
.l1 -> row4.r2, .r1 -> row3.l1
.l2 -> row4.l2, .r2 -> row3.l2

row4.Generic<0,0,1,-1,0><0,0,1,-1,0>
.l1 -> row2.r2, .r1 -> row2.r1, .o1 -> row5.l1
.l2 -> row3.r2, .r2 -> row3.r1, .o2 -> row4.o1

row5.Generic<1,0,0,0,-1>
.l1 -> row4.o2

I don't necessarily think this is the prettiest language, again I did what was useful to me when I needed to look at the compiled version of my circuits to ensure that there were no bugs in the compilation.

Writing gadgets using the ASM-language

This proposal, so far, assumes that the ASM language won't be used directly to write gadgets or circuits. But is this something that we would potentially want to support? If so we'd have to think about specifying what are the input and output of the gadget. I don't think this would be too useful personally, but perhaps someone has a strong argument in favor of supporting this use case.

Support for custom gates

More problematic: how do we make the language work when users can add their own custom gates? Do we need to support a unique namespace for adding custom gates?

Downsides and alternatives

A criticism of this feature is that it will add some overhead to our work: as we extend kimchi we will need to continuously support this ASM language.

Another criticism is that people who want to make use of it in other languages will have to write their own encoder or parser (in the case we would want to support use cases for parsing these).

Note: our encoder is currently ~200LOC)

An alternative is to simply encode a circuit using a standard encoding like JSON.

More examples

For snarky examples, you can see https://github.com/MinaProtocol/mina/pull/12128/files which I took the following circuit from:

let main (x : Impl.Field.t) () =
    let y = Impl.Field.one in
    let res = Impl.Field.(x + y) in
    let two = Impl.Field.of_int 2 in

    Impl.Field.Assert.equal res two ;
    Impl.Field.Assert.not_equal res Impl.Field.one ;
    Impl.Field.Assert.non_zero res

which translates to:

row0.pub.Generic<1,0,0,0,0>
.l1 -> row2.l1

row1.Generic<1,0,0,0,-2><1,0,-1,0,1>
.l1 -> row1.o2
.l2 -> row0.l1, .o2 -> row1.l1

row2.Generic<1,0,-1,0,1><0,0,0,1,-1>
.l1 -> row2.l2, .o1 -> row3.l1
.l2 -> row1.l2

row3.Generic<0,0,0,1,-1>
.l1 -> row2.o1

you can also check how I use it in noname: https://github.com/mimoo/noname/tree/main/examples

[mitschabaude]

Nice! Here's my take on ASM-like language vs JSON format:

• JSON's main advantage is that it's trivial to parse / integrate with all kinds of environments
• ASM format's main advantage is that it can be optimized for readability, in a way that JSON can't

It sounds to me like this ASM format is very simple to parse and integrate as well. Also, I'm sure the ASM format can be easily mapped to JSON and back. So it's like an optional readability / writability layer, and there's no strong reason against using this layer wherever it can be integrated.

So, is there a good reason in favor of using the ASM-like language? I think yes!

Snark circuits are a case where improved readability can make a huge difference. It can mean the difference between a broken protocol and a secure one. That's why I would advocate for using the ASM format in places that are meant for the human eye, to get a second view into a circuit, as a check on the DSL that's used to write the circuit. The snarky tests seem like a reasonable example of that.

[rbonichon]

Looks interesting for debugging.

A JSON encoding would be interesting if we need to exchange data but at this point I don't see much value in it.

On a more shallow point, regarding the syntax, since it's aimed at human consumption, I would remove the , operator and force a newline for each wiring. The < > notation looks also a bit weird to my eyes: is there a rationale for this. I would have expected either ( ) or [ ] depending on the semantics (parameters, or vectors)

As of now, the .l1, .r1, .o1 naming scheme is a little bit opaque but I guess there's going to be some documentation for that.

[mimoo]

The < > notation looks also a bit weird to my eyes: is there a rationale for this

no not really, I reached out for the first thing that came to mind. I don't really feel strongly about.

I would remove the , operator and force a newline for each wiring

there's two considerations. If we're talking more generally (not just about the generic gate), the wiring is constructed via cycles, and so you can end up with sort of unrelated wiring (or wiring that might make you pause) until you look at a bigger subset of the cells that are part of that wiring.

BTW in noname I display wiring like this in debug mode:

For the (double) generic gate, since it actually packs two generic gates under the hood, I think it's useful to be able to quickly distinguish the first generic gate from the second one. That's why I split them in their own lines

As of now, the .l1, .r1, .o1 naming scheme is a little bit opaque but I guess there's going to be some documentation for that.

yeah agree, I needed to quickly differentiate the two gates under the double generic gate, I came up with this but open to suggestions : o

[mrmr1993]

An alternative is to simply encode a circuit using a standard encoding like JSON.

I think we should go this route, especially for the snarky tests. The tests that we'll use to check consistency between the rust and OCaml backends are not the place to smuggle in a new assembly language.

On the proposal in particular, I don't like the syntax, but also would prefer that we don't spend time bikeshedding it. If there's a canonical, easy-to-manipulate representation, like JSON, it's easy for anyone -- internal or external -- to write a visualiser or equivalent language.

I propose closing this discussion and backing out PR #831.

[mitschabaude]

I agree that we should have a canonical JSON representation (as well). Here's one that almost works for me, the only thing that should be changed is the representation of field elements, from an array of numbers (= bytes) to a decimal string:
MinaProtocol/mina@0809d58#diff-717932239baee2bc394e9cd7ffdc31abeeea7638532f61c6f3d142577ad1ad23L131

[mrmr1993]

I'll have to think about how to make the serialisation of field elements nicer, serde doesn't make that easy.

Do you have a sample output?

[mitschabaude]

@mrmr1993 here's an example output
cs.txt