Skip to content

Commit 1c3ab6c

Browse files
iajoineriajoiner
authored
feat(sol): support varchar and varbinary literals (#840)
# Overview This PR adds support for `VARCHAR` and `VARBINARY` literals in the Solidity‐based proof code, enabling variable-length string and binary data types in Proof-of-SQL. # Changes - **Constants.sol** Added new data-type variant constants `DATA_TYPE_VARCHAR_VARIANT = 7` and `DATA_TYPE_VARBINARY_VARIANT = 11` - **DataType.pre.sol** Implemented `case 7` (varchar) and `case 11` (varbinary) in `__readEntry` to: 1. Read a 64-bit length prefix 2. Copy the payload into EVM memory at `FREE_PTR` 3. Compute `keccak256` over that data 4. Update `FREE_PTR` and advance the result pointer - **DataType.t.pre.sol** Added unit tests covering: - `testReadVarcharEntryExpr`, `testReadNonAsciiVarcharEntryExpr`, `testFuzzReadVarcharEntryExpr` - `testReadVarbinaryEntryExpr`, `testFuzzReadVarbinaryEntryExpr` - **LiteralExpr.t.pre.sol** Extended the proof-expression tests to include parsing and proof generation of `VARCHAR` and `VARBINARY` literal expressions
1 parent f90020e commit 1c3ab6c

20 files changed

+246
-11
lines changed

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

Lines changed: 31 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -116,18 +116,43 @@ fn we_can_verify_a_query_with_all_supported_types_using_the_evm() {
116116
1_746_627_940,
117117
],
118118
),
119+
varchar("lang", ["en", "he", "hu", "ru", "hy"]),
120+
varchar(
121+
"sxt",
122+
[
123+
"Space and Time",
124+
"מרחב וזמן",
125+
"Tér és idő",
126+
"Пространство и время",
127+
"Տարածություն և ժամանակ",
128+
],
129+
),
130+
varbinary(
131+
"bin",
132+
[
133+
&b""[..],
134+
&b"\x00\x01\x02\x03\x04"[..],
135+
&b"\xFF\xFE\xFD\xFC\xFB"[..],
136+
&b"\xFF\xFE\xFD\xFC\xFB"[..],
137+
&b"\xFF\xFE\xFD\xFC\xFB"[..],
138+
],
139+
),
119140
]),
120141
0,
121142
&ps[..],
122143
);
123144

124145
let sql_list = [
125-
"SELECT b, i8, i16, i32, i64, d, t from table where b",
126-
"SELECT b, i8, i16, i32, i64, d, t from table where i8 = 0",
127-
"SELECT b, i8, i16, i32, i64, d, t from table where i16 = 0",
128-
"SELECT b, i8, i16, i32, i64, d, t from table where i32 = 1",
129-
"SELECT b, i8, i16, i32, i64, d, t from table where i64 = 0",
130-
"SELECT b, i8, i16, i32, i64, d, t from table where d = 1",
146+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where bin = 0x",
147+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where bin = 0x0001020304",
148+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where lang = 'en'",
149+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where sxt = 'מרחב וזמן'",
150+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where b",
151+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where i8 = 0",
152+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where i16 = 0",
153+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where i32 = 1",
154+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where i64 = 0",
155+
"SELECT b, i8, i16, i32, i64, d, t, lang, sxt, bin from table where d = 1",
131156
];
132157

133158
for sql in sql_list {

‎solidity/slither.config.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
{
2-
"detectors_to_exclude": "assembly,naming-conventions",
2+
"detectors_to_exclude": "assembly,naming-conventions,too-many-digits",
33
"fail_on": "pedantic"
44
}

‎solidity/src/base/Constants.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,10 +115,14 @@ uint32 constant DATA_TYPE_SMALLINT_VARIANT = 3;
115115
uint32 constant DATA_TYPE_INT_VARIANT = 4;
116116
/// @dev BigInt variant constant for column types
117117
uint32 constant DATA_TYPE_BIGINT_VARIANT = 5;
118+
/// @dev Varchar variant constant for column types
119+
uint32 constant DATA_TYPE_VARCHAR_VARIANT = 7;
118120
/// @dev Decimal75 variant constant for column types
119121
uint32 constant DATA_TYPE_DECIMAL75_VARIANT = 8;
120122
/// @dev Timestamp variant constant for column types
121123
uint32 constant DATA_TYPE_TIMESTAMP_VARIANT = 9;
124+
/// @dev Varbinary variant constant for column types
125+
uint32 constant DATA_TYPE_VARBINARY_VARIANT = 11;
122126

123127
/// @dev Position of the free memory pointer in the context of the EVM memory.
124128
uint256 constant FREE_PTR = 0x40;

‎solidity/src/base/DataType.pre.sol

Lines changed: 64 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,53 @@ library DataType {
3737
function case_const(lhs, rhs) {
3838
revert(0, 0)
3939
}
40+
function read_binary(result_ptr) -> result_ptr_out, entry {
41+
let free_ptr := mload(FREE_PTR)
42+
let len := shr(UINT64_PADDING_BITS, calldataload(result_ptr))
43+
result_ptr := add(result_ptr, UINT64_SIZE)
44+
45+
// temps with their empty‐slice defaults
46+
entry := 0
47+
48+
// only run this when len != 0
49+
if len {
50+
calldatacopy(free_ptr, result_ptr, len)
51+
let hash_val := keccak256(free_ptr, len)
52+
53+
// endian-swap steps
54+
hash_val :=
55+
or(
56+
shr(128, and(hash_val, 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000000000000000000000000000)),
57+
shl(128, and(hash_val, 0x00000000000000000000000000000000FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF))
58+
)
59+
hash_val :=
60+
or(
61+
shr(64, and(hash_val, 0xFFFFFFFFFFFFFFFF0000000000000000FFFFFFFFFFFFFFFF0000000000000000)),
62+
shl(64, and(hash_val, 0x0000000000000000FFFFFFFFFFFFFFFF0000000000000000FFFFFFFFFFFFFFFF))
63+
)
64+
hash_val :=
65+
or(
66+
shr(32, and(hash_val, 0xFFFFFFFF00000000FFFFFFFF00000000FFFFFFFF00000000FFFFFFFF00000000)),
67+
shl(32, and(hash_val, 0x00000000FFFFFFFF00000000FFFFFFFF00000000FFFFFFFF00000000FFFFFFFF))
68+
)
69+
hash_val :=
70+
or(
71+
shr(16, and(hash_val, 0xFFFF0000FFFF0000FFFF0000FFFF0000FFFF0000FFFF0000FFFF0000FFFF0000)),
72+
shl(16, and(hash_val, 0x0000FFFF0000FFFF0000FFFF0000FFFF0000FFFF0000FFFF0000FFFF0000FFFF))
73+
)
74+
hash_val :=
75+
or(
76+
shr(8, and(hash_val, 0xFF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00)),
77+
shl(8, and(hash_val, 0x00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF00FF))
78+
)
79+
80+
entry := and(hash_val, MODULUS_MASK)
81+
}
82+
83+
// single assign to named returns
84+
result_ptr_out := add(result_ptr, len)
85+
}
86+
4087
function read_entry(result_ptr, data_type_variant) -> result_ptr_out, entry {
4188
result_ptr_out := result_ptr
4289
switch data_type_variant
@@ -45,44 +92,58 @@ library DataType {
4592
entry := shr(BOOLEAN_PADDING_BITS, calldataload(result_ptr))
4693
if shr(1, entry) { err(ERR_INVALID_BOOLEAN) }
4794
result_ptr_out := add(result_ptr, BOOLEAN_SIZE)
95+
entry := mod(entry, MODULUS)
4896
}
4997
case 2 {
5098
case_const(2, DATA_TYPE_TINYINT_VARIANT)
5199
entry :=
52100
add(MODULUS, signextend(INT8_SIZE_MINUS_ONE, shr(INT8_PADDING_BITS, calldataload(result_ptr))))
53101
result_ptr_out := add(result_ptr, INT8_SIZE)
102+
entry := mod(entry, MODULUS)
54103
}
55104
case 3 {
56105
case_const(3, DATA_TYPE_SMALLINT_VARIANT)
57106
entry :=
58107
add(MODULUS, signextend(INT16_SIZE_MINUS_ONE, shr(INT16_PADDING_BITS, calldataload(result_ptr))))
59108
result_ptr_out := add(result_ptr, INT16_SIZE)
109+
entry := mod(entry, MODULUS)
60110
}
61111
case 4 {
62112
case_const(4, DATA_TYPE_INT_VARIANT)
63113
entry :=
64114
add(MODULUS, signextend(INT32_SIZE_MINUS_ONE, shr(INT32_PADDING_BITS, calldataload(result_ptr))))
65115
result_ptr_out := add(result_ptr, INT32_SIZE)
116+
entry := mod(entry, MODULUS)
66117
}
67118
case 5 {
68119
case_const(5, DATA_TYPE_BIGINT_VARIANT)
69120
entry :=
70121
add(MODULUS, signextend(INT64_SIZE_MINUS_ONE, shr(INT64_PADDING_BITS, calldataload(result_ptr))))
71122
result_ptr_out := add(result_ptr, INT64_SIZE)
123+
entry := mod(entry, MODULUS)
124+
}
125+
case 7 {
126+
case_const(7, DATA_TYPE_VARCHAR_VARIANT)
127+
result_ptr_out, entry := read_binary(result_ptr)
72128
}
73129
case 8 {
74130
case_const(8, DATA_TYPE_DECIMAL75_VARIANT)
75131
entry := calldataload(result_ptr)
76132
result_ptr_out := add(result_ptr, WORD_SIZE)
133+
entry := mod(entry, MODULUS)
77134
}
78135
case 9 {
79136
case_const(9, DATA_TYPE_TIMESTAMP_VARIANT)
80137
entry :=
81138
add(MODULUS, signextend(INT64_SIZE_MINUS_ONE, shr(INT64_PADDING_BITS, calldataload(result_ptr))))
82139
result_ptr_out := add(result_ptr, INT64_SIZE)
140+
entry := mod(entry, MODULUS)
141+
}
142+
case 11 {
143+
case_const(11, DATA_TYPE_VARBINARY_VARIANT)
144+
result_ptr_out, entry := read_binary(result_ptr)
83145
}
84146
default { err(ERR_UNSUPPORTED_DATA_TYPE_VARIANT) }
85-
entry := mod(entry, MODULUS)
86147
}
87148
let __exprOutOffset
88149
__exprOutOffset, __entry := read_entry(__expr.offset, __dataTypeVariant)
@@ -128,6 +189,7 @@ library DataType {
128189
case 3 { case_const(3, DATA_TYPE_SMALLINT_VARIANT) }
129190
case 4 { case_const(4, DATA_TYPE_INT_VARIANT) }
130191
case 5 { case_const(5, DATA_TYPE_BIGINT_VARIANT) }
192+
case 7 { case_const(7, DATA_TYPE_VARCHAR_VARIANT) }
131193
case 8 {
132194
case_const(8, DATA_TYPE_DECIMAL75_VARIANT)
133195
ptr_out := add(ptr_out, UINT8_SIZE) // Skip precision
@@ -138,6 +200,7 @@ library DataType {
138200
ptr_out := add(ptr_out, UINT32_SIZE) // Skip timeunit
139201
ptr_out := add(ptr_out, INT32_SIZE) // Skip timezone
140202
}
203+
case 11 { case_const(11, DATA_TYPE_VARBINARY_VARIANT) }
141204
default { err(ERR_UNSUPPORTED_DATA_TYPE_VARIANT) }
142205
}
143206

‎solidity/src/proof_exprs/AddExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,10 @@ library AddExpr {
114114
revert(0, 0)
115115
}
116116
// IMPORT-YUL ../base/DataType.pre.sol
117+
function read_binary(result_ptr) -> result_ptr_out, entry {
118+
revert(0, 0)
119+
}
120+
// IMPORT-YUL ../base/DataType.pre.sol
117121
function read_data_type(ptr) -> ptr_out, data_type {
118122
revert(0, 0)
119123
}

‎solidity/src/proof_exprs/AndExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,10 @@ library AndExpr {
114114
revert(0, 0)
115115
}
116116
// IMPORT-YUL ../base/DataType.pre.sol
117+
function read_binary(result_ptr) -> result_ptr_out, entry {
118+
revert(0, 0)
119+
}
120+
// IMPORT-YUL ../base/DataType.pre.sol
117121
function read_data_type(ptr) -> ptr_out, data_type {
118122
revert(0, 0)
119123
}

‎solidity/src/proof_exprs/CastExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,10 @@ library CastExpr {
6565
revert(0, 0)
6666
}
6767
// IMPORT-YUL ../base/DataType.pre.sol
68+
function read_binary(result_ptr) -> result_ptr_out, entry {
69+
revert(0, 0)
70+
}
71+
// IMPORT-YUL ../base/DataType.pre.sol
6872
function read_data_type(ptr) -> ptr_out, data_type {
6973
revert(0, 0)
7074
}

‎solidity/src/proof_exprs/EqualsExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,10 @@ library EqualsExpr {
140140
revert(0, 0)
141141
}
142142
// IMPORT-YUL ../base/DataType.pre.sol
143+
function read_binary(result_ptr) -> result_ptr_out, entry {
144+
revert(0, 0)
145+
}
146+
// IMPORT-YUL ../base/DataType.pre.sol
143147
function read_data_type(ptr) -> ptr_out, data_type {
144148
revert(0, 0)
145149
}

‎solidity/src/proof_exprs/LiteralExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,10 @@ library LiteralExpr {
5252
revert(0, 0)
5353
}
5454
// IMPORT-YUL ../base/DataType.pre.sol
55+
function read_binary(result_ptr) -> result_ptr_out, entry {
56+
revert(0, 0)
57+
}
58+
// IMPORT-YUL ../base/DataType.pre.sol
5559
function read_data_type(ptr) -> ptr_out, data_type {
5660
revert(0, 0)
5761
}

‎solidity/src/proof_exprs/MultiplyExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,10 @@ library MultiplyExpr {
114114
revert(0, 0)
115115
}
116116
// IMPORT-YUL ../base/DataType.pre.sol
117+
function read_binary(result_ptr) -> result_ptr_out, entry {
118+
revert(0, 0)
119+
}
120+
// IMPORT-YUL ../base/DataType.pre.sol
117121
function read_data_type(ptr) -> ptr_out, data_type {
118122
revert(0, 0)
119123
}

‎solidity/src/proof_exprs/NotExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,10 @@ library NotExpr {
113113
revert(0, 0)
114114
}
115115
// IMPORT-YUL ../base/DataType.pre.sol
116+
function read_binary(result_ptr) -> result_ptr_out, entry {
117+
revert(0, 0)
118+
}
119+
// IMPORT-YUL ../base/DataType.pre.sol
116120
function read_data_type(ptr) -> ptr_out, data_type {
117121
revert(0, 0)
118122
}

‎solidity/src/proof_exprs/OrExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,10 @@ library OrExpr {
114114
revert(0, 0)
115115
}
116116
// IMPORT-YUL ../base/DataType.pre.sol
117+
function read_binary(result_ptr) -> result_ptr_out, entry {
118+
revert(0, 0)
119+
}
120+
// IMPORT-YUL ../base/DataType.pre.sol
117121
function read_data_type(ptr) -> ptr_out, data_type {
118122
revert(0, 0)
119123
}

‎solidity/src/proof_exprs/ProofExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,10 @@ library ProofExpr {
9898
revert(0, 0)
9999
}
100100
// IMPORT-YUL ../base/DataType.pre.sol
101+
function read_binary(result_ptr) -> result_ptr_out, entry {
102+
revert(0, 0)
103+
}
104+
// IMPORT-YUL ../base/DataType.pre.sol
101105
function read_data_type(ptr) -> ptr_out, data_type {
102106
revert(0, 0)
103107
}

‎solidity/src/proof_exprs/SubtractExpr.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,10 @@ library SubtractExpr {
114114
revert(0, 0)
115115
}
116116
// IMPORT-YUL ../base/DataType.pre.sol
117+
function read_binary(result_ptr) -> result_ptr_out, entry {
118+
revert(0, 0)
119+
}
120+
// IMPORT-YUL ../base/DataType.pre.sol
117121
function read_data_type(ptr) -> ptr_out, data_type {
118122
revert(0, 0)
119123
}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -170,6 +170,10 @@ library FilterExec {
170170
revert(0, 0)
171171
}
172172
// IMPORT-YUL ../base/DataType.pre.sol
173+
function read_binary(result_ptr) -> result_ptr_out, entry {
174+
revert(0, 0)
175+
}
176+
// IMPORT-YUL ../base/DataType.pre.sol
173177
function read_data_type(ptr) -> ptr_out, data_type {
174178
revert(0, 0)
175179
}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -149,6 +149,10 @@ library ProofPlan {
149149
revert(0, 0)
150150
}
151151
// 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
152156
function read_data_type(ptr) -> ptr_out, data_type {
153157
revert(0, 0)
154158
}

‎solidity/src/verifier/ResultVerifier.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,10 @@ library ResultVerifier {
5151
revert(0, 0)
5252
}
5353
// IMPORT-YUL ../base/DataType.pre.sol
54+
function read_binary(result_ptr) -> result_ptr_out, entry {
55+
revert(0, 0)
56+
}
57+
// IMPORT-YUL ../base/DataType.pre.sol
5458
function read_data_type(ptr) -> ptr_out, data_type {
5559
revert(0, 0)
5660
}

‎solidity/src/verifier/Verifier.pre.sol

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -463,6 +463,10 @@ library Verifier {
463463
function read_entry(result_ptr, data_type_variant) -> result_ptr_out, entry {
464464
revert(0, 0)
465465
}
466+
// IMPORT-YUL ../base/DataType.pre.sol
467+
function read_binary(result_ptr) -> result_ptr_out, entry {
468+
revert(0, 0)
469+
}
466470

467471
// IMPORT-YUL ../base/DataType.pre.sol
468472
function read_data_type(ptr) -> ptr_out, data_type {

0 commit comments

Comments
 (0)