An idea for a language that can be integrated with gnark

[aybehrouz]

I've written a description for a language that is inspired by gnark's API, and can be used for declaring polynomial constraint systems. I call it CsGo: Constraint systems with Go! It is very similar to the current gnark's API. However, it can improve ergonomics and clarify semantics. I'd love to know what you think and have some feedback from you. The document is still a draft and likely has lots of errors! 😅

My idea is to write a transpiler that translates CsGo code to gnark code. I believe that would be relatively easy, since they are very close. The CsGo transpiler could be added to gnark and users could optionally use it if they want to. Some gnark's users may prefer using a domain specific language.

Github repo:
https://github.com/aybehrouz/csgo/tree/main

[gbotrel]

There are couple of advantages of not doing a DSL;

1. less maintenance work to do (documentation, ide plugins, dependency management, ...) for the team
2. easier to use go-like tools; pprof, go test, benchmark, ... it integrates well with larger projects (like zk-rollups / zk-evm).

That being said, as you pointed out, a DSL can lead to better ergonomics & even in some cases (but not always) enable some frontend optimisations by providing more context to the compiler.

I think we should evolve gnark in a way that "plugging" different frontends or DSL (like CsGo, CirC or Noir: https://github.com/lambdaclass/noir_backend_using_gnark ), is straightforward, and if at some point the DSL ecosystem is mature enough, look for tighter integration.

[aybehrouz]

I totally agree with the benefits that you've counted for the API based approach. However, as you've mentioned, unfortunately there are some drawbacks too. One is the fact that preventing invalid usages of the API is usually a difficult task, and producing informative errors when those invalid usages are detected, can be another challenge.

In my opinion the gnark API actually is very nice, and I personally found it more intuitive than circom. That's why the design of CsGo is based on gnark's API.

[ThomasPiellard]

Hi @aybehrouz , thanks for the writeup, when you say "declaring polynomial constraint systems", do you mean custom gates? Like a generalisation of plonk where the constraints definition is up to the user, for instance instead of having ql*L+qr*R+qm*L*R+qo*O+qk=0 you could have your own multivariate polynomial P(X_1,..,X_n)=0, where some of the X_i are tagged to be wires (like L, R, O), and the others to be public values (like ql, qr, qm, qo, qk) ? Because we were thinking about that actually and it turns out it's not that easy to make it user friendly (we didn't contemplate using a DSL though).

So far the solution that seems the most flexible is to let the user register a function f(x ...fr.Element) {...}(which would encode the polynomial P encoding the constraint as described above). Then we would need the user to tag which variables are public (i.e. that would play the same role as ql, qr, etc) and which one are the wires (i.e. the one that will play the same role as L,R,O). We would also need some functions to solve such constraints (we hardcoded the way to solve them in our implementation but this should be generalised). This will impact a lot the api as well (Add, Mul, etc have been hardcoded for the systems that we have so far, but there must be a smart way to auto generate this for any type of constraints represented by a multivariate polynomial).

If you look at the way the plonk prover is implemented on the develop branch you should see a first step in that direction, where the polynomials that capture the full plonk relation (i.e. ql*L+..+qk + \alpha*Z(..) + \alpha^2*L_1(Z-1) ) are encoded as functions (the functions called fic, fo, fone). We would really like to make that tunable for the user (the function fic specifically). The rest of the prover should be unchanged... expect for the linearized polynomial but this is a handcrafted optimisation for the original plonk version and we can easily get rid of this... Don't know if it corresponds to what you wanted to originally with your DSL.

[aybehrouz]

Hi @ThomasPiellard, Thank you so much.

when you say "declaring polynomial constraint systems", do you mean custom gates? Like a generalisation of plonk where the constraints definition is up to the user, for instance instead of having qlL+qrR+qmLR+qo*O+qk=0 you could have your own multivariate polynomial P(X_1,..,X_n)=0, where some of the X_i are tagged to be wires (like L, R, O), and the others to be public values (like ql, qr, qm, qo, qk) ?

Yes, to declare a constraint, the user writes something like this in his code: expr1 === expr2, where expr1 and expr2 are expressions that only involve *,+,- and (). I have not considered tagging.

For example x*(y + w) === z*z - 3. I can easily convert this constraint to

api.AssertIsEqual(api.Mul(x, api.Add(y, w)), api.Sub(api.Mul(z, z), 3))

[aybehrouz]

Thanks a lot for your interesting explanation. I should definitely take a look at that implementation.

[ivokub]

Yup, in some contexts it would really benefit to have some DSL. In my case when I implemented field emulation then I'd prefer to know if any variable is used later as an input to other operations or not and use this information to ensure/avoid modular reductions. But it seemed too complicated vs. exposing different variations of the operations (Mul vs MulMod) and requiring the user to hand-optimize. Theoretically, we could parse Go source code and analyze this, but I'm not really sold on how big gain it would give given the complexity of the work.

[aybehrouz]

In my opinion, even with a DSL, having two functions might be the right solution. You will tag the output of MulMod as a field member, so people who use it know they don't need to calculate an extra modulus.

Automatically optimizing this, seems like a low level task to me, that can be done in lower levels.

[aybehrouz]

Another important issue that we should consider here is portability. Let's say I have a complex circuit, and Implementing/declaring it takes a lot time. Certainly I'd prefer to implement/describe this circuit in a way that is not coupled with a backend, so I can easily use different proof systems or even different implementations of the same proof system.

A DSL can be designed to be proof system agnostic. The compilers can be written to support targeting different backends, or even backend implementers may decide to provide special compilers for some DSLs.

On the other hand an API is usually coupled with its backend, unless we use some smart hacks. For example we should add the ability to generate some type of intermediate representation (IR) of the circuit, which is compatible with other backends/implementations. (This is actually some type of DSL usage, since an IR is a low level DSL) However an IR which is supported by different backends may not be available always.

[aybehrouz]

I was trying to say that a constraint definition can be complex, like this one:

Σx_i == 0, where i is a prime less than 2^28

So in our IR we either need to have a high level language, or we have to to be ready to handle very large expressions involving millions of variables. (we need to expand constraints like that one in our example)

[ivokub]

I think we definitely have to be able to handle very large linear expressions. Already in some circuits we have LE with hundreds of thousands terms (long boolean operation chains, e.g. Keccak).

[aybehrouz]

For gnark, my initial idea was to generate gnark code directly from CsGo, (by gnark code I mean the code that we are currently using to write circuits) So people write their circuit in CsGo then it will be compiled to a normal gnark code and then it can be saved in that format.

I just wanted to share the idea here. Who knows? someday It might come in handy. However, it doesn't make sense to start developing a language, if there is not enough interested people (or even contributors) Language development is a task that needs some amount of collaboration and can't be done in isolation.

[ivokub]

Agree. Imo it really would make sense if there would be more users to a language, but seeing VampIR not getting any traction, I'm a bit cautious for now. I guess everyone is spending all the time in improving provers and writing more optimized circuits that they don't have time to think about compatibility.

[aybehrouz]

Well said.

[aybehrouz]

@ivokub @gbotrel
heh yesterday, I was bored and I wrote a simple transpiler for CsGo expressions. 😄
I just tested it on one of functions I'd written and It's kinda cool! 😎
You can write something like this:

func stepMask(api frontend.API, outputLen int,
	stepPosition, startValue, endValue csv) []csv {
	if outputLen < 2 {
		panic("the output len of StepMask must be >= 2")
	}
	// get the output as a hint
	out, err := api.Compiler().NewHint(stepOutput, outputLen, stepPosition, startValue, endValue)
	if err != nil {
		panic(fmt.Sprintf("error in calling StepMask hint: %v", err))
	}

	// add the boundary constraints:
	(out[0] - startValue) * stepPosition === 0
	(out[len(out)-1] - endValue) * (len(out) - stepPosition) === 0

	// add constraints for the correct form of a step function that steps at the stepPosition
	for i := 1; i < len(out); i++ {
		(out[i] - out[i-1]) * (i - stepPosition) === 0
	}
	return out
}

...and it gets converted to this, which is exactly like the original source code:

func stepMask(api frontend.API, outputLen int,
	stepPosition, startValue, endValue frontend.Variable) []frontend.Variable {
	if outputLen < 2 {
		panic("the output len of StepMask must be >= 2")
	}
	// get the output as a hint
	out, err := api.Compiler().NewHint(stepOutput, outputLen, stepPosition, startValue, endValue)
	if err != nil {
		panic(fmt.Sprintf("error in calling StepMask hint: %v", err))
	}

	// add the boundary constraints:
	api.AssertIsEqual(api.Mul(api.Sub(out[0], startValue), stepPosition), 0)
	api.AssertIsEqual(api.Mul(api.Sub(out[len(out)-1], endValue), api.Sub(len(out), stepPosition)), 0)

	// add constraints for the correct form of a step function that steps at the stepPosition
	for i := 1; i < len(out); i++ {
		api.AssertIsEqual(api.Mul(api.Sub(out[i], out[i-1]), api.Sub(i, stepPosition)), 0)
	}
	return out
}

[ivokub]

Looks cool. Are you doing only string manipulation or are you parsing AST? If you parse AST, then you could track information about variables and where they are being used.

I think it may allow for some optimisations in the future if we have more throughput :)

[aybehrouz]

I'm using the parse tree, and creating the conversion by annotating the tree. I just added a simple rule to the grammar, and ANTLR4 did most of the hard work. 😂

The cool thing is, while it is only 30-40 lines of code, it can handle everything:

func main() {
    x + y*z === (a+b)*(c+d) + 1
}

func main() {
    api.AssertIsEqual(api.Add(x, api.Mul(y, z)), api.Add(api.Mul(api.Add(a, b), api.Add(c, d)), 1))
}

[aybehrouz]

Theoretically you should be able to write a semantic analyzer at least as powerful as Go's analyzer.
I personally do not have a good estimate about the amount of work that should be done. Writing compilers is tricky, sometimes you can easily implement something that looks hard, but doing something simple takes a lot of time.

[gbotrel]

an idea that cross my mind few times is to use something like that a bit like scripting languages (like Lua) in game engine; i.e have an interpreter that runs in your process to parse these snippets.

Not talking too much on this thread because I personally prefer this with IDE auto complete across the projects, in tests etc:

func main() {
    api.AssertIsEqual(api.Add(x, api.Mul(y, z)), api.Add(api.Mul(api.Add(a, b), api.Add(c, d)), 1))
}

than having a script that transpiles my circuit each time I do a modif on it 🙄

[aybehrouz]

I agree that only for getting a better syntax for expressions, that language and parser would not make much sense. However, arguably there will be many other benefits in having such a language. The IDE support also can be added by writing a plug in. Specially for VS code that has an open source Go plug in.

[hussein-aitlahcen]

Very intersting subject, I started tackling this, but instead of creating a language, reusing an existing one (https://dhall-lang.org/#).
You can directly hook into the AST and transpile, I just started and already have interesting results such as pattern matching:

let State = { dummy : Natural, counter : Natural }

let Message = < One | Ten | Hundred >

let Cpu =
      { load :
          forall (State : Type) ->
          forall (Message : Type) ->
            { state : State, message : Message }
      , save : forall (State : Type) -> State -> {}
      }

in  \(cpu : Cpu) ->
      let input = cpu.load State Message

      in  cpu.save
            State
            { dummy = input.state.dummy + input.state.counter + 1
            , counter =
                  input.state.counter
                + merge { One = 1, Ten = 10, Hundred = 100 } input.message
            }

The interface is simple, you define a State, a Message and a transition function. Both the state and message are private input right now but I plan to introduce tagging to allow the user to chose. The Cpu is a builtin provided by the transpiler (the save function is present to avoid Dhall normalizing too much).
The transpiler produce the following (very trivial for now, haven't even checked if this is valid Go/Gnark yet)

"___res0 := frontend.Variable(0)"
"___lit1 := frontend.Variable(100)"
"___res0 = api.Select(api.IsZero(api.Sub(circuit.input[0], 0)), ___lit1, ___res0)"
"___lit2 := frontend.Variable(1)"
"___res0 = api.Select(api.IsZero(api.Sub(circuit.input[0], 1)), ___lit2, ___res0)"
"___lit3 := frontend.Variable(10)"
"___res0 = api.Select(api.IsZero(api.Sub(circuit.input[0], 2)), ___lit3, ___res0)"
"___add4 := api.Add(circuit.input[1][0], ___res0)"
"___add5 := api.Add(circuit.input[1][1], circuit.input[1][0])"
"___lit6 := frontend.Variable(1)"
"___add7 := api.Add(___add5, ___lit6)"
```

[aybehrouz]

That's great. How you're using the state machine model is very interesting. It somehow reminds me of STARK libraries like winterfell.

I think your approach is more high level and is an attempt for developing a more high level language for writing circuits. My approach is more low level and I'm trying to develop some type of portable intermediate representation (IR) for proof systems, and at the same time develop some type of low level tool for directly using that IR, when you need to design a very efficient circuit.

[hussein-aitlahcen]

I pushed the experiment and it's looking pretty cool:
Given this Dhall program: https://gist.github.com/hussein-aitlahcen/5d1c15f9be4acc449dcf5d246fec766a
Here is the generated Gnark circuit: https://gist.github.com/hussein-aitlahcen/5238d7548ab73df39096b3583f4791c1

• product/coproducts(sum types as tagged product) data types
• recursive equality by value
• abstract folding/unfolding

[aybehrouz]

Thanks for sharing. That's so interesting.
For me, the Dhall syntax is a bit hard to understand, but I guess that's because I don't have any experience working with that language.