Constraint with variable number of signals

[hilder-vitor]

How can I express a constraint that depends on a variable number of signals instead of a fixed one?

For example, let's say I want to prove I have computed the inner product of two given vectors, then, I could have a template like this:

template InnerProd(n) {

    signal input a[n];
    signal input b[n];
    signal output out;
    
   // First compute the inner product
    var x = 0;
    for(var i = 0; i < n; i++){
	x += a[i]*b[i];
    }

    out <-- x;
    // Now check 
   // so, at this point, I would like to use a single R1CS constraint to write something like
    out === a[0]*b[0] + a[1]*b[1] + .... + a[n-1]*b[n-1];
}

component main {public [a, b]} = InnerProd(10); // fix a value of n

How can I express out === a[0]*b[0] + a[1]*b[1] + .... + a[n-1]*b[n-1] with a single constraint?

[SozinM]

I'm noob so take it with a grain of salt.
a[0]*b[0] + a[1]*b[1] + .... + a[n-1]*b[n-1]; is non-quadratic so you can't express it with a single circuit.
I think you will need to use witness, like this for example:

    var x = 0;
    for(var i = 0; i < n; i++){
	    x += a[i]*b[i];
    }

    signal sum <-- x;

    out <== sum;

The problem with above that witness is not constrained, so need to find a clever way to do this.
Another option is to do this trick:

template InnerProd(n) {

    signal input a[n];
    signal input b[n];
    signal output out;
    
    signal acc[n];
    acc[0] <== a[0] * b[0];
    for(var i = 1; i < n; i++){
	    acc[i] <== a[i]*b[i] + acc[i-1];
    }
    out <== acc[n-1];
}

This way witness is constrained

Also you could try to use built-in components, construct witness with a[i]*b[i] and use built-in Sum component from circom (i wasn't able to find it but i assume it exists x)