Skip to content

Commit dbb4790

Browse files
authored
feat(sol): add AddExpr and SubtractExpr (#719)
Please be sure to look over the pull request guidelines here: https://github.com/spaceandtimelabs/sxt-proof-of-sql/blob/main/CONTRIBUTING.md#submit-pr. # Please go through the following checklist - [x] The PR title and commit messages adhere to guidelines here: https://github.com/spaceandtimelabs/sxt-proof-of-sql/blob/main/CONTRIBUTING.md. In particular `!` is used if and only if at least one breaking change has been introduced. - [x] I have run the ci check script with `source scripts/run_ci_checks.sh`. - [x] I have run the clean commit check script with `source scripts/check_commits.sh`, and the commit history is certified to follow clean commit guidelines as described here: https://github.com/spaceandtimelabs/sxt-proof-of-sql/blob/main/COMMIT_GUIDELINES.md - [x] The latest changes from `main` have been incorporated to this PR by simple rebase if possible, if not, then conflicts are resolved appropriately. # Rationale for this change It is necessary to allow `AddExpr` and `SubtractExpr`. <!-- Why are you proposing this change? If this is already explained clearly in the linked issue then this section is not needed. Explaining clearly why changes are proposed helps reviewers understand your changes and offer better suggestions for fixes. Example: Add `NestedLoopJoinExec`. Closes #345. Since we added `HashJoinExec` in #323 it has been possible to do provable inner joins. However performance is not satisfactory in some cases. Hence we need to fix the problem by implement `NestedLoopJoinExec` and speed up the code for `HashJoinExec`. --> # What changes are included in this PR? - add `AddExpr` and `SubtractExpr` <!-- There is no need to duplicate the description in the ticket here but it is sometimes worth providing a summary of the individual changes in this PR. Example: - Add `NestedLoopJoinExec`. - Speed up `HashJoinExec`. - Route joins to `NestedLoopJoinExec` if the outer input is sufficiently small. --> # Are these changes tested? <!-- We typically require tests for all PRs in order to: 1. Prevent the code from being accidentally broken by subsequent changes 2. Serve as another way to document the expected behavior of the code If tests are not included in your PR, please explain why (for example, are they covered by existing tests)? Example: Yes. --> Will be.
2 parents 7854e2a + e1b6569 commit dbb4790

File tree

12 files changed

+474
-2
lines changed

12 files changed

+474
-2
lines changed

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

+40
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,46 @@ fn we_can_verify_a_simple_filter_with_negative_literal_using_the_evm() {
160160
.unwrap();
161161
}
162162

163+
#[ignore = "This test requires the forge binary to be present"]
164+
#[test]
165+
fn we_can_verify_a_filter_with_arithmetic_using_the_evm() {
166+
let (ps, vk) = hyperkzg::load_small_setup_for_testing();
167+
168+
let accessor = OwnedTableTestAccessor::<HyperKZGCommitmentEvaluationProof>::new_from_table(
169+
"namespace.table".parse().unwrap(),
170+
owned_table([
171+
bigint("a", [5, 3, 2, 5, 3, 2]),
172+
bigint("b", [0, 1, 2, 3, 4, 5]),
173+
]),
174+
0,
175+
&ps[..],
176+
);
177+
let query = QueryExpr::try_new(
178+
"SELECT a, b FROM table WHERE a + b = a - b"
179+
.parse()
180+
.unwrap(),
181+
"namespace".into(),
182+
&accessor,
183+
)
184+
.unwrap();
185+
let plan = query.proof_expr();
186+
187+
let verifiable_result = VerifiableQueryResult::<HyperKZGCommitmentEvaluationProof>::new(
188+
&EVMProofPlan::new(plan.clone()),
189+
&accessor,
190+
&&ps[..],
191+
&[],
192+
)
193+
.unwrap();
194+
195+
verifiable_result
196+
.clone()
197+
.verify(&EVMProofPlan::new(plan.clone()), &accessor, &&vk, &[])
198+
.unwrap();
199+
200+
assert!(evm_verifier_all(plan, &verifiable_result, &accessor));
201+
}
202+
163203
#[ignore = "This test requires the forge binary to be present"]
164204
#[test]
165205
fn we_can_verify_a_complex_filter_using_the_evm() {

solidity/src/base/Constants.sol

+4
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,10 @@ uint32 constant COLUMN_EXPR_VARIANT = 0;
5757
uint32 constant LITERAL_EXPR_VARIANT = 1;
5858
/// @dev Equals variant constant for proof expressions
5959
uint32 constant EQUALS_EXPR_VARIANT = 2;
60+
/// @dev Add variant constant for proof expressions
61+
uint32 constant ADD_EXPR_VARIANT = 3;
62+
/// @dev Subtract variant constant for proof expressions
63+
uint32 constant SUBTRACT_EXPR_VARIANT = 4;
6064

6165
/// @dev Filter variant constant for proof plans
6266
uint32 constant FILTER_EXEC_VARIANT = 0;
+112
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
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 AddExpr
10+
/// @dev Library for handling adding two proof expressions
11+
library AddExpr {
12+
/// @notice Evaluates an add expression by adding two sub-expressions
13+
/// @custom:as-yul-wrapper
14+
/// #### Wrapped Yul Function
15+
/// ##### Signature
16+
/// ```yul
17+
/// add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval
18+
/// ```
19+
/// ##### Parameters
20+
/// * `expr_ptr` - calldata pointer to the expression data
21+
/// * `builder_ptr` - memory pointer to the verification builder
22+
/// * `chi_eval` - the chi value for evaluation
23+
/// ##### Return Values
24+
/// * `expr_ptr_out` - pointer to the remaining expression after consuming both sub-expressions
25+
/// * `eval` - the evaluation result from the builder's final round MLE
26+
/// @notice Evaluates two sub-expressions and adds them together
27+
/// ##### Proof Plan Encoding
28+
/// The add expression is encoded as follows:
29+
/// 1. The left hand side expression
30+
/// 2. The right hand side expression
31+
/// @param __expr The add expression data
32+
/// @param __builder The verification builder
33+
/// @param __chiEval The chi value for evaluation
34+
/// @return __exprOut The remaining expression after processing
35+
/// @return __builderOut The verification builder result
36+
/// @return __eval The evaluated result
37+
function __addExprEvaluate( // solhint-disable-line gas-calldata-parameters
38+
bytes calldata __expr, VerificationBuilder.Builder memory __builder, uint256 __chiEval)
39+
external
40+
pure
41+
returns (bytes calldata __exprOut, VerificationBuilder.Builder memory __builderOut, uint256 __eval)
42+
{
43+
assembly {
44+
// IMPORT-YUL ../base/Errors.sol
45+
function err(code) {
46+
revert(0, 0)
47+
}
48+
// IMPORT-YUL ../base/Queue.pre.sol
49+
function dequeue(queue_ptr) -> value {
50+
revert(0, 0)
51+
}
52+
// IMPORT-YUL ../base/SwitchUtil.pre.sol
53+
function case_const(lhs, rhs) {
54+
revert(0, 0)
55+
}
56+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
57+
function builder_get_column_evaluation(builder_ptr, column_num) -> eval {
58+
revert(0, 0)
59+
}
60+
// IMPORT-YUL ../base/Array.pre.sol
61+
function get_array_element(arr_ptr, index) -> value {
62+
revert(0, 0)
63+
}
64+
// IMPORT-YUL ColumnExpr.pre.sol
65+
function column_expr_evaluate(expr_ptr, builder_ptr) -> expr_ptr_out, eval {
66+
revert(0, 0)
67+
}
68+
// IMPORT-YUL LiteralExpr.pre.sol
69+
function literal_expr_evaluate(expr_ptr, chi_eval) -> expr_ptr_out, eval {
70+
revert(0, 0)
71+
}
72+
// IMPORT-YUL EqualsExpr.pre.sol
73+
function equals_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
74+
revert(0, 0)
75+
}
76+
// IMPORT-YUL SubtractExpr.pre.sol
77+
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
78+
revert(0, 0)
79+
}
80+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
81+
function builder_consume_final_round_mle(builder_ptr) -> value {
82+
revert(0, 0)
83+
}
84+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
85+
function builder_produce_identity_constraint(builder_ptr, evaluation, degree) {
86+
revert(0, 0)
87+
}
88+
// IMPORT-YUL ProofExpr.pre.sol
89+
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
90+
revert(0, 0)
91+
}
92+
93+
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
94+
let lhs_eval
95+
expr_ptr, lhs_eval := proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval)
96+
97+
let rhs_eval
98+
expr_ptr, rhs_eval := proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval)
99+
100+
result_eval := addmod(lhs_eval, rhs_eval, MODULUS)
101+
expr_ptr_out := expr_ptr
102+
}
103+
104+
let __exprOutOffset
105+
__exprOutOffset, __eval := add_expr_evaluate(__expr.offset, __builder, __chiEval)
106+
__exprOut.offset := __exprOutOffset
107+
// slither-disable-next-line write-after-write
108+
__exprOut.length := sub(__expr.length, sub(__exprOutOffset, __expr.offset))
109+
}
110+
__builderOut = __builder;
111+
}
112+
}

solidity/src/proof_exprs/EqualsExpr.pre.sol

+8
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,14 @@ library EqualsExpr {
9595
function literal_expr_evaluate(expr_ptr, chi_eval) -> expr_ptr_out, eval {
9696
revert(0, 0)
9797
}
98+
// IMPORT-YUL AddExpr.pre.sol
99+
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
100+
revert(0, 0)
101+
}
102+
// IMPORT-YUL SubtractExpr.pre.sol
103+
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
104+
revert(0, 0)
105+
}
98106
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
99107
function builder_consume_final_round_mle(builder_ptr) -> value {
100108
revert(0, 0)

solidity/src/proof_exprs/ProofExpr.pre.sol

+19-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,9 @@ library ProofExpr {
1212
enum ExprVariant {
1313
Column,
1414
Literal,
15-
Equals
15+
Equals,
16+
Add,
17+
Subtract
1618
}
1719

1820
/// @notice Evaluates a proof expression
@@ -90,6 +92,14 @@ library ProofExpr {
9092
function equals_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
9193
revert(0, 0)
9294
}
95+
// IMPORT-YUL AddExpr.pre.sol
96+
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
97+
revert(0, 0)
98+
}
99+
// IMPORT-YUL SubtractExpr.pre.sol
100+
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
101+
revert(0, 0)
102+
}
93103

94104
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
95105
let proof_expr_variant := shr(UINT32_PADDING_BITS, calldataload(expr_ptr))
@@ -108,6 +118,14 @@ library ProofExpr {
108118
case_const(2, EQUALS_EXPR_VARIANT)
109119
expr_ptr_out, eval := equals_expr_evaluate(expr_ptr, builder_ptr, chi_eval)
110120
}
121+
case 3 {
122+
case_const(3, ADD_EXPR_VARIANT)
123+
expr_ptr_out, eval := add_expr_evaluate(expr_ptr, builder_ptr, chi_eval)
124+
}
125+
case 4 {
126+
case_const(4, SUBTRACT_EXPR_VARIANT)
127+
expr_ptr_out, eval := subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval)
128+
}
111129
default { err(ERR_UNSUPPORTED_PROOF_EXPR_VARIANT) }
112130
}
113131
let __exprOutOffset
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
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 SubtractExpr
10+
/// @dev Library for handling subtracting two proof expressions
11+
library SubtractExpr {
12+
/// @notice Evaluates an subtract expression by subtracting one sub-expression from the other
13+
/// @custom:as-yul-wrapper
14+
/// #### Wrapped Yul Function
15+
/// ##### Signature
16+
/// ```yul
17+
/// subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval
18+
/// ```
19+
/// ##### Parameters
20+
/// * `expr_ptr` - calldata pointer to the expression data
21+
/// * `builder_ptr` - memory pointer to the verification builder
22+
/// * `chi_eval` - the chi value for evaluation
23+
/// ##### Return Values
24+
/// * `expr_ptr_out` - pointer to the remaining expression after consuming both sub-expressions
25+
/// * `eval` - the evaluation result from the builder's final round MLE
26+
/// @notice Evaluates two sub-expressions and subtract one from the other
27+
/// ##### Proof Plan Encoding
28+
/// The subtract expression is encoded as follows:
29+
/// 1. The left hand side expression
30+
/// 2. The right hand side expression
31+
/// @param __expr The subtract expression data
32+
/// @param __builder The verification builder
33+
/// @param __chiEval The chi value for evaluation
34+
/// @return __exprOut The remaining expression after processing
35+
/// @return __builderOut The verification builder result
36+
/// @return __eval The evaluated result
37+
function __subtractExprEvaluate( // solhint-disable-line gas-calldata-parameters
38+
bytes calldata __expr, VerificationBuilder.Builder memory __builder, uint256 __chiEval)
39+
external
40+
pure
41+
returns (bytes calldata __exprOut, VerificationBuilder.Builder memory __builderOut, uint256 __eval)
42+
{
43+
assembly {
44+
// IMPORT-YUL ../base/Errors.sol
45+
function err(code) {
46+
revert(0, 0)
47+
}
48+
// IMPORT-YUL ../base/Queue.pre.sol
49+
function dequeue(queue_ptr) -> value {
50+
revert(0, 0)
51+
}
52+
// IMPORT-YUL ../base/SwitchUtil.pre.sol
53+
function case_const(lhs, rhs) {
54+
revert(0, 0)
55+
}
56+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
57+
function builder_get_column_evaluation(builder_ptr, column_num) -> eval {
58+
revert(0, 0)
59+
}
60+
// IMPORT-YUL ../base/Array.pre.sol
61+
function get_array_element(arr_ptr, index) -> value {
62+
revert(0, 0)
63+
}
64+
// IMPORT-YUL ColumnExpr.pre.sol
65+
function column_expr_evaluate(expr_ptr, builder_ptr) -> expr_ptr_out, eval {
66+
revert(0, 0)
67+
}
68+
// IMPORT-YUL LiteralExpr.pre.sol
69+
function literal_expr_evaluate(expr_ptr, chi_eval) -> expr_ptr_out, eval {
70+
revert(0, 0)
71+
}
72+
// IMPORT-YUL EqualsExpr.pre.sol
73+
function equals_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
74+
revert(0, 0)
75+
}
76+
// IMPORT-YUL AddExpr.pre.sol
77+
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
78+
revert(0, 0)
79+
}
80+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
81+
function builder_consume_final_round_mle(builder_ptr) -> value {
82+
revert(0, 0)
83+
}
84+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
85+
function builder_produce_identity_constraint(builder_ptr, evaluation, degree) {
86+
revert(0, 0)
87+
}
88+
// IMPORT-YUL ProofExpr.pre.sol
89+
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
90+
revert(0, 0)
91+
}
92+
93+
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
94+
let lhs_eval
95+
expr_ptr, lhs_eval := proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval)
96+
97+
let rhs_eval
98+
expr_ptr, rhs_eval := proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval)
99+
100+
result_eval := addmod(lhs_eval, mulmod(MODULUS_MINUS_ONE, rhs_eval, MODULUS), MODULUS)
101+
expr_ptr_out := expr_ptr
102+
}
103+
104+
let __exprOutOffset
105+
__exprOutOffset, __eval := subtract_expr_evaluate(__expr.offset, __builder, __chiEval)
106+
__exprOut.offset := __exprOutOffset
107+
// slither-disable-next-line write-after-write
108+
__exprOut.length := sub(__expr.length, sub(__exprOutOffset, __expr.offset))
109+
}
110+
__builderOut = __builder;
111+
}
112+
}

solidity/src/proof_plans/FilterExec.pre.sol

+8
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,14 @@ library FilterExec {
132132
function equals_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
133133
revert(0, 0)
134134
}
135+
// IMPORT-YUL ../proof_exprs/AddExpr.pre.sol
136+
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
137+
revert(0, 0)
138+
}
139+
// IMPORT-YUL ../proof_exprs/SubtractExpr.pre.sol
140+
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
141+
revert(0, 0)
142+
}
135143
// IMPORT-YUL ../proof_exprs/ProofExpr.pre.sol
136144
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
137145
revert(0, 0)

solidity/src/proof_plans/ProofPlan.pre.sol

+8
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,14 @@ library ProofPlan {
9595
function equals_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
9696
revert(0, 0)
9797
}
98+
// IMPORT-YUL ../proof_exprs/AddExpr.pre.sol
99+
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
100+
revert(0, 0)
101+
}
102+
// IMPORT-YUL ../proof_exprs/SubtractExpr.pre.sol
103+
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
104+
revert(0, 0)
105+
}
98106
// IMPORT-YUL ../proof_exprs/ProofExpr.pre.sol
99107
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
100108
revert(0, 0)

solidity/src/verifier/Verifier.pre.sol

+8
Original file line numberDiff line numberDiff line change
@@ -270,6 +270,14 @@ library Verifier {
270270
function literal_expr_evaluate(expr_ptr, chi_eval) -> expr_ptr_out, eval {
271271
revert(0, 0)
272272
}
273+
// IMPORT-YUL ../proof_exprs/AddExpr.pre.sol
274+
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
275+
revert(0, 0)
276+
}
277+
// IMPORT-YUL ../proof_exprs/SubtractExpr.pre.sol
278+
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
279+
revert(0, 0)
280+
}
273281
// IMPORT-YUL ../proof_exprs/ProofExpr.pre.sol
274282
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
275283
revert(0, 0)

0 commit comments

Comments
 (0)