proof_of_sql/sql/proof_exprs/
proof_expr.rs

1use crate::{
2    base::{
3        database::{Column, ColumnRef, ColumnType, Table},
4        map::{IndexMap, IndexSet},
5        proof::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 result_evaluate<'a, S: Scalar>(
23        &self,
24        alloc: &'a Bump,
25        table: &Table<'a, S>,
26    ) -> Column<'a, S>;
27
28    /// Evaluate the expression, add components needed to prove it, and return thet resulting column
29    /// of values
30    fn prover_evaluate<'a, S: Scalar>(
31        &self,
32        builder: &mut FinalRoundBuilder<'a, S>,
33        alloc: &'a Bump,
34        table: &Table<'a, S>,
35    ) -> Column<'a, S>;
36
37    /// Compute the evaluation of a multilinear extension from this expression
38    /// at the random sumcheck point and adds components needed to verify the expression to
39    /// [`VerificationBuilder<S>`]
40    fn verifier_evaluate<S: Scalar>(
41        &self,
42        builder: &mut impl VerificationBuilder<S>,
43        accessor: &IndexMap<ColumnRef, S>,
44        chi_eval: S,
45    ) -> Result<S, ProofError>;
46
47    /// Insert in the [`IndexSet`] `columns` all the column
48    /// references in the `BoolExpr` or forwards the call to some
49    /// subsequent `bool_expr`
50    fn get_column_references(&self, columns: &mut IndexSet<ColumnRef>);
51}