Skip to content

Commit ca12a17

Browse files
committed
feat(sol) add CastExpr to Solidity and EVMCastExpr to evm_proof_plan
1 parent b13e1dc commit ca12a17

File tree

9 files changed

+231
-1
lines changed

9 files changed

+231
-1
lines changed

Diff for: crates/proof-of-sql/src/sql/evm_proof_plan/exprs.rs

+43-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use crate::{
44
database::{ColumnRef, LiteralValue},
55
map::IndexSet,
66
},
7-
sql::proof_exprs::{AddExpr, ColumnExpr, DynProofExpr, EqualsExpr, LiteralExpr, SubtractExpr},
7+
sql::proof_exprs::{AddExpr, CastExpr, ColumnExpr, DynProofExpr, EqualsExpr, LiteralExpr, SubtractExpr},
88
};
99
use alloc::boxed::Box;
1010
use serde::{Deserialize, Serialize};
@@ -17,6 +17,7 @@ pub(crate) enum EVMDynProofExpr {
1717
Equals(EVMEqualsExpr),
1818
Add(EVMAddExpr),
1919
Subtract(EVMSubtractExpr),
20+
Cast(EVMCastExpr),
2021
}
2122
impl EVMDynProofExpr {
2223
/// Try to create an `EVMDynProofExpr` from a `DynProofExpr`.
@@ -64,6 +65,9 @@ impl EVMDynProofExpr {
6465
EVMDynProofExpr::Subtract(subtract_expr) => Ok(DynProofExpr::Subtract(
6566
subtract_expr.try_into_proof_expr(column_refs)?,
6667
)),
68+
EVMDynProofExpr::Cast(cast_expr) => Ok(DynProofExpr::Cast(
69+
cast_expr.try_into_proof_expr(column_refs)?,
70+
)),
6771
}
6872
}
6973
}
@@ -263,6 +267,44 @@ impl EVMSubtractExpr {
263267
}
264268
}
265269

270+
/// Represents a cast expression.
271+
#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
272+
pub(crate) struct EVMCastExpr {
273+
from_expr: Box<EVMDynProofExpr>,
274+
}
275+
276+
impl EVMCastExpr {
277+
#[cfg_attr(not(test), expect(dead_code))]
278+
pub(crate) fn new(from_expr: EVMDynProofExpr) -> Self {
279+
Self {
280+
from_expr: Box::new(from_expr),
281+
}
282+
}
283+
284+
/// Try to create an `EVMCastExpr` from a `CastExpr`.
285+
pub(crate) fn try_from_proof_expr(
286+
expr: &CastExpr,
287+
column_refs: &IndexSet<ColumnRef>,
288+
) -> EVMProofPlanResult<Self> {
289+
Ok(EVMCastExpr {
290+
from_expr: Box::new(EVMDynProofExpr::try_from_proof_expr(
291+
&expr.from_expr,
292+
column_refs,
293+
)?),
294+
})
295+
}
296+
297+
pub(crate) fn try_into_proof_expr(
298+
&self,
299+
column_refs: &IndexSet<ColumnRef>,
300+
) -> EVMProofPlanResult<CastExpr> {
301+
Ok(CastExpr {
302+
from_expr: Box::new(self.from_expr.try_into_proof_expr(column_refs)?),
303+
})
304+
}
305+
}
306+
307+
266308
#[cfg(test)]
267309
mod tests {
268310
use super::*;

Diff for: solidity/src/proof_exprs/AddExpr.pre.sol

+4
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,10 @@ library AddExpr {
7777
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
7878
revert(0, 0)
7979
}
80+
// IMPORT-YUL CastExpr.pre.sol
81+
function cast_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
82+
revert(0, 0)
83+
}
8084
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
8185
function builder_consume_final_round_mle(builder_ptr) -> value {
8286
revert(0, 0)

Diff for: solidity/src/proof_exprs/CastExpr.pre.sol

+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 CastExpr
10+
/// @dev Library for handling casting a proof expression
11+
library CastExpr {
12+
/// @notice Evaluates an cast expression by casting a sub-expression
13+
/// @custom:as-yul-wrapper
14+
/// #### Wrapped Yul Function
15+
/// ##### Signature
16+
/// ```yul
17+
/// cast_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 the sub-expression
25+
/// * `eval` - the evaluation result from the builder's final round MLE
26+
/// @notice Evaluates a sub-expression and casts it
27+
/// ##### Proof Plan Encoding
28+
/// The cast expression is encoded as follows:
29+
/// 1. The input expression
30+
/// @param __expr The cast expression data
31+
/// @param __builder The verification builder
32+
/// @param __chiEval The chi value for evaluation
33+
/// @return __exprOut The remaining expression after processing
34+
/// @return __builderOut The verification builder result
35+
/// @return __eval The evaluated result
36+
function __CastExprEvaluate( // solhint-disable-line gas-calldata-parameters
37+
bytes calldata __expr, VerificationBuilder.Builder memory __builder, uint256 __chiEval)
38+
external
39+
pure
40+
returns (bytes calldata __exprOut, VerificationBuilder.Builder memory __builderOut, uint256 __eval)
41+
{
42+
assembly {
43+
// IMPORT-YUL ../base/Errors.sol
44+
function err(code) {
45+
revert(0, 0)
46+
}
47+
// IMPORT-YUL ../base/Queue.pre.sol
48+
function dequeue(queue_ptr) -> value {
49+
revert(0, 0)
50+
}
51+
// IMPORT-YUL ../base/SwitchUtil.pre.sol
52+
function case_const(lhs, rhs) {
53+
revert(0, 0)
54+
}
55+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
56+
function builder_get_column_evaluation(builder_ptr, column_num) -> eval {
57+
revert(0, 0)
58+
}
59+
// IMPORT-YUL ../base/Array.pre.sol
60+
function get_array_element(arr_ptr, index) -> value {
61+
revert(0, 0)
62+
}
63+
// IMPORT-YUL ColumnExpr.pre.sol
64+
function column_expr_evaluate(expr_ptr, builder_ptr) -> expr_ptr_out, eval {
65+
revert(0, 0)
66+
}
67+
// IMPORT-YUL LiteralExpr.pre.sol
68+
function literal_expr_evaluate(expr_ptr, chi_eval) -> expr_ptr_out, eval {
69+
revert(0, 0)
70+
}
71+
// IMPORT-YUL EqualsExpr.pre.sol
72+
function equals_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
73+
revert(0, 0)
74+
}
75+
// IMPORT-YUL AddExpr.pre.sol
76+
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
77+
revert(0, 0)
78+
}
79+
// IMPORT-YUL SubtractExpr.pre.sol
80+
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
81+
revert(0, 0)
82+
}
83+
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
84+
function builder_consume_final_round_mle(builder_ptr) -> value {
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 ProofExpr.pre.sol
92+
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
93+
revert(0, 0)
94+
}
95+
96+
function cast_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
97+
let input_eval
98+
expr_ptr, input_eval := proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval)
99+
100+
result_eval := input_eval
101+
expr_ptr_out := expr_ptr
102+
}
103+
104+
let __exprOutOffset
105+
__exprOutOffset, __eval := cast_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+
}

Diff for: solidity/src/proof_exprs/EqualsExpr.pre.sol

+4
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,10 @@ library EqualsExpr {
103103
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
104104
revert(0, 0)
105105
}
106+
// IMPORT-YUL CastExpr.pre.sol
107+
function cast_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
108+
revert(0, 0)
109+
}
106110
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
107111
function builder_consume_final_round_mle(builder_ptr) -> value {
108112
revert(0, 0)

Diff for: solidity/src/proof_exprs/SubtractExpr.pre.sol

+4
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,10 @@ library SubtractExpr {
7777
function add_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
7878
revert(0, 0)
7979
}
80+
// IMPORT-YUL CastExpr.pre.sol
81+
function cast_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
82+
revert(0, 0)
83+
}
8084
// IMPORT-YUL ../builder/VerificationBuilder.pre.sol
8185
function builder_consume_final_round_mle(builder_ptr) -> value {
8286
revert(0, 0)

Diff for: solidity/src/proof_plans/FilterExec.pre.sol

+4
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,10 @@ library FilterExec {
140140
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
141141
revert(0, 0)
142142
}
143+
// IMPORT-YUL ../proof_exprs/CastExpr.pre.sol
144+
function cast_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
145+
revert(0, 0)
146+
}
143147
// IMPORT-YUL ../proof_exprs/ProofExpr.pre.sol
144148
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
145149
revert(0, 0)

Diff for: solidity/src/proof_plans/ProofPlan.pre.sol

+4
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,10 @@ library ProofPlan {
103103
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
104104
revert(0, 0)
105105
}
106+
// IMPORT-YUL ../proof_exprs/CastExpr.pre.sol
107+
function cast_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
108+
revert(0, 0)
109+
}
106110
// IMPORT-YUL ../proof_exprs/ProofExpr.pre.sol
107111
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
108112
revert(0, 0)

Diff for: solidity/src/verifier/Verifier.pre.sol

+4
Original file line numberDiff line numberDiff line change
@@ -278,6 +278,10 @@ library Verifier {
278278
function subtract_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, result_eval {
279279
revert(0, 0)
280280
}
281+
// IMPORT-YUL ../proof_exprs/CastExpr.pre.sol
282+
function cast_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
283+
revert(0, 0)
284+
}
281285
// IMPORT-YUL ../proof_exprs/ProofExpr.pre.sol
282286
function proof_expr_evaluate(expr_ptr, builder_ptr, chi_eval) -> expr_ptr_out, eval {
283287
revert(0, 0)

Diff for: solidity/test/proof_exprs/CastExpr.t.pre.sol

+52
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
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 {Test} from "forge-std/Test.sol";
6+
import "../../src/base/Constants.sol";
7+
import {VerificationBuilder} from "../../src/builder/VerificationBuilder.pre.sol";
8+
import {CastExpr} from "../../src/proof_exprs/CastExpr.pre.sol";
9+
import {F} from "../base/FieldUtil.sol";
10+
11+
contract CastExprTest is Test {
12+
function testSimpleCastExpr() public pure {
13+
bytes memory expr = abi.encodePacked(
14+
abi.encodePacked(LITERAL_EXPR_VARIANT, LITERAL_BIGINT_VARIANT, int64(7)),
15+
hex"abcdef"
16+
);
17+
VerificationBuilder.Builder memory builder;
18+
19+
uint256 eval;
20+
(expr, builder, eval) = CastExpr.__CastExprEvaluate(expr, builder, 10);
21+
22+
assert(eval == 70);
23+
bytes memory expectedExprOut = hex"abcdef";
24+
assert(expr.length == expectedExprOut.length);
25+
uint256 exprOutLength = expr.length;
26+
for (uint256 i = 0; i < exprOutLength; ++i) {
27+
assert(expr[i] == expectedExprOut[i]);
28+
}
29+
}
30+
31+
function testFuzzCastExpr(
32+
VerificationBuilder.Builder memory builder,
33+
uint256 chiEvaluation,
34+
int64 inputValue,
35+
bytes memory trailingExpr
36+
) public pure {
37+
bytes memory expr = abi.encodePacked(
38+
abi.encodePacked(LITERAL_EXPR_VARIANT, LITERAL_BIGINT_VARIANT, inputValue),
39+
trailingExpr
40+
);
41+
42+
uint256 eval;
43+
(expr, builder, eval) = CastExpr.__CastExprEvaluate(expr, builder, chiEvaluation);
44+
45+
assert(eval == (F.from(inputValue) * F.from(chiEvaluation)).into());
46+
assert(expr.length == trailingExpr.length);
47+
uint256 exprOutLength = expr.length;
48+
for (uint256 i = 0; i < exprOutLength; ++i) {
49+
assert(expr[i] == trailingExpr[i]);
50+
}
51+
}
52+
}

0 commit comments

Comments
 (0)