[Question]: a problem with some pil constraints

[UrsaMajor-t]

Version

v6.0.0

Description

I tried to change part of the logic in zkasm, and when I execute the main_executor.js file and enter a specific input, it prompts me to execute successfully. However, when I tried to use verifyPil to verify it (zkasm's N = = pil's N), I was prompted with the following error. I understand that this is a problem with some constraints. I want to know how to troubleshoot the problem in this case. Or is it that after changing zkasm logic, pil files need to be changed accordingly? Is there any convenient way to generate the corresponding pil according to zkasm?

arith.pil:4434:  plookup not found w=0 values: 1:0
arith.pil:4435:  plookup not found w=0 values: 1:0
arith.pil:4436:  plookup not found w=0 values: 1:0
binary.pil:164:  plookup not found w=0 values: 1:0,8,65,1,0,0,8
binary.pil:167:  plookup not found w=0 values: 1:0,8,244,0,0,0,8
climb_key.pil:107:  plookup not found w=1 values: 1:1,0,53660,0,2
main.pil:211:  plookup not found w=72 values: 1:8384459

[UrsaMajor-t]

@laisolizq can you help me solve this question? I found that arith sm restricts range and limits the type of value. when I try to use n = 2 21, arith sm cannot pass the plonkup check

[krlosMata]

cc: @zkronos73

[zkronos73]

The lookup tables are optimized for 2^23, you must use N=2^23 if not, some lookups fail. For example, the tree first lookups verify a range with size 2^23:

    carry[0] in GL_SIGNED_22BITS;
    carry[1] in GL_SIGNED_22BITS;
    carry[2] in GL_SIGNED_22BITS;

buildRange(pols, N, 'GL_SIGNED_22BITS', -(2n**22n), (2n**22n)-1n);

To verify constrains need to use N = 2^23

[UrsaMajor-t]

@zkronos73 Thank you for your answer, then I have a few questions:

1. For the cases N = 2^23, fromValue = -2^22, toValue = 2^22 - 1, buildRange function fills the pols[GL_SIGNED_22BITS] array with an increasing sequence from − 4194304 to 4194303, and repeats the sequence until the array is filled with 2^23 elements. So, the range of this lookup table can be interpreted as -2^22 to 2^22-1? Is the earliest example of GL_SIGNED_18BITS similar situation?

2. Then I tried to set n to 2^22, and then changed the following code. when zkasm is the compiled file corresponding to n, I tested it and found that both executor and verify pil can pass, but once n is set to 2^21, verify pil will start to fail. According to the above statement, this seems to conflict with the answer I just got, because I can set N to 22, even if 21 still reports an error. I want to understand the deeper logic. main.pil

   
   constant %N = 2**22;

include "main_common.pil";

namespace Main(%N);

lJmpnCondValue in Global.STEP;

pol commit hJmpnCondValueBit[10];

hJmpnCondValueBit[9] * (1-hJmpnCondValueBit[9]) = 0;
hJmpnCondValueBit[8] * (1-hJmpnCondValueBit[8]) = 0;
hJmpnCondValueBit[7] * (1-hJmpnCondValueBit[7]) = 0;
hJmpnCondValueBit[6] * (1-hJmpnCondValueBit[6]) = 0;
hJmpnCondValueBit[5] * (1-hJmpnCondValueBit[5]) = 0;
hJmpnCondValueBit[4] * (1-hJmpnCondValueBit[4]) = 0;
hJmpnCondValueBit[3] * (1-hJmpnCondValueBit[3]) = 0;
hJmpnCondValueBit[2] * (1-hJmpnCondValueBit[2]) = 0;
hJmpnCondValueBit[1] * (1-hJmpnCondValueBit[1]) = 0;
hJmpnCondValueBit[0] * (1-hJmpnCondValueBit[0]) = 0;

jmpnCondValue = 2**31*hJmpnCondValueBit[9] + 2**30*hJmpnCondValueBit[8] + 2**29*hJmpnCondValueBit[7] + 2**28*hJmpnCondValueBit[6] +
                2**27*hJmpnCondValueBit[5] + 2**26*hJmpnCondValueBit[4] + 2**25*hJmpnCondValueBit[3] + 2**24*hJmpnCondValueBit[2] +
                2**23*hJmpnCondValueBit[1] + 2**22*hJmpnCondValueBit[0] + lJmpnCondValue;

 sm_arith.js

module.exports.buildConstants = async function (pols) { const N = pols.SEL_BYTE2_BIT21.length; buildByte2Bits16(pols, N); const BITSN = BigInt(Math.log2(N)) - 1n; console.log("GL_SIGNED_22BITS BITSN", BITSN); buildRange(pols, N, 'GL_SIGNED_22BITS', -(2n BITSN), (2n BITSN) - 1n); buildRangeSelector(pols.RANGE_SEL, N, 2 ** 16, [0xFFFF, 0xFFFE, 0xFFFD, 0xFC2F, 0xFC2E, 0x3064, 0x3063, 0x4E72, 0x4E71, 0xE131, 0xE130, 0xA029, 0xA028, 0xB850, 0xB84F, 0x45B6, 0x45B5, 0x8181, 0x8180, 0x585D, 0x585C, 0x9781, 0x9780, 0x6A91, 0x6A90, 0x6871, 0x6870, 0xCA8D, 0xCA8C, 0x3C20, 0x3C1F, 0x8C16, 0x8C15, 0xD87C, 0xD87B, 0xFD47, 0xFD46]); }

sm_main_exec.js

pols.lJmpnCondValue[i] = jmpnCondValue & JMPN_COND_MASK; jmpnCondValue = jmpnCondValue >> JMPN_COND_VALUE_BITS; for (let index = 0; index < H_JMPN_COND_VALUE_BITS_LENGTH; ++index) { pols.hJmpnCondValueBit[index][i] = jmpnCondValue & 0x01n; jmpnCondValue = jmpnCondValue >> 1n; }

  3. I saw that there was an implementation before fork6, which is different from the current implementation of fork9,

buildRange(pols, N, 'GL_SIGNED_22BITS', -(2n 22), (2n 22) - 1n);

 The implementation of the buildByte2Bits16 at this time is like this

function buildByte2Bits16(pols, N) { let p = 0; // when SEL_BYTE2_BIT19 is zero, only values from 0 to (216)-1 are included for (let i = 0; i < 2 16; ++i) { pols.SEL_BYTE2_BIT19[p] = 0n; pols.BYTE2_BIT19[p] = BigInt(i); ++p; }

// when SEL_BYTE2_BIT19 is one, only values from 0 to (2**19)-1 are included
for (let i = 0; i < 2 ** 19; ++i) {
    pols.SEL_BYTE2_BIT19[p] = 1n;
    pols.BYTE2_BIT19[p] = BigInt(i);
    ++p;
}
// fill to end with zero and zero, a valid combination
for (let i = p; i < N; ++i) {
    pols.SEL_BYTE2_BIT19[i] = 0n;
    pols.BYTE2_BIT19[i] = 0n;
}

}

Is there any connection between the `GL_SIGNED_22BITS` and `SEL_BYTE2_BIT19`?