proof_of_sql/sql/proof_exprs/
proof_expr.rs

1use crate::{
2    base::{
3        database::{Column, ColumnRef, ColumnType, LiteralValue, Table},
4        map::{IndexMap, IndexSet},
5        proof::{PlaceholderResult, ProofError},
6        scalar::Scalar,
7    },
8    sql::proof::{FinalRoundBuilder, VerificationBuilder},
9};
10use bumpalo::Bump;
11use core::fmt::Debug;
12
13/// Provable AST column expression that evaluates to a `Column`
14#[enum_dispatch::enum_dispatch(DynProofExpr)]
15pub trait ProofExpr: Debug + Send + Sync {
16    /// Get the data type of the expression
17    fn data_type(&self) -> ColumnType;
18
19    /// This returns the result of evaluating the expression on the given table, and returns
20    /// a column of values. This result slice is guaranteed to have length `table_length`.
21    /// Implementations must ensure that the returned slice has length `table_length`.
22    fn first_round_evaluate<'a, S: Scalar>(
23        &self,
24        alloc: &'a Bump,
25        table: &Table<'a, S>,
26        params: &[LiteralValue],
27    ) -> PlaceholderResult<Column<'a, S>>;
28
29    /// Evaluate the expression, add components needed to prove it, and return thet resulting column
30    /// of values
31    fn final_round_evaluate<'a, S: Scalar>(
32        &self,
33        builder: &mut FinalRoundBuilder<'a, S>,
34        alloc: &'a Bump,
35        table: &Table<'a, S>,
36        params: &[LiteralValue],
37    ) -> PlaceholderResult<Column<'a, S>>;
38
39    /// Compute the evaluation of a multilinear extension from this expression
40    /// at the random sumcheck point and adds components needed to verify the expression to
41    /// [`VerificationBuilder<S>`]
42    fn verifier_evaluate<S: Scalar>(
43        &self,
44        builder: &mut impl VerificationBuilder<S>,
45        accessor: &IndexMap<ColumnRef, S>,
46        chi_eval: S,
47        params: &[LiteralValue],
48    ) -> Result<S, ProofError>;
49
50    /// Insert in the [`IndexSet`] `columns` all the column
51    /// references in the `BoolExpr` or forwards the call to some
52    /// subsequent `bool_expr`
53    fn get_column_references(&self, columns: &mut IndexSet<ColumnRef>);
54}