-
Notifications
You must be signed in to change notification settings - Fork 80
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
7 changed files
with
302 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,123 @@ | ||
| use super::{ProvableExpr, ProvableExprPlan}; | ||
| use crate::{ | ||
| base::{ | ||
| commitment::Commitment, | ||
| database::{Column, ColumnRef, ColumnType, CommitmentAccessor, DataAccessor}, | ||
| proof::ProofError, | ||
| }, | ||
| sql::{ | ||
| ast::{try_multiply_column_types, try_multiply_columns}, | ||
| parse::ConversionError, | ||
| proof::{CountBuilder, ProofBuilder, SumcheckSubpolynomialType, VerificationBuilder}, | ||
| }, | ||
| }; | ||
| use bumpalo::Bump; | ||
| use num_traits::One; | ||
| use serde::{Deserialize, Serialize}; | ||
| use std::collections::HashSet; | ||
|
|
||
| /// Provable numerical * expression | ||
| #[derive(Debug, PartialEq, Serialize, Deserialize)] | ||
| pub struct MultiplyExpr<C: Commitment> { | ||
| lhs: Box<ProvableExprPlan<C>>, | ||
| rhs: Box<ProvableExprPlan<C>>, | ||
| } | ||
|
|
||
| impl<C: Commitment> MultiplyExpr<C> { | ||
| /// Create numerical * expression | ||
| pub fn new(lhs: Box<ProvableExprPlan<C>>, rhs: Box<ProvableExprPlan<C>>) -> Self { | ||
| Self { lhs, rhs } | ||
| } | ||
| } | ||
|
|
||
| impl<C: Commitment> ProvableExpr<C> for MultiplyExpr<C> { | ||
| fn count(&self, builder: &mut CountBuilder) -> Result<(), ProofError> { | ||
| self.lhs.count(builder)?; | ||
| self.rhs.count(builder)?; | ||
| builder.count_subpolynomials(1); | ||
| builder.count_intermediate_mles(1); | ||
| builder.count_degree(3); | ||
| Ok(()) | ||
| } | ||
|
|
||
| fn data_type(&self) -> ColumnType { | ||
| try_multiply_column_types(self.lhs.data_type(), self.rhs.data_type()) | ||
| .expect("Failed to multiply column types") | ||
| } | ||
|
|
||
| fn result_evaluate<'a>( | ||
| &self, | ||
| table_length: usize, | ||
| alloc: &'a Bump, | ||
| accessor: &'a dyn DataAccessor<C::Scalar>, | ||
| ) -> Column<'a, C::Scalar> { | ||
| let lhs_column: Column<'a, C::Scalar> = | ||
| self.lhs.result_evaluate(table_length, alloc, accessor); | ||
| let rhs_column: Column<'a, C::Scalar> = | ||
| self.rhs.result_evaluate(table_length, alloc, accessor); | ||
| let scalars = try_multiply_columns(lhs_column, rhs_column, alloc) | ||
| .expect("Failed to multiply columns"); | ||
| Column::Scalar(scalars) | ||
| } | ||
|
|
||
| #[tracing::instrument( | ||
| name = "proofs.sql.ast.and_expr.prover_evaluate", | ||
| level = "info", | ||
| skip_all | ||
| )] | ||
| fn prover_evaluate<'a>( | ||
| &self, | ||
| builder: &mut ProofBuilder<'a, C::Scalar>, | ||
| alloc: &'a Bump, | ||
| accessor: &'a dyn DataAccessor<C::Scalar>, | ||
| ) -> Column<'a, C::Scalar> { | ||
| let lhs_column: Column<'a, C::Scalar> = self.lhs.prover_evaluate(builder, alloc, accessor); | ||
| let rhs_column: Column<'a, C::Scalar> = self.rhs.prover_evaluate(builder, alloc, accessor); | ||
| let lhs_scalars = lhs_column.to_scalar_with_scaling(0); | ||
| let rhs_scalars = rhs_column.to_scalar_with_scaling(0); | ||
| let lhs_bump: &'a [C::Scalar] = alloc.alloc_slice_copy(&lhs_scalars); | ||
| let rhs_bump: &'a [C::Scalar] = alloc.alloc_slice_copy(&rhs_scalars); | ||
|
|
||
| // lhs_times_rhs | ||
| let lhs_times_rhs: &'a [C::Scalar] = try_multiply_columns(lhs_column, rhs_column, alloc) | ||
| .expect("Failed to multiply columns"); | ||
| builder.produce_intermediate_mle(lhs_times_rhs); | ||
|
|
||
| // subpolynomial: lhs_times_rhs - lhs * rhs | ||
| builder.produce_sumcheck_subpolynomial( | ||
| SumcheckSubpolynomialType::Identity, | ||
| vec![ | ||
| (C::Scalar::one(), vec![Box::new(lhs_times_rhs)]), | ||
| ( | ||
| -C::Scalar::one(), | ||
| vec![Box::new(lhs_bump), Box::new(rhs_bump)], | ||
| ), | ||
| ], | ||
| ); | ||
| Column::Scalar(lhs_times_rhs) | ||
| } | ||
|
|
||
| fn verifier_evaluate( | ||
| &self, | ||
| builder: &mut VerificationBuilder<C>, | ||
| accessor: &dyn CommitmentAccessor<C>, | ||
| ) -> Result<C::Scalar, ProofError> { | ||
| let lhs = self.lhs.verifier_evaluate(builder, accessor)?; | ||
| let rhs = self.rhs.verifier_evaluate(builder, accessor)?; | ||
|
|
||
| // lhs_times_rhs | ||
| let lhs_times_rhs = builder.consume_intermediate_mle(); | ||
|
|
||
| // subpolynomial: lhs_times_rhs - lhs * rhs | ||
| let eval = builder.mle_evaluations.random_evaluation * (lhs_times_rhs - lhs * rhs); | ||
| builder.produce_sumcheck_subpolynomial_evaluation(&eval); | ||
|
|
||
| // selection | ||
| Ok(lhs_times_rhs) | ||
| } | ||
|
|
||
| fn get_column_references(&self, columns: &mut HashSet<ColumnRef>) { | ||
| self.lhs.get_column_references(columns); | ||
| self.rhs.get_column_references(columns); | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,62 @@ | ||
| use super::{test_utility::*, FilterExpr, ProvableExpr}; | ||
| use crate::{ | ||
| base::{ | ||
| commitment::InnerProductProof, | ||
| database::{ | ||
| make_random_test_accessor_data, Column, ColumnType, OwnedTable, OwnedTableTestAccessor, | ||
| RandomTestAccessorDescriptor, TestAccessor, | ||
| }, | ||
| scalar::Curve25519Scalar, | ||
| }, | ||
| owned_table, | ||
| sql::{ | ||
| ast::{test_utility::*, ProvableExprPlan}, | ||
| proof::{exercise_verification, VerifiableQueryResult}, | ||
| }, | ||
| }; | ||
| /// This function creates a TestAccessor, adds a table, and then creates a FilterExpr with the given parameters. | ||
| /// It then executes the query, verifies the result, and returns the table. | ||
| /// The query is `select r_0,\cdots r_k from table where res = lhs * rhs` | ||
| fn create_and_verify_test_col_mul_expr( | ||
| table_ref: &str, | ||
| results: &[&str], | ||
| lhs: &str, | ||
| rhs: &str, | ||
| res: &str, | ||
| data: OwnedTable<Curve25519Scalar>, | ||
| offset: usize, | ||
| ) -> OwnedTable<Curve25519Scalar> { | ||
| let mut accessor = OwnedTableTestAccessor::<InnerProductProof>::new_empty_with_setup(()); | ||
| let t = table_ref.parse().unwrap(); | ||
| accessor.add_table(t, data, offset); | ||
| let mul_expr = mul(column(t, lhs, &accessor), column(t, rhs, &accessor)); | ||
| let eq_expr = equal(column(t, res, &accessor), mul_expr); | ||
| let ast = FilterExpr::new(cols_result(t, results, &accessor), tab(t), eq_expr); | ||
| let res = VerifiableQueryResult::new(&ast, &accessor, &()); | ||
| exercise_verification(&res, &ast, &accessor, t); | ||
| res.verify(&ast, &accessor, &()).unwrap().table | ||
| } | ||
|
|
||
| #[test] | ||
| fn we_can_prove_a_simple_mul_query() { | ||
| let data = owned_table!( | ||
| "product" => [1_i64, -4, 0, 4], | ||
| "c0" => [0_i32, -2, 0, -1], | ||
| "d" => ["ab", "t", "efg", "g"], | ||
| "c1" => [0_i16, 2, -2, 0], | ||
| ); | ||
| let res = create_and_verify_test_col_mul_expr( | ||
| "sxt.t", | ||
| &["product", "c0"], | ||
| "c0", | ||
| "c1", | ||
| "product", | ||
| data, | ||
| 0, | ||
| ); | ||
| let expected_res = owned_table!( | ||
| "product" => [-4_i64, 0], | ||
| "c0" => [-2_i32, 0] | ||
| ); | ||
| assert_eq!(res, expected_res); | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.