Skip to content

Commit

Permalink
Col to expression renaming
Browse files Browse the repository at this point in the history
  • Loading branch information
hecmas committed Dec 12, 2024
1 parent 536f319 commit 4f5c057
Show file tree
Hide file tree
Showing 8 changed files with 233 additions and 232 deletions.
2 changes: 1 addition & 1 deletion pil2-components/lib/std/pil/std_connection.pil
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ require "std_constants.pil";
require "std_permutation.pil";

/*
* Module for performing connection checks on expression vectors of any degree,
* Module for performing connection checks on columns,
* as described in https://eprint.iacr.org/2019/953.pdf.
*
* This module facilitates connection checks between vectors of expressions, reducing the problem
Expand Down
82 changes: 41 additions & 41 deletions pil2-components/lib/std/pil/std_direct.pil
Original file line number Diff line number Diff line change
Expand Up @@ -17,69 +17,69 @@ const int DEFAULT_DIRECT_BUS_TYPE = PIOP_BUS_SUM;
/**
* Performs a local direct update to the bus.
*
* @param opid The operation ID that uniquely identifies this direct update operation.
* @param cols The vector of expressions to be updated in the direct update operation.
* @param sel A selector to parameterize the direct update operation.
* Defaults to `1`, meaning the direct update is performed.
* @param proves A flag specifying whether the direct update operation is a prove or an assume.
* Defaults to `1`, meaning the operation is a prove.
* @param bus_type The bus type to use for the direct update operation.
* @param name An optional name for the PIOP consuming the direct update operation.
* This is useful for debugging and tracing operations.
* @param opid The operation ID that uniquely identifies this direct update operation.
* @param expressions The vector of expressions to be updated in the direct update operation.
* @param sel A selector to parameterize the direct update operation.
* Defaults to `1`, meaning the direct update is performed.
* @param proves A flag specifying whether the direct update operation is a prove or an assume.
* Defaults to `1`, meaning the operation is a prove.
* @param bus_type The bus type to use for the direct update operation.
* @param name An optional name for the PIOP consuming the direct update operation.
* This is useful for debugging and tracing operations.
*/
function direct_update(const int opid, const expr cols[], const expr sel = 1, const int proves = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_initial_checks(cols, sel);
function direct_update(const int opid, const expr expressions[], const expr sel = 1, const int proves = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_initial_checks(expressions, sel);

if (AIR_ID == -1) {
error("A direct update has to be performed inside an air");
}

direct_to_bus(opid, cols, sel, proves, bus_type, name, PIOP_DIRECT_TYPE_AIR);
direct_to_bus(opid, expressions, sel, proves, bus_type, name, PIOP_DIRECT_TYPE_AIR);
}

function direct_update_assumes(const int opid, const expr cols[], const expr sel = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_update(opid, cols, sel, 0, bus_type, name);
function direct_update_assumes(const int opid, const expr expressions[], const expr sel = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_update(opid, expressions, sel, 0, bus_type, name);
}

function direct_update_proves(const int opid, const expr cols[], const expr sel = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_update(opid, cols, sel, 1, bus_type, name);
function direct_update_proves(const int opid, const expr expressions[], const expr sel = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_update(opid, expressions, sel, 1, bus_type, name);
}

/**
* Performs a global direct update to the bus.
*
* @param opid The operation ID that uniquely identifies this direct update operation.
* @param cols The vector of expressions to be updated in the direct update operation.
* @param sel A selector to parameterize the direct update operation.
* Defaults to `1`, meaning the direct update is performed.
* @param proves A flag specifying whether the direct update operation is a prove or an assume.
* Defaults to `1`, meaning the operation is a prove.
* @param bus_type The bus type to use for the direct update operation.
* @param name An optional name for the PIOP consuming the direct update operation.
* This is useful for debugging and tracing operations.
* @param opid The operation ID that uniquely identifies this direct update operation.
* @param expressions The vector of expressions to be updated in the direct update operation.
* @param sel A selector to parameterize the direct update operation.
* Defaults to `1`, meaning the direct update is performed.
* @param proves A flag specifying whether the direct update operation is a prove or an assume.
* Defaults to `1`, meaning the operation is a prove.
* @param bus_type The bus type to use for the direct update operation.
* @param name An optional name for the PIOP consuming the direct update operation.
* This is useful for debugging and tracing operations.
*/
function direct_global_update(const int opid, const expr cols[], const expr sel = 1, const int proves = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_initial_checks(cols, sel);
function direct_global_update(const int opid, const expr expressions[], const expr sel = 1, const int proves = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_initial_checks(expressions, sel);

direct_to_bus(opid, cols, sel, proves, bus_type, name, PIOP_DIRECT_TYPE_GLOBAL);
direct_to_bus(opid, expressions, sel, proves, bus_type, name, PIOP_DIRECT_TYPE_GLOBAL);
}

function direct_global_update_assumes(const int opid, const expr cols[], const expr sel = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_global_update(opid, cols, sel, 0, bus_type, name);
function direct_global_update_assumes(const int opid, const expr expressions[], const expr sel = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_global_update(opid, expressions, sel, 0, bus_type, name);
}

function direct_global_update_proves(const int opid, const expr cols[], const expr sel = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_global_update(opid, cols, sel, 1, bus_type, name);
function direct_global_update_proves(const int opid, const expr expressions[], const expr sel = 1, const int bus_type = PIOP_BUS_DEFAULT, const int name = PIOP_NAME_DEFAULT) {
direct_global_update(opid, expressions, sel, 1, bus_type, name);
}

private function direct_initial_checks(const expr cols[], const expr sel) {
private function direct_initial_checks(const expr expressions[], const expr sel) {
if (AIRGROUP_ID == -1) {
error("A direct update has to be performed inside an airgroup");
}

for (int i = 0; i < length(cols); i++) {
if (degree(cols[i]) > 0) {
error(`Only field elements can be used for a direct update. The column[${i}] = ${cols[i]} is not a field element`);
for (int i = 0; i < length(expressions); i++) {
if (degree(expressions[i]) > 0) {
error(`Only field elements can be used for a direct update. The expression[${i}] = ${expressions[i]} is not a field element`);
}
}

Expand All @@ -88,23 +88,23 @@ private function direct_initial_checks(const expr cols[], const expr sel) {
}
}

private function direct_to_bus(const int opid, const expr cols[], const expr sel, const int proves, const int bus_type, const int name, const int direct_type) {
private function direct_to_bus(const int opid, const expr expressions[], const expr sel, const int proves, const int bus_type, const int name, const int direct_type) {
if (name == PIOP_NAME_DEFAULT) name = DEFAULT_DIRECT_NAME;

if (bus_type == PIOP_BUS_DEFAULT) bus_type = DEFAULT_DIRECT_BUS_TYPE;

switch (bus_type) {
case PIOP_BUS_SUM:
if (proves) {
sum_proves(name, [opid], opid, cols, sel, direct_type);
sum_proves(name, [opid], opid, expressions, sel, direct_type);
} else {
sum_assumes(name, [opid], opid, cols, sel, direct_type);
sum_assumes(name, [opid], opid, expressions, sel, direct_type);
}
case PIOP_BUS_PROD:
if (proves) {
prod_proves(name, opid, cols, sel, direct_type);
prod_proves(name, opid, expressions, sel, direct_type);
} else {
prod_assumes(name, opid, cols, sel, direct_type);
prod_assumes(name, opid, expressions, sel, direct_type);
}
default:
error(`Unknown bus type: ${bus_type} for opid: ${opid}`);
Expand Down
64 changes: 32 additions & 32 deletions pil2-components/lib/std/pil/std_lookup.pil
Original file line number Diff line number Diff line change
Expand Up @@ -10,87 +10,87 @@ require "std_sum.pil";
* The assumed vector is (optionally) assumed to receive a selector `sel` that should be either equal to 0 or 1.
* The proven vector is (optionally) proven to receive a multiplicity `mul` that should be equal to some non-negative integer.
* Example:
* // Assume the values in `cols_assume` under selector `sel` and prove the values in `cols_prove` with multiplicity `mul`.
* lookup_assumes(opid, cols_assume, sel);
* lookup_proves(opid, cols_prove, mul);
* // Assume the values in `expressions_assume` under selector `sel` and prove the values in `expressions_prove` with multiplicity `mul`.
* lookup_assumes(opid, expressions_assume, sel);
* lookup_proves(opid, expressions_prove, mul);
*
* 2. **Free Lookup**:
* Syntax where the responsibility of assuming or proving is left to the user-specified selector:
* - In rows where `mul` is negative, the lookup behaves as an assume.
* - In rows where `mul` is positive, the lookup behaves as a prove.
* Example:
* // Perform a lookup where responsibility alternates based on the value of `mul`.
* lookup(opid, cols, mul);
* lookup(opid, expressions, mul);
*
* 3. **Dynamic Lookup**:
* Given a vector of operation ids, a "assumed" vector and a expression `sum_id`, it performs a lookup where
* the vector has an operation id that is dynamically selected by the `sum_id` expression.
* Example:
* // Dynamically perform a lookup using a sum ID expression.
* lookup_assumes_dynamic(opids, sumid, cols, sel);
* lookup_assumes_dynamic(opids, sumid, expressions, sel);
*/

const int DEFAULT_LOOKUP_NAME = PIOP_NAME_LOOKUP;

/**
* Performs the "assumes" part of a lookup check.
*
* @param opid The operation ID that uniquely identifies this lookup operation.
* @param cols The vector of expressions to be assumed in the lookup check.
* @param sel A selector specifying which rows are subject to the lookup check.
* Defaults to `1`, meaning all rows are included.
* @param name An optional name for the PIOP consuming the lookup check.
* This is useful for debugging and tracing operations.
* @param opid The operation ID that uniquely identifies this lookup operation.
* @param expressions The vector of expressions to be assumed in the lookup check.
* @param sel A selector specifying which rows are subject to the lookup check.
* Defaults to `1`, meaning all rows are included.
* @param name An optional name for the PIOP consuming the lookup check.
* This is useful for debugging and tracing operations.
*/
function lookup_assumes(const int opid, const expr cols[], const expr sel = 1, int name = PIOP_NAME_DEFAULT) {
function lookup_assumes(const int opid, const expr expressions[], const expr sel = 1, int name = PIOP_NAME_DEFAULT) {
if (name == PIOP_NAME_DEFAULT) name = DEFAULT_LOOKUP_NAME;

sum_assumes(name, [opid], opid, cols, sel);
sum_assumes(name, [opid], opid, expressions, sel);
}

/**
* Performs the "proves" part of a lookup check.
*
* @param opid The operation ID that uniquely identifies this lookup operation.
* @param cols The vector of expressions to be proven in the lookup check.
* @param expressions The vector of expressions to be proven in the lookup check.
* @param mul A multiplicity specifying how many times rows have been looked up.
* @param name An optional name for the PIOP consuming the lookup check.
* This is useful for debugging and tracing operations.
*/
function lookup_proves(const int opid, const expr cols[], const expr mul = 1, int name = PIOP_NAME_DEFAULT) {
function lookup_proves(const int opid, const expr expressions[], const expr mul = 1, int name = PIOP_NAME_DEFAULT) {
if (name == PIOP_NAME_DEFAULT) name = DEFAULT_LOOKUP_NAME;

sum_proves(name, [opid], opid, cols, mul);
sum_proves(name, [opid], opid, expressions, mul);
}

/**
* Performs a raw lookup check.
*
* @param opid The operation ID that uniquely identifies this lookup operation.
* @param cols The vector of expressions.
* @param mul A multiplicity specifying how many times rows are part of the lookup.
* @param name An optional name for the PIOP consuming the lookup check.
* This is useful for debugging and tracing operations.
* @param opid The operation ID that uniquely identifies this lookup operation.
* @param expressions The vector of expressions.
* @param mul A multiplicity specifying how many times rows are part of the lookup.
* @param name An optional name for the PIOP consuming the lookup check.
* This is useful for debugging and tracing operations.
*/
function lookup(const int opid, const expr cols[], const expr mul = 1, int name = PIOP_NAME_DEFAULT) {
function lookup(const int opid, const expr expressions[], const expr mul = 1, int name = PIOP_NAME_DEFAULT) {
if (name == PIOP_NAME_DEFAULT) name = DEFAULT_LOOKUP_NAME;

sum(name, 2, [opid], opid, cols, mul);
sum(name, 2, [opid], opid, expressions, mul);
}

/**
* Performs a dynamic lookup check.
*
* @param opids The vector of operation IDs that uniquely identify this lookup operation.
* @param sumid The expression that dynamically selects the operation ID from `opids`.
* @param cols The vector of expressions.
* @param sel A selector specifying which rows are subject to the lookup check.
* Defaults to `1`, meaning all rows are included.
* @param name An optional name for the PIOP consuming the lookup check.
* This is useful for debugging and tracing operations.
* @param opids The vector of operation IDs that uniquely identify this lookup operation.
* @param sumid The expression that dynamically selects the operation ID from `opids`.
* @param expressions The vector of expressions.
* @param sel A selector specifying which rows are subject to the lookup check.
* Defaults to `1`, meaning all rows are included.
* @param name An optional name for the PIOP consuming the lookup check.
* This is useful for debugging and tracing operations.
*/
function lookup_assumes_dynamic(const int opids[], const expr sumid, const expr cols[], const expr sel = 1, int name = PIOP_NAME_DEFAULT) {
function lookup_assumes_dynamic(const int opids[], const expr sumid, const expr expressions[], const expr sel = 1, int name = PIOP_NAME_DEFAULT) {
if (name == PIOP_NAME_DEFAULT) name = DEFAULT_LOOKUP_NAME;

sum_assumes(name, opids, sumid, cols, sel);
sum_assumes(name, opids, sumid, expressions, sel);
}
Loading

0 comments on commit 4f5c057

Please sign in to comment.