Merge pull request #119 from 0xPolygonHermez/feature/isolated-term

Isolated term into sum

pil2-components/lib/std/pil/std_sum.pil

@@ -224,33 +224,50 @@ 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
-        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 {
-            low_degree_term[low_degree_len] = i;
-            low_degree_len++;
+        } 
+        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;
+                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];
@@ -331,17 +348,27 @@ 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ᵢ
+          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ⱼ + ɣ) - den·∑ⱼ 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 +381,11 @@ 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};
+    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) * 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;
 }
 

pil2-components/lib/std/rs/src/std_sum.rs

@@ -10,7 +10,7 @@ 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,
+    acc_mul_hint_fields, get_hint_field, get_hint_field_a, get_hint_ids_by_name, mul_hint_fields, HintFieldOptions,
     HintFieldOutput,
 };
 
@@ -256,20 +256,17 @@ impl<F: PrimeField> WitnessComponent<F> for StdSum<F> {
                     // 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_add_hint_fields::<F>(
+                    let (pol_id, airgroupvalue_id) = acc_mul_hint_fields::<F>(
                         &sctx,
                         &pctx,
                         air_instance,
                         gsum_hint,
                         "reference",
                         "result",
-                        "direct_num",
-                        "direct_den",
-                        "sum_ims",
+                        "numerator",
+                        "denominator",
                         HintFieldOptions::default(),
                         HintFieldOptions::inverse(),
-                        HintFieldOptions::default(),
                         true,
                     );
 

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