0xpolygonhermez / pil-stark Goto Github PK

I notice that in circuits.gl/mux1.circom, the output of MultiMux1(n) is like this:

out[i] <== (c[1][i] - c[0][i])*s + c[0][i];

It seemed like a non-deterministic circuit, when "s=0" or "c[1][i] - c[0][i]=0", the other factor can be any value.
I'm not pretty sure, does that sound like a real problem for the team?

  const starkStruct = {
    "nBits": 10, 
    "nBitsExt": 11, 
    "nQueries": 128, 
    "verificationHashType": "GL", 
    "steps": [ 
      {"nBits": 11}, 
      {"nBits": 5}, 
      {"nBits": 3}, 
      {"nBits": 1} 
    ]
  };

I think nBits and nBitsExt are corresponding to domain field size and extension field size, GL means Goldilocks field.

What about nQueries and steps?

For example: "test fibonacci" output ends with:

1) test fibonacci sm
       It should create the pols main:
     RangeError: Array buffer allocation failed
      at new ArrayBuffer (<anonymous>)
      at new BigUint64Array (<anonymous>)
      at new BigBuffer (node_modules\pilcom\src\bigbuffer.js:11:36)
      at starkGen (src\stark_gen.js:74:20)
      at async Context.<anonymous> (test\stark_fibonacci.test.js:51:22)

node_modules/mocha/lib/reporters/base.js:305
Process exited with code 1

Running x64 node v16.17.0, Windows 11, lots of RAM, nothing else running. "test plookup" executes correctly

There are no references to goldenPrime. Seems relevant. Should this be incorporated or is it deprecated?

I really don't understand it:

            for (let g = 0; g < pol.length / nX; g++) {
                if (si == 0) {
                    pol2_e[g] = pol[g];
                } else {
                    const ppar = new Array(nX);
                    for (let i = 0; i < nX; i++) {
                        ppar[i] = pol[(i * pol2N) + g];
                    }
                    const ppar_c = F.ifft(ppar);
                    polMulAxi(F, ppar_c, F.one, sinv);    // Multiplies coefs by 1, shiftInv, shiftInv^2, shiftInv^3, ......

                    pol2_e[g] = evalPol(F, ppar_c, special_x);
                    sinv = F.mul(sinv, wi);
                }
            }

Does it mean that:

• 1. we can prove "the verification of a STARK proof" with a SNARK proof? Then how can I get the specific SNARK proof JSON file?
• 2. OR we can prove "the verification fo a SNARK proof" with a STARK proof?

Does our "recursive STARK" mean:
"stark_proof_1" -> "snark_proof_1" -> "with input_2 then get stark_proof_2" -> "snark_proof_2" -> ....
OR just:
"stark_proof_1" -> "with input_2 then get stark_proof_2" -> ....

Maybe support bls12381?

TL;DR: The quotient $(f_i(X) - f_i(z))(X - z)$ can be moved entirely over the base field when the polynomial $f_i$ is defined over the base field, with a small overhead in the proof size and verification time that justifies a big improvement in proving time.

In the following, we denote by $\mathbb{F}$ a finite field of prime order and by $\mathbb{K}$ an extension field of $\mathbb{F}$ of degree $d$. We also denote by $\omega$ to a primitive $n$-th root of unity over $\mathbb{F}$.

In Round 6 of our eSTARK, we compute the following polynomial:

where $z \in \mathbb{K}$ is the opening challenge set by the verifier in Round 5, $\epsilon_1,\epsilon_2 \in \mathbb{K}$ are sent by the verifier at the start of Round 6 and $f_i,h_j$ are polynomials whose coefficients can be either over $\mathbb{F}$ or over $\mathbb{K}$ .

Notice that when the polynomial is over $\mathbb{F}$ we are "paying too much" in each of the quotients that involve such polynomials, i.e., we operate entirely over the extension field (including the division) even tho both the numerator and the denominator only have the constant coefficient in $\mathbb{K}$.

Explanation

Here is a trick¹ from the Polygon Zero team to reduce this cost. The idea starts by noticing that an extension field element $z$ is completely characterised by its minimal polynomial $m_z(X)$, that is, the (monic) polynomial of least degree (at most $d$) over $\mathbb{F}$ such that $m_z(z) = 0$.

Notice that such polynomial $m_z$ satisfies:

1. The value of a base field $f$ at $z$ coincides with that of the remainder $r(X) = f(X) \pmod{m_z(X)}$ (which is also a polynomial over $\mathbb{F}$): $$f(z) = q(z) \cdot m_z(z) + r(z) = r(z).$$
2. Proving that $f(X) - r(X)$ is divisible by $m_z(X)$ implies 1. and therefore the original eSTARK quotient claim.

Thus, the prover provides the polynomial $r$ instead of the value $f(z)$ and then it prove to V the low-degreeness of the quotient $(f(X) - r(X)) / m_z(X)$ rather than $(f(X) - f(z)) / X - z$, avoiding extension field operations at all.

Costs

First, both newly introduced polynomials $m_z$ and $r$ are defined over $\mathbb{F}$ and computing the its LDE is cheaper than computing the LDE over the extension field alternative. Also, notice that in our case there are only two minimal polynomials that need to be computed, namely $m_z$ and $m_{\omega z}$.

Second, the minimal polynomial $m_z$ is computed by searching for the smallest $2 \leq \ell \leq d$ such that the following linear system of $d$ equations and $\ell$ unknowns : $$c_0 + c_1 \cdot z + \dots + c_{\ell - 1} \cdot z^{\ell - 1} = - z^{\ell},$$ has solutions such that at least one of $c_0,c_1,\dots,c_{\ell - 1}$ is distinct from $0$.

Unrolling it out for our case, one must solve one of the following:

$$\left. \begin{array}{r} c_0+c_1 \cdot z_0 + z_0' = 0 \\ c_1 \cdot z_1 + z_1' = 0 \\ c_1 \cdot z_2 + z_2' = 0 \end{array} \right\} \qquad \left. \begin{array}{r} c_0+c_1 \cdot z_0 + c_2 \cdot z_0' + z_0'' = 0 \\ c_1 \cdot z_1 + c_2 \cdot z_1' + z_1'' = 0 \\ c_1 \cdot z_2 + c_2 \cdot z_2' + z_2'' = 0 \end{array} \right\}$$

where $z := (z_0,z_1,z_2), z^2 := (z_0,'z_1',z_2')$ and $z^3 := (z_0'',z_1'',z_2'')$.

The polynomials $m_z, m_{\omega z}$ are computed by both the prover and the verifier.

Use Case

This idea does not overcome the costs of the basic idea if the polynomials involved in the computation of $F(X)$ are not, in a huge amount, over the base filed. However, only those polynomials computed in the auxiliary trace of the eSTARK protocol are those the appear to be over the extension field. Following the ideas in pilcom-#53 would avoid having auxiliary columns and constraints and therefore this trick would be a big overall improvement.

 for (let i = maxDeg + 1; i < lastPol_c.length; i++) {
            if (!F.isZero(lastPol_c[i])) return false;
}

for the last low-degree test, should it be i = maxDeg instead of i = maxDeg + 1? please check it.

I'm following Jordi Baylina's steps to try to learn our tool.

1. mkdir tmp
2. fibonacci exec
3. fibonacci PIL verify
4. fibonacci build constree
5. fibonacci prove: get errors as below, how can I fix this?

/usr/local/bin/node --max-old-space-size=32000 src/main_prover.js -m /Users/lanyu/zyd/0xPolygonHermez/pil-stark/tmp/fibonacci.commit -c /Users/lanyu/zyd/0xPolygonHermez/pil-stark/tmp/fibonacci.const -t /Users/lanyu/zyd/0xPolygonHermez/pil-stark/tmp/fibonacci.consttree -p /Users/lanyu/zyd/0xPolygonHermez/pil-stark/test/sm_fibonacci/fibonacci_main.pil -s /Users/lanyu/zyd/0xPolygonHermez/pil-stark/test/sm_fibonacci/fibonacci.starkstruct.json -o /Users/lanyu/zyd/0xPolygonHermez/pil-stark/tmp/fibonacci.proof.json -z /Users/lanyu/zyd/0xPolygonHermez/pil-stark/tmp/fibonacci.proof.zkin.json -b /Users/lanyu/zyd/0xPolygonHermez/pil-stark/tmp/fibonacci.public.json
loading /Users/lanyu/zyd/0xPolygonHermez/pil-stark/tmp/fibonacci.const.. 0 of 0.001953125
loading /Users/lanyu/zyd/0xPolygonHermez/pil-stark/tmp/fibonacci.commit.. 0 of 0.001953125
The "offset" argument must be of type number. Received an instance of Object
TypeError [ERR_INVALID_ARG_TYPE]: The "offset" argument must be of type number. Received an instance of Object
    at read (node:internal/fs/promises:478:5)
    at fsCall (node:internal/fs/promises:313:18)
    at FileHandle.read (node:internal/fs/promises:154:12)
    at MerkleHash.readFromFile (/Users/lanyu/zyd/0xPolygonHermez/pil-stark/src/merklehash_p.js:246:18)
    at async run (/Users/lanyu/zyd/0xPolygonHermez/pil-stark/src/main_prover.js:65:23)
Process exited with code 1