Skip to content

Commit

Permalink
Final fixes done
Browse files Browse the repository at this point in the history
  • Loading branch information
hecmas committed Oct 16, 2024
1 parent 8b34152 commit d1fb1b6
Show file tree
Hide file tree
Showing 3 changed files with 18 additions and 39 deletions.
18 changes: 11 additions & 7 deletions pil2-components/lib/std/pil/std_prod.pil
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ private function init_containers_prod(int name, int opid) {
private function initial_checks_prod(int proves, int opid, expr cols[], int is_direct) {
const int cols_count = length(cols);

// Assumes and proves of the same opid must have the same number of columns
// Assumes and proves of the same opid must have the same number of columns (except for the is_direct case)
if (proof.std.gprod.`id${opid}`.cols == 0) {
// first time called
proof.std.gprod.`id${opid}`.cols = cols_count;
Expand All @@ -70,11 +70,13 @@ private function initial_checks_prod(int proves, int opid, expr cols[], int is_d
}

// 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
if (proves) {
proof.std.gprod.`id${opid}`.proves++;
// proves and assumes to verify at the end that all of them match (except for the is_direct case)
const string name_str = proves ? "proves" : "assumes";
const string other_name_str = proves ? "assumes" : "proves";
if (!is_direct) {
proof.std.gprod.`id${opid}`.`${name_str}`++;
} else {
proof.std.gprod.`id${opid}`.assumes++;
proof.std.gprod.`id${opid}`.`${name_str}` = proof.std.gprod.`id${opid}`.`${other_name_str}`;
}
}

Expand Down Expand Up @@ -240,8 +242,8 @@ private function piop_gprod_proof() {
* @param name name of the PIOP
*/
private function check_opids_were_completed_prod() {
for (int index = 0; index < proof.std.gprod.opids_count; index++) {
int opid = proof.std.gprod.opids[index];
for (int i = 0; i < proof.std.gprod.opids_count; i++) {
int opid = proof.std.gprod.opids[i];
use proof.std.gprod.`id${opid}`;

if (name == PIOP_NAME_ISOLATED) continue;
Expand All @@ -252,6 +254,8 @@ private function check_opids_were_completed_prod() {
error(`${name_str} #${opid} defined without assume`);
} else if (proves == 0) {
error(`${name_str} #${opid} defined without proves`);
}else if (assumes != proves) {
error(`${name_str} #${opid} defined with #${assumes} assumes and #${proves} proves`);
}
}
}
7 changes: 2 additions & 5 deletions pil2-components/lib/std/pil/std_sum.pil
Original file line number Diff line number Diff line change
Expand Up @@ -72,11 +72,8 @@ private function initial_checks_sum(int proves, int opid[], expr cols[], int is_

// 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
if (proves) {
proof.std.gsum.`id${opid[i]}`.proves++;
} else {
proof.std.gsum.`id${opid[i]}`.assumes++;
}
const string name_str = proves ? "proves" : "assumes";
proof.std.gsum.`id${opid[i]}`.`${name_str}`++;
}
}

Expand Down
32 changes: 5 additions & 27 deletions pil2-components/test/std/special/direct_update.pil
Original file line number Diff line number Diff line change
Expand Up @@ -26,32 +26,14 @@ airtemplate DirectUpdateLookup(const int N = 2**5) {
const int OP_BUS_ID = 200;
const int OPID = 444;

col witness a[2],b[2],c[2];
col witness flag;
col witness perform_operation;
lookup_assumes(OP_BUS_ID, [OPID, ...a, ...b, ...c, flag], sel: perform_operation);

for (int i = 0; i < length(input2)/2; i++) {
direct_update(OP_BUS_ID, [OPID, 0, 0, i, 0, input2[2*i], input2[2*i+1], 0])
}
}

airtemplate DirectUpdateExhaustive(const int N = 2**4) {

const int OPID = 19;
const int VALUE1 = 256;
const int VALUE2 = 111;
const int VALUE3 = 222;
const int SEL = 1;

col witness a;

permutation_assumes(OPID, [a]);

direct_update(OPID, [VALUE1], SEL, bus_type: PIOP_BUS_PROD);
direct_update(OPID, [VALUE2], 1-SEL, bus_type: PIOP_BUS_PROD);
direct_update(OPID, [VALUE3], SEL, bus_type: PIOP_BUS_PROD);
direct_update(OPID, [VALUE2], 1-SEL, bus_type: PIOP_BUS_PROD);
col witness a[2],b[2],c[2];
col witness flag;
col witness perform_operation;
lookup_assumes(OP_BUS_ID, [OPID, ...a, ...b, ...c, flag], sel: perform_operation);
}

// TODO: Do an example with multiple elements in the direct_update
Expand All @@ -62,8 +44,4 @@ airgroup Permutation {

airgroup Lookup {
DirectUpdateLookup();
}

// airgroup TestAll {
// DirectUpdateExhaustive();
// }
}

0 comments on commit d1fb1b6

Please sign in to comment.