Skip to content

Commit 2b402a6

Browse files
iajoineriajoiner
committed
feat: add GroupByExec in sol
1 parent 6452f46 commit 2b402a6

File tree

7 files changed

+693
-3
lines changed

7 files changed

+693
-3
lines changed

‎crates/proof-of-sql/src/sql/evm_proof_plan/plans.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -314,10 +314,10 @@ impl EVMSliceExec {
314314
#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
315315
pub(crate) struct EVMGroupByExec {
316316
table_number: usize,
317+
where_clause: EVMDynProofExpr,
317318
group_by_exprs: Vec<usize>,
318319
sum_expr: Vec<EVMDynProofExpr>,
319320
count_alias_name: String,
320-
where_clause: EVMDynProofExpr,
321321
}
322322

323323
impl EVMGroupByExec {

‎solidity/src/base/Constants.sol

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,8 @@ uint32 constant CAST_EXPR_VARIANT = 9;
104104

105105
/// @dev Filter variant constant for proof plans
106106
uint32 constant FILTER_EXEC_VARIANT = 0;
107+
/// @dev Group By variant constant for proof plans
108+
uint32 constant GROUP_BY_EXEC_VARIANT = 1;
107109

108110
/// @dev Boolean variant constant for column types
109111
uint32 constant DATA_TYPE_BOOLEAN_VARIANT = 0;

‎solidity/src/proof_plans/GroupByExec.pre.sol

Lines changed: 326 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,326 @@
1+
// SPDX-License-Identifier: UNLICENSED
2+
// This is licensed under the Cryptographic Open Software License 1.0
3+
pragma solidity ^0.8.28;
4+
5+
import "../base/Constants.sol";
6+
import "../base/Errors.sol";
7+
import {VerificationBuilder} from "../builder/VerificationBuilder.pre.sol";
8+
9+
/// @title GroupByExec
10+
/// @dev Library for handling group by execution plans
11+
library GroupByExec {
12+
/// @notice Evaluates a group by execution plan
13+
/// @custom:as-yul-wrapper
14+
/// #### Wrapped Yul Function
15+
/// ##### Signature
16+
/// ```yul
17+
/// group_by_exec_evaluate(plan_ptr, builder_ptr) -> plan_ptr_out, evaluations_ptr
18+
/// ```
19+
/// ##### Parameters
20+
/// * `plan_ptr` - calldata pointer to the group by execution plan
21+
/// * `builder_ptr` - memory pointer to the verification builder
22+
/// ##### Return Values
23+
/// * `plan_ptr_out` - pointer to the remaining plan after consuming the group by execution plan
24+
/// * `evaluations_ptr` - pointer to the evaluations
25+
/// @notice Evaluates expressions for group by operation and verifies the aggregation constraints
26+
/// @notice ##### Constraints
27+
/// * Inputs: \\(G_1,\ldots,G_\ell=\texttt{g_in}\\), \\(A_1,\ldots,A_m=\texttt{sum_in}\\),
28+
/// and \\(S=\texttt{sel_in}\\) with input characteristic \\(\chi_{[0,n)}=\texttt{input_chi_eval}\\).
29+
/// * Outputs: \\(G_1',\ldots,G_\ell'=\texttt{g_out}\\), \\(A_1',\ldots,A_m'=\texttt{sum_out}\\),
30+
/// and \\(C=\texttt{count_out}\\) with output characteristic \\(\chi_{[0,m')}=\texttt{output_chi_eval}\\).
31+
/// * Challenges: \\(\alpha=\texttt{alpha}\\), \\(\beta=\texttt{beta}\\)
32+
/// * Helpers:
33+
/// \\(g_{in,fold} \=\texttt{g_in_fold} :\equiv \alpha \sum_{j=1}^{\ell} G_j \beta^{\ell-j}\\)
34+
/// \\(g_{out,fold} \=\texttt{g_out_fold} :\equiv \alpha \sum_{j=1}^{\ell} G_j' \beta^{\ell-j}\\)
35+
/// \\(sum_{in,fold} \=\texttt{sum_in_fold} :\equiv \chi_{[0,n)} + \beta \sum_{j=1}^{m} A_j \beta^{m-j}\\)
36+
/// \\(sum_{out,fold} \=\texttt{sum_out_fold} :\equiv C + \beta \sum_{j=1}^{m} A_j' \beta^{m-j}\\)
37+
/// \\(G^\star = \texttt{g_in_star}\\) and \\(G^{\star'} = \texttt{g_out_star}\\)
38+
/// * Constraints:
39+
/// \\[\begin{aligned}
40+
/// G^\star \cdot S \cdot sum_{in,fold} - G^{\star'} \cdot sum_{out,fold} &\overset{\sum}{=} 0\\\\
41+
/// G^\star + G^\star \cdot g_{in,fold} - \chi_{[0,n)} &\equiv 0\\\\
42+
/// G^{\star'} + G^{\star'} \cdot g_{out,fold} - \chi_{[0,m')} &\equiv 0\\\\
43+
/// \end{aligned}\\]
44+
/// Note: the notation \\(A\overset{\sum}{=}B\\) is used to indicate the zero-sum constraint.
45+
/// @dev Evaluates a group by execution plan
46+
/// @param __plan The group by execution plan data
47+
/// @param __builder The verification builder
48+
/// @return __planOut The remaining plan after processing
49+
/// @return __builderOut The verification builder result
50+
/// @return __evaluationsPtr The evaluations pointer
51+
function __groupByExecEvaluate( // solhint-disable-line gas-calldata-parameters
52+
bytes calldata __plan, VerificationBuilder.Builder memory __builder)
53+
external
54+
pure
55+
returns (
56+
bytes calldata __planOut,
57+
VerificationBuilder.Builder memory __builderOut,
58+
uint256[] memory __evaluationsPtr
59+
)
60+
{
61+
uint256[] memory __evaluations;
62+
assembly {
63+
// IMPORT-YUL ../base/Errors.sol
64+
function err(code) {
65+
revert(0, 0)
66+
}
67+
// IMPORT-YUL ../base/Queue.pre.sol
68+
function dequeue(queue_ptr) -> value {
69+
revert(0, 0)
70+
}
71+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
72+
function builder_consume_challenge(builder_ptr) -> value {
73+
revert(0, 0)
74+
}
75+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
76+
function builder_consume_final_round_mle(builder_ptr) -> value {
77+
revert(0, 0)
78+
}
79+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
80+
function builder_consume_chi_evaluation(builder_ptr) -> value {
81+
revert(0, 0)
82+
}
83+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
84+
function builder_produce_zerosum_constraint(builder_ptr, evaluation, degree) {
85+
revert(0, 0)
86+
}
87+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
88+
function builder_produce_identity_constraint(builder_ptr, evaluation, degree) {
89+
revert(0, 0)
90+
}
91+
// IMPORT-YUL ../base/SwitchUtil.pre.sol
92+
function case_const(lhs, rhs) {
93+
revert(0, 0)
94+
}
95+
// IMPORT-YUL ../base/Array.pre.sol
96+
function get_array_element(arr_ptr, index) -> value {
97+
revert(0, 0)
98+
}
99+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
100+
function builder_get_column_evaluation(builder_ptr, column_num) -> value {
101+
revert(0, 0)
102+
}
103+
// IMPORT-YUL ../proof_exprs/ColumnExpr.pre.sol
104+
function column_expr_evaluate(expr_ptr, builder_ptr) -> expr_ptr_out, eval {
105+
revert(0, 0)
106+
}
107+
// IMPORT-YUL ../proof_exprs/LiteralExpr.pre.sol
108+
function literal_expr_evaluate(expr_ptr, chi_eval) -> expr_ptr_out, eval {
109+
revert(0, 0)
110+
}
111+
// IMPORT-YUL ../proof_exprs/EqualsExpr.pre.sol
112+
function equals_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
113+
revert(0, 0)
114+
}
115+
// IMPORT-YUL ../proof_exprs/AddExpr.pre.sol
116+
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
117+
revert(0, 0)
118+
}
119+
// IMPORT-YUL ../proof_exprs/SubtractExpr.pre.sol
120+
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
121+
revert(0, 0)
122+
}
123+
// IMPORT-YUL ../proof_exprs/MultiplyExpr.pre.sol
124+
function multiply_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
125+
revert(0, 0)
126+
}
127+
// IMPORT-YUL ../proof_exprs/AndExpr.pre.sol
128+
function and_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
129+
revert(0, 0)
130+
}
131+
// IMPORT-YUL ../proof_exprs/OrExpr.pre.sol
132+
function or_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
133+
revert(0, 0)
134+
}
135+
// IMPORT-YUL ../proof_exprs/NotExpr.pre.sol
136+
function not_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
137+
revert(0, 0)
138+
}
139+
// IMPORT-YUL ../proof_exprs/CastExpr.pre.sol
140+
function cast_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
141+
revert(0, 0)
142+
}
143+
// IMPORT-YUL ../proof_exprs/ProofExpr.pre.sol
144+
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
145+
revert(0, 0)
146+
}
147+
// IMPORT-YUL ../base/DataType.pre.sol
148+
function read_entry(result_ptr, data_type_variant) -> result_ptr_out, entry {
149+
revert(0, 0)
150+
}
151+
// IMPORT-YUL ../base/DataType.pre.sol
152+
function read_binary(result_ptr) -> result_ptr_out, entry {
153+
revert(0, 0)
154+
}
155+
// IMPORT-YUL ../base/DataType.pre.sol
156+
function read_data_type(ptr) -> ptr_out, data_type {
157+
revert(0, 0)
158+
}
159+
// IMPORT-YUL FilterExec.pre.sol
160+
function compute_folds(plan_ptr, builder_ptr, input_chi_eval) ->
161+
plan_ptr_out,
162+
c_fold,
163+
d_fold,
164+
evaluations_ptr
165+
{
166+
revert(0, 0)
167+
}
168+
// IMPORT-YUL FilterExec.pre.sol
169+
function filter_exec_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
170+
revert(0, 0)
171+
}
172+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
173+
function builder_get_table_chi_evaluation(builder_ptr, table_num) -> value {
174+
revert(0, 0)
175+
}
176+
177+
function compute_groupby_folds(plan_ptr, builder_ptr, input_chi_eval) ->
178+
plan_ptr_out,
179+
g_in_fold,
180+
g_out_fold,
181+
sum_in_fold,
182+
sum_out_fold,
183+
evaluations_ptr
184+
{
185+
let beta := builder_consume_challenge(builder_ptr)
186+
187+
// Process group by columns
188+
let group_by_column_count := shr(UINT64_PADDING_BITS, calldataload(plan_ptr))
189+
plan_ptr := add(plan_ptr, UINT64_SIZE)
190+
191+
evaluations_ptr := mload(FREE_PTR)
192+
mstore(evaluations_ptr, group_by_column_count)
193+
evaluations_ptr := add(evaluations_ptr, WORD_SIZE)
194+
195+
g_in_fold := 0
196+
for { let i := group_by_column_count } i { i := sub(i, 1) } {
197+
let g_in
198+
plan_ptr, g_in := column_expr_evaluate(plan_ptr, builder_ptr)
199+
g_in_fold := addmod(mulmod(g_in_fold, beta, MODULUS), g_in, MODULUS)
200+
}
201+
202+
g_out_fold := 0
203+
for { let i := group_by_column_count } i { i := sub(i, 1) } {
204+
let g_out := builder_consume_final_round_mle(builder_ptr)
205+
g_out_fold := addmod(mulmod(g_out_fold, beta, MODULUS), g_out, MODULUS)
206+
207+
mstore(evaluations_ptr, g_out)
208+
evaluations_ptr := add(evaluations_ptr, WORD_SIZE)
209+
}
210+
211+
// Process sum columns
212+
let sum_count := shr(UINT64_PADDING_BITS, calldataload(plan_ptr))
213+
plan_ptr := add(plan_ptr, UINT64_SIZE)
214+
215+
evaluations_ptr := mload(FREE_PTR)
216+
mstore(FREE_PTR, add(evaluations_ptr, mul(add(sum_count, 1), WORD_SIZE)))
217+
mstore(evaluations_ptr, sum_count)
218+
evaluations_ptr := add(evaluations_ptr, WORD_SIZE)
219+
220+
sum_in_fold := 0
221+
for { let i := sum_count } i { i := sub(i, 1) } {
222+
let sum_in
223+
plan_ptr, sum_in := proof_expr_evaluate(plan_ptr, builder_ptr, input_chi_eval)
224+
sum_in_fold := addmod(mulmod(sum_in_fold, beta, MODULUS), sum_in, MODULUS)
225+
}
226+
sum_in_fold := mulmod(sum_in_fold, beta, MODULUS)
227+
228+
sum_out_fold := 0
229+
for { let i := sum_count } i { i := sub(i, 1) } {
230+
let sum_out := builder_consume_final_round_mle(builder_ptr)
231+
sum_out_fold := addmod(mulmod(sum_out_fold, beta, MODULUS), sum_out, MODULUS)
232+
233+
mstore(evaluations_ptr, sum_out)
234+
evaluations_ptr := add(evaluations_ptr, WORD_SIZE)
235+
}
236+
sum_out_fold := addmod(sum_out_fold, beta, MODULUS)
237+
238+
evaluations_ptr := mload(FREE_PTR)
239+
mstore(FREE_PTR, add(evaluations_ptr, add(WORD_SIZE, mul(sum_count, WORD_SIZE))))
240+
plan_ptr_out := plan_ptr
241+
}
242+
243+
function group_by_exec_evaluate(plan_ptr, builder_ptr) -> plan_ptr_out, evaluations_ptr {
244+
let alpha := builder_consume_challenge(builder_ptr)
245+
246+
// Table input
247+
let input_chi_eval :=
248+
builder_get_table_chi_evaluation(builder_ptr, shr(UINT64_PADDING_BITS, calldataload(plan_ptr)))
249+
plan_ptr := add(plan_ptr, UINT64_SIZE)
250+
251+
// Where clause evaluation
252+
let selection_eval
253+
plan_ptr, selection_eval := proof_expr_evaluate(plan_ptr, builder_ptr, input_chi_eval)
254+
255+
// Compute the folds
256+
let g_in_fold, g_out_fold, sum_in_fold, sum_out_fold
257+
plan_ptr, g_in_fold, g_out_fold, sum_in_fold, sum_out_fold, evaluations_ptr :=
258+
compute_groupby_folds(plan_ptr, builder_ptr, input_chi_eval)
259+
260+
// Skip the count alias (we don't need to parse it for verification)
261+
let count_alias
262+
plan_ptr, count_alias := read_binary(plan_ptr)
263+
264+
// Consume count column evaluation
265+
let count_out_eval := builder_consume_final_round_mle(builder_ptr)
266+
267+
// Get chi evaluation
268+
let output_chi_eval := builder_consume_chi_evaluation(builder_ptr)
269+
270+
// Adjustments
271+
g_in_fold := mulmod(g_in_fold, alpha, MODULUS)
272+
g_out_fold := mulmod(g_out_fold, alpha, MODULUS)
273+
sum_in_fold := addmod(sum_in_fold, input_chi_eval, MODULUS)
274+
sum_out_fold := addmod(sum_out_fold, count_out_eval, MODULUS)
275+
276+
// Verify the group by operation
277+
// Get the g_in_star and g_out_star evaluations
278+
let g_in_star_eval := builder_consume_final_round_mle(builder_ptr)
279+
let g_out_star_eval := builder_consume_final_round_mle(builder_ptr)
280+
281+
// First constraint: sum g_in_star * sel_in * sum_in_fold - g_out_star * sum_out_fold = 0
282+
builder_produce_zerosum_constraint(
283+
builder_ptr,
284+
addmod(
285+
mulmod(mulmod(g_in_star_eval, selection_eval, MODULUS), sum_in_fold, MODULUS),
286+
mulmod(mulmod(g_out_star_eval, sum_out_fold, MODULUS), MODULUS_MINUS_ONE, MODULUS),
287+
MODULUS
288+
),
289+
3
290+
)
291+
292+
// Second constraint: g_in_star + g_in_star * g_in_fold - input_chi_eval = 0
293+
builder_produce_identity_constraint(
294+
builder_ptr,
295+
addmod(
296+
addmod(g_in_star_eval, mulmod(g_in_star_eval, g_in_fold, MODULUS), MODULUS),
297+
mulmod(input_chi_eval, MODULUS_MINUS_ONE, MODULUS),
298+
MODULUS
299+
),
300+
2
301+
)
302+
303+
// Third constraint: g_out_star + g_out_star * g_out_fold - output_chi_eval = 0
304+
builder_produce_identity_constraint(
305+
builder_ptr,
306+
addmod(
307+
addmod(g_out_star_eval, mulmod(g_out_star_eval, g_out_fold, MODULUS), MODULUS),
308+
mulmod(output_chi_eval, MODULUS_MINUS_ONE, MODULUS),
309+
MODULUS
310+
),
311+
2
312+
)
313+
314+
plan_ptr_out := plan_ptr
315+
}
316+
317+
let __planOutOffset
318+
__planOutOffset, __evaluations := group_by_exec_evaluate(__plan.offset, __builder)
319+
__planOut.offset := __planOutOffset
320+
// slither-disable-next-line write-after-write
321+
__planOut.length := sub(__plan.length, sub(__planOutOffset, __plan.offset))
322+
}
323+
__evaluationsPtr = __evaluations;
324+
__builderOut = __builder;
325+
}
326+
}

‎solidity/src/proof_plans/ProofPlan.pre.sol

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@ import {VerificationBuilder} from "../builder/VerificationBuilder.pre.sol";
1010
/// @dev Library for handling proof plans
1111
library ProofPlan {
1212
enum PlanVariant {
13-
Filter
13+
Filter,
14+
GroupBy
1415
}
1516

1617
/// @notice Evaluates a proof plan
@@ -156,6 +157,21 @@ library ProofPlan {
156157
function filter_exec_evaluate(plan_ptr, builder_ptr) -> plan_ptr_out, evaluations_ptr {
157158
revert(0, 0)
158159
}
160+
// IMPORT-YUL GroupByExec.pre.sol
161+
function compute_groupby_folds(plan_ptr, builder_ptr, input_chi_eval) ->
162+
plan_ptr_out,
163+
g_in_fold,
164+
g_out_fold,
165+
sum_in_fold,
166+
sum_out_fold,
167+
evaluations_ptr
168+
{
169+
revert(0, 0)
170+
}
171+
// IMPORT-YUL GroupByExec.pre.sol
172+
function group_by_exec_evaluate(plan_ptr, builder_ptr) -> plan_ptr_out, evaluations_ptr {
173+
revert(0, 0)
174+
}
159175
// IMPORT-YUL ../base/DataType.pre.sol
160176
function read_entry(result_ptr, data_type_variant) -> result_ptr_out, entry {
161177
revert(0, 0)
@@ -178,6 +194,10 @@ library ProofPlan {
178194
case_const(0, FILTER_EXEC_VARIANT)
179195
plan_ptr_out, evaluations_ptr := filter_exec_evaluate(plan_ptr, builder_ptr)
180196
}
197+
case 1 {
198+
case_const(1, GROUP_BY_EXEC_VARIANT)
199+
plan_ptr_out, evaluations_ptr := group_by_exec_evaluate(plan_ptr, builder_ptr)
200+
}
181201
default { err(ERR_UNSUPPORTED_PROOF_PLAN_VARIANT) }
182202
}
183203

0 commit comments

Comments
 (0)