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

### 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
};