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}