Skip to content

Commit

Permalink
Merge pull request #227 from 0xPolygonHermez/develop
Browse files Browse the repository at this point in the history 
Develop
  • Loading branch information
@krlosMata
krlosMata committed Nov 22, 2023
2 parents 84ca95f + 4a71ccc commit 07d9299
Show file tree
Hide file tree
Showing 224 changed files with 375,754 additions and 121 deletions.
6 changes: 3 additions & 3 deletions .github/workflows/main.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ name: Main CI

on:
pull_request:
branches:
branches:
- main
- develop
push:
Expand All @@ -30,7 +30,7 @@ jobs:
- name: Clone repos
run: |
cd ..
git clone https://github.com/0xPolygonHermez/zkevm-testvectors.git --branch v2.0.0-fork.5
git clone https://github.com/0xPolygonHermez/zkevm-testvectors.git --branch v3.0.0-rc.1-fork.6
cd zkevm-testvectors/tools/ethereum-tests
git clone https://github.com/0xPolygonHermez/ethereum-tests tests
cd tests
Expand All @@ -44,4 +44,4 @@ jobs:
chmod -R 777 tools
npm run test:full-tracer
- name: eslint:tracer
run: npm run eslint:tracer
run: npm run eslint:tracer
1 change: 1 addition & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,3 +17,4 @@ pil-config.json
parallel-tests
verbose-config.json
*.stats
tools/full-tracer-tests/ft-traces/
10 changes: 5 additions & 5 deletions package.json
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"name": "@0xpolygonhermez/zkevm-proverjs",
"version": "1.1.0",
"version": "3.0.0",
"description": "JS version of the zkProver.",
"main": "index.js",
"config": {
Expand Down Expand Up @@ -118,8 +118,8 @@
"license": "UNLICENSED",
"dependencies": {
"@0xpolygonhermez/zkasmcom": "https://github.com/0xPolygonHermez/zkasmcom.git#v1.0.0",
"@0xpolygonhermez/zkevm-commonjs": "https://github.com/0xPolygonHermez/zkevm-commonjs.git#v2.0.0-fork.5",
"@0xpolygonhermez/zkevm-rom": "https://github.com/0xPolygonHermez/zkevm-rom.git#v2.0.0-fork.5",
"@0xpolygonhermez/zkevm-commonjs": "https://github.com/0xPolygonHermez/zkevm-commonjs.git#v3.0.0-fork.6",
"@0xpolygonhermez/zkevm-rom": "https://github.com/0xPolygonHermez/zkevm-rom.git#v3.0.0-fork.6",
"@0xpolygonhermez/zkevm-storage-rom": "https://github.com/0xPolygonHermez/zkevm-storage-rom.git#v1.0.0-fork.3",
"@grpc/grpc-js": "^1.8.14",
"chalk": "^3.0.0",
Expand All @@ -132,7 +132,7 @@
"fs": "^0.0.1-security",
"json-bigint": "^1.0.0",
"lodash": "^4.17.21",
"pil-stark": "https://github.com/0xPolygonHermez/pil-stark.git#develop",
"pil-stark": "https://github.com/0xPolygonHermez/pil-stark.git#b6f11e43459ec4c4d81af1dff9d68aed1b8c8cb2",
"pilcom": "0.0.23",
"snarkjs": "0.7.0",
"yargs": "^17.4.0"
Expand All @@ -146,4 +146,4 @@
"eslint-plugin-mocha": "^10.1.0",
"mocha": "^9.1.3"
}
}
}
212 changes: 205 additions & 7 deletions pil/arith.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,13 +30,218 @@ namespace Arith(%N);
pol commit q1[16];
pol commit q2[16];

pol commit selEq[4];

pol commit resultEq0;
pol commit resultEq1;
pol commit resultEq2;

resultEq0 * (1 - resultEq0) = 0;
resultEq1 * (1 - resultEq1) = 0;
resultEq2 * (1 - resultEq2) = 0;

// FEATURE:

// PRE: x1, x2 are alias free

// Verify that the x1 x2 are different when using the add function on elliptic curve with different points.

// In the first 16 clocks of 32 clocks cycle contains: x2[0]-x1[0], x2[1]-x1[1], ..., x2[15]-x1[15]
// In last 16 clocks of 32 clocks cycle all values was 0.
pol xDeltaChunk = x2[0]*Global.CLK32[0] + x2[1]*Global.CLK32[1] + x2[2]*Global.CLK32[2] + x2[3]*Global.CLK32[3] + x2[4]*Global.CLK32[4] + x2[5]*Global.CLK32[5] + x2[6]*Global.CLK32[6] + x2[7]*Global.CLK32[7]
+ x2[8]*Global.CLK32[8] + x2[9]*Global.CLK32[9] + x2[10]*Global.CLK32[10] + x2[11]*Global.CLK32[11] + x2[12]*Global.CLK32[12] + x2[13]*Global.CLK32[13] + x2[14]*Global.CLK32[14] + x2[15]*Global.CLK32[15]
- x1[0]*Global.CLK32[0] - x1[1]*Global.CLK32[1] - x1[2]*Global.CLK32[2] - x1[3]*Global.CLK32[3] - x1[4]*Global.CLK32[4] - x1[5]*Global.CLK32[5] - x1[6]*Global.CLK32[6] - x1[7]*Global.CLK32[7]
- x1[8]*Global.CLK32[8] - x1[9]*Global.CLK32[9] - x1[10]*Global.CLK32[10] - x1[11]*Global.CLK32[11] - x1[12]*Global.CLK32[12] - x1[13]*Global.CLK32[13] - x1[14]*Global.CLK32[14] - x1[15]*Global.CLK32[15];

// Inverse of current xDeltaChunk. Used to verify that xDeltaChunk was ≠ 0 ==> x1[i] ≠ x2[i].
// This inverse only calculated one clock by cycle when selEq[1] = 1.
pol commit xDeltaChunkInverse;

// Intermediate pol to define that in the current chunks of x1 and x2 are differents.
// IMPORTANT: xChunkDifferent == 1 ==> x1[i] ≠ x2[i]
// xChunkDifferent == 0 no implies anything, x1[i] ≠ x2[i] or x1[i] == x2[i].
// xChunkDifferent was binary, only when xDeltaChunkInverse === inv(xDeltaChunk), its value is 1.
pol xChunkDifferent = xDeltaChunk * xDeltaChunkInverse;

// Important, binary constraint
xChunkDifferent * (1 - xChunkDifferent) = 0;

// xDeltaChunk xDeltaChunkInverse xChunkDifferent
// ----------- ------------------ -----------------------
// 0 any 0 * any = 0 OK (A)
// x (≠ 0) 0 x * 0 = 0 OK (B)
// x (≠ 0) inv(x) x * inv(x) = 1 OK (C)
// x (≠ 0) y ≠ {inv(x),0} x * y = k (≠ 0,1) FAILS (D)
//
// (A) and (C) are the standard cases, but (B) was introduced to avoid calculate the inverse when
// it is not necessary. xChunkDifferent is well calculed because it's 1 only when x ≠ 0 and inverse
// it's calculated.

// xAreDifferent is used to indicate that in current clock we knows that x1 and x2 are different
pol commit xAreDifferent;

// Binary constraint
xAreDifferent * (1 - xAreDifferent) = 0;

// In first clock of 16 clocks cycle, xAreDifferent should not be considered
// Constraint to force next value of xAreDifferent

xAreDifferent' = xAreDifferent * (1 - Global.CLK32[0] - Global.CLK32[16]) + xChunkDifferent;

// xAreDifferent CLK0+CLK16 xChunkDifferent xAreDifferent'
// ------------- ---------- --------------- --------------
// 0 0 0 0 OK
// 0 0 1 1 OK
// 0 1 0 1 OK
// 0 1 1 1 OK
// 1 0 0 1 OK
// 1 0 1 2 FAILS (A)
// 1 1 0 1 OK
// 1 1 1 1 OK
//
// xChunkDifferent = 0 ==> (x2[i] - x1[i]) = 0
// xChunkDifferent = 1 ==> (x2[i] - x1[i]) ≠ 0 ==> x1 and x2 are different
// (A) forbidden, executor must control this situation, because expending an
// unnecessary inverse.

(xAreDifferent - selEq[1]) * Global.CLK32[16] = 0;

// COST: 2 commit, 2 im, 0 constant, 4 constraints



// FEATURE:
//
// Verify that the result of the addition is free of aliases, means x3 ∊ [0, FPEC-1] and y3 ∊ [0, FPEC-1]
//
// FPEC: 0xffffffffffffffffffffffffffffffffffffffffffffffffffff fffe 0000 fc2fn
//
// Approach, compare from most significant chunk to less significant chunk of x3,y3 (A). On each chunk,
// a chunkLtPrime indicates if the chunk is minor than the FPEC chunk. The valueLtPrime indicates when any
// previous chunk was minor than the FPEC chunk, and this implies that x3,y3 is minor than prime.
//
// (A) on first 16 clocks of 32 clocks cycle is verified x3
// on last 16 clocks of 32 clocks cycle is verified y3
//
// k x chunks equals (B) ===> 1 x chunk minor ===> (15 - k) x any 16 bits value
//
// (B) really I must verify that chunk are equal or minor, never greater at this point. If malicious prover (MAP)
// said is equal but it's minor, is its problem. At the end, it needs at least one minor chunk to be minor value.
//
// k x chunks ∊ [0,chunkPrime] => 1 x chunk ∊ [0, chunkPrime-1] => (15 - k) x chunk ∊ [0, 0xFFFF]
//
// CLK0 CLK12 CLK13 CLK14 CLK15
// max(chunkPrime(0..15)) = [0xFFFF, ..... , 0xFFFF, 0xFFFE, 0xFFFF, 0xFC2F]
// max(chunkPrime(0..15) - 1) = [0xFFFE, ..... , 0xFFFE, 0xFFFD, 0xFFFE, 0xFC2E]
//
// differents max range [0xFFFF, 0xFFFE, 0xFFFD, 0xFC2F, 0xFC2E]
// CLK14 CLK15
// FPEC: 0xffffffffffffffffffffffffffffffffffffffffffffffffffff fffe f000 fc2f
// V : 0xffffffffffffffffffffffffffffffffffffffffffffffffffff fffe f001 0000
//
// RANGE_SEL P_RANGE BASE
// 0 [0,0xFFFF] CLK0,...,CLK12
// 1 [0,0xFFFE] CLK13
// 2 [0,0xFFFD]
// 3 [0,0xFC2F] CLK15
// 4 [0,0xFC2E]
// 5 [0,0xF000] CLK14
// 6 [0,0xEFFF]
//
// pRange = (CLK13 + 3 * CLK15 + 5 * CLK14 + chunkLtPrime) * (1 - valueLtPrime)
//
// CLK pRange pRange
// [chunkLtPrime == 0] [chunkLtPrime == 1]
//
// 0 0 + 3 * 0 + 0 = 0 0 + 3 * 0 + 1 = 1
// : :
// 12 0 + 3 * 0 + 0 = 0 0 + 3 * 0 + 1 = 1
// 13 1 + 3 * 0 + 0 = 1 1 + 3 * 0 + 1 = 2
// 14 0 + 3 * 0 + 0 = 0 0 + 3 * 0 + 1 = 1
// 15 0 + 3 * 1 + 0 = 3 0 + 3 * 1 + 1 = 4
//
// pRange = (CLK13 + 3 * CLK15 + chunkLtPrime) * (1 - valueLtPrime)
//
// valueLtPrime' = valueLtPrime * (1 - CLK0 + CLK16) + chunkLtPrime
//
// valueLtPrime chunkLtPrime CLK0+CLK16 valueLtPrime'
//
// 0 0 0 0 OK
// 0 1 0 1 OK
// 1 0 0 1 OK
// 1 1 0 2 FAILS, valueLtPrime not binary (D)
//
// 0 0 1 0 OK
// 0 1 1 1 OK
// 1 0 1 0 OK
// 1 1 1 1 OK (E)
//
// (D) when valueLtPrime == 0 ==> chunkLtPrime must be zero, if not FAILS
// (E) on clocks 0 and 16, previous value of valueLtPrime isn't considered
//
//
// ┌──────── pRange
// ┌── max_value │ ┌───── chunkLtPrime
// │ ┌─ example │ │ ┌── valueLtPrime
// │ │ │ │ │
// CLK0 0xFFFF 0xFFFF 0 0 0
// CLK1 0xFFFF 0xFF00 1 1 0 // RANGE [0, 0xFFFE]
// CLK2 0xFFFF 0x0000 0 0 1
// CLK3 0xFFFF 0x0000 0 0 1
// CLK4 0xFFFF 0xFFFF 0 0 1
// :
// CLK15 0xFC2F 0xFFFF 0 0 1
// CLK16 0xFFFF 0xFFFF 0 0 1
//
//
// ┌──────── pRange
// ┌── max_value │ ┌───── chunkLtPrime
// │ ┌─ example │ │ ┌── valueLtPrime
// │ │ │ │ │
// CLK0 0xFFFF 0xFFFF 0 0 0
// CLK1 0xFFFF 0xFFFF 0 0 0
// CLK2 0xFFFF 0xFFFF 0 0 0
// :
// CLK12 0xFFFF 0xFFFF 0 0 0
// CLK13 0xFFFE 0xFFFF 1 0 0 // CLK13 == 1 RANGE [0, 0xFFFE]
// CLK14 0xFFFF 0xFFFF 0 0 0
// CLK15 0xFC2F 0xFC00 4 1 0 // CLK15 == 1 RANGE [0, 0xFC2F]
// CLK16 0xFFFF 0xFFFF 0 0 1

// indicates that any previous chunk was minor and the rest of previous are
// equal o minors than the FPEC chunk. If selEq[3] = 0, it must be 0.
pol commit valueLtPrime;

// indicates that current was minor than the FPEC chunk. If selEq[3] = 0 or
// valuePtPrime = 1, it must be 0.
pol commit chunkLtPrime;

// binary constraints
chunkLtPrime * (1 - chunkLtPrime) = 0;
valueLtPrime * (1 - valueLtPrime) = 0;

// Constraint over next value of valueLtPrime. At begining of each 16 clock cycle
// ignore valueLtPrime because it is refers previous value.
valueLtPrime' = valueLtPrime * (1 - Global.CLK32[0] - Global.CLK32[16]) + chunkLtPrime;

// constraint to verify at end of 16 clock cycle than valueLtPrime is 1. this constraint
// applies when selEq[3] = 1.
(valueLtPrime' - selEq[3]) * (Global.CLK32[15] + Global.CLK32[31]) = 0;


pol constant RANGE_SEL; // 0:2**16,
// 1:2**16-1,0
// 2:2**16-2,0:2
// 3:2**16-976,0:976
// 4:2**16-977,0:977

// logout with pRange as first column

{(Global.CLK32[13] + Global.CLK32[29] + (Global.CLK32[15] + Global.CLK32[31]) * 3 + chunkLtPrime) * (selEq[3] - valueLtPrime), x3[15]*Global.CLK32[0] + x3[14]*Global.CLK32[1] + x3[13]*Global.CLK32[2] + x3[12]*Global.CLK32[3] + x3[11]*Global.CLK32[4] + x3[10]*Global.CLK32[5] + x3[9]*Global.CLK32[6] + x3[8]*Global.CLK32[7]
+ x3[7]*Global.CLK32[8] + x3[6]*Global.CLK32[9] + x3[5]*Global.CLK32[10] + x3[4]*Global.CLK32[11] + x3[3]*Global.CLK32[12] + x3[2]*Global.CLK32[13] + x3[1]*Global.CLK32[14] + x3[0]*Global.CLK32[15]
+ y3[15]*Global.CLK32[16] + y3[14]*Global.CLK32[17] + y3[13]*Global.CLK32[18] + y3[12]*Global.CLK32[19] + y3[11]*Global.CLK32[20] + y3[10]*Global.CLK32[21] + y3[9]*Global.CLK32[22] + y3[8]*Global.CLK32[23]
+ y3[7]*Global.CLK32[24] + y3[6]*Global.CLK32[25] + y3[5]*Global.CLK32[26] + y3[4]*Global.CLK32[27] + y3[3]*Global.CLK32[28] + y3[2]*Global.CLK32[29] + y3[1]*Global.CLK32[30] + y3[0]*Global.CLK32[31]} in {RANGE_SEL, Global.BYTE2};

/****
*
* LATCH POLS: x1,y1,x2,y2,x3,y3,s,q0,q1,q2
Expand Down Expand Up @@ -239,11 +444,6 @@ namespace Arith(%N);
+ y2[0]*Global.CLK32[16] + y2[1]*Global.CLK32[17] + y2[2]*Global.CLK32[18] + y2[3]*Global.CLK32[19] + y2[4]*Global.CLK32[20] + y2[5]*Global.CLK32[21] + y2[6]*Global.CLK32[22] + y2[7]*Global.CLK32[23]
+ y2[8]*Global.CLK32[24] + y2[9]*Global.CLK32[25] + y2[10]*Global.CLK32[26] + y2[11]*Global.CLK32[27] + y2[12]*Global.CLK32[28] + y2[13]*Global.CLK32[29] + y2[14]*Global.CLK32[30] + y2[15]*Global.CLK32[31] in Global.BYTE2;

x3[0]*Global.CLK32[0] + x3[1]*Global.CLK32[1] + x3[2]*Global.CLK32[2] + x3[3]*Global.CLK32[3] + x3[4]*Global.CLK32[4] + x3[5]*Global.CLK32[5] + x3[6]*Global.CLK32[6] + x3[7]*Global.CLK32[7]
+ x3[8]*Global.CLK32[8] + x3[9]*Global.CLK32[9] + x3[10]*Global.CLK32[10] + x3[11]*Global.CLK32[11] + x3[12]*Global.CLK32[12] + x3[13]*Global.CLK32[13] + x3[14]*Global.CLK32[14] + x3[15]*Global.CLK32[15]
+ y3[0]*Global.CLK32[16] + y3[1]*Global.CLK32[17] + y3[2]*Global.CLK32[18] + y3[3]*Global.CLK32[19] + y3[4]*Global.CLK32[20] + y3[5]*Global.CLK32[21] + y3[6]*Global.CLK32[22] + y3[7]*Global.CLK32[23]
+ y3[8]*Global.CLK32[24] + y3[9]*Global.CLK32[25] + y3[10]*Global.CLK32[26] + y3[11]*Global.CLK32[27] + y3[12]*Global.CLK32[28] + y3[13]*Global.CLK32[29] + y3[14]*Global.CLK32[30] + y3[15]*Global.CLK32[31] in Global.BYTE2;

s[0]*Global.CLK32[0] + s[1]*Global.CLK32[1] + s[2]*Global.CLK32[2] + s[3]*Global.CLK32[3] + s[4]*Global.CLK32[4] + s[5]*Global.CLK32[5] + s[6]*Global.CLK32[6] + s[7]*Global.CLK32[7]
+ s[8]*Global.CLK32[8] + s[9]*Global.CLK32[9] + s[10]*Global.CLK32[10] + s[11]*Global.CLK32[11] + s[12]*Global.CLK32[12] + s[13]*Global.CLK32[13] + s[14]*Global.CLK32[14] + s[15]*Global.CLK32[15]
+ q0[0]*Global.CLK32[16] + q0[1]*Global.CLK32[17] + q0[2]*Global.CLK32[18] + q0[3]*Global.CLK32[19] + q0[4]*Global.CLK32[20] + q0[5]*Global.CLK32[21] + q0[6]*Global.CLK32[22] + q0[7]*Global.CLK32[23]
Expand Down Expand Up @@ -1894,8 +2094,6 @@ namespace Arith(%N);
+ eq4_16*Global.CLK32[16] + eq4_17*Global.CLK32[17] + eq4_18*Global.CLK32[18] + eq4_19*Global.CLK32[19] + eq4_20*Global.CLK32[20] + eq4_21*Global.CLK32[21] + eq4_22*Global.CLK32[22] + eq4_23*Global.CLK32[23]
+ eq4_24*Global.CLK32[24] + eq4_25*Global.CLK32[25] + eq4_26*Global.CLK32[26] + eq4_27*Global.CLK32[27] + eq4_28*Global.CLK32[28] + eq4_29*Global.CLK32[29] + eq4_30*Global.CLK32[30] + eq4_31*Global.CLK32[31];

pol commit selEq[4];

selEq[0]' * (1-Global.CLK32[31]) = selEq[0] * (1-Global.CLK32[31]);
selEq[1]' * (1-Global.CLK32[31]) = selEq[1] * (1-Global.CLK32[31]);
selEq[2]' * (1-Global.CLK32[31]) = selEq[2] * (1-Global.CLK32[31]);
Expand Down
21 changes: 3 additions & 18 deletions recursive/final.circom
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,20 +17,9 @@ Total: 1696

include "sha256/sha256.circom";
include "bitify.circom";
include "lessthangl.circom";
include "recursivef.verifier.circom";

template LessThanGoldilocks() {
var n = 64;
var p = 0xFFFFFFFF00000001;
signal input in;
signal output out;

component n2b = Num2Bits(n+1);

n2b.in <== in + (1<<n) - p;

out <== 1-n2b.out[n];
}

template Main() {
signal output publicsHash;
Expand Down Expand Up @@ -129,10 +118,8 @@ template Main() {
}
}

signal isValidOldStateRoot[4];
for (var i = 0; i < 4; i++) {
isValidOldStateRoot[i] <== LessThanGoldilocks()(publics[0 + 2*i] + (1 << 32) * publics[0 + 2*i + 1]);
isValidOldStateRoot[i] === 1;
_<== LessThanGoldilocks()(publics[0 + 2*i] + (1 << 32) * publics[0 + 2*i + 1]);
}

signal n2bOldAccInputHash[8][32];
Expand Down Expand Up @@ -170,10 +157,8 @@ template Main() {
}
}

signal isValidNewStateRoot[4];
for (var i = 0; i < 4; i++) {
isValidNewStateRoot[i] <== LessThanGoldilocks()(publics[19 + 2*i] + (1 << 32)*publics[19 + 2*i + 1]);
isValidNewStateRoot[i] === 1;
_<== LessThanGoldilocks()(publics[19 + 2*i] + (1 << 32)*publics[19 + 2*i + 1]);
}

signal n2bNewAccInputHash[8][32];
Expand Down
Loading

0 comments on commit 07d9299

Please sign in to comment.