Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

jmp static addr #97

Merged
merged 5 commits into from
Dec 9, 2022
Merged

jmp static addr #97

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
5a5e05c
first jmp addr implementation
zkronos73 Nov 30, 2022
8f5029e
add new instructions JMPx and HASHx
zkronos73 Dec 9, 2022
a4d6da1
Merge branch 'develop' into jmp-static-addr
zkronos73 Dec 9, 2022
784e726
minor fixs
zkronos73 Dec 9, 2022
9901f0d
Merge branch 'develop' into jmp-static-addr
zkronos73 Dec 9, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
144 changes: 83 additions & 61 deletions pil/main.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,8 @@ namespace Main(%N);
pol commit CONST7, CONST6, CONST5, CONST4, CONST3, CONST2, CONST1, CONST0;
pol commit FREE7, FREE6, FREE5, FREE4, FREE3, FREE2, FREE1, FREE0;
pol commit inA, inB, inC, inROTL_C, inD, inE, inSR, inFREE, inCTX, inSP, inPC, inGAS, inMAXMEM, inSTEP, inRR, inHASHPOS, inRCX;
pol commit setA, setB, setC, setD, setE, setSR, setCTX, setSP, setPC, setGAS, setMAXMEM, JMP, JMPN, JMPC, setRR, setHASHPOS, setRCX;
pol commit offset;
pol commit setA, setB, setC, setD, setE, setSR, setCTX, setSP, setPC, setGAS, setMAXMEM, setRR, setHASHPOS, setRCX;
pol commit JMP, JMPN, JMPC, JMPZ, offset;
pol commit incStack;
pol commit isStack;
pol commit isMem;
Expand All @@ -64,18 +64,17 @@ namespace Main(%N);
pol commit sWR, sRD;
pol commit arithEq0, arithEq1, arithEq2;
pol commit memAlignRD, memAlignWR, memAlignWR8;
pol commit hashK, hashKLen, hashKDigest;
pol commit hashP, hashPLen, hashPDigest;
pol commit hashK, hashK1, hashKLen, hashKDigest;
pol commit hashP, hashP1, hashPLen, hashPDigest;
pol commit bin;
pol commit binOpcode;
pol commit assert;
pol commit repeat;
pol commit repeat, call, return;

/////// Intermediary commit polynomials
pol commit isNeg;
pol commit isMaxMem;


/// Counters
pol commit cntArith, cntBinary, cntMemAlign, cntKeccakF, cntPoseidonG, cntPaddingPG;
pol commit inCntArith, inCntBinary, inCntMemAlign, inCntKeccakF, inCntPoseidonG, inCntPaddingPG;
Expand Down Expand Up @@ -236,6 +235,11 @@ namespace Main(%N);
pol RCXIsZero = 1 - RCX*RCXInv;
RCXIsZero*RCX = 0;

/// op0 check zero
pol commit op0Inv;
pol op0IsZero = 1 - op0*op0Inv;
op0IsZero*op0 = 0;

/////// MAXMEM intermediary vals New State

pol diffMem = isMaxMem* ( (maxMemRel - MAXMEM) -
Expand Down Expand Up @@ -306,20 +310,31 @@ namespace Main(%N);
CTX' = setCTX * (op0 - CTX) + CTX;
SP' = setSP * (op0 - (SP +incStack)) + (SP +incStack);
PC' = setPC * (op0 - PC) + PC;
RR' = setRR * (op0 - RR) + RR;

// ROM constraint: call * setRR = 0
RR' = setRR * (op0 - RR) + call * (zkPC + 1 - RR) + RR;
GAS' = setGAS * (op0 - GAS) + GAS;

pol decRCX = repeat * (1-RCXIsZero);
RCX' = setRCX * (op0 - (RCX-decRCX)) + (RCX-decRCX);

MAXMEM' = setMAXMEM * (op0 - maxMemCalculated) + maxMemCalculated;

HASHPOS' = setHASHPOS * (op0 - HASHPOS) + HASHPOS + (hashK + hashP)*D0;
HASHPOS' = setHASHPOS * (op0 - HASHPOS) + HASHPOS + (hashK + hashP)*D0 + hashK1 + hashP1;

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 doJMP = JMPN*isNeg + JMP + JMPC*carry;
// ROM/Zkasm constraint: useJmpAddr * return = 0
pol finalJmpAddr = useJmpAddr * (jmpAddr - addr ) + return * (RR - addr) + addr;
pol nextNoJmpZkPC = zkPC + 1 - ((1-RCXIsZero)*repeat);

zkPC' = doJMP * (addr - (zkPC+1-decRCX)) +
(zkPC+1-decRCX);
// if elseAddr wasn't specified on zkasm, compiler put current address + 1
zkPC' = doJMP * (finalJmpAddr - nextNoJmpZkPC) + elseJMP * (elseAddr - nextNoJmpZkPC) + nextNoJmpZkPC;

(A0-op0)*assert = 0;
(A1-op1)*assert = 0;
Expand Down Expand Up @@ -440,7 +455,7 @@ namespace Main(%N);

/*
code generated with:
node tools/pil_pol_table/bits_compose.js "arithEq0,arithEq1,arithEq2,assert,bin,hashK,hashKDigest,hashKLen,hashP,hashPDigest,hashPLen,ind,indRR,isMem,isStack,JMP,JMPC,JMPN,memAlignRD,memAlignWR,memAlignWR8,mOp,mWR,repeat,setA,setB,setC,setCTX,setD,setE,setGAS,setHASHPOS,setMAXMEM,setPC,setRCX,setRR,setSP,setSR,sRD,sWR,useCTX" -b
node tools/pil_pol_table/bits_compose.js "arithEq0,arithEq1,arithEq2,assert,bin,hashK,hashKDigest,hashKLen,hashP,hashPDigest,hashPLen,ind,indRR,isMem,isStack,JMP,JMPC,JMPN,memAlignRD,memAlignWR,memAlignWR8,mOp,mWR,repeat,setA,setB,setC,setCTX,setD,setE,setGAS,setHASHPOS,setMAXMEM,setPC,setRCX,setRR,setSP,setSR,sRD,sWR,useCTX,useJmpAddr,JMPZ,call,return,hashK1,hashP1" -b
*/

pol operations =
Expand All @@ -454,62 +469,69 @@ namespace Main(%N);
+ 2**28 * setD + 2**29 * setE + 2**30 * setGAS + 2**31 * setHASHPOS
+ 2**32 * setMAXMEM + 2**33 * setPC + 2**34 * setRCX + 2**35 * setRR
+ 2**36 * setSP + 2**37 * setSR + 2**38 * sRD + 2**39 * sWR
+ 2**40 * useCTX;

(1 - arithEq0) * arithEq0 = 0;
(1 - arithEq1) * arithEq1 = 0;
(1 - arithEq2) * arithEq2 = 0;
(1 - assert) * assert = 0;
(1 - bin) * bin = 0;
(1 - hashK) * hashK = 0;
(1 - hashKDigest) * hashKDigest = 0;
(1 - hashKLen) * hashKLen = 0;
(1 - hashP) * hashP = 0;
(1 - hashPDigest) * hashPDigest = 0;
(1 - hashPLen) * hashPLen = 0;
(1 - ind) * ind = 0;
(1 - indRR) * indRR = 0;
(1 - isMem) * isMem = 0;
(1 - isStack) * isStack = 0;
(1 - JMP) * JMP = 0;
(1 - JMPC) * JMPC = 0;
(1 - JMPN) * JMPN = 0;
(1 - memAlignRD) * memAlignRD = 0;
(1 - memAlignWR) * memAlignWR = 0;
(1 - memAlignWR8) * memAlignWR8 = 0;
(1 - mOp) * mOp = 0;
(1 - mWR) * mWR = 0;
(1 - repeat) * repeat = 0;
(1 - setA) * setA = 0;
(1 - setB) * setB = 0;
(1 - setC) * setC = 0;
(1 - setCTX) * setCTX = 0;
(1 - setD) * setD = 0;
(1 - setE) * setE = 0;
(1 - setGAS) * setGAS = 0;
(1 - setHASHPOS) * setHASHPOS = 0;
(1 - setMAXMEM) * setMAXMEM = 0;
(1 - setPC) * setPC = 0;
(1 - setRCX) * setRCX = 0;
(1 - setRR) * setRR = 0;
(1 - setSP) * setSP = 0;
(1 - setSR) * setSR = 0;
(1 - sRD) * sRD = 0;
(1 - sWR) * sWR = 0;
(1 - useCTX) * useCTX = 0;
+ 2**40 * useCTX + 2**41 * useJmpAddr + 2**42 * JMPZ + 2**43 * call
+ 2**44 * return + 2**45 * hashK1 + 2**46 * hashP1;

(1 - arithEq0) * arithEq0 = 0;
(1 - arithEq1) * arithEq1 = 0;
(1 - arithEq2) * arithEq2 = 0;
(1 - assert) * assert = 0;
(1 - bin) * bin = 0;
(1 - hashK) * hashK = 0;
(1 - hashKDigest) * hashKDigest = 0;
(1 - hashKLen) * hashKLen = 0;
(1 - hashP) * hashP = 0;
(1 - hashPDigest) * hashPDigest = 0;
(1 - hashPLen) * hashPLen = 0;
(1 - ind) * ind = 0;
(1 - indRR) * indRR = 0;
(1 - isMem) * isMem = 0;
(1 - isStack) * isStack = 0;
(1 - JMP) * JMP = 0;
(1 - JMPC) * JMPC = 0;
(1 - JMPN) * JMPN = 0;
(1 - memAlignRD) * memAlignRD = 0;
(1 - memAlignWR) * memAlignWR = 0;
(1 - memAlignWR8) * memAlignWR8 = 0;
(1 - mOp) * mOp = 0;
(1 - mWR) * mWR = 0;
(1 - repeat) * repeat = 0;
(1 - setA) * setA = 0;
(1 - setB) * setB = 0;
(1 - setC) * setC = 0;
(1 - setCTX) * setCTX = 0;
(1 - setD) * setD = 0;
(1 - setE) * setE = 0;
(1 - setGAS) * setGAS = 0;
(1 - setHASHPOS) * setHASHPOS = 0;
(1 - setMAXMEM) * setMAXMEM = 0;
(1 - setPC) * setPC = 0;
(1 - setRCX) * setRCX = 0;
(1 - setRR) * setRR = 0;
(1 - setSP) * setSP = 0;
(1 - setSR) * setSR = 0;
(1 - sRD) * sRD = 0;
(1 - sWR) * sWR = 0;
(1 - useCTX) * useCTX = 0;
(1 - useJmpAddr) * useJmpAddr = 0;
(1 - JMPZ) * JMPZ = 0;
(1 - call) * call = 0;
(1 - return) * return = 0;
(1 - hashK1) * hashK1 = 0;
(1 - hashP1) * hashP1 = 0;

{
CONST0, CONST1, CONST2, CONST3, CONST4, CONST5, CONST6, CONST7,
inA, inB, inC, inROTL_C, inD, inE, inSR, inFREE,
inCTX, inSP, inPC, inGAS, inMAXMEM, inHASHPOS, inSTEP, inRR, inHASHPOS, inRCX,
inCntArith, inCntBinary, inCntKeccakF, inCntMemAlign, inCntPaddingPG, inCntPoseidonG,
operations, offset, incStack, binOpcode, zkPC
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.inMAXMEM, Rom.inHASHPOS, Rom.inSTEP, Rom.inRR, Rom.inHASHPOS, Rom.inRCX,
Rom.inCntArith, Rom.inCntBinary, Rom.inCntKeccakF, Rom.inCntMemAlign, Rom.inCntPaddingPG, Rom.inCntPoseidonG,
Rom.operations, Rom.offset, Rom.incStack, Rom.binOpcode, Rom.line
Rom.operations, Rom.offset, Rom.incStack, Rom.binOpcode, Rom.jmpAddr, Rom.elseAddr, Rom.line
};

pol commit sKeyI[4];
Expand Down Expand Up @@ -648,10 +670,10 @@ namespace Main(%N);
/////////
// HASHK Plookpups
/////////
hashK {
hashK + hashK1 {
addr,
HASHPOS,
D0,
D0 * hashK + hashK1,
op0, op1, op2, op3,
op4, op5, op6, op7
} in
Expand Down Expand Up @@ -690,10 +712,10 @@ namespace Main(%N);
/////////
// HASHP Plookpups
/////////
hashP {
hashP + hashP1 {
addr,
HASHPOS,
D0,
D0 * hashP + hashP1,
op0, op1, op2, op3,
op4, op5, op6, op7
} in
Expand Down
29 changes: 16 additions & 13 deletions pil/rom.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,25 +14,28 @@ namespace Rom(%N);
pol constant inCntArith, inCntBinary, inCntKeccakF, inCntMemAlign, inCntPaddingPG, inCntPoseidonG;
pol constant incStack;
pol constant binOpcode;
pol constant jmpAddr, elseAddr;

pol constant line;

pol constant operations;

/*

comment genereated with:
node tools/pil_pol_table/bits_compose.js "arithEq0,arithEq1,arithEq2,assert,bin,hashK,hashKDigest,hashKLen,hashP,hashPDigest,hashPLen,ind,indRR,isMem,isStack,JMP,JMPC,JMPN,memAlignRD,memAlignWR,memAlignWR8,mOp,mWR,repeat,setA,setB,setC,setCTX,setD,setE,setGAS,setHASHPOS,setMAXMEM,setPC,setRCX,setRR,setSP,setSR,sRD,sWR,useCTX"
node tools/pil_pol_table/bits_compose.js "arithEq0,arithEq1,arithEq2,assert,bin,hashK,hashKDigest,hashKLen,hashP,hashPDigest,hashPLen,ind,indRR,isMem,isStack,JMP,JMPC,JMPN,memAlignRD,memAlignWR,memAlignWR8,mOp,mWR,repeat,setA,setB,setC,setCTX,setD,setE,setGAS,setHASHPOS,setMAXMEM,setPC,setRCX,setRR,setSP,setSR,sRD,sWR,useCTX,useJmpAddr,JMPZ,call,return,hashK1,hashP1"

operations =
2**0 * arithEq0 + 2**1 * arithEq1 + 2**2 * arithEq2 + 2**3 * assert
+ 2**4 * bin + 2**5 * hashK + 2**6 * hashKDigest + 2**7 * hashKLen
+ 2**8 * hashP + 2**9 * hashPDigest + 2**10 * hashPLen + 2**11 * ind
+ 2**12 * indRR + 2**13 * isMem + 2**14 * isStack + 2**15 * JMP
+ 2**16 * JMPC + 2**17 * JMPN + 2**18 * memAlignRD + 2**19 * memAlignWR
+ 2**20 * memAlignWR8 + 2**21 * mOp + 2**22 * mWR + 2**23 * repeat
+ 2**24 * setA + 2**25 * setB + 2**26 * setC + 2**27 * setCTX
+ 2**28 * setD + 2**29 * setE + 2**30 * setGAS + 2**31 * setHASHPOS
+ 2**32 * setMAXMEM + 2**33 * setPC + 2**34 * setRCX + 2**35 * setRR
+ 2**36 * setSP + 2**37 * setSR + 2**38 * sRD + 2**39 * sWR
+ 2**40 * useCTX + 2**41 * useJmpAddr + 2**42 * JMPZ + 2**43 * call
+ 2**44 * return + 2**45 * hashK1 + 2**46 * hashP1;

operations = 2**0 * arithEq0 + 2**1 * arithEq1 + 2**2 * arithEq2 + 2**3 * assert
+ 2**4 * bin + 2**5 * hashK + 2**6 * hashKDigest + 2**7 * hashKLen
+ 2**8 * hashP + 2**9 * hashPDigest + 2**10 * hashPLen + 2**11 * ind
+ 2**12 * indRR + 2**13 * isMem + 2**14 * isStack + 2**15 * JMP
+ 2**16 * JMPC + 2**17 * JMPN + 2**18 * memAlignRD + 2**19 * memAlignWR
+ 2**20 * memAlignWR8 + 2**21 * mOp + 2**22 * mWR + 2**23 * repeat
+ 2**24 * setA + 2**25 * setB + 2**26 * setC + 2**27 * setCTX
+ 2**28 * setD + 2**29 * setE + 2**30 * setGAS + 2**31 * setHASHPOS
+ 2**32 * setMAXMEM + 2**33 * setPC + 2**34 * setRCX + 2**35 * setRR
+ 2**36 * setSP + 2**37 * setSR + 2**38 * sRD + 2**39 * sWR
+ 2**40 * useCTX
*/
Loading