feat: add GroupByExec in sol

Author: iajoiner

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

@@ -306,10 +306,10 @@ impl EVMSliceExec {
 #[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
 pub(crate) struct EVMGroupByExec {
     table_number: usize,
+    where_clause: EVMDynProofExpr,
     group_by_exprs: Vec<usize>,
     sum_expr: Vec<EVMDynProofExpr>,
     count_alias_name: String,
-    where_clause: EVMDynProofExpr,
 }
 
 impl EVMGroupByExec {

solidity/src/base/Constants.sol

@@ -104,6 +104,8 @@ uint32 constant CAST_EXPR_VARIANT = 9;
 
 /// @dev Filter variant constant for proof plans
 uint32 constant FILTER_EXEC_VARIANT = 0;
+/// @dev Group By variant constant for proof plans
+uint32 constant GROUP_BY_EXEC_VARIANT = 1;
 
 /// @dev Boolean variant constant for column types
 uint32 constant DATA_TYPE_BOOLEAN_VARIANT = 0;

solidity/src/proof_plans/GroupByExec.pre.sol

@@ -0,0 +1,337 @@
+// SPDX-License-Identifier: UNLICENSED
+// This is licensed under the Cryptographic Open Software License 1.0
+pragma solidity ^0.8.28;
+
+import "../base/Constants.sol";
+import "../base/Errors.sol";
+import {VerificationBuilder} from "../builder/VerificationBuilder.pre.sol";
+
+/// @title GroupByExec
+/// @dev Library for handling group by execution plans
+library GroupByExec {
+    /// @notice Evaluates a group by execution plan
+    /// @custom:as-yul-wrapper
+    /// #### Wrapped Yul Function
+    /// ##### Signature
+    /// ```yul
+    /// group_by_exec_evaluate(plan_ptr, builder_ptr) -> plan_ptr_out, evaluations_ptr
+    /// ```
+    /// ##### Parameters
+    /// * `plan_ptr` - calldata pointer to the group by execution plan
+    /// * `builder_ptr` - memory pointer to the verification builder
+    /// ##### Return Values
+    /// * `plan_ptr_out` - pointer to the remaining plan after consuming the group by execution plan
+    /// * `evaluations_ptr` - pointer to the evaluations
+    /// @notice Evaluates expressions for group by operation and verifies the aggregation constraints
+    /// @notice ##### Constraints
+    /// * Inputs: \\(G_1,\ldots,G_\ell=\texttt{g_in}\\), \\(A_1,\ldots,A_m=\texttt{sum_in}\\),
+    ///   and \\(S=\texttt{sel_in}\\) with input characteristic \\(\chi_{[0,n)}=\texttt{input_chi_eval}\\).
+    /// * Outputs: \\(G_1',\ldots,G_\ell'=\texttt{g_out}\\), \\(A_1',\ldots,A_m'=\texttt{sum_out}\\),
+    ///   and \\(C=\texttt{count_out}\\) with output characteristic \\(\chi_{[0,m')}=\texttt{output_chi_eval}\\).
+    /// * Challenges: \\(\alpha=\texttt{alpha}\\), \\(\beta=\texttt{beta}\\)
+    /// * Helpers:
+    ///   \\(g_{in,fold} \=\texttt{g_in_fold} :\equiv \alpha \sum_{j=1}^{\ell} G_j \beta^{\ell-j}\\)
+    ///   \\(g_{out,fold} \=\texttt{g_out_fold} :\equiv \alpha \sum_{j=1}^{\ell} G_j' \beta^{\ell-j}\\)
+    ///   \\(sum_{in,fold} \=\texttt{sum_in_fold} :\equiv \chi_{[0,n)} + \beta \sum_{j=1}^{m} A_j \beta^{m-j}\\)
+    ///   \\(sum_{out,fold} \=\texttt{sum_out_fold} :\equiv C + \beta \sum_{j=1}^{m} A_j' \beta^{m-j}\\)
+    ///   \\(G^\star = \texttt{g_in_star}\\) and \\(G^{\star'} = \texttt{g_out_star}\\)
+    /// * Constraints:
+    /// \\[\begin{aligned}
+    /// G^\star \cdot S \cdot sum_{in,fold} - G^{\star'} \cdot sum_{out,fold} &\overset{\sum}{=} 0\\\\
+    /// G^\star + G^\star \cdot g_{in,fold} - \chi_{[0,n)} &\equiv 0\\\\
+    /// G^{\star'} + G^{\star'} \cdot g_{out,fold} - \chi_{[0,m')} &\equiv 0\\\\
+    /// \end{aligned}\\]
+    /// Note: the notation \\(A\overset{\sum}{=}B\\) is used to indicate the zero-sum constraint.
+    /// @dev Evaluates a group by execution plan
+    /// @param __plan The group by execution plan data
+    /// @param __builder The verification builder
+    /// @return __planOut The remaining plan after processing
+    /// @return __builderOut The verification builder result
+    /// @return __evaluationsPtr The evaluations pointer
+    function __groupByExecEvaluate( // solhint-disable-line gas-calldata-parameters
+    bytes calldata __plan, VerificationBuilder.Builder memory __builder)
+        external
+        pure
+        returns (
+            bytes calldata __planOut,
+            VerificationBuilder.Builder memory __builderOut,
+            uint256[] memory __evaluationsPtr
+        )
+    {
+        uint256[] memory __evaluations;
+        assembly {
+            // IMPORT-YUL ../base/Errors.sol
+            function err(code) {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/Queue.pre.sol
+            function dequeue(queue_ptr) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_consume_challenge(builder_ptr) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_consume_final_round_mle(builder_ptr) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_consume_chi_evaluation(builder_ptr) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_produce_zerosum_constraint(builder_ptr, evaluation, degree) {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_produce_identity_constraint(builder_ptr, evaluation, degree) {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/SwitchUtil.pre.sol
+            function case_const(lhs, rhs) {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/Array.pre.sol
+            function get_array_element(arr_ptr, index) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_get_column_evaluation(builder_ptr, column_num) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/ColumnExpr.pre.sol
+            function column_expr_evaluate(expr_ptr, builder_ptr) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/LiteralExpr.pre.sol
+            function literal_expr_evaluate(expr_ptr, chi_eval) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/EqualsExpr.pre.sol
+            function equals_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/AddExpr.pre.sol
+            function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/SubtractExpr.pre.sol
+            function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/MultiplyExpr.pre.sol
+            function multiply_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/AndExpr.pre.sol
+            function and_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/OrExpr.pre.sol
+            function or_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/NotExpr.pre.sol
+            function not_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../proof_exprs/ProofExpr.pre.sol
+            function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/DataType.pre.sol
+            function read_entry(result_ptr, data_type_variant) -> result_ptr_out, entry {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/DataType.pre.sol
+            function read_data_type(ptr) -> ptr_out, data_type {
+                revert(0, 0)
+            }
+            // IMPORT-YUL FilterExec.pre.sol
+            function compute_folds(plan_ptr, builder_ptr, input_chi_eval) ->
+                plan_ptr_out,
+                c_fold,
+                d_fold,
+                evaluations_ptr
+            {
+                revert(0, 0)
+            }
+            // IMPORT-YUL FilterExec.pre.sol
+            function filter_exec_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_get_table_chi_evaluation(builder_ptr, table_num) -> value {
+                revert(0, 0)
+            }
+
+            function compute_groupby_folds(plan_ptr, builder_ptr, input_chi_eval) ->
+                plan_ptr_out,
+                g_in_fold,
+                g_out_fold,
+                sum_in_fold,
+                sum_out_fold,
+                evaluations_ptr
+            {
+                let beta := builder_consume_challenge(builder_ptr)
+
+                // Process group by columns
+                let group_by_column_count := shr(UINT64_PADDING_BITS, calldataload(plan_ptr))
+                plan_ptr := add(plan_ptr, UINT64_SIZE)
+
+                evaluations_ptr := mload(FREE_PTR)
+                mstore(evaluations_ptr, group_by_column_count)
+                evaluations_ptr := add(evaluations_ptr, WORD_SIZE)
+
+                g_in_fold := 0
+                for { let i := group_by_column_count } i { i := sub(i, 1) } {
+                    let g_in
+                    plan_ptr, g_in := column_expr_evaluate(plan_ptr, builder_ptr)
+                    g_in_fold := addmod(mulmod(g_in_fold, beta, MODULUS), g_in, MODULUS)
+                }
+
+                g_out_fold := 0
+                for { let i := group_by_column_count } i { i := sub(i, 1) } {
+                    let g_out := builder_consume_final_round_mle(builder_ptr)
+                    g_out_fold := addmod(mulmod(g_out_fold, beta, MODULUS), g_out, MODULUS)
+
+                    mstore(evaluations_ptr, g_out)
+                    evaluations_ptr := add(evaluations_ptr, WORD_SIZE)
+                }
+
+                // Process sum columns
+                let sum_count := shr(UINT64_PADDING_BITS, calldataload(plan_ptr))
+                plan_ptr := add(plan_ptr, UINT64_SIZE)
+
+                evaluations_ptr := mload(FREE_PTR)
+                mstore(FREE_PTR, add(evaluations_ptr, mul(add(sum_count, 1), WORD_SIZE)))
+                mstore(evaluations_ptr, sum_count)
+                evaluations_ptr := add(evaluations_ptr, WORD_SIZE)
+
+                sum_in_fold := 0
+                for { let i := sum_count } i { i := sub(i, 1) } {
+                    let sum_in
+                    plan_ptr, sum_in := proof_expr_evaluate(plan_ptr, builder_ptr, input_chi_eval)
+                    sum_in_fold := addmod(mulmod(sum_in_fold, beta, MODULUS), sum_in, MODULUS)
+                }
+
+                sum_out_fold := 0
+                for { let i := sum_count } i { i := sub(i, 1) } {
+                    let sum_out := builder_consume_final_round_mle(builder_ptr)
+                    sum_out_fold := addmod(mulmod(sum_out_fold, beta, MODULUS), sum_out, MODULUS)
+
+                    mstore(evaluations_ptr, sum_out)
+                    evaluations_ptr := add(evaluations_ptr, WORD_SIZE)
+                }
+
+                evaluations_ptr := mload(FREE_PTR)
+                mstore(FREE_PTR, add(evaluations_ptr, add(WORD_SIZE, mul(sum_count, WORD_SIZE))))
+                plan_ptr_out := plan_ptr
+            }
+
+            function group_by_exec_evaluate(plan_ptr, builder_ptr) -> plan_ptr_out, evaluations_ptr {
+                let alpha := builder_consume_challenge(builder_ptr)
+
+                // Table input
+                let input_chi_eval :=
+                    builder_get_table_chi_evaluation(builder_ptr, shr(UINT64_PADDING_BITS, calldataload(plan_ptr)))
+                plan_ptr := add(plan_ptr, UINT64_SIZE)
+
+                // Where clause evaluation
+                let selection_eval
+                plan_ptr, selection_eval := proof_expr_evaluate(plan_ptr, builder_ptr, input_chi_eval)
+
+                // Compute the folds
+                plan_ptr, g_in_fold, g_out_fold, sum_in_fold, sum_out_fold, evaluations_ptr
+                = compute_groupby_folds(plan_ptr, builder_ptr, input_chi_eval)
+                // Skip the count alias (we don't need to parse it for verification)
+                let count_alias
+                plan_ptr, count_alias := read_binary(plan_ptr)
+
+                // Consume count column evaluation
+                let count_out_eval := builder_consume_final_round_mle(builder_ptr)
+
+                // Get chi evaluation
+                let output_chi_eval := builder_consume_chi_evaluation(builder_ptr)
+
+                // Verify the group by operation
+                // Get the g_in_star and g_out_star evaluations
+                let g_in_star_eval := builder_consume_final_round_mle(builder_ptr)
+                let g_out_star_eval := builder_consume_final_round_mle(builder_ptr)
+
+                // First constraint: sum g_in_star * sel_in * sum_in_fold - g_out_star * sum_out_fold = 0
+                builder_produce_zerosum_constraint(
+                    builder_ptr,
+                    addmod(
+                        mulmod(mulmod(g_in_star_eval, selection_eval, MODULUS), sum_in_fold, MODULUS),
+                        mulmod(mulmod(g_out_star_eval, sum_out_fold, MODULUS), MODULUS_MINUS_ONE, MODULUS),
+                        MODULUS
+                    ),
+                    3
+                )
+
+                // Second constraint: g_in_star + g_in_star * g_in_fold - input_chi_eval = 0
+                builder_produce_identity_constraint(
+                    builder_ptr,
+                    addmod(
+                        addmod(g_in_star_eval, mulmod(g_in_star_eval, g_in_fold, MODULUS), MODULUS),
+                        mulmod(input_chi_eval, MODULUS_MINUS_ONE, MODULUS),
+                        MODULUS
+                    ),
+                    2
+                )
+
+                // Third constraint: g_out_star + g_out_star * g_out_fold - output_chi_eval = 0
+                builder_produce_identity_constraint(
+                    builder_ptr,
+                    addmod(
+                        addmod(g_out_star_eval, mulmod(g_out_star_eval, g_out_fold, MODULUS), MODULUS),
+                        mulmod(output_chi_eval, MODULUS_MINUS_ONE, MODULUS),
+                        MODULUS
+                    ),
+                    2
+                )
+
+                // Prepare result evaluations (group_by + sum + count columns)
+                let evaluations_length := add(add(group_by_count, sum_count), 1)
+                evaluations_ptr := mload(FREE_PTR)
+                mstore(evaluations_ptr, evaluations_length)
+
+                // Copy group by column evaluations
+                for { let i := 0 } lt(i, group_by_count) { i := add(i, 1) } {
+                    mstore(
+                        add(add(evaluations_ptr, WORD_SIZE), mul(i, WORD_SIZE)),
+                        mload(add(add(g_out_evals_ptr, WORD_SIZE), mul(i, WORD_SIZE)))
+                    )
+                }
+
+                // Copy sum column evaluations
+                for { let i := 0 } lt(i, sum_count) { i := add(i, 1) } {
+                    mstore(
+                        add(add(evaluations_ptr, WORD_SIZE), mul(add(i, group_by_count), WORD_SIZE)),
+                        mload(add(add(sum_out_evals_ptr, WORD_SIZE), mul(i, WORD_SIZE)))
+                    )
+                }
+
+                // Add count column evaluation
+                mstore(
+                    add(add(evaluations_ptr, WORD_SIZE), mul(add(group_by_count, sum_count), WORD_SIZE)), count_out_eval
+                )
+
+                // Update free memory pointer
+                mstore(FREE_PTR, add(evaluations_ptr, mul(add(evaluations_length, 1), WORD_SIZE)))
+
+                plan_ptr_out := plan_ptr
+            }
+
+            let __planOutOffset
+            __planOutOffset, __evaluations := group_by_exec_evaluate(__plan.offset, __builder)
+            __planOut.offset := __planOutOffset
+            // slither-disable-next-line write-after-write
+            __planOut.length := sub(__plan.length, sub(__planOutOffset, __plan.offset))
+        }
+        __evaluationsPtr = __evaluations;
+        __builderOut = __builder;
+    }
+}

solidity/src/proof_plans/ProofPlan.pre.sol

@@ -10,7 +10,8 @@ import {VerificationBuilder} from "../builder/VerificationBuilder.pre.sol";
 /// @dev Library for handling proof plans
 library ProofPlan {
     enum PlanVariant {
-        Filter
+        Filter,
+        GroupBy
     }
 
     /// @notice Evaluates a proof plan
@@ -156,6 +157,14 @@ library ProofPlan {
             function read_data_type(ptr) -> ptr_out, data_type {
                 revert(0, 0)
             }
+            // IMPORT-YUL GroupByExec.pre.sol
+            function fold_vals(beta, vals_ptr, vals_length) -> result {
+                revert(0, 0)
+            }
+            // IMPORT-YUL GroupByExec.pre.sol
+            function group_by_exec_evaluate(plan_ptr, builder_ptr) -> plan_ptr_out, evaluations_ptr {
+                revert(0, 0)
+            }
 
             function proof_plan_evaluate(plan_ptr, builder_ptr) -> plan_ptr_out, evaluations_ptr {
                 let proof_plan_variant := shr(UINT32_PADDING_BITS, calldataload(plan_ptr))
@@ -166,6 +175,10 @@ library ProofPlan {
                     case_const(0, FILTER_EXEC_VARIANT)
                     plan_ptr_out, evaluations_ptr := filter_exec_evaluate(plan_ptr, builder_ptr)
                 }
+                case 1 {
+                    case_const(1, GROUP_BY_EXEC_VARIANT)
+                    plan_ptr_out, evaluations_ptr := group_by_exec_evaluate(plan_ptr, builder_ptr)
+                }
                 default { err(ERR_UNSUPPORTED_PROOF_PLAN_VARIANT) }
             }