PIL2 Library

src/pil_verifier.js

@@ -393,11 +393,4 @@ function getConnectionMap(F, N, nk) {
 
     cacheConnectionMaps[kc] = m;
     return m;
-}
-
-
-
-
-
-
-
+}

test/pil2/vadcop/std_connect.pil

@@ -0,0 +1,317 @@
+// A this moment, connection arguments are only applicable within the same AIR.
+// However, I think they can be extended to the subproof level.
+
+private function init_challenges() {
+    if (!defined(std_alpha)) {
+        challenge stage(2) std_alpha;
+    }
+    if (!defined(std_beta)) {
+        challenge stage(2) std_beta;
+    }
+}
+
+private function init_coset_constants(int len) {
+    global std_ks[len];
+
+    std_ks[0] = 1;
+    for (int i = 1; i < len; ++i) {
+        std_ks[i] = global constant k[i-1];
+    }
+}
+
+// Two user interfaces
+
+// 1] Interface where the user uses either the update_one_cell() or the update_multiple_cells() method to define the permutation "on the fly"
+//    and when it is done, executes the connect() method to perform the connection argument.
+//    The user also needs to execute init() at the beginning.
+
+// TODO (Héctor): Throw an error if the calling path is not being called correctly? (as explained in the comment)
+
+function connection_init(int opid, expr cols[]) {
+    check_opid_and_cols(opid, length(cols), 0, 0);
+}
+
+private function find_col_index(expr column) {
+    use proof.std.connect.`id${opid}`;
+
+    for (int icol = 0; icol < length(map_cols); ++icol) {
+        if (map_cols[icol] == column) {
+            return icol;
+        }
+    }
+
+    error(`Column ${column} has not been initialized in connect #${opid}`);
+}
+
+function connection_update_one_cell(int opid, expr cols1[], int rows1[], expr cols2[], int rows2[]) {
+    use proof.std.connect.`id${opid}`;
+
+    if (!(length(cols1) == length(rows1) == length(cols2) == length(rows2))) {
+        error(`The number of columns and rows of connect #${opid} must be the same`);
+    } else if (length(cols1) < 1) {
+        error(`The number of columns of connect #${opid} must be at least 1`);
+    }
+
+    for (int i = 0; i < length(cols1); ++i) {
+            int col1_index = find_col_index(cols1[i]);
+            int col2_index = find_col_index(cols2[i]);
+
+            expr tmp = SIDs[col1_index][rows1[i]]
+            SIDs[col1_index][rows1[i]] = SIDs[col2_index][rows2[i]];
+            SIDs[col2_index][rows2[i]] = tmp;
+    }
+}
+
+function connection_update_multiple_cells(int opid, expr cols[], int rows[][]) {
+    use proof.std.connect.`id${opid}`;
+
+    if (length(cols) != length(rows)) {
+        error(`The number of columns and rows of connect #${opid} must be the same`);
+    } else if (length(cols) < 1) {
+        error(`The number of columns of connect #${opid} must be at least 1`);
+    }
+
+    expr SID_lasts[length(cols)];
+    // To avoid a double loop, we need the last element of the last column
+    int last_len = length(rows[length(rows)-1]);
+    int last_col_index = find_col_index(cols[length(cols)-1]);
+    SID_lasts[length(cols)-1] = SIDs[last_col_index][rows[length(rows)-1][last_len-1]];
+
+    for (int i = 0; i < length(cols); ++i) {
+        int len = length(rows[i]);
+
+        int col_index = find_col_index(cols[i]);
+        expr SID = SIDs[col_index];
+        SID_lasts[i] = SID[rows[i][len-1]];
+
+        if (len == 1) {
+            continue;
+        }
+
+        for (int j = len - 2; j >= 0; --j) {
+            int row1 = rows[i][j];
+            int row2 = rows[i][j+1];
+
+            SID[row2] = SID[row1]
+        }
+
+        SID[rows[i][0]] = SID_last[i-1];
+    }
+}
+
+function connection_connect(int opid) {
+    use proof.std.connect.`id${opid}`;
+
+    connection_update_require(opid, map_cols, 0);
+    connection_update_provide(opid, map_cols, SIDs);
+}
+
+// 2] Interface where the user knows both the inputs (placed in require) and the
+//    permutation (placed in provide) of the argument.
+function connection_require(int opid, expr cols[]) {
+    check_opid_and_cols(opid, length(cols), 0, 1);
+
+    use proof.std.connect.`id${opid}`;
+
+    tmpR = cols;
+
+    if (provide == 1) {
+        connection_update_provide(opid, cols, tmpP);
+    }
+    connection_update_require(opid, cols, 1);
+}
+
+function connection_provide(int opid, expr cols[]) {
+    check_opid_and_cols(opid, length(cols), 1, 1);
+
+    use proof.std.connect.`id${opid}`;
+
+    if (require == 1) {
+        connection_update_provide(opid, tmpR, cols);
+    } else {
+        tmpP = cols;
+    }
+}
+
+/**
+ * Verifies the number of columns of same connect check (require, provide) is the same.
+ * @param opid (unique) identifier of the connect check
+ * @param cols_count number of columns of the connect check
+ * @param provide 1 if provide, 0 if require
+ */
+private function check_opid_and_cols(int opid, int cols_count, int provide, int is_second_interface) {
+
+    if (cols_count < 1) {
+        error(`The number of columns of connect #${opid} must be at least 1`);
+    }
+
+    container proof.std.connect alias conn {
+        // FIX: dynamic arrays not ready
+        int opids_count = 0;
+        int opids[100];
+    }
+
+    container air.std.connect {
+        // FIX: dynamic arrays not ready
+        expr gsum_require[100];
+        expr gsum_provide[100];
+    }
+
+    container proof.std.connect.`id${opid}` alias connid {
+        int cols_num;
+        int provide = 0;
+        int require = 0;
+
+        expr SIDs[];
+        expr map_cols[]; // Used in connection_init()
+
+        // Used in connection_require() and connection_provide()
+        expr tmpR[];
+        expr tmpP[];
+    }
+
+    if (connid.cols_num == 0) {
+        // first time called
+        connid.cols_num = cols_count;
+        // add opid on a list to verify at final
+        conn.opids[conn.opids_count] = opid;
+        ++conn.opids_count;
+    } else if (connid.cols_num != cols_count) {
+        error(`The number of columns of connect #${opid} must be ${connid.cols_num}`);
+    }
+
+    if (is_second_interface) {
+        if (provide) {
+            if (connid.provide > 0) {
+                error(`Connection #${opid} provide was called previously`);
+            }
+            ++connid.provide;
+        } else {
+            if (connid.require > 0) {
+                error(`Connection #${opid} require was called previously`);
+            }
+            ++connid.require;
+        }
+    } else {
+        // Create a mapping of indexes to set an order of the columns the first time it is called
+        for (int icol = 0; icol < cols_count; ++icol) {
+            connid.map_cols[icol] = cols[icol];
+        }
+
+        init_coset_constants(cols_count);
+
+        col fixed IDEN = [1,omega,..*..,omega**(N-1)]; // {1,𝛚,𝛚²,...,𝛚ᴺ⁻¹}
+
+        // Compute polynomials SID_i(X) := k_i·X
+        for (int icol = 0; icol < cols_count; ++icol) {
+            connid.SIDs[icol] = std_ks[icol] * IDEN;
+        }
+    }
+}
+
+/**
+ * Given columns C₀,...,Cₙ₋₁, it computes the polynomial Cᵢ(X) + alpha·kᵢ·X + beta
+ * @param opid (unique) identifier of the connection
+ * @param colsR require columns of the connection
+ */
+private function connection_update_require(int opid, expr colsR[], int is_second_interface) {
+    init_challenges();
+
+    use proof.std.connect.`id${opid}`;
+
+    if (is_second_interface) {
+        init_coset_constants(length(colsR));
+
+        once col fixed IDEN = [1,omega,..*..,omega**(N-1)]; // {1,𝛚,𝛚²,...,𝛚ᴺ⁻¹}
+
+        // Compute polynomials SID_i(X) := k_i·X
+        for (int icol = 0; icol < length(colsR); ++icol) {
+            SIDs[icol] = std_ks[icol] * IDEN;
+        }
+    }
+
+    for (int icol = 0; icol < length(colsR); ++icol) {
+        air.std.connect.gsum_require[] = colsR[icol] + std_alpha*SIDs[icol] + std_beta;
+    }
+
+    // define constraints at the air level
+    on final air connection_air();
+}
+
+/**
+ * Given columns C₀,...,Cₙ₋₁, and C'₀,...,C'ₙ₋₁, it computes the polynomial Cᵢ(X) + alpha·C'ᵢ(X) + beta
+ * @param opid (unique) identifier of the connection
+ * @param colsR require columns of the connection
+ * @param colsP provide columns of the connection
+ */
+private function connection_update_provide(int opid, expr colsR[], expr colsP[]) {
+    init_challenges();
+
+    for (int icol = 0; icol < length(colsP); ++icol) {
+        air.std.connect.gsum_provide[] = colsR[icol] + std_alpha*colsP[icol] + std_beta;
+    }
+
+    // define constraints at the air level
+    on final air connection_air();
+}
+
+private function connection_air() {
+    check_connection_was_completed();
+
+    use air.std.connect;
+
+    col witness stage(2) gsum;
+
+    //                            1                              1                                  1                              1                       1                                1
+    //  gsum === 'gsum + ------------------------ + --------------------------- + ... + -------------------------- - ------------------------ - ------------------------ - ... - ------------------------
+    //                   (f_0 + alpha·X + beta)      (f_1 + alpha·k_1·X + beta)         (f_N + alpha·k_n·X + beta)   (f_0 + alpha·S_0 + beta) · (f_1 + alpha·S_1 + beta)         (f_N + alpha·S_n + beta)
+
+    expr LHS = 1;
+    expr RHS1 = 0;
+    for (int i = 0; i < length(gsum_require); ++i) {
+        LHS = LHS * gsum_require[i];
+
+        expr tmp = 1;
+        for (int j = 0; j < length(gsum_require); ++j) {
+            if (j != i) {
+                tmp = tmp * gsum_require[j];
+            }
+        }
+        RHS1 = RHS1 + tmp;
+    }
+
+    expr RHS2a = LHS;
+    expr RHS2b = 0;
+    for (int i = 0; i < length(gsum_provide); ++i) {
+        LHS = LHS * gsum_provide[i];
+        RHS1 = RHS1 * gsum_provide[i];
+
+        expr tmp = 1;
+        for (int j = 0; j < length(gsum_provide); ++j) {
+            if (j != i) {
+                tmp = tmp * gsum_provide[j];
+            }
+        }
+        RHS2b = RHS2b + tmp;
+    }
+
+    expr RHS2 = RHS2a * RHS2b;
+    expr RHS = RHS1 - RHS2;
+
+    col fixed L1 = [1,0...];
+
+    (gsum - 'gsum) * LHS === RHS;
+    L1' * gsum === 0;
+}
+
+// It checks wheter there is some connection check without either provide or require
+private function check_connection_was_completed() {
+    for (int opid in proof.std.connect.opids) {
+        if (proof.std.connect.`id${opid}`.require == 0) {
+            error(`Connection #${opid} defined without require`);
+        }
+        if (proof.std.connect.`id${opid}`.provide == 0) {
+            error(`Connection #${opid} defined without provide`);
+        }
+    }
+}