Skip to content

Commit

Permalink
chore: modify pil format
Browse files Browse the repository at this point in the history
  • Loading branch information
@ibmp33
ibmp33 committed Dec 28, 2024
1 parent 058d3eb commit 009356f
Show file tree
Hide file tree
Showing 4 changed files with 98 additions and 95 deletions.
1 change: 1 addition & 0 deletions Cargo.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions recursion/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ algebraic = { path = "../algebraic", default-features = false }
powdr-ast = { git = "https://github.com/powdr-labs/powdr.git", branch = "main", package = "powdr-ast", default-features = false }
powdr-number = { git = "https://github.com/powdr-labs/powdr.git", branch = "main", package = "powdr-number", default-features = false }
powdr-pil-analyzer = { git = "https://github.com/powdr-labs/powdr.git", branch = "main", package = "powdr-pil-analyzer", default-features = false }
powdr-pilopt = { git = "https://github.com/powdr-labs/powdr.git", branch = "main", package = "powdr-pilopt", default-features = false }
powdr-parser-util = { git = "https://github.com/powdr-labs/powdr.git", branch = "main", package = "powdr-parser-util", default-features = false }

#powdr = { path = "../../powdr/powdr", default-features = false }
Expand Down
184 changes: 91 additions & 93 deletions recursion/src/compressor12/compressor12_pil.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,15 +52,14 @@ pub fn render(n_bits: usize, n_publics: usize) -> String {
res.push_str(&format!(
r#"
let N: int = 2**{n_bits};
namespace Global(N);
pol constant L1;
pol constant L1 = [0]*;
"#
));
for i in (12..n_publics).step_by(12) {
res.push_str(&format!(
r#"
pol constant L{};
pol constant L{} = [0]*;
"#,
i / 12 + 1
));
Expand All @@ -69,14 +68,36 @@ namespace Global(N);
res.push_str(
r#"
namespace Compressor(N);
pol constant S[12];
pol constant C[12];
pol constant PARTIAL;
pol constant POSEIDON12;
pol constant GATE;
pol constant CMULADD;
pol constant EVPOL4;
pol constant FFT4;
pol constant S_0 = [0]*;
pol constant S_1 = [0]*;
pol constant S_2 = [0]*;
pol constant S_3 = [0]*;
pol constant S_4 = [0]*;
pol constant S_5 = [0]*;
pol constant S_6 = [0]*;
pol constant S_7 = [0]*;
pol constant S_8 = [0]*;
pol constant S_9 = [0]*;
pol constant S_10 = [0]*;
pol constant S_11 = [0]*;
pol constant C_0 = [0]*;
pol constant C_1 = [0]*;
pol constant C_2 = [0]*;
pol constant C_3 = [0]*;
pol constant C_4 = [0]*;
pol constant C_5 = [0]*;
pol constant C_6 = [0]*;
pol constant C_7 = [0]*;
pol constant C_8 = [0]*;
pol constant C_9 = [0]*;
pol constant C_10 = [0]*;
pol constant C_11 = [0]*;
pol constant PARTIAL = [0]*;
pol constant POSEIDON12 = [0]*;
pol constant GATE = [0]*;
pol constant CMULADD = [0]*;
pol constant EVPOL4 = [0]*;
pol constant FFT4 = [0]*;
pol commit a[12];
"#,
);
Expand All @@ -95,7 +116,7 @@ namespace Compressor(N);
for i in 0..n_publics {
res.push_str(&format!(
r#"
Global.L{} * (a[{}] - :pub{}) = 0;
Global::L{} * (a[{}] - :pub{}) = 0;
"#,
i / 12 + 1,
i % 12,
Expand All @@ -106,32 +127,26 @@ namespace Compressor(N);
// Normal plonk gate
res.push_str(
r#"
// Normal plonk gates
pol a01 = a[0]*a[1];
pol g012 = C[3]*a01 + C[0]*a[0] + C[1]*a[1] + C[2]*a[2] + C[4];
g012*GATE = 0;
pol a34 = a[3]*a[4];
pol g345 = C[3]*a34 + C[0]*a[3] + C[1]*a[4] + C[2]*a[5] + C[4];
g345*GATE = 0;
pol a67 = a[6]*a[7];
pol g678 = C[9]*a67 + C[6]*a[6] + C[7]*a[7] + C[8]*a[8] + C[10];
g678*GATE = 0;
pol a910 = a[9]*a[10];
pol g91011 = C[9]*a910 + C[6]*a[9] + C[7]*a[10] + C[8]*a[11] + C[10];
g91011*GATE = 0;
// POSEIDON12 GATE
pol a01 = a[0] * a[1];
pol g012 = C_3 * a01 + C_0 * a[0] + C_1 * a[1] + C_2 * a[2] + C_4;
g012 * GATE = 0;
pol a34 = a[3] * a[4];
pol g345 = C_3 * a34 + C_0 * a[3] + C_1 * a[4] + C_2 * a[5] + C_4;
g345 * GATE = 0;
pol a67 = a[6] * a[7];
pol g678 = C_9 * a67 + C_6 * a[6] + C_7 * a[7] + C_8 * a[8] + C_10;
g678 * GATE = 0;
pol a910 = a[9] * a[10];
pol g91011 = C_9 * a910 + C_6 * a[9] + C_7 * a[10] + C_8 * a[11] + C_10;
g91011 * GATE = 0;
"#,
);

// POSEIDON12 GATE
for i in 0..12 {
res.push_str(&format!(
r#"
pol a{i}_1 = a[{i}] + C[{i}];
pol a{i}_1 = a[{i}] + C_{i};
"#
));

Expand Down Expand Up @@ -171,63 +186,51 @@ namespace Compressor(N);
}
res.push_str(
r#"
POSEIDON12 * (a[ 0]' - (25*a0_R + 15*a1_R + 41*a2_R + 16*a3_R + 2*a4_R + 28*a5_R + 13*a6_R + 13*a7_R + 39*a8_R + 18*a9_R + 34*a10_R + 20*a11_R)) = 0;
POSEIDON12 * (a[ 1]' - (20*a0_R + 17*a1_R + 15*a2_R + 41*a3_R + 16*a4_R + 2*a5_R + 28*a6_R + 13*a7_R + 13*a8_R + 39*a9_R + 18*a10_R + 34*a11_R)) = 0;
POSEIDON12 * (a[ 2]' - (34*a0_R + 20*a1_R + 17*a2_R + 15*a3_R + 41*a4_R + 16*a5_R + 2*a6_R + 28*a7_R + 13*a8_R + 13*a9_R + 39*a10_R + 18*a11_R)) = 0;
POSEIDON12 * (a[ 3]' - (18*a0_R + 34*a1_R + 20*a2_R + 17*a3_R + 15*a4_R + 41*a5_R + 16*a6_R + 2*a7_R + 28*a8_R + 13*a9_R + 13*a10_R + 39*a11_R)) = 0;
POSEIDON12 * (a[ 4]' - (39*a0_R + 18*a1_R + 34*a2_R + 20*a3_R + 17*a4_R + 15*a5_R + 41*a6_R + 16*a7_R + 2*a8_R + 28*a9_R + 13*a10_R + 13*a11_R)) = 0;
POSEIDON12 * (a[ 5]' - (13*a0_R + 39*a1_R + 18*a2_R + 34*a3_R + 20*a4_R + 17*a5_R + 15*a6_R + 41*a7_R + 16*a8_R + 2*a9_R + 28*a10_R + 13*a11_R)) = 0;
POSEIDON12 * (a[ 6]' - (13*a0_R + 13*a1_R + 39*a2_R + 18*a3_R + 34*a4_R + 20*a5_R + 17*a6_R + 15*a7_R + 41*a8_R + 16*a9_R + 2*a10_R + 28*a11_R)) = 0;
POSEIDON12 * (a[ 7]' - (28*a0_R + 13*a1_R + 13*a2_R + 39*a3_R + 18*a4_R + 34*a5_R + 20*a6_R + 17*a7_R + 15*a8_R + 41*a9_R + 16*a10_R + 2*a11_R)) = 0;
POSEIDON12 * (a[ 8]' - ( 2*a0_R + 28*a1_R + 13*a2_R + 13*a3_R + 39*a4_R + 18*a5_R + 34*a6_R + 20*a7_R + 17*a8_R + 15*a9_R + 41*a10_R + 16*a11_R)) = 0;
POSEIDON12 * (a[ 9]' - (16*a0_R + 2*a1_R + 28*a2_R + 13*a3_R + 13*a4_R + 39*a5_R + 18*a6_R + 34*a7_R + 20*a8_R + 17*a9_R + 15*a10_R + 41*a11_R)) = 0;
POSEIDON12 * (a[10]' - (41*a0_R + 16*a1_R + 2*a2_R + 28*a3_R + 13*a4_R + 13*a5_R + 39*a6_R + 18*a7_R + 34*a8_R + 20*a9_R + 17*a10_R + 15*a11_R)) = 0;
POSEIDON12 * (a[11]' - (15*a0_R + 41*a1_R + 16*a2_R + 2*a3_R + 28*a4_R + 13*a5_R + 13*a6_R + 39*a7_R + 18*a8_R + 34*a9_R + 20*a10_R + 17*a11_R)) = 0;
// CMULADD GATE
pol ca0 = (a[0] + C[0])*C[9];
pol ca1 = (a[1] + C[1])*C[9];
pol ca2 = (a[2] + C[2])*C[9];
pol ca3 = a[3] + C[3];
pol ca4 = a[4] + C[4];
pol ca5 = a[5] + C[5];
pol ca6 = (a[6] + C[6])*C[10];
pol ca7 = (a[7] + C[7])*C[10];
pol ca8 = (a[8] + C[8])*C[10];
POSEIDON12 * (a[0]' - (25 * a0_R + 15 * a1_R + 41 * a2_R + 16 * a3_R + 2 * a4_R + 28 * a5_R + 13 * a6_R + 13 * a7_R + 39 * a8_R + 18 * a9_R + 34 * a10_R + 20 * a11_R)) = 0;
POSEIDON12 * (a[1]' - (20 * a0_R + 17 * a1_R + 15 * a2_R + 41 * a3_R + 16 * a4_R + 2 * a5_R + 28 * a6_R + 13 * a7_R + 13 * a8_R + 39 * a9_R + 18 * a10_R + 34 * a11_R)) = 0;
POSEIDON12 * (a[2]' - (34 * a0_R + 20 * a1_R + 17 * a2_R + 15 * a3_R + 41 * a4_R + 16 * a5_R + 2 * a6_R + 28 * a7_R + 13 * a8_R + 13 * a9_R + 39 * a10_R + 18 * a11_R)) = 0;
POSEIDON12 * (a[3]' - (18 * a0_R + 34 * a1_R + 20 * a2_R + 17 * a3_R + 15 * a4_R + 41 * a5_R + 16 * a6_R + 2 * a7_R + 28 * a8_R + 13 * a9_R + 13 * a10_R + 39 * a11_R)) = 0;
POSEIDON12 * (a[4]' - (39 * a0_R + 18 * a1_R + 34 * a2_R + 20 * a3_R + 17 * a4_R + 15 * a5_R + 41 * a6_R + 16 * a7_R + 2 * a8_R + 28 * a9_R + 13 * a10_R + 13 * a11_R)) = 0;
POSEIDON12 * (a[5]' - (13 * a0_R + 39 * a1_R + 18 * a2_R + 34 * a3_R + 20 * a4_R + 17 * a5_R + 15 * a6_R + 41 * a7_R + 16 * a8_R + 2 * a9_R + 28 * a10_R + 13 * a11_R)) = 0;
POSEIDON12 * (a[6]' - (13 * a0_R + 13 * a1_R + 39 * a2_R + 18 * a3_R + 34 * a4_R + 20 * a5_R + 17 * a6_R + 15 * a7_R + 41 * a8_R + 16 * a9_R + 2 * a10_R + 28 * a11_R)) = 0;
POSEIDON12 * (a[7]' - (28 * a0_R + 13 * a1_R + 13 * a2_R + 39 * a3_R + 18 * a4_R + 34 * a5_R + 20 * a6_R + 17 * a7_R + 15 * a8_R + 41 * a9_R + 16 * a10_R + 2 * a11_R)) = 0;
POSEIDON12 * (a[8]' - (2 * a0_R + 28 * a1_R + 13 * a2_R + 13 * a3_R + 39 * a4_R + 18 * a5_R + 34 * a6_R + 20 * a7_R + 17 * a8_R + 15 * a9_R + 41 * a10_R + 16 * a11_R)) = 0;
POSEIDON12 * (a[9]' - (16 * a0_R + 2 * a1_R + 28 * a2_R + 13 * a3_R + 13 * a4_R + 39 * a5_R + 18 * a6_R + 34 * a7_R + 20 * a8_R + 17 * a9_R + 15 * a10_R + 41 * a11_R)) = 0;
POSEIDON12 * (a[10]' - (41 * a0_R + 16 * a1_R + 2 * a2_R + 28 * a3_R + 13 * a4_R + 13 * a5_R + 39 * a6_R + 18 * a7_R + 34 * a8_R + 20 * a9_R + 17 * a10_R + 15 * a11_R)) = 0;
POSEIDON12 * (a[11]' - (15 * a0_R + 41 * a1_R + 16 * a2_R + 2 * a3_R + 28 * a4_R + 13 * a5_R + 13 * a6_R + 39 * a7_R + 18 * a8_R + 34 * a9_R + 20 * a10_R + 17 * a11_R)) = 0;
pol ca0 = (a[0] + C_0) * C_9;
pol ca1 = (a[1] + C_1) * C_9;
pol ca2 = (a[2] + C_2) * C_9;
pol ca3 = a[3] + C_3;
pol ca4 = a[4] + C_4;
pol ca5 = a[5] + C_5;
pol ca6 = (a[6] + C_6) * C_10;
pol ca7 = (a[7] + C_7) * C_10;
pol ca8 = (a[8] + C_8) * C_10;
pol ca9 = a[9];
pol ca10 = a[10];
pol ca11 = a[11];
pol cA = (ca0 + ca1) * (ca3 + ca4);
pol cB = (ca0 + ca2) * (ca3 + ca5);
pol cC = (ca1 + ca2) * (ca4 + ca5);
pol cD = ca0*ca3;
pol cE = ca1*ca4;
pol cF = ca2*ca5;
pol cA = (ca0 + ca1) * (ca3 + ca4);
pol cB = (ca0 + ca2) * (ca3 + ca5);
pol cC = (ca1 + ca2) * (ca4 + ca5);
pol cD = ca0 * ca3;
pol cE = ca1 * ca4;
pol cF = ca2 * ca5;
CMULADD * (ca9 - (cC + cD - cE - cF) - ca6) = 0;
CMULADD * (ca10 - (cA + cC - 2*cE - cD) - ca7) = 0;
CMULADD * (ca10 - (cA + cC - 2 * cE - cD) - ca7) = 0;
CMULADD * (ca11 - (cB - cD + cE) - ca8) = 0;
// FFT4
pol g0 = C[0]*a[0] + C[1]*a[3] + C[2]*a[6] + C[3]*a[9] + C[6]*a[0] + C[7]*a[3];
pol g1 = C[0]*a[1] + C[1]*a[4] + C[2]*a[7] + C[3]*a[10] + C[6]*a[1] + C[7]*a[4];
pol g2 = C[0]*a[2] + C[1]*a[5] + C[2]*a[8] + C[3]*a[11] + C[6]*a[2] + C[7]*a[5];
pol g3 = C[0]*a[0] - C[1]*a[3] + C[4]*a[6] - C[5]*a[9] + C[6]*a[0] - C[7]*a[3];
pol g4 = C[0]*a[1] - C[1]*a[4] + C[4]*a[7] - C[5]*a[10] + C[6]*a[1] - C[7]*a[4];
pol g5 = C[0]*a[2] - C[1]*a[5] + C[4]*a[8] - C[5]*a[11] + C[6]*a[2] - C[7]*a[5];
pol g6 = C[0]*a[0] + C[1]*a[3] - C[2]*a[6] - C[3]*a[9] + C[6]*a[6] + C[8]*a[9];
pol g7 = C[0]*a[1] + C[1]*a[4] - C[2]*a[7] - C[3]*a[10] + C[6]*a[7] + C[8]*a[10];
pol g8 = C[0]*a[2] + C[1]*a[5] - C[2]*a[8] - C[3]*a[11] + C[6]*a[8] + C[8]*a[11];
pol g9 = C[0]*a[0] - C[1]*a[3] - C[4]*a[6] + C[5]*a[9] + C[6]*a[6] - C[8]*a[9];
pol g10 = C[0]*a[1] - C[1]*a[4] - C[4]*a[7] + C[5]*a[10] + C[6]*a[7] - C[8]*a[10];
pol g11 = C[0]*a[2] - C[1]*a[5] - C[4]*a[8] + C[5]*a[11] + C[6]*a[8] - C[8]*a[11];
pol g0 = C_0 * a[0] + C_1 * a[3] + C_2 * a[6] + C_3 * a[9] + C_6 * a[0] + C_7 * a[3];
pol g1 = C_0 * a[1] + C_1 * a[4] + C_2 * a[7] + C_3 * a[10] + C_6 * a[1] + C_7 * a[4];
pol g2 = C_0 * a[2] + C_1 * a[5] + C_2 * a[8] + C_3 * a[11] + C_6 * a[2] + C_7 * a[5];
pol g3 = C_0 * a[0] - C_1 * a[3] + C_4 * a[6] - C_5 * a[9] + C_6 * a[0] - C_7 * a[3];
pol g4 = C_0 * a[1] - C_1 * a[4] + C_4 * a[7] - C_5 * a[10] + C_6 * a[1] - C_7 * a[4];
pol g5 = C_0 * a[2] - C_1 * a[5] + C_4 * a[8] - C_5 * a[11] + C_6 * a[2] - C_7 * a[5];
pol g6 = C_0 * a[0] + C_1 * a[3] - C_2 * a[6] - C_3 * a[9] + C_6 * a[6] + C_8 * a[9];
pol g7 = C_0 * a[1] + C_1 * a[4] - C_2 * a[7] - C_3 * a[10] + C_6 * a[7] + C_8 * a[10];
pol g8 = C_0 * a[2] + C_1 * a[5] - C_2 * a[8] - C_3 * a[11] + C_6 * a[8] + C_8 * a[11];
pol g9 = C_0 * a[0] - C_1 * a[3] - C_4 * a[6] + C_5 * a[9] + C_6 * a[6] - C_8 * a[9];
pol g10 = C_0 * a[1] - C_1 * a[4] - C_4 * a[7] + C_5 * a[10] + C_6 * a[7] - C_8 * a[10];
pol g11 = C_0 * a[2] - C_1 * a[5] - C_4 * a[8] + C_5 * a[11] + C_6 * a[8] - C_8 * a[11];
FFT4 * (a[0]' - g0) = 0;
FFT4 * (a[1]' - g1) = 0;
FFT4 * (a[2]' - g2) = 0;
Expand All @@ -240,7 +243,6 @@ namespace Compressor(N);
FFT4 * (a[9]' - g9) = 0;
FFT4 * (a[10]' - g10) = 0;
FFT4 * (a[11]' - g11) = 0;
"#
);

Expand All @@ -260,23 +262,23 @@ namespace Compressor(N);
res.push_str(
format!(
r#"
pol {r0}_A = ({a0} + {a1}) * ({b0} + {b1});
pol {r0}_A = ({a0} + {a1}) * ({b0} + {b1});
"#
)
.as_str(),
);
res.push_str(
format!(
r#"
pol {r0}_B = ({a0} + {a2}) * ({b0} + {b2});
pol {r0}_B = ({a0} + {a2}) * ({b0} + {b2});
"#
)
.as_str(),
);
res.push_str(
format!(
r#"
pol {r0}_C = ({a1} + {a2}) * ({b1} + {b2});
pol {r0}_C = ({a1} + {a2}) * ({b1} + {b2});
"#
)
.as_str(),
Expand Down Expand Up @@ -316,7 +318,7 @@ namespace Compressor(N);
res.push_str(
format!(
r#"
pol {r1} = {r0}_A + {r0}_C - 2*{r0}_E - {r0}_D + {c1};
pol {r1} = {r0}_A + {r0}_C - 2 * {r0}_E - {r0}_D + {c1};
"#
)
.as_str(),
Expand Down Expand Up @@ -354,11 +356,7 @@ namespace Compressor(N);
EVPOL4 * (a[6]' - acc4_0 ) = 0;
EVPOL4 * (a[7]' - acc4_1 ) = 0;
EVPOL4 * (a[8]' - acc4_2 ) = 0;
// Connection equations
[a[0], a[1], a[2], a[3], a[4], a[5], a[6], a[7], a[8], a[9], a[10], a[11]] connect
[S[0], S[1], S[2], S[3], S[4], S[5], S[6], S[7], S[8], S[9], S[10], S[11]];
[a[0], a[1], a[2], a[3], a[4], a[5], a[6], a[7], a[8], a[9], a[10], a[11]] connect [S_0, S_1, S_2, S_3, S_4, S_5, S_6, S_7, S_8, S_9, S_10, S_11];
"#,
);

Expand Down
7 changes: 5 additions & 2 deletions recursion/src/pilcom.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,14 @@ use starky::types::PIL;
use std::path::Path;

pub fn compile_pil_from_str(pil_str: &str) -> PIL {
let analyze = powdr_pil_analyzer::analyze_string::<GoldilocksField>(pil_str).unwrap();
let analyzed_pil = powdr_pil_analyzer::analyze_string::<GoldilocksField>(pil_str).unwrap();
let analyze = powdr_pilopt::optimize(analyzed_pil);
export(&analyze)
}
pub fn compile_pil_from_path(pil_path: &str) -> PIL {
let analyze = powdr_pil_analyzer::analyze_file::<GoldilocksField>(Path::new(pil_path)).unwrap();
let analyzed_pil =
powdr_pil_analyzer::analyze_file::<GoldilocksField>(Path::new(pil_path)).unwrap();
let analyze = powdr_pilopt::optimize(analyzed_pil);
export(&analyze)
}

Expand Down

0 comments on commit 009356f

Please sign in to comment.