feat: handle circom tags

[alinush]

From a discussion here with @erhant, it appears that circomkit does not yet handle automatically-generating wrappers for circom templates whose input signals are tagged.

This would be nice to have for several reasons:

1. Tags add a much needed layer of sanity checks to circom development
2. Manually writing stubs for different tests of the same template does not scale well

I am not sure what's the best way to actually allow for tags in circomkit though. Here's my two cents:

Non-valued tags: These seem simple to handle: just add them automatically in the auto-generated wrapper by circomkit!

Valued tags: These may need special handling.

I think it would be best if developers using circomkit could, in their TypeScript tests, specify the value of the tags they want to test with for their input signals. (This means that the circom wrapper has to be generated at run time?)

[erhant]

Im kind of slammed with other work these days, I've been wanting to get to Circomkit to do a wide issue-squashing session, I will definitely include this in it especially since you need it as well 🙏🏻

I can't yet give a time when I can work on this though, apologies... :(

[erhant]

It would be awesome for the sake of quick-starting this, that if you could paste some tiny circuits here and the wrappers that you expect to be generated! 💐

[alinush]

I'll give you some examples from circom-stdlib: my attempt to learn how to write (safer?) circom by rewriting (some of) circomlib to leverage tags.

LessThan template

The template I'd like to test (see full code):

// File: comparators.circom

template LessThan(N) {
    // We have to make sure the 1 << N (which is N+1 bits wide) fits in the scalar 
    // field. Otherwise, we lose soundness.
    AssertBitsFitScalar(N+1)();

    // We leverage the tag system to guarantee the numbers are at most N-bits.
    // If not, we would lose soundness again.
    signal input {maxbits} lhs;
    signal input {maxbits} rhs;
    assert(lhs.maxbits <= N);
    assert(rhs.maxbits <= N);

    signal {binary} bits[N + 1] <== Num2Bits(N + 1)(lhs + (1 << N) - rhs);

    signal output {binary} out <== 1 - bits[N];
}

The wrapper I am currently writing:

pragma circom 2.1.7;

include "comparators.circom";

template LessThan_wrapper(N) {
    signal input lhs, rhs;
    
    signal {maxbits} lhs_m, rhs_m;

    lhs_m.maxbits = N; // Note: this is what the circomkit dev wants to control
    lhs_m <== lhs;
    
    rhs_m.maxbits = N; // Note: this is what the circomkit dev wants to control
    rhs_m <== rhs;
    
    signal output out <== LessThan(N)(lhs_m, rhs_m);
}

component main { public [lhs, rhs] } = LessThan_wrapper(252);

DivRem template

The template I'd like to test (unsure if this is sound as is):

// File: integers.circom

template DivRem() {
    signal input {maxbits} a;
    signal input {nonzero, maxbits} b;
    signal output {maxbits} q;
    signal output {maxbits} r;

    var N = a.maxbits;
    var M = b.maxbits;

    // Tags must be assigned first before assigning the signals (ugh)
    r.maxbits = M;
    r <-- a % b;
    q.maxbits = N;
    q <-- a \ b;

    // We only need to test 2^M(2^N + 1) <= p, but no easy way to in circom.
    // Instead, we can test that a slighlty larger 2^{M + N + 1} < p.
    // We do lose the ability of using this with higher (N, M), but that's okay.
    AssertBitsFitScalar(N+M+1)();

    // Check Euclidean division theorem, including r \in [0, b)
    a === q * b + r;

    // We can assume b < 2^M, because it is tagged.
    // But, for the remainder r, we have to enforce it:
    // (Of course, r may is a bit smaller than M bits, because r < b)
    _ <== Num2Bits(M)(r);

    // We know that r, b < 2^M => can safely call LessThan(M)
    signal valid_remainder <== LessThan(M)(r, b);
    valid_remainder === 1;

    // Check that q is bounded, otherwise we are in trouble
    _ <== Num2Bits(N)(q);
}

The wrappers I have to write:

pragma circom 2.2.2;

include "integers.circom";

template DivRem_wrapper() {
    signal input a, b;

    signal {maxbits} a_m;
    // Note: The `nonzero` tag is non-valued, so it is just being applied here directly "by force"
    // Nonetheless, the developer may want to test cases where it is not applied to ensure that compilation fails?
    signal {nonzero, maxbits} b_m;

    a_m.maxbits = 64; // Note: this is what the circomkit dev wants to control
    a_m <== a;

    b_m.maxbits = 64; // Note: this is what the circomkit dev wants to control
    b_m <== b;

    signal output (q, r) <== DivRem()(a_m, b_m);
}

component main { public [a, b] } = DivRem_wrapper();

Notes

For valued tags, (I think) the goal should be for devs to have an easy way to specify the values that tags are initialized with (like the maxbits tag above).

This may be best done via new fields in circuit.json?

For non-valued tags, an "automated" approach may be to always apply non-valued tags on any input signal that needs them. This ensures compilation will always succeed.

However, if circomkit is supposed to allow devs to test for failed compilations, then maybe even non-valued tags should be specified via circuit.json? This way, a dev may choose to not apply a tag and check that their template that requires it fails compilation.

Disclaimer: I have not yet played with circomkit to know enough (ironically, because I can't: all my code is tagged! 😝); only looked at examples.

Thank you!

Appreciate you considering this! 🙏

FWIW, I think developing circom code is incredibly-difficult to do safely.

To me, tags seems like a low-hanging when it comes to making circom code safer & actively prevent many silly bugs.

By adding support for tags in circomkit, you would be encouraging developers to use this feature more & making the ZK ecosystem much safer! (And I would be supporting, by re-writing circomlib to be tagged!)

There are also other folks doing the same, btw, but they are using circom_tester.

• See their tagged LessThan
• And their wrapper here

[alinush]

I will eagerly await any progress on this 🙏

Until then, I think I will have to write manual wrappers that tag my inputs and invoke them with circom_tester.