From 7f3e17841bb04929e417b17ca7753a8e1f359e57 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?H=C3=A9ctor=20Masip?= Date: Wed, 27 Nov 2024 18:40:55 +0000 Subject: [PATCH 1/5] Isolated term into sum --- pil2-components/lib/std/pil/std_sum.pil | 38 +++++++++++++++------- pil2-components/test/std/special/table.pil | 34 +++++++++++++++++++ 2 files changed, 61 insertions(+), 11 deletions(-) create mode 100644 pil2-components/test/std/special/table.pil diff --git a/pil2-components/lib/std/pil/std_sum.pil b/pil2-components/lib/std/pil/std_sum.pil index 8c3ae577..947ed2ed 100644 --- a/pil2-components/lib/std/pil/std_sum.pil +++ b/pil2-components/lib/std/pil/std_sum.pil @@ -224,13 +224,14 @@ private function piop_gsum_air(const int blowupFactor = 2) { /* Transform the rational constraint to a polynomial one by substituting - all the rational terms by terms of degree 1: - gsum === 'gsum * (1 - L1) + ∑ᵢ imi + all the rational terms by terms of degree 1 (except for one to optimize): + gsum === 'gsum * (1 - L1) + ∑ᵢ imi + num / den */ int low_degree_term[gsum_nargs]; int high_degree_term[gsum_nargs]; int low_degree_len = 0; int high_degree_len = 0; + int isolated_term = -1; for (int i = 0; i < gsum_nargs; i++) { // In the case that both the numerator and the denominator are constants, // we can directly add them through the direct terms @@ -242,15 +243,20 @@ private function piop_gsum_air(const int blowupFactor = 2) { high_degree_term[high_degree_len] = i; high_degree_len++; } else { - low_degree_term[low_degree_len] = i; - low_degree_len++; + // The first low-degree term is isolated + if (isolated_term == -1) { + isolated_term = i; + } else { + low_degree_term[low_degree_len] = i; + low_degree_len++; + } } } expr sum_ims = 0; + // Create an intermediate for clusters of low-degree terms so that + // the degree of the constraint is lower than the maximum allowed if (low_degree_len > 0) { - // Group terms in clusters so that the degree of the constraint - // is lower than the maximum allowed const int nIm = low_degree_len/blowupFactor; col witness stage(2) im[nIm]; @@ -333,15 +339,17 @@ private function piop_gsum_air(const int blowupFactor = 2) { /* At this point, the constraint has been transformed to: - gsum === 'gsum * (1 - L1) + ∑ᵢ imᵢ + gsum === 'gsum * (1 - L1) + ∑ᵢ imᵢ + num / den Now, we whould add the direct terms to the constraint: - gsum === 'gsum * (1 - L1) + ∑ᵢ imᵢ + ∑ⱼ sⱼ / (eⱼ + ɣ) + gsum === 'gsum * (1 - L1) + ∑ᵢ imᵢ + num / den + ∑ⱼ sⱼ / (eⱼ + ɣ) where both sⱼ and eⱼ are field elements, for all j. We rewrite it as: - (gsum - 'gsum * (1 - L1) - ∑ᵢ imᵢ)·∏ⱼ (eⱼ + ɣ) - ∑ⱼ sⱼ · ∏ₖ≠ⱼ (eₖ + ɣ) === 0 + ((gsum - 'gsum * (1 - L1) - ∑ᵢ imᵢ)·den - num)·∏ⱼ (eⱼ + ɣ) - ∑ⱼ sⱼ·∏ₖ≠ⱼ (eₖ + ɣ) === 0 */ + + // Compute the direct terms numerator and denominator expr direct_num = 0; expr direct_den = 1; for (int i = 0; i < direct_gsum_nargs; i++) { @@ -354,9 +362,17 @@ private function piop_gsum_air(const int blowupFactor = 2) { direct_num += _tmp; } - @gsum_col{reference: gsum, direct_num: direct_num, direct_den: direct_den, sum_ims: sum_ims, result: airgroup.std.gsum.gsum_result}; + // Compute the isolated term numerator and denominator + expr isolated_num = 0; + expr isolated_den = 1; + if (isolated_term != -1) { + isolated_den = (gsum_e[isolated_term] + std_gamma); + isolated_num = gsum_s[isolated_term]; + } + + @gsum_col{reference: gsum, direct_num: direct_num, direct_den: direct_den, isolated_num: isolated_num, isolated_den: isolated_den, sum_ims: sum_ims, result: airgroup.std.gsum.gsum_result}; - (gsum - 'gsum * (1 - __L1) - sum_ims) * direct_den - direct_num === 0; + ((gsum - 'gsum * (1 - __L1) - sum_ims) * isolated_den - isolated_num) * direct_den - direct_num === 0; __L1' * (gsum - airgroup.std.gsum.gsum_result) === 0; } diff --git a/pil2-components/test/std/special/table.pil b/pil2-components/test/std/special/table.pil new file mode 100644 index 00000000..64a4f6ec --- /dev/null +++ b/pil2-components/test/std/special/table.pil @@ -0,0 +1,34 @@ +require "std_constants.pil"; +require "std_lookup.pil" + +const int OP_ID = 333; +const int TABLE_ID = 666; + +airtemplate Example(const int N = 2**10) { + col witness a[2]; + col witness b[2]; + col witness sel[2]; + + a[0] * a[1] * b[0] === 3; + + lookup_assumes(OP_ID, [...a], sel[0], name: PIOP_NAME_ISOLATED); +} + +airtemplate Table(const int N = 2**10) { + col witness multiplicity; + + col fixed A = [0..255]...; + col fixed B = [0..255]...; + + lookup_proves(TABLE_ID, [A, B], multiplicity, name: PIOP_NAME_ISOLATED); +} + +airgroup Table { + Example(); + Table(); +} + +// (Table.gsum - 'Table.gsum * (1 - Table.__L1)) * ((Table.B * std_alpha + Table.A) * std_alpha + 666 + std_gamma) - Table.multiplicity === 0 + +// Table.im_extra * ((Table.B * std_alpha + Table.A) * std_alpha + 666 + std_gamma) - Table.multiplicity === 0 +// (Table.gsum - 'Table.gsum * (1 - Table.__L1)) - Table.im_extra === 0 \ No newline at end of file From 36cd7eed19758ffd05bf41554e78b27f582c8346 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?H=C3=A9ctor=20Masip?= Date: Thu, 28 Nov 2024 07:16:39 +0000 Subject: [PATCH 2/5] Typo fixed --- pil2-components/lib/std/pil/std_sum.pil | 43 ++++++++----- pil2-components/lib/std/rs/src/std_sum.rs | 73 ++++++++++++++++++++--- 2 files changed, 93 insertions(+), 23 deletions(-) diff --git a/pil2-components/lib/std/pil/std_sum.pil b/pil2-components/lib/std/pil/std_sum.pil index 947ed2ed..df561905 100644 --- a/pil2-components/lib/std/pil/std_sum.pil +++ b/pil2-components/lib/std/pil/std_sum.pil @@ -233,18 +233,29 @@ private function piop_gsum_air(const int blowupFactor = 2) { int high_degree_len = 0; int isolated_term = -1; for (int i = 0; i < gsum_nargs; i++) { - // In the case that both the numerator and the denominator are constants, - // we can directly add them through the direct terms - if (degree(gsum_s[i]) == 0 && degree(gsum_e[i]) == 0) { + const int gsum_s_degree = degree(gsum_s[i]); + const int gsum_e_degree = degree(gsum_e[i]); + if (gsum_s_degree == 0 && gsum_e_degree == 0) { + // In the case that both the numerator and the denominator are constants, + // we can directly add them through the direct terms direct_gsum_s[direct_gsum_nargs] = gsum_s[i]; direct_gsum_e[direct_gsum_nargs] = gsum_e[i]; direct_gsum_nargs++; - } else if (degree(gsum_s[i]) > 2 || degree(gsum_e[i]) > 1) { // Discriminator conditions + } + else if ((gsum_s_degree == 3 && gsum_e_degree == 1) || + (gsum_s_degree == 2 && gsum_e_degree == 1)) { + // Identify isolated terms of specific degrees + isolated_term = i; + } + else if (gsum_s_degree > 2 || gsum_e_degree > 1) { + // Track high-degree terms high_degree_term[high_degree_len] = i; high_degree_len++; - } else { - // The first low-degree term is isolated + } + else { + // Handle low-degree terms if (isolated_term == -1) { + // The first low-degree term is isolated isolated_term = i; } else { low_degree_term[low_degree_len] = i; @@ -337,6 +348,14 @@ private function piop_gsum_air(const int blowupFactor = 2) { } } + // Compute the isolated term numerator and denominator + expr isolated_num = 0; + expr isolated_den = 1; + if (isolated_term != -1) { + isolated_den = (gsum_e[isolated_term] + std_gamma); + isolated_num = gsum_s[isolated_term]; + } + /* At this point, the constraint has been transformed to: gsum === 'gsum * (1 - L1) + ∑ᵢ imᵢ + num / den @@ -346,7 +365,7 @@ private function piop_gsum_air(const int blowupFactor = 2) { where both sⱼ and eⱼ are field elements, for all j. We rewrite it as: - ((gsum - 'gsum * (1 - L1) - ∑ᵢ imᵢ)·den - num)·∏ⱼ (eⱼ + ɣ) - ∑ⱼ sⱼ·∏ₖ≠ⱼ (eₖ + ɣ) === 0 + ((gsum - 'gsum * (1 - L1) - ∑ᵢ imᵢ)·den - num)·∏ⱼ (eⱼ + ɣ) - den·∑ⱼ sⱼ·∏ₖ≠ⱼ (eₖ + ɣ) === 0 */ // Compute the direct terms numerator and denominator @@ -362,17 +381,9 @@ private function piop_gsum_air(const int blowupFactor = 2) { direct_num += _tmp; } - // Compute the isolated term numerator and denominator - expr isolated_num = 0; - expr isolated_den = 1; - if (isolated_term != -1) { - isolated_den = (gsum_e[isolated_term] + std_gamma); - isolated_num = gsum_s[isolated_term]; - } - @gsum_col{reference: gsum, direct_num: direct_num, direct_den: direct_den, isolated_num: isolated_num, isolated_den: isolated_den, sum_ims: sum_ims, result: airgroup.std.gsum.gsum_result}; - ((gsum - 'gsum * (1 - __L1) - sum_ims) * isolated_den - isolated_num) * direct_den - direct_num === 0; + ((gsum - 'gsum * (1 - __L1) - sum_ims) * isolated_den - isolated_num) * direct_den - isolated_den * direct_num === 0; __L1' * (gsum - airgroup.std.gsum.gsum_result) === 0; } diff --git a/pil2-components/lib/std/rs/src/std_sum.rs b/pil2-components/lib/std/rs/src/std_sum.rs index e4e3484d..785f15aa 100644 --- a/pil2-components/lib/std/rs/src/std_sum.rs +++ b/pil2-components/lib/std/rs/src/std_sum.rs @@ -257,24 +257,83 @@ impl WitnessComponent for StdSum { // Alternatively, this could be done using get_hint_field and set_hint_field methods and doing the accumulation in Rust, // TODO: GENERALIZE CALLS - let (pol_id, airgroupvalue_id) = acc_mul_add_hint_fields::( + let direct_num = get_hint_field::( &sctx, &pctx, air_instance, gsum_hint, - "reference", - "result", "direct_num", + HintFieldOptions::default(), + ); + let direct_den_inv = get_hint_field::( + &sctx, + &pctx, + air_instance, + gsum_hint, "direct_den", - "sum_ims", + HintFieldOptions::inverse(), + ); + let isolated_num = get_hint_field::( + &sctx, + &pctx, + air_instance, + gsum_hint, + "isolated_num", + HintFieldOptions::default(), + ); + let isolated_den = get_hint_field::( + &sctx, + &pctx, + air_instance, + gsum_hint, + "isolated_den", HintFieldOptions::default(), + ); + let isolated_den_inv = get_hint_field::( + &sctx, + &pctx, + air_instance, + gsum_hint, + "isolated_den", HintFieldOptions::inverse(), + ); + let sum_ims = get_hint_field::( + &sctx, + &pctx, + air_instance, + gsum_hint, + "sum_ims", HintFieldOptions::default(), - true, ); + let mut gsum = get_hint_field::( + &sctx, + &pctx, + air_instance, + gsum_hint, + "reference", + HintFieldOptions::default(), + ); + gsum.set( + 0, + (isolated_den.get(0) * direct_num.get(0) * direct_den_inv.get(0) + isolated_num.get(0)) + * isolated_den_inv.get(0) + + sum_ims.get(0), + ); + for i in 1..num_rows { + gsum.set( + i, + gsum.get(i - 1) + + (isolated_den.get(i) * direct_num.get(i) * direct_den_inv.get(i) + + isolated_num.get(i)) + * isolated_den_inv.get(i) + + sum_ims.get(i), + ); + } + + let result = gsum.get(num_rows - 1); - air_instance.set_commit_calculated(pol_id as usize); - air_instance.set_airgroupvalue_calculated(airgroupvalue_id as usize); + set_hint_field::(&sctx, air_instance, gsum_hint as u64, "reference", &gsum); + set_hint_field_val::(&sctx, air_instance, gsum_hint as u64, "result", result); } } } From cdafa74d3ec3c0672b3049b85aa593b2468d82af Mon Sep 17 00:00:00 2001 From: RogerTaule Date: Thu, 28 Nov 2024 10:54:19 +0000 Subject: [PATCH 3/5] Optimizing std_sum --- pil2-components/lib/std/pil/std_sum.pil | 6 +- pil2-components/lib/std/rs/src/std_sum.rs | 81 +++-------------------- 2 files changed, 13 insertions(+), 74 deletions(-) diff --git a/pil2-components/lib/std/pil/std_sum.pil b/pil2-components/lib/std/pil/std_sum.pil index df561905..d9a5df8c 100644 --- a/pil2-components/lib/std/pil/std_sum.pil +++ b/pil2-components/lib/std/pil/std_sum.pil @@ -380,9 +380,9 @@ private function piop_gsum_air(const int blowupFactor = 2) { } direct_num += _tmp; } - - @gsum_col{reference: gsum, direct_num: direct_num, direct_den: direct_den, isolated_num: isolated_num, isolated_den: isolated_den, sum_ims: sum_ims, result: airgroup.std.gsum.gsum_result}; - + expr numerator = direct_num*isolated_den + (isolated_num + sum_ims*isolated_den)*direct_den; + expr denominator = direct_den * isolated_den; + @gsum_col{reference: gsum, numerator: numerator, denominator: denominator, result: airgroup.std.gsum.gsum_result}; ((gsum - 'gsum * (1 - __L1) - sum_ims) * isolated_den - isolated_num) * direct_den - isolated_den * direct_num === 0; __L1' * (gsum - airgroup.std.gsum.gsum_result) === 0; } diff --git a/pil2-components/lib/std/rs/src/std_sum.rs b/pil2-components/lib/std/rs/src/std_sum.rs index 785f15aa..1bd00f17 100644 --- a/pil2-components/lib/std/rs/src/std_sum.rs +++ b/pil2-components/lib/std/rs/src/std_sum.rs @@ -10,8 +10,8 @@ use rayon::prelude::*; use proofman::{WitnessComponent, WitnessManager}; use proofman_common::{AirInstance, ExecutionCtx, ProofCtx, SetupCtx}; use proofman_hints::{ - get_hint_field, get_hint_field_a, get_hint_ids_by_name, mul_hint_fields, acc_mul_add_hint_fields, HintFieldOptions, - HintFieldOutput, + acc_mul_hint_fields, format_vec, get_hint_field, get_hint_field_a, get_hint_ids_by_name, mul_hint_fields, + HintFieldOptions, HintFieldOutput, }; use crate::{print_debug_info, BusValue, DebugData, Decider, ModeName, StdMode}; @@ -257,83 +257,22 @@ impl WitnessComponent for StdSum { // Alternatively, this could be done using get_hint_field and set_hint_field methods and doing the accumulation in Rust, // TODO: GENERALIZE CALLS - let direct_num = get_hint_field::( - &sctx, - &pctx, - air_instance, - gsum_hint, - "direct_num", - HintFieldOptions::default(), - ); - let direct_den_inv = get_hint_field::( - &sctx, - &pctx, - air_instance, - gsum_hint, - "direct_den", - HintFieldOptions::inverse(), - ); - let isolated_num = get_hint_field::( - &sctx, - &pctx, - air_instance, - gsum_hint, - "isolated_num", - HintFieldOptions::default(), - ); - let isolated_den = get_hint_field::( - &sctx, - &pctx, - air_instance, - gsum_hint, - "isolated_den", - HintFieldOptions::default(), - ); - let isolated_den_inv = get_hint_field::( - &sctx, - &pctx, - air_instance, - gsum_hint, - "isolated_den", - HintFieldOptions::inverse(), - ); - let sum_ims = get_hint_field::( - &sctx, - &pctx, - air_instance, - gsum_hint, - "sum_ims", - HintFieldOptions::default(), - ); - let mut gsum = get_hint_field::( + let (pol_id, airgroupvalue_id) = acc_mul_hint_fields::( &sctx, &pctx, air_instance, gsum_hint, "reference", + "result", + "numerator", + "denominator", HintFieldOptions::default(), + HintFieldOptions::inverse(), + true, ); - gsum.set( - 0, - (isolated_den.get(0) * direct_num.get(0) * direct_den_inv.get(0) + isolated_num.get(0)) - * isolated_den_inv.get(0) - + sum_ims.get(0), - ); - for i in 1..num_rows { - gsum.set( - i, - gsum.get(i - 1) - + (isolated_den.get(i) * direct_num.get(i) * direct_den_inv.get(i) - + isolated_num.get(i)) - * isolated_den_inv.get(i) - + sum_ims.get(i), - ); - } - - let result = gsum.get(num_rows - 1); - set_hint_field::(&sctx, air_instance, gsum_hint as u64, "reference", &gsum); - set_hint_field_val::(&sctx, air_instance, gsum_hint as u64, "result", result); + air_instance.set_commit_calculated(pol_id as usize); + air_instance.set_airgroupvalue_calculated(airgroupvalue_id as usize); } } } From 5ce6c076a6f9995f813c17a3c43dff5fffb59949 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?H=C3=A9ctor=20Masip?= Date: Thu, 28 Nov 2024 11:12:00 +0000 Subject: [PATCH 4/5] Minor changes --- pil2-components/lib/std/pil/std_sum.pil | 8 +++++--- pil2-components/lib/std/rs/src/std_sum.rs | 1 - 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/pil2-components/lib/std/pil/std_sum.pil b/pil2-components/lib/std/pil/std_sum.pil index d9a5df8c..c391d151 100644 --- a/pil2-components/lib/std/pil/std_sum.pil +++ b/pil2-components/lib/std/pil/std_sum.pil @@ -380,9 +380,11 @@ private function piop_gsum_air(const int blowupFactor = 2) { } direct_num += _tmp; } - expr numerator = direct_num*isolated_den + (isolated_num + sum_ims*isolated_den)*direct_den; - expr denominator = direct_den * isolated_den; - @gsum_col{reference: gsum, numerator: numerator, denominator: denominator, result: airgroup.std.gsum.gsum_result}; + + expr hint_den = direct_den * isolated_den; + expr hint_num = sum_ims * hint_den + direct_num * isolated_den + isolated_num * direct_den; + @gsum_col{reference: gsum, numerator: hint_num, denominator: hint_den, result: airgroup.std.gsum.gsum_result}; + ((gsum - 'gsum * (1 - __L1) - sum_ims) * isolated_den - isolated_num) * direct_den - isolated_den * direct_num === 0; __L1' * (gsum - airgroup.std.gsum.gsum_result) === 0; } diff --git a/pil2-components/lib/std/rs/src/std_sum.rs b/pil2-components/lib/std/rs/src/std_sum.rs index 1bd00f17..c00f3a06 100644 --- a/pil2-components/lib/std/rs/src/std_sum.rs +++ b/pil2-components/lib/std/rs/src/std_sum.rs @@ -256,7 +256,6 @@ impl WitnessComponent for StdSum { // This call accumulates "expression" into "reference" expression and stores its last value to "result" // Alternatively, this could be done using get_hint_field and set_hint_field methods and doing the accumulation in Rust, // TODO: GENERALIZE CALLS - let (pol_id, airgroupvalue_id) = acc_mul_hint_fields::( &sctx, &pctx, From c21c8d7a73ac9a5402bd621291e75da78297b73f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?H=C3=A9ctor=20Masip?= Date: Thu, 28 Nov 2024 11:14:47 +0000 Subject: [PATCH 5/5] minor --- pil2-components/lib/std/rs/src/std_sum.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pil2-components/lib/std/rs/src/std_sum.rs b/pil2-components/lib/std/rs/src/std_sum.rs index c00f3a06..253edae5 100644 --- a/pil2-components/lib/std/rs/src/std_sum.rs +++ b/pil2-components/lib/std/rs/src/std_sum.rs @@ -10,8 +10,8 @@ use rayon::prelude::*; use proofman::{WitnessComponent, WitnessManager}; use proofman_common::{AirInstance, ExecutionCtx, ProofCtx, SetupCtx}; use proofman_hints::{ - acc_mul_hint_fields, format_vec, get_hint_field, get_hint_field_a, get_hint_ids_by_name, mul_hint_fields, - HintFieldOptions, HintFieldOutput, + acc_mul_hint_fields, get_hint_field, get_hint_field_a, get_hint_ids_by_name, mul_hint_fields, HintFieldOptions, + HintFieldOutput, }; use crate::{print_debug_info, BusValue, DebugData, Decider, ModeName, StdMode};