From e336d62d427e307f292e290bf0298f610ccc52dc Mon Sep 17 00:00:00 2001 From: zkronos73 Date: Mon, 4 Nov 2024 17:54:20 +0000 Subject: [PATCH 1/3] add optimization for sum bus using degree builtin --- pil2-components/lib/std/pil/std_sum.pil | 53 +++++++++++++++++++------ 1 file changed, 41 insertions(+), 12 deletions(-) diff --git a/pil2-components/lib/std/pil/std_sum.pil b/pil2-components/lib/std/pil/std_sum.pil index 036131e3..c04a4515 100644 --- a/pil2-components/lib/std/pil/std_sum.pil +++ b/pil2-components/lib/std/pil/std_sum.pil @@ -25,9 +25,9 @@ private function init_proof_containers_sum(int name, int opid[]) { int opids[100]; // Resulting sum of every airgroup and every air - // It is the accumulation of each partial sum that each instance + // It is the accumulation of each partial sum that each instance // of each air constributes to. It must be zero at the end. - expr gsum = 0; + expr gsum = 0; // Direct shortcut to the previous sum int direct_gsum_count = 0; @@ -136,7 +136,7 @@ private function update_piop_sum(int name, int proves, int opid[], expr sumid, e direct_gsum_count++; } else { use air.std.gsum; - + gsum_s[gsum_nargs] = proves ? sel : 0-sel; gsum_e[gsum_nargs] = cols_compressed; gsum_t[gsum_nargs] = proves; @@ -184,7 +184,23 @@ private function find_repeated_proves() { private function piop_gsum_air(const int nTerms = 2) { use air.std.gsum; - const int nIm = gsum_nargs/nTerms; + const int max_degree = 1; + int gsum_low_degree[gsum_nargs]; + int gsum_high_degree[gsum_nargs]; + int gsum_low_degree_len = 0; + int gsum_high_degree_len = 0; + + for (int i = 0; i < gsum_nargs; i++) { + if (degree(gsum_e[i]) > max_degree || degree(gsum_s[i]) > max_degree) { + gsum_high_degree[gsum_high_degree_len] = i; + ++gsum_high_degree_len; + } else { + gsum_low_degree[gsum_low_degree_len] = i; + ++gsum_low_degree_len; + } + } + + const int nIm = gsum_low_degree_len/nTerms; col witness stage(2) im[nIm]; @@ -214,12 +230,12 @@ private function piop_gsum_air(const int nTerms = 2) { expr prods = 1; expr sums = 0; for (int j = 0; j < nTerms; j++) { - prods *= (gsum_e[nTerms * i + j] + std_gamma); + prods *= (gsum_e[gsum_low_degree[nTerms * i + j]] + std_gamma); - expr _partial = gsum_s[nTerms * i + j]; + expr _partial = gsum_s[gsum_low_degree[nTerms * i + j]]; for (int k = 0; k < nTerms; k++) { if (k == j) continue; - _partial *= (gsum_e[nTerms * i + k] + std_gamma); + _partial *= (gsum_e[gsum_low_degree[nTerms * i + k]] + std_gamma); } sums += _partial; } @@ -232,21 +248,21 @@ private function piop_gsum_air(const int nTerms = 2) { sumIms += im[i]; } - if (gsum_nargs % nTerms != 0) { + if (gsum_low_degree_len % nTerms != 0) { col witness stage(2) im_extra; // This col is defined with a number of terms between 1 and nTerms-1 - const int nRemTerms = gsum_nargs % nTerms; + const int nRemTerms = gsum_low_degree_len % nTerms; expr prods = 1; expr sums = 0; for (int j = 0; j < nRemTerms; j++) { - prods *= (gsum_e[nTerms * nIm + j] + std_gamma); + prods *= (gsum_e[gsum_low_degree[nTerms * nIm + j]] + std_gamma); - expr _partial = gsum_s[nTerms * nIm + j]; + expr _partial = gsum_s[gsum_low_degree[nTerms * nIm + j]]; for (int k = 0; k < nRemTerms; k++) { if (k == j) continue; - _partial *= (gsum_e[nTerms * nIm + k] + std_gamma); + _partial *= (gsum_e[gsum_low_degree[nTerms * nIm + k]] + std_gamma); } sums += _partial; } @@ -257,6 +273,19 @@ private function piop_gsum_air(const int nTerms = 2) { sumIms += im_extra; } + if (gsum_high_degree_len > 0) { + col witness stage(2) im_high_degree[gsum_high_degree_len]; + + for (int i = 0; i < gsum_high_degree_len; ++i) { + int index = gsum_high_degree[i]; + + @im_col{reference: im_high_degree[i], numerator: gsum_s[index], denominator: gsum_e[index] + std_gamma}; + + im_high_degree[i] * gsum_e[index] === gsum_s[index]; + sumIms += im_high_degree[i]; + } + } + @gsum_col{reference: gsum, expression: sumIms, result: airgroup.std.gsum.gsum_result}; gsum === 'gsum * (1 - __L1) + sumIms; From 7038134794718e8b456d6ec05a6ba9bb94ce102e Mon Sep 17 00:00:00 2001 From: RogerTaule Date: Tue, 5 Nov 2024 07:44:59 +0000 Subject: [PATCH 2/3] Pil2-compiler pointing to develop --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index bbc34696..4163d861 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -147,7 +147,7 @@ jobs: with: repository: 0xPolygonHermez/pil2-compiler token: ${{ secrets.GITHUB_TOKEN }} - ref: feature/pilout_v2_airgroup + ref: develop path: pil2-compiler - name: Install pil2-compiler dependencies From e33622f9afa10a24d83beb0aba920a960b528ad4 Mon Sep 17 00:00:00 2001 From: zkronos73 Date: Tue, 5 Nov 2024 16:38:39 +0100 Subject: [PATCH 3/3] fix bug on constraint --- pil2-components/lib/std/pil/std_sum.pil | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pil2-components/lib/std/pil/std_sum.pil b/pil2-components/lib/std/pil/std_sum.pil index c04a4515..fbd53620 100644 --- a/pil2-components/lib/std/pil/std_sum.pil +++ b/pil2-components/lib/std/pil/std_sum.pil @@ -281,7 +281,7 @@ private function piop_gsum_air(const int nTerms = 2) { @im_col{reference: im_high_degree[i], numerator: gsum_s[index], denominator: gsum_e[index] + std_gamma}; - im_high_degree[i] * gsum_e[index] === gsum_s[index]; + im_high_degree[i] * (gsum_e[index] + std_gamma) === gsum_s[index]; sumIms += im_high_degree[i]; } }