From 009356f9a289930a7f1760f5f6ff5bfae9975d8a Mon Sep 17 00:00:00 2001 From: ibmp33 <2285673866@qq.com> Date: Sun, 29 Dec 2024 01:34:45 +0800 Subject: [PATCH] chore: modify pil format --- Cargo.lock | 1 + recursion/Cargo.toml | 1 + .../src/compressor12/compressor12_pil.rs | 184 +++++++++--------- recursion/src/pilcom.rs | 7 +- 4 files changed, 98 insertions(+), 95 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index c27f2752..a9ee8cfb 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4340,6 +4340,7 @@ dependencies = [ "powdr-number", "powdr-parser-util", "powdr-pil-analyzer", + "powdr-pilopt", "proptest", "serde", "serde_json", diff --git a/recursion/Cargo.toml b/recursion/Cargo.toml index 9c4b5e16..242dbb5f 100644 --- a/recursion/Cargo.toml +++ b/recursion/Cargo.toml @@ -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 } diff --git a/recursion/src/compressor12/compressor12_pil.rs b/recursion/src/compressor12/compressor12_pil.rs index 4bdc6c7f..0b1924a0 100644 --- a/recursion/src/compressor12/compressor12_pil.rs +++ b/recursion/src/compressor12/compressor12_pil.rs @@ -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 )); @@ -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]; "#, ); @@ -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, @@ -106,24 +127,18 @@ 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; "#, ); @@ -131,7 +146,7 @@ namespace Compressor(N); 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}; "# )); @@ -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; @@ -240,7 +243,6 @@ namespace Compressor(N); FFT4 * (a[9]' - g9) = 0; FFT4 * (a[10]' - g10) = 0; FFT4 * (a[11]' - g11) = 0; - "# ); @@ -260,7 +262,7 @@ namespace Compressor(N); res.push_str( format!( r#" - pol {r0}_A = ({a0} + {a1}) * ({b0} + {b1}); + pol {r0}_A = ({a0} + {a1}) * ({b0} + {b1}); "# ) .as_str(), @@ -268,7 +270,7 @@ namespace Compressor(N); res.push_str( format!( r#" - pol {r0}_B = ({a0} + {a2}) * ({b0} + {b2}); + pol {r0}_B = ({a0} + {a2}) * ({b0} + {b2}); "# ) .as_str(), @@ -276,7 +278,7 @@ namespace Compressor(N); res.push_str( format!( r#" - pol {r0}_C = ({a1} + {a2}) * ({b1} + {b2}); + pol {r0}_C = ({a1} + {a2}) * ({b1} + {b2}); "# ) .as_str(), @@ -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(), @@ -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]; "#, ); diff --git a/recursion/src/pilcom.rs b/recursion/src/pilcom.rs index aaa964e1..60d5db05 100644 --- a/recursion/src/pilcom.rs +++ b/recursion/src/pilcom.rs @@ -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::(pil_str).unwrap(); + let analyzed_pil = powdr_pil_analyzer::analyze_string::(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::(Path::new(pil_path)).unwrap(); + let analyzed_pil = + powdr_pil_analyzer::analyze_file::(Path::new(pil_path)).unwrap(); + let analyze = powdr_pilopt::optimize(analyzed_pil); export(&analyze) }