Skip to content

Commit

Permalink
Grand fixes, small refactors and cleanups
Browse files Browse the repository at this point in the history
  • Loading branch information
@hecmas
hecmas committed Dec 13, 2024
1 parent a246f5f commit 0df9e72
Show file tree
Hide file tree
Showing 9 changed files with 247 additions and 275 deletions.
9 changes: 9 additions & 0 deletions pil2-components/lib/std/pil/std_constants.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,15 @@ const int PIOP_BUS_DEFAULT = 0;
const int PIOP_BUS_SUM = 1;
const int PIOP_BUS_PROD = 2;

function set_bus_type(const int bus_type) {
if (bus_type != PIOP_BUS_SUM && bus_type != PIOP_BUS_PROD) {
error(`Unknown bus type: ${bus_type}`);
}

// Set the bus type for the std components that allow for different bus types
DEFAULT_PERMUTATION_BUS_TYPE = bus_type;
}

/*
Available direct types:

Expand Down
8 changes: 4 additions & 4 deletions pil2-components/lib/std/pil/std_lookup.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ require "std_sum.pil";
* 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, expressions, sel);
* lookup_assumes_dynamic(opids, busid, expressions, sel);
*/

const int DEFAULT_LOOKUP_NAME = PIOP_NAME_LOOKUP;
Expand Down Expand Up @@ -82,15 +82,15 @@ function lookup(const int opid, const expr expressions[], const expr mul = 1, in
* 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 busid 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 expressions[], const expr sel = 1, int name = PIOP_NAME_DEFAULT) {
function lookup_assumes_dynamic(const int opids[], const expr busid, 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, expressions, sel);
sum_assumes(name, opids, busid, expressions, sel);
}
214 changes: 103 additions & 111 deletions pil2-components/lib/std/pil/std_prod.pil
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
require "std_constants.pil";
require "std_tools.pil";

// Note: When name is "isolated" we don't check if the number of expressions is the same for all the PIOPs

function prod_assumes(const int name, const int opid, const expr expressions[], const expr sel = 1, const int direct_type = PIOP_DIRECT_TYPE_DEFAULT) {
update_piop_prod(name, 0, opid, sel, expressions, direct_type);
}
Expand All @@ -11,18 +9,78 @@ function prod_proves(const int name, const int opid, const expr expressions[], c
update_piop_prod(name, 1, opid, sel, expressions, direct_type);
}

/**
* It updates the product check constraints.
*
* @param name The name of the PIOP consuming the product check
* @param proves 1 if the PIOP proves a statement, 0 if it assumes a statement
* @param opid The ID that uniquely identifies the PIOP in the bus
* @param sel The selector of the PIOP
* @param expressions The vector of expressions of the PIOP
* @param direct_type Defines wheter the update has to be done at the global, air or default level
*/
private function update_piop_prod(const int name, const int proves, const int opid, const expr sel, const expr expressions[], const int direct_type = PIOP_DIRECT_TYPE_DEFAULT) {
const int exprs_num = length(expressions);
if (exprs_num < 1) {
string side = proves ? "proves" : "assumes";
error(`The number of expressions of ${side} #${opid} must be at least 1`);
}

init_proof_containers_prod(name, opid);

if (direct_type == PIOP_DIRECT_TYPE_AIR || direct_type == PIOP_DIRECT_TYPE_DEFAULT) {
init_air_containers_prod(name);
}

// Create debug hints for the witness computation
string name_expr[exprs_num];
expr sum_expr = 0;
for (int i = 0; i < exprs_num; i++) {
name_expr[i] = string(expressions[i]);
sum_expr += expressions[i];
}
@gprod_member_data{name_piop: get_piop_name(name), name_expr: name_expr, busid: opid, is_global: direct_type == PIOP_DIRECT_TYPE_GLOBAL,
proves: proves, selector: sel, expressions: expressions, deg_expr: degree(sum_expr), deg_sel: degree(sel)};

initial_checks_prod(proves, opid, exprs_num, direct_type);

// selected vector to simple expression reduction
expr exprs_compressed = compress_exprs(opid, expressions);

switch (direct_type) {
case PIOP_DIRECT_TYPE_GLOBAL:
gprod_update_global_constraint_data(proves, sel, exprs_compressed);
case PIOP_DIRECT_TYPE_AIR, PIOP_DIRECT_TYPE_DEFAULT:
gprod_update_air_constraint_data(proves, sel, exprs_compressed, direct_type);

// Update the constraints at the air level
on final air piop_gprod_air();

// Update the constraints at the airgroup level
on final airgroup piop_gprod_airgroup();
default:
error("Invalid direct_type: ${direct_type}");
}

// Update the constraints at the proof level
on final proof piop_gprod_proof();

// At the end, check consistency of all the opids
on final proof check_opids_were_completed_prod();
}

private function init_proof_containers_prod(const int name, const int opid) {
container proof.std.gprod {
// Used for final checks
int opids_count = 0;
int opids[100];

// Resulting product of every airgroup and every air
// It is the accumulation of each partial product that each instance
// of each air constributes to. It must be zero at the end.
// It is the accumulation of each partial product that each air
// constributes to.
expr gprod = 1;

// Direct shortcut to the previous product
// Direct-related data, used to update `gprod` at the proof level
int direct_gprod_assumes_count = 0;
expr direct_gprod_assumes_sel[100];
expr direct_gprod_assumes[100];
Expand All @@ -32,17 +90,20 @@ private function init_proof_containers_prod(const int name, const int opid) {
expr direct_gprod_proves[100];
}

// Container used for final checks
// Opid-specific data
// It must be defined at the proof level because the same opid can appear in different airs
container proof.std.gprod.`id${opid}` {
int name = name;
int expressions;
int exprs_num;
int proves = 0;
int assumes = 0;
}
}

private function init_air_containers_prod(const int name) {
// AIR-specific data
container air.std.gprod {
// Assumes and proves of the air
int gprod_assumes_count = 0;
expr gprod_assumes_sel[100];
expr gprod_assumes[100];
Expand All @@ -51,7 +112,7 @@ private function init_air_containers_prod(const int name) {
expr gprod_proves_sel[100];
expr gprod_proves[100];

// Direct shortcut to the previous product
// Direct-related data, used to update `gprod` at the air level
int direct_gprod_assumes_count = 0;
expr direct_gprod_assumes_sel[100];
expr direct_gprod_assumes[100];
Expand All @@ -62,91 +123,39 @@ private function init_air_containers_prod(const int name) {
}
}

private function initial_checks_prod(const int proves, const int opid, const int exprs_count, const int direct_type) {
private function initial_checks_prod(const int proves, const int opid, const int exprs_num, const int direct_type) {
// Assumes and proves of the same opid must have the same number of expressions
if (proof.std.gprod.`id${opid}`.expressions == 0) {
// first time called
proof.std.gprod.`id${opid}`.expressions = exprs_count;
// add opid on a list to verify at final
if (proof.std.gprod.`id${opid}`.exprs_num == 0) {
// The first time we see this opid, we store the number of expressions
proof.std.gprod.`id${opid}`.exprs_num = exprs_num;

// Store the opid to check at the end that all the opids have been completed
proof.std.gprod.opids[proof.std.gprod.opids_count] = opid;
proof.std.gprod.opids_count++;
} else if (exprs_count != proof.std.gprod.`id${opid}`.expressions) {
const int expected_exprs = proof.std.gprod.`id${opid}`.expressions;
error(`The number of expressions of PIOP #${opid} must be ${expected_exprs} but was ${exprs_count}`);
} else if (exprs_num != proof.std.gprod.`id${opid}`.exprs_num) {
// If this is not the first time we see this opid, we check that the number of expressions is the same
const int expected_exprs = proof.std.gprod.`id${opid}`.exprs_num;
error(`The number of expressions of PIOP #${opid} must be ${expected_exprs} but was ${exprs_num}`);
}

// The same opid is shared among multiple instances of the same air, so we must keep track of the number of
// proves and assumes to verify at the end that all of them match
const string name_str = proves ? "proves" : "assumes";
proof.std.gprod.`id${opid}`.`${name_str}`++;
}

/**
* Given a selector sel and expressions C₀,...,Cₙ₋₁, it:
* · 1] defines the running grandproduct constraints for each air
* · 2] add each airgroupvalue of each airgroup to the running prod
* · 3] checks that the overall prod is zero
* @param name name of the PIOP
* @param proves boolean indicating if updating a proves or a assumes
* @param opid (unique) identifier of the PIOP
* @param sel selector of the PIOP
* @param expressions expressions of the PIOP
*/
private function update_piop_prod(const int name, const int proves, const int opid, const expr sel, const expr expressions[], const int direct_type = PIOP_DIRECT_TYPE_DEFAULT) {
const int exprs_count = length(expressions);
if (exprs_count < 1) {
string side = proves ? "proves" : "assumes";
error(`The number of expressions of ${side} #${opid} must be at least 1`);
}

init_proof_containers_prod(name, opid);

if (direct_type == PIOP_DIRECT_TYPE_AIR || direct_type == PIOP_DIRECT_TYPE_DEFAULT) {
init_air_containers_prod(name);
}

// Create debug hints for the witness computation
string name_expr[exprs_count];
expr sum_expr = 0;
for (int i = 0; i < exprs_count; i++) {
name_expr[i] = string(expressions[i]);
sum_expr += expressions[i];
}
@gprod_member_data{name_piop: get_piop_name(name), name_expr: name_expr, opid: opid, is_global: direct_type == PIOP_DIRECT_TYPE_GLOBAL,
proves: proves, selector: sel, expressions: expressions, deg_expr: degree(sum_expr), deg_sel: degree(sel)};

initial_checks_prod(proves, opid, exprs_count, direct_type);

init_challenges();

// selected vector to simple expression reduction
expr exprs_compressed = compress_exprs(opid, expressions);

switch (direct_type) {
case PIOP_DIRECT_TYPE_GLOBAL:
gprod_update_global_constraint_data(proves, sel, exprs_compressed);
case PIOP_DIRECT_TYPE_AIR, PIOP_DIRECT_TYPE_DEFAULT:
gprod_update_air_constraint_data(proves, sel, exprs_compressed, direct_type);
default:
error("Invalid direct_type: ${direct_type}");
}

// Define and update constraints at the proof level
on final proof piop_gprod_proof();
// The same opid can appear in different airs, so we keep track of the number of proves and assumes
// for final checks
const string is_proves_str = proves ? "proves" : "assumes";
proof.std.gprod.`id${opid}`.`${is_proves_str}`++;
}

private function gprod_update_global_constraint_data(const int proves, const expr sel, const expr exprs_compressed) {
use proof.std.gprod;
use proof.std.gprod;

if (proves) {
direct_gprod_proves_sel[direct_gprod_proves_count] = sel;
direct_gprod_proves[direct_gprod_proves_count] = exprs_compressed;
direct_gprod_proves_count++;
} else {
direct_gprod_assumes_sel[direct_gprod_assumes_count] = sel;
direct_gprod_assumes[direct_gprod_assumes_count] = exprs_compressed;
direct_gprod_assumes_count++;
}
if (proves) {
direct_gprod_proves_sel[direct_gprod_proves_count] = sel;
direct_gprod_proves[direct_gprod_proves_count] = exprs_compressed;
direct_gprod_proves_count++;
} else {
direct_gprod_assumes_sel[direct_gprod_assumes_count] = sel;
direct_gprod_assumes[direct_gprod_assumes_count] = exprs_compressed;
direct_gprod_assumes_count++;
}
}

private function gprod_update_air_constraint_data(const int proves, const expr sel, const expr exprs_compressed, const int direct_type) {
Expand All @@ -172,25 +181,14 @@ private function gprod_update_air_constraint_data(const int proves, const expr s
gprod_assumes[gprod_assumes_count] = exprs_compressed;
gprod_assumes_count++;
}

// at the end, check consistency of all the opids
on final proof check_opids_were_completed_prod();
}

// Define and update constraints at the air level
on final air piop_gprod_air();

// Define and update constraints at the airgroup level
on final airgroup piop_gprod_airgroup();
}

/**
* It defines the constraints for the grandproduct based on the rapidUp protocol https://eprint.iacr.org/2022/1050.pdf
*/
// Deferred functions
private function piop_gprod_air() {
use air.std.gprod;

col fixed _L1 = [1,0...]; // TODO: Fix
const expr L1 = get_L1(); // [1,0,...]

col witness stage(2) gprod;

Expand All @@ -202,6 +200,10 @@ private function piop_gprod_air() {
//
// Note: The ti and fi are not necessarily related to each other

if (!defined(std_gamma)) {
challenge stage(2) std_gamma;
}

expr air_num = 1;
for (int i = 0; i < gprod_proves_count; i++) {
air_num *= (gprod_proves_sel[i] * (gprod_proves[i] + std_gamma - 1) + 1);
Expand All @@ -215,7 +217,7 @@ private function piop_gprod_air() {
// At this point, the constraint has been transformed to:
// gprod === ('gprod * (1 - L1) + L1) * air_num / air_den
// check that the constraint is satisfied
gprod * air_den === ('gprod * (1 - _L1) + _L1) * air_num;
gprod * air_den === ('gprod * (1 - L1) + L1) * air_num;


/*
Expand All @@ -239,26 +241,22 @@ private function piop_gprod_air() {

@gprod_col{reference: gprod, numerator_air: air_num, denominator_air: air_den,
numerator_direct: air_num, denominator_direct: air_den, result: gprod_result};
_L1' * (gprod_result * direct_den - gprod * direct_num) === 0;
L1' * (gprod_result * direct_den - gprod * direct_num) === 0;
}

// Note: We don't "update" the prod at the airgroup level (i.e., all the resulting prods generated by each air)
// because we don't know how many airs will be generated at compile time. Therefore we use the same
// term to refer to both things: the value generated at each air and the value generated at each airgroup.
// It is like jumping from the air level to the proof (global) level, from the constraint point of view.

/**
* It updates the expression for the grandprod at the proof level indirectly with the airgroup values
*/
private function piop_gprod_airgroup() {
// The `gprod_result` from each airgroup is added to the overall global product
proof.std.gprod.gprod *= gprod_result;
}

/**
* It defines the constraints for the grandprod at the proof level
*/
private function piop_gprod_proof() {
use proof.std.gprod;

//
// gprod · f(s_1·(e_1 - 1) + 1) · f(s_2·(e_2 - 1) + 1) · f(s_3·(e_3 - 1) + 1) === 1
//
Expand All @@ -274,8 +272,6 @@ private function piop_gprod_proof() {
// Note: We cannot update this constraint directly if some of the elements
// are not globally defined: constants, public inputs, airgroupvalues, ...

use proof.std.gprod;

expr global_num = 1;
for (int i = 0; i < direct_gprod_proves_count; i++) {
global_num *= (direct_gprod_proves_sel[i] * (direct_gprod_proves[i] + std_gamma - 1) + 1);
Expand All @@ -289,10 +285,6 @@ private function piop_gprod_proof() {
gprod * global_num === global_den;
}

/**
* It checks that all the assumes and proves of the same opid have been defined
* @param name name of the PIOP
*/
private function check_opids_were_completed_prod() {
for (int i = 0; i < proof.std.gprod.opids_count; i++) {
int opid = proof.std.gprod.opids[i];
Expand Down
Loading

0 comments on commit 0df9e72

Please sign in to comment.