---
# System prepended metadata

title: '==='

---

Polygon ZKEVM PIL Constraints
===

### main.pil 19 - 33

definition of **Generic Registers**

A, B, C, D, E

### main.pil 35 - 36
definition of evm register **Additional Registers**


### main.pil 45 - 56
definition of intermediate register **Intermediate Registers**
CONST, FREE, in.., set.., JMP(N, C, Z, offset), incStark, isStack, isMem, ind, indRR, useCTX, carry.

### main.pil 58 - 76
    pol commit mOp, mWR; // memory Operation, memory Write
    pol commit sWR, sRD; // storage Write, storage Read
    pol commit arithEq0, arithEq1, arithEq2; // arithEq type

    pol commit memAlignRD, memAlignWR, memAlignWR8;
    pol commit hashK, hashK1, hashKLen, hashKDigest; // keccak
    pol commit hashP, hashP1, hashPLen, hashPDigest; // poseidon
    pol commit bin; // is binary operations
    pol commit binOpcode; // binary opcode (ADD, SUB, AND, OR, XOR)



    pol commit assert;
    pol commit repeat, call, return; // Call related
    pol commit isNeg;

    pol commit cntArith, cntBinary, cntMemAlign, cntKeccakF, cntPoseidonG, cntPaddingPG;
    pol commit inCntArith, inCntBinary, inCntMemAlign, inCntKeccakF, inCntPoseidonG, inCntPaddingPG;
    pol commit incCounter;

### main.pil 83 - 186

    /////// op
    pol op0 =
        A0 * inA +
        B0 * inB +
        C0 * inC +
        C7 * inROTL_C +
        D0 * inD +
        E0 * inE +
        FREE0 * inFREE +
        SR0 * inSR +
        CTX * inCTX +
        SP * inSP +
        PC * inPC +
        GAS * inGAS +
        Global.STEP * inSTEP +
        RR * inRR +
        HASHPOS * inHASHPOS +
        cntArith * inCntArith +
        cntBinary * inCntBinary +
        cntMemAlign * inCntMemAlign +
        cntKeccakF * inCntKeccakF +
        cntPoseidonG * inCntPoseidonG +
        cntPaddingPG * inCntPaddingPG +
        RCX * inRCX +
        CONST0; // const has no selector, for it will be 0
        
    pol op1 =
        A1 * inA +
        B1 * inB +
        C1 * inC +
        C0 * inROTL_C +
        D1 * inD +
        E1 * inE +
        SR1 * inSR +
        FREE1 * inFREE +
        CONST1;

    ...
    
### main.pil 202-226

    /////// isNeg

    pol commit lJmpnCondValue;
    pol jmpnCondValue = JMPN*(isNeg*2**32 + op0);
    isNeg * (1 - isNeg) = 0;

    lJmpnCondValue in Global.STEP;

    pol commit hJmpnCondValueBit[9];

    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[8] + 2**30*hJmpnCondValueBit[7] + 2**29*hJmpnCondValueBit[6] + 2**28*hJmpnCondValueBit[5] +
                    2**27*hJmpnCondValueBit[4] + 2**26*hJmpnCondValueBit[3] + 2**25*hJmpnCondValueBit[2] + 2**24*hJmpnCondValueBit[1] +
                    2**23*hJmpnCondValueBit[0] + lJmpnCondValue;
                    
 
 https://github.com/0xPolygonHermez/zkasmcom/blob/main/instructions.md
 
 JMPN constraint op0 to be in $[-2^{32}, 2^{32}]$
 
 
 ### main.pil 227-235
     /// RCX check zero
    pol commit RCXInv;
    pol RCXIsZero = 1 - RCX*RCXInv;
    RCXIsZero*RCX = 0;

    /// op0 check zero
    pol commit op0Inv;
    pol op0IsZero = 1 - op0*op0Inv;
    op0IsZero*op0 = 0;
    
### main.pil 237-306

set A,B,C,D,E,SR,CTX,SP,PC,RR,GAS,RCX,HASHPOS

    A0' = setA * (op0 - A0) + A0;
    A1' = setA * (op1 - A1) + A1;
    A2' = setA * (op2 - A2) + A2;
    A3' = setA * (op3 - A3) + A3;
    A4' = setA * (op4 - A4) + A4;
    A5' = setA * (op5 - A5) + A5;
    A6' = setA * (op6 - A6) + A6;
    A7' = setA * (op7 - A7) + A7;

    B0' = setB * (op0 - B0) + B0;
    B1' = setB * (op1 - B1) + B1;
    B2' = setB * (op2 - B2) + B2;
    B3' = setB * (op3 - B3) + B3;
    B4' = setB * (op4 - B4) + B4;
    B5' = setB * (op5 - B5) + B5;
    B6' = setB * (op6 - B6) + B6;
    B7' = setB * (op7 - B7) + B7;

    C0' = setC * (op0 - C0) + C0;
    C1' = setC * (op1 - C1) + C1;
    C2' = setC * (op2 - C2) + C2;
    C3' = setC * (op3 - C3) + C3;
    C4' = setC * (op4 - C4) + C4;
    C5' = setC * (op5 - C5) + C5;
    C6' = setC * (op6 - C6) + C6;
    C7' = setC * (op7 - C7) + C7;

    D0' = setD * (op0 - D0) + D0;
    D1' = setD * (op1 - D1) + D1;
    D2' = setD * (op2 - D2) + D2;
    D3' = setD * (op3 - D3) + D3;
    D4' = setD * (op4 - D4) + D4;
    D5' = setD * (op5 - D5) + D5;
    D6' = setD * (op6 - D6) + D6;
    D7' = setD * (op7 - D7) + D7;

    E0' = setE * (op0 - E0) + E0;
    E1' = setE * (op1 - E1) + E1;
    E2' = setE * (op2 - E2) + E2;
    E3' = setE * (op3 - E3) + E3;
    E4' = setE * (op4 - E4) + E4;
    E5' = setE * (op5 - E5) + E5;
    E6' = setE * (op6 - E6) + E6;
    E7' = setE * (op7 - E7) + E7;

    SR0' = setSR * (op0 - SR0) + SR0;
    SR1' = setSR * (op1 - SR1) + SR1;
    SR2' = setSR * (op2 - SR2) + SR2;
    SR3' = setSR * (op3 - SR3) + SR3;
    SR4' = setSR * (op4 - SR4) + SR4;
    SR5' = setSR * (op5 - SR5) + SR5;
    SR6' = setSR * (op6 - SR6) + SR6;
    SR7' = setSR * (op7 - SR7) + SR7;

    SP' = setSP * (op0 - (SP +incStack)) + (SP +incStack);
    // call * RR = 0
    RR' = setRR * (op0 - RR) + call * (zkPC + 1 - RR) + RR;
    
### main.pil 307-324

jump related

    pol doJMP = JMPN*isNeg + JMP + JMPC*carry + JMPZ*op0IsZero + return + call;
    pol elseJMP = JMPN*(1-isNeg) + JMPC*(1-carry) + JMPZ*(1-op0IsZero);
    
    pol commit jmpAddr;
    pol commit elseAddr;
    pol commit useJmpAddr;
    pol commit useElseAddr;
    
    pol finalJmpAddr = useJmpAddr * (jmpAddr - addr) + return * (RR - addr) + addr;
    pol nextNoJmpZkPC = zkPC + 1 - ((1-RCXIsZero)*repeat);
    pol finalElseAddr = useElseAddr * (elseAddr - nextNoJmpZkPC) + nextNoJmpZkPC;
    
     // if elseAddr wasn't specified on zkasm, compiler put current address + 1
    zkPC' = doJMP * (finalJmpAddr - nextNoJmpZkPC) + elseJMP * (finalElseAddr - nextNoJmpZkPC) + nextNoJmpZkPC;
    zkPC * Global.L1 = 0;
    
### main.pil 325-333
asserting

### main.pil 335-430
oldStateRoot -> newStateRoot
oldAccInputHash -> newAccInputHash
oldBatchNum -> newBatchNum
chainId -> |>|
forkId -> |>|
|>| -> localExitRoot
![00010121_0017039506](https://docs.polygon.technology/img/zkEVM/04circom-batch-prover.png)

### main.pil 434-440
    // Check that the calculated hash is well formed
    sWR + hashPDigest {
        op0, op1, op2, op3, op4, op5, op6, op7
    } is
    Binary.resultValidRange {
        Binary.a[0], Binary.a[1], Binary.a[2], Binary.a[3], Binary.a[4], Binary.a[5], Binary.a[6], Binary.a[7]
    };


### main.pil 442-530
    /////////
    // ROM Plookpups
    /////////
    
        {
        CONST0, CONST1, CONST2, CONST3, CONST4, CONST5, CONST6, CONST7,
        inA, inB, inC, inROTL_C, inD, inE, inSR, inFREE,
        inCTX, inSP, inPC, inGAS, inHASHPOS, inSTEP, inRR, inRCX,
        inCntArith, inCntBinary, inCntKeccakF, inCntMemAlign, inCntPaddingPG, inCntPoseidonG,
        operations, offset, incStack, binOpcode, jmpAddr, elseAddr, zkPC
    } in {
        Rom.CONST0, Rom.CONST1, Rom.CONST2, Rom.CONST3, Rom.CONST4, Rom.CONST5, Rom.CONST6, Rom.CONST7,
        Rom.inA, Rom.inB, Rom.inC, Rom.inROTL_C, Rom.inD, Rom.inE, Rom.inSR, Rom.inFREE,
        Rom.inCTX, Rom.inSP, Rom.inPC, Rom.inGAS, Rom.inHASHPOS, Rom.inSTEP, Rom.inRR, Rom.inRCX,
        Rom.inCntArith, Rom.inCntBinary, Rom.inCntKeccakF, Rom.inCntMemAlign, Rom.inCntPaddingPG, Rom.inCntPoseidonG,
        Rom.operations, Rom.offset, Rom.incStack, Rom.binOpcode, Rom.jmpAddr, Rom.elseAddr, Rom.line
    };


### main.pil 640-658 Binary
    bin {
        binOpcode,
        A0, A1, A2, A3, A4, A5, A6, A7,
        B0, B1, B2, B3, B4, B5, B6, B7,
        op0, op1, op2, op3, op4, op5, op6, op7,
        carry
    } is
    Binary.resultBinOp {
        Binary.lOpcode,
        Binary.a[0], Binary.a[1], Binary.a[2], Binary.a[3], Binary.a[4], Binary.a[5], Binary.a[6], Binary.a[7],
        Binary.b[0], Binary.b[1], Binary.b[2], Binary.b[3], Binary.b[4], Binary.b[5], Binary.b[6], Binary.b[7],
        Binary.c[0], Binary.c[1], Binary.c[2], Binary.c[3], Binary.c[4], Binary.c[5], Binary.c[6], Binary.c[7],
        Binary.lCout
    };

    cntBinary' = cntBinary*(1-Global.L1) + bin + sWR + hashPDigest;

### main.pil 660-704 Keccak
    /////////
    // HASHK Plookpups
    /////////
        hashK + hashK1 {
            addr,
            HASHPOS,
            D0 * hashK + hashK1,
            op0, op1, op2, op3,
            op4, op5, op6, op7
        } in
        PaddingKK.crLatch * PaddingKK.r8valid {
            PaddingKK.addr,
            PaddingKK.len - PaddingKK.rem - PaddingKK.crLen + 1,
            PaddingKK.crLen,
            PaddingKK.crV0C, PaddingKK.crV1C, PaddingKK.crV2C, PaddingKK.crV3C,
            PaddingKK.crV4C, PaddingKK.crV5C, PaddingKK.crV6C, PaddingKK.crV7C
        };

    hashKLen {
        addr,
        op0
    } is
    PaddingKK.lastHashLen {
        PaddingKK.addr,
        PaddingKK.len
    };

    hashKDigest {
        addr,
        op0, op1, op2, op3,
        op4, op5, op6, op7,
        incCounter
    } is
    PaddingKK.lastHashDigest {
        PaddingKK.addr,
        PaddingKK.hash0, PaddingKK.hash1, PaddingKK.hash2, PaddingKK.hash3,
        PaddingKK.hash4, PaddingKK.hash5, PaddingKK.hash6, PaddingKK.hash7,
        PaddingKK.incCounter
    };

    cntKeccakF' = cntKeccakF*(1-Global.L1) + incCounter*hashKDigest;

### main.pil 705-748 Poseidon

    /////////
    // HASHP Plookpups
    /////////
        hashP + hashP1 {
            addr,
            HASHPOS,
            D0 * hashP + hashP1,
            op0, op1, op2, op3,
            op4, op5, op6, op7
        } in
        PaddingPG.crLatch * PaddingPG.crValid {
            PaddingPG.addr,
            PaddingPG.len - PaddingPG.rem - PaddingPG.crLen + 1,
            PaddingPG.crLen,
            PaddingPG.crV0C, PaddingPG.crV1C, PaddingPG.crV2C, PaddingPG.crV3C,
            PaddingPG.crV4C, PaddingPG.crV5C, PaddingPG.crV6C, PaddingPG.crV7C
        };

    hashPLen {
        addr,
        op0
    } is
    PaddingPG.lastHashLen {
        PaddingPG.addr,
        PaddingPG.len
    };

    hashPDigest {
        addr,
        op0 + 2**32 * op1,
        op2 + 2**32 * op3,
        op4 + 2**32 * op5,
        op6 + 2**32 * op7,
        incCounter
    } is
    PaddingPG.lastHashDigest {
        PaddingPG.addr,
        PaddingPG.curHash0,
        PaddingPG.curHash1,
        PaddingPG.curHash2,
        PaddingPG.curHash3,
        PaddingPG.incCounter
    };

    cntPaddingPG' = cntPaddingPG*(1-Global.L1) + hashPDigest*incCounter;
    cntPoseidonG' = cntPoseidonG*(1-Global.L1) + (hashPDigest + sRD + sWR) * incCounter;



### main.pil 749-768 Memory

    /////////
    // Mem Plookpups
    /////////
        mOp {
            addr,
            Global.STEP,
            mWR,
            op0, op1, op2, op3,
            op4, op5, op6, op7
        } is
        Mem.mOp {
            Mem.addr,
            Mem.step,
            Mem.mWr,
            Mem.val[0], Mem.val[1], Mem.val[2], Mem.val[3],
            Mem.val[4], Mem.val[5], Mem.val[6], Mem.val[7]
        };


### main.pil 769-856 Storage

    /////////
    // Storage Plookpups
    /////////

    (sRD + sWR) {
        1, 0, 0, // Poseidon Result ID
        C0, C1, C2, C3, C4, C5, C6, C7,
        0, 0, 0, 0,
        sKeyI[0], sKeyI[1], sKeyI[2], sKeyI[3]
    } is
    PoseidonG.result1 {
        PoseidonG.result1, PoseidonG.result2, PoseidonG.result3,
        PoseidonG.in0,
        PoseidonG.in1,
        PoseidonG.in2,
        PoseidonG.in3,
        PoseidonG.in4,
        PoseidonG.in5,
        PoseidonG.in6,
        PoseidonG.in7,
        PoseidonG.hashType,
        PoseidonG.cap1,
        PoseidonG.cap2,
        PoseidonG.cap3,
        PoseidonG.hash0,
        PoseidonG.hash1,
        PoseidonG.hash2,
        PoseidonG.hash3
    };

    (sRD + sWR) {
        0, 1, 0,
        A0, A1, A2, A3, A4, 0, B0, B1,
        sKeyI[0], sKeyI[1], sKeyI[2], sKeyI[3],
        sKey[0], sKey[1], sKey[2], sKey[3],
        A5, A6, A7, B2, B3, B4, B5, B6, B7 } is
    PoseidonG.result2 {
        PoseidonG.result1, PoseidonG.result2, PoseidonG.result3,
        PoseidonG.in0,
        PoseidonG.in1,
        PoseidonG.in2,
        PoseidonG.in3,
        PoseidonG.in4,
        PoseidonG.in5,
        PoseidonG.in6,
        PoseidonG.in7,
        PoseidonG.hashType,
        PoseidonG.cap1,
        PoseidonG.cap2,
        PoseidonG.cap3,
        PoseidonG.hash0,
        PoseidonG.hash1,
        PoseidonG.hash2,
        PoseidonG.hash3,
        0, 0, 0, 0, 0, 0, 0, 0, 0
    };

    sRD {
        SR0 + 2**32*SR1, SR2 + 2**32*SR3, SR4 + 2**32*SR5, SR6 + 2**32*SR7,
        sKey[0], sKey[1], sKey[2], sKey[3],
        op0, op1, op2, op3,
        op4, op5, op6, op7,
        incCounter
    } is
    Storage.iLatchGet {
        Storage.oldRoot0, Storage.oldRoot1, Storage.oldRoot2, Storage.oldRoot3,
        Storage.rkey0, Storage.rkey1, Storage.rkey2, Storage.rkey3,
        Storage.valueLow0, Storage.valueLow1, Storage.valueLow2, Storage.valueLow3,
        Storage.valueHigh0, Storage.valueHigh1, Storage.valueHigh2, Storage.valueHigh3,
        Storage.incCounter + 2
    };


    sWR {
        SR0 + 2**32*SR1, SR2 + 2**32*SR3, SR4 + 2**32*SR5, SR6 + 2**32*SR7,
        sKey[0], sKey[1], sKey[2], sKey[3],
        D0, D1, D2, D3,
        D4, D5, D6, D7,
        op0 + 2**32*op1, op2 + 2**32*op3, op4 + 2**32*op5, op6 + 2**32*op7,
        incCounter
    } is
    Storage.iLatchSet {
        Storage.oldRoot0, Storage.oldRoot1, Storage.oldRoot2, Storage.oldRoot3,
        Storage.rkey0, Storage.rkey1, Storage.rkey2, Storage.rkey3,
        Storage.valueLow0, Storage.valueLow1, Storage.valueLow2, Storage.valueLow3,
        Storage.valueHigh0, Storage.valueHigh1, Storage.valueHigh2, Storage.valueHigh3,
        Storage.newRoot0, Storage.newRoot1, Storage.newRoot2, Storage.newRoot3,
        Storage.incCounter + 2
    };