Add POD uniqueness module

[ax0]

This PR adds a POD uniqueness module to GPCs. Summary of changes:

• Addition of uniqueness module to gpcircuits package.
• Minor refactoring of list membership module in gpcircuits package.
• Changes to ProtoPODGPC circuit.
• Addition of uniquePODs field to GPCProofConfig together with changes to the GPC compiler.
• Corresponding tests.

This PR depends on the artifact changes in proofcarryingdata/snark-artifacts#13.

[artwyman]

Applying this in the GPCPCD filter (so it doesn't let the user choose the same POD twice) would be a cool addition, though it requires access to all the args at once, so I think the current framework doesn't allow for it.

[artwyman]

Slice? Maybe that name implies there should be a separate start index vs. hard-coded zero.

[artwyman]

Did the thumbs-up suggest you intended to implement this suggestion? Or does it not work because of the circom limitation discussed elsewhere?

[ax0]

The thumbs-up was in response to the latter comment. I suppose I could replace the take-inspired template with a slice-inspired one.

[artwyman]

This seems out-of-place for this as a general list-non-membership template. The need to take only the head of the list is motivated only by the uniqueness use case, so maybe Take should happen at that level, on the input array?

[ax0]

This is how I initially did it, but Circom doesn't like that approach:

thread 'main' panicked at compiler/src/intermediate_representation/translate.rs:959:25:
internal error: entered unreachable code: On development: Circom compiler does not accept for now the assignment of arrays of unknown sizes during the execution of loops

[artwyman]

Where's the unknown size? I'd expect all the array lenghts to be known (based on template args) at the point of use. I'd have to see the specific code to comment on it, though, and I'm fully willing to believe that circom is broken.

[ax0]

All of the array sizes depend only on the template parameter and loop index. I assume there is a bug in the loop + anonymous component unrolling code. What I did was replace the list non-membership and uniqueness module templates with the following:

template NotEqualsAny(MAX_LIST_ELEMENTS) {
    signal input comparisonValue; 

    signal input values[MAX_LIST_ELEMENTS];

    signal output isNotEqual;

    if (MAX_LIST_ELEMENTS == 0) {
        isNotEqual <== 1;
    } else {
        isNotEqual <== MultiAND(MAX_LIST_ELEMENTS)(
            ArrayAddScalar(MAX_LIST_ELEMENTS)(
                -comparisonValue,
                values
            )
        );
    }
}

template UniquenessModule(
    NUM_LIST_ELEMENTS
) {
    signal input values[NUM_LIST_ELEMENTS];

    signal output valuesAreUnique;

    signal noDupsAfter[NUM_LIST_ELEMENTS];

    for(var i = 0; i < NUM_LIST_ELEMENTS; i++) {
        var j = i+1;
        noDupsAfter[i] <==
            NotEqualsAny(NUM_LIST_ELEMENTS - j)(
                values[i],
                Take(NUM_LIST_ELEMENTS - j, NUM_LIST_ELEMENTS)(
                    ArrayRotl(j, NUM_LIST_ELEMENTS)(values)
                )
            );
    }

    valuesAreUnique <== NOT()(
        IsZero()(
            MultiAND(NUM_LIST_ELEMENTS)(
                noDupsAfter
            )
        )
    );
}

My original version used Drop instead of Take and Rotl (which is what I believe you suggested in your other comment) but yielded the same result.

[artwyman]

Interesting. Seems like a circom limitation keeps us from sizing arrays based on loop variables, but not if they're inside of templates. It's unintuitive to me that a loop variable can be a template argument (as demonstrated in our use of Take and Rotl) but can't be an array size. Take does return an array of a size which depends on its template argument, so it shouldn't matter if it's directly in the loop or in a template instantiated in the loop.

Would it help if you combined Take and Rotl into a single Slice template which returned array elements from [I, I+N)? Or would that make the situation worse? I don't really understand what circom's limitation is, so it's hard to know what to suggest. If there's no obvious solution I'm okay with accepting what works, given the final number of constraints is the same.

[ax0]

I tried doing this with a single drop-like template but ran into the same error, which is what led me to the current approach.

[artwyman]

This is clever, though it took me a while to verify that MultiAND really expands to just a sequence of multiplies identical to what you had before (assuming that trivial b <== a constraints get optimized out). I find the partial product easier to reason about.

I wonder if the MultiAND module comes from an older version of circom which didn't have for loops. The whole recursive divide-and-conquer algorithm feels like a lot of complexity to obfuscate the fact it's performing n-1 multiplies to calculate the product of n elements.

This is a stylistic opinion, so I don't mind if you keep the current solution.

[artwyman]

Interesting. Seems like a circom limitation keeps us from sizing arrays based on loop variables, but not if they're inside of templates. It's unintuitive to me that a loop variable can be a template argument (as demonstrated in our use of Take and Rotl) but can't be an array size. Take does return an array of a size which depends on its template argument, so it shouldn't matter if it's directly in the loop or in a template instantiated in the loop.

Would it help if you combined Take and Rotl into a single Slice template which returned array elements from [I, I+N)? Or would that make the situation worse? I don't really understand what circom's limitation is, so it's hard to know what to suggest. If there's no obvious solution I'm okay with accepting what works, given the final number of constraints is the same.

[artwyman]

Shouldn't this be != 0 rather than = 0? Otherwise I'd reverse the naming of the variable so it indicates what's true, not what's false.

[artwyman]

Did the thumbs-up suggest you intended to implement this suggestion? Or does it not work because of the circom limitation discussed elsewhere?

[artwyman]

Oh, I was oversimplifying this wasn't I. Took me a moment to realize what the last clause was for.
Had I realized the need for this, I might've just had k start at 0 and be separately incremented, but this is equivalent and cleverer.