Skip to content

Commit

Permalink
Merge pull request #79 from 0xPolygonHermez/feature/pil-binary-update-2
Browse files Browse the repository at this point in the history 
Feature/pil binary update 2
  • Loading branch information
@zkronos73
zkronos73 authored Sep 12, 2024
2 parents f0d8474 + 7adce52 commit ad7a5c9
Show file tree
Hide file tree
Showing 10 changed files with 121 additions and 75 deletions.
30 changes: 14 additions & 16 deletions pil/fork_0/pil/zisk.pil
View file
Original file line number Diff line number Diff line change
@@ -1,32 +1,30 @@
require "constants.pil"
// require "std_permutation.pil"
require "../../../state-machines/main/pil/main.pil"
// require "binary/pil/binary.pil"
// require "binary/pil/binary_table.pil"
// require "binary/pil/binary_extension.pil"
// require "binary/pil/binary_extension_table.pil"
require "binary/pil/binary.pil"
require "binary/pil/binary_table.pil"
require "binary/pil/binary_extension.pil"
require "binary/pil/binary_extension_table.pil"

const int OPERATION_BUS_ID = 5000;
airgroup Main {
Main(N: 2**21, RC: 2, operation_bus_id: OPERATION_BUS_ID);
}

// airgroup Binary {
// Binary(N: 2**21, operation_bus_id: OPERATION_BUS_ID);
// }
airgroup Binary {
Binary(N: 2**21, operation_bus_id: OPERATION_BUS_ID);
}


/*
airgroup BinaryTable {
BinaryTable(N: 2**21);
BinaryTable(disable_fixed: 1);
}
*/

// airgroup BinaryExtension {
// BinaryExtension(N: 2**21, operation_bus_id: OPERATION_BUS_ID);
// }

/*
airgroup BinaryExtension {
BinaryExtension(N: 2**21, operation_bus_id: OPERATION_BUS_ID);
}

airgroup BinaryExtensionTable {
BinaryExtensionTable(N: 2**21);
BinaryExtensionTable(disable_fixed: 1);
}
*/
Binary file modified pil/fork_0/pil/zisk.pilout
View file
Binary file not shown.
32 changes: 32 additions & 0 deletions pil/fork_0/src/pil_helpers/pilout.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,26 @@ pub const PILOUT_HASH: &[u8] = b"Zisk-hash";

pub const MAIN_SUBPROOF_ID: &[usize] = &[0];

pub const BINARY_SUBPROOF_ID: &[usize] = &[1];

pub const BINARY_TABLE_SUBPROOF_ID: &[usize] = &[2];

pub const BINARY_EXTENSION_SUBPROOF_ID: &[usize] = &[3];

pub const BINARY_EXTENSION_TABLE_SUBPROOF_ID: &[usize] = &[4];

//AIR CONSTANTS

pub const MAIN_AIR_IDS: &[usize] = &[0];

pub const BINARY_AIR_IDS: &[usize] = &[0];

pub const BINARY_TABLE_AIR_IDS: &[usize] = &[0];

pub const BINARY_EXTENSION_AIR_IDS: &[usize] = &[0];

pub const BINARY_EXTENSION_TABLE_AIR_IDS: &[usize] = &[0];

pub struct Pilout;

impl Pilout {
Expand All @@ -22,6 +38,22 @@ impl Pilout {

air_group.add_air(Some("Main"), 2097152);

let air_group = pilout.add_air_group(Some("Binary"));

air_group.add_air(Some("Binary"), 2097152);

let air_group = pilout.add_air_group(Some("BinaryTable"));

air_group.add_air(Some("BinaryTable"), 4194304);

let air_group = pilout.add_air_group(Some("BinaryExtension"));

air_group.add_air(Some("BinaryExtension"), 2097152);

let air_group = pilout.add_air_group(Some("BinaryExtensionTable"));

air_group.add_air(Some("BinaryExtensionTable"), 524288);

pilout
}
}
12 changes: 10 additions & 2 deletions pil/fork_0/src/pil_helpers/traces.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,17 @@ trace!(Main0Row, Main0Trace<F> {
});

trace!(Binary0Row, Binary0Trace<F> {
op: F, mode32: F, free_in_a: [F; 8], free_in_b: [F; 8], free_in_c: [F; 8], carry: [F; 9], use_last_carry: F, multiplicity: F,
m_op: F, mode32: F, free_in_a: [F; 8], free_in_b: [F; 8], free_in_c: [F; 8], carry: [F; 9], use_last_carry: F, multiplicity: F,
});

trace!(BinaryTable0Row, BinaryTable0Trace<F> {
multiplicity: F,
});

trace!(BinaryExtension0Row, BinaryExtension0Trace<F> {
op: F, mode8: F, mode16: F, mode32: F, in1: [F; 8], in2_low: F, out: [F; 8], free_in2: [F; 4], multiplicity: F,
m_op: F, mode8: F, mode16: F, mode32: F, in1: [F; 8], in2_low: F, out: [F; 8], free_in2: [F; 4], multiplicity: F,
});

trace!(BinaryExtensionTable0Row, BinaryExtensionTable0Trace<F> {
multiplicity: F,
});
20 changes: 14 additions & 6 deletions state-machines/binary/pil/binary_extension_table.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,20 @@ require "constants.pil"
const int EXT_OP = 6;
const int BINARY_EXTENSION_TABLE_ID = 124;

airtemplate BinaryExtensionTable(const int N = 2**10) {

airtemplate BinaryExtensionTable(const int N = 2**19, const int disable_fixed = 0) {

col witness multiplicity;
lookup_proves(BINARY_EXTENSION_TABLE_ID, cols: [0, 0, 0, 0, 0, 0], mul: multiplicity);
}

airtemplate _BinaryExtensionTable(const int N = 2**19) {
if (disable_fixed) {
col fixed _K = [0...];
// FORCE ONE TRACE
multiplicity * _K === 0;

println("*** DISABLE_FIXED ***");
return;
}

if (N < 2**19) {
error("N must be at least 2^19");
}
Expand All @@ -43,6 +51,7 @@ airtemplate _BinaryExtensionTable(const int N = 2**19) {
col fixed C0; // Output C0 (32 bits)
col fixed C1; // Output C1 (32 bits)
for (int i = 0; i < N; i++) {
println(i);
int [op, offset, a, b] = [OP[i], OFFSET[i], A[i], B[i]];
int _out = 0;
switch (op) {
Expand Down Expand Up @@ -104,6 +113,5 @@ airtemplate _BinaryExtensionTable(const int N = 2**19) {
C1[i] = _out >> 32;
}

col witness mul;
lookup_proves(BINARY_EXTENSION_TABLE_ID, mul, [OP, OFFSET, A, B, C0, C1]);
lookup_proves(BINARY_EXTENSION_TABLE_ID, [OP, OFFSET, A, B, C0, C1], multiplicity);
}
25 changes: 16 additions & 9 deletions state-machines/binary/pil/binary_table.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,12 +26,19 @@ require "constants.pil";
const int EXT_32_OP = 0x23;
const int BINARY_TABLE_ID = 125;

airtemplate BinaryTable(int N = 2**10) {
airtemplate BinaryTable(int N = 2**22, const int disable_fixed = 0) {

col witness multiplicity;
lookup_proves(BINARY_TABLE_ID, [0, 0, 0, 0, 0, 0, 0], multiplicity);
}

airtemplate _BinaryTable(int N = 2**22) {
if (disable_fixed) {
col fixed _K = [0...];
// FORCE ONE TRACE
multiplicity * _K === 0;

println("*** DISABLE_FIXED ***");
return;
}

if (N < 2**22) {
error(`N must be at least 2^22, but N=${N} was provided`);
}
Expand Down Expand Up @@ -77,7 +84,7 @@ airtemplate _BinaryTable(int N = 2**22) {
}

// If the chunk is signed, then the result is the sign of a
if (3 && plast && (a & 0x80) != (b & 0x80)) {
if (op == 0x05 && plast && (a & 0x80) != (b & 0x80)) {
c = (a & 0x80) ? 1 : 0;
cout = c;
}
Expand All @@ -87,7 +94,7 @@ airtemplate _BinaryTable(int N = 2**22) {
cout = 1;
c = plast;
}
if (5 && plast && (a & 0x80) != (b & 0x80)) {
if (op == 0x07 && plast && (a & 0x80) != (b & 0x80)) {
c = (a & 0x80) ? 1 : 0;
cout = c;
}
Expand All @@ -104,7 +111,7 @@ airtemplate _BinaryTable(int N = 2**22) {
} else {
c = b;
}
if (8 && plast && (a & 0x80) != (b & 0x80)) {
if (op == 0x0a && plast && (a & 0x80) != (b & 0x80)) {
c = (a & 0x80) ? a : b;
cout = (a & 0x80) ? 1 : 0;
}
Expand All @@ -116,7 +123,7 @@ airtemplate _BinaryTable(int N = 2**22) {
} else {
c = b;
}
if (10 && plast && (a & 0x80) != (b & 0x80)) {
if (op == 0x0c && plast && (a & 0x80) != (b & 0x80)) {
c = (a & 0x80) ? b : a;
cout = (a & 0x80) ? 0 : 1;
}
Expand Down Expand Up @@ -144,6 +151,6 @@ airtemplate _BinaryTable(int N = 2**22) {
for (int i = 0; i < N; i++) {
FLAGS[i] = COUT[i] + 2 * USE_CARRY[i];
}
col witness multiplicity;

lookup_proves(BINARY_TABLE_ID, [LAST, OP, A, B, CIN, C, FLAGS], multiplicity);
}
50 changes: 25 additions & 25 deletions state-machines/binary/src/binary_basic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,127 +76,127 @@ impl BinaryBasicSM {
match i.opcode {
0x02 /*ADD*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x02);
t.m_op = F::from_canonical_u64(0x02);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x03 /*SUB*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x03);
t.m_op = F::from_canonical_u64(0x03);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x04 /*LTU*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x04);
t.m_op = F::from_canonical_u64(0x04);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x05 /*LT*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x05);
t.m_op = F::from_canonical_u64(0x05);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x06 /*LEU*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x06);
t.m_op = F::from_canonical_u64(0x06);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x07 /*LE*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x07);
t.m_op = F::from_canonical_u64(0x07);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x08 /*EQ*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x08);
t.m_op = F::from_canonical_u64(0x08);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x09 /*MINU*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x09);
t.m_op = F::from_canonical_u64(0x09);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x0a /*MIN*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x0a);
t.m_op = F::from_canonical_u64(0x0a);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x0b /*MAXU*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x0b);
t.m_op = F::from_canonical_u64(0x0b);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x0c /*MAX*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x0c);
t.m_op = F::from_canonical_u64(0x0c);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x20 /*AND*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x20);
t.m_op = F::from_canonical_u64(0x20);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x21 /*OR*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x21);
t.m_op = F::from_canonical_u64(0x21);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x22 /*XOR*/ => {
t.mode32 = F::from_canonical_u64(0);
t.op = F::from_canonical_u64(0x22);
t.m_op = F::from_canonical_u64(0x22);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x12 /*ADD_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x02);
t.m_op = F::from_canonical_u64(0x02);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x13 /*SUB_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x03);
t.m_op = F::from_canonical_u64(0x03);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x14 /*LTU_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x04);
t.m_op = F::from_canonical_u64(0x04);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x15 /*LT_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x05);
t.m_op = F::from_canonical_u64(0x05);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x16 /*LEU_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x06);
t.m_op = F::from_canonical_u64(0x06);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x17 /*LE_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x07);
t.m_op = F::from_canonical_u64(0x07);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x18 /*EQ_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x08);
t.m_op = F::from_canonical_u64(0x08);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x19 /*MINU_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x09);
t.m_op = F::from_canonical_u64(0x09);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x1a /*MIN_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x0a);
t.m_op = F::from_canonical_u64(0x0a);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x1b /*MAXU_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x0b);
t.m_op = F::from_canonical_u64(0x0b);
(c, flag) = opcode_execute(i.opcode, a, b);
}
0x1c /*MAX_W*/ => {
t.mode32 = F::from_canonical_u64(1);
t.op = F::from_canonical_u64(0x0c);
t.m_op = F::from_canonical_u64(0x0c);
(c, flag) = opcode_execute(i.opcode, a, b);
}
_ => panic!("BinaryBasicSM::process_slice() found invalid opcode={}", i.opcode),
Expand Down
Loading

0 comments on commit ad7a5c9

Please sign in to comment.