Skip to content

Commit

Permalink
Merge pull request #49 from 0xPolygonHermez/feature/pil2-stl
Browse files Browse the repository at this point in the history
PIL2 Library
  • Loading branch information
hecmas authored Sep 19, 2023
2 parents a948cf5 + 70d4e27 commit f2f0a37
Show file tree
Hide file tree
Showing 10 changed files with 1,575,612 additions and 258 deletions.
9 changes: 1 addition & 8 deletions src/pil_verifier.js
Original file line number Diff line number Diff line change
Expand Up @@ -392,11 +392,4 @@ function getConnectionMap(F, N, nk) {

cacheConnectionMaps[kc] = m;
return m;
}







}
317 changes: 317 additions & 0 deletions test/pil2/vadcop/std_connect.pil
Original file line number Diff line number Diff line change
@@ -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`);
}
}
}
Loading

0 comments on commit f2f0a37

Please sign in to comment.