proof_of_sql/sql/proof_exprs/
dyn_proof_expr.rs

1use super::{
2    AddExpr, AndExpr, CastExpr, ColumnExpr, EqualsExpr, InequalityExpr, LiteralExpr, MultiplyExpr,
3    NotExpr, OrExpr, PlaceholderExpr, ProofExpr, ScalingCastExpr, SubtractExpr,
4};
5use crate::{
6    base::{
7        database::{Column, ColumnRef, ColumnType, LiteralValue, Table},
8        map::{IndexMap, IndexSet},
9        proof::{PlaceholderResult, ProofError},
10        scalar::Scalar,
11    },
12    sql::{
13        proof::{FinalRoundBuilder, VerificationBuilder},
14        AnalyzeResult,
15    },
16};
17use alloc::boxed::Box;
18use bumpalo::Bump;
19use core::fmt::Debug;
20use serde::{Deserialize, Serialize};
21use sqlparser::ast::Ident;
22
23/// Enum of AST column expression types that implement `ProofExpr`. Is itself a `ProofExpr`.
24#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)]
25#[enum_dispatch::enum_dispatch]
26pub enum DynProofExpr {
27    /// Column
28    Column(ColumnExpr),
29    /// Provable logical AND expression
30    And(AndExpr),
31    /// Provable logical OR expression
32    Or(OrExpr),
33    /// Provable logical NOT expression
34    Not(NotExpr),
35    /// Provable CONST expression
36    Literal(LiteralExpr),
37    /// Provable placeholder expression
38    Placeholder(PlaceholderExpr),
39    /// Provable AST expression for an equals expression
40    Equals(EqualsExpr),
41    /// Provable AST expression for an inequality expression
42    Inequality(InequalityExpr),
43    /// Provable numeric `+` expression
44    Add(AddExpr),
45    /// Provable numeric `-` expression
46    Subtract(SubtractExpr),
47    /// Provable numeric `*` expression
48    Multiply(MultiplyExpr),
49    /// Provable CAST expression
50    Cast(CastExpr),
51    /// Provable expression for casting numeric expressions to decimal expressions
52    ScalingCast(ScalingCastExpr),
53}
54impl DynProofExpr {
55    /// Create column expression
56    #[must_use]
57    pub fn new_column(column_ref: ColumnRef) -> Self {
58        Self::Column(ColumnExpr::new(column_ref))
59    }
60    /// Create logical AND expression
61    pub fn try_new_and(lhs: DynProofExpr, rhs: DynProofExpr) -> AnalyzeResult<Self> {
62        AndExpr::try_new(Box::new(lhs), Box::new(rhs)).map(DynProofExpr::And)
63    }
64    /// Create logical OR expression
65    pub fn try_new_or(lhs: DynProofExpr, rhs: DynProofExpr) -> AnalyzeResult<Self> {
66        OrExpr::try_new(Box::new(lhs), Box::new(rhs)).map(DynProofExpr::Or)
67    }
68    /// Create logical NOT expression
69    pub fn try_new_not(expr: DynProofExpr) -> AnalyzeResult<Self> {
70        NotExpr::try_new(Box::new(expr)).map(DynProofExpr::Not)
71    }
72    /// Create CONST expression
73    #[must_use]
74    pub fn new_literal(value: LiteralValue) -> Self {
75        Self::Literal(LiteralExpr::new(value))
76    }
77    /// Create placeholder expression
78    pub fn try_new_placeholder(id: usize, column_type: ColumnType) -> AnalyzeResult<Self> {
79        Ok(Self::Placeholder(PlaceholderExpr::try_new(
80            id,
81            column_type,
82        )?))
83    }
84    /// Create a new equals expression
85    pub fn try_new_equals(lhs: DynProofExpr, rhs: DynProofExpr) -> AnalyzeResult<Self> {
86        EqualsExpr::try_new(Box::new(lhs), Box::new(rhs)).map(DynProofExpr::Equals)
87    }
88    /// Create a new inequality expression
89    pub fn try_new_inequality(
90        lhs: DynProofExpr,
91        rhs: DynProofExpr,
92        is_lt: bool,
93    ) -> AnalyzeResult<Self> {
94        InequalityExpr::try_new(Box::new(lhs), Box::new(rhs), is_lt).map(DynProofExpr::Inequality)
95    }
96
97    /// Create a new add expression
98    pub fn try_new_add(lhs: DynProofExpr, rhs: DynProofExpr) -> AnalyzeResult<Self> {
99        AddExpr::try_new(Box::new(lhs), Box::new(rhs)).map(DynProofExpr::Add)
100    }
101
102    /// Create a new subtract expression
103    pub fn try_new_subtract(lhs: DynProofExpr, rhs: DynProofExpr) -> AnalyzeResult<Self> {
104        SubtractExpr::try_new(Box::new(lhs), Box::new(rhs)).map(DynProofExpr::Subtract)
105    }
106
107    /// Create a new multiply expression
108    pub fn try_new_multiply(lhs: DynProofExpr, rhs: DynProofExpr) -> AnalyzeResult<Self> {
109        MultiplyExpr::try_new(Box::new(lhs), Box::new(rhs)).map(DynProofExpr::Multiply)
110    }
111
112    /// Create a new cast expression
113    pub fn try_new_cast(from_column: DynProofExpr, to_datatype: ColumnType) -> AnalyzeResult<Self> {
114        CastExpr::try_new(Box::new(from_column), to_datatype).map(DynProofExpr::Cast)
115    }
116
117    /// Create a new decimal scale cast expression
118    pub fn try_new_scaling_cast(
119        from_expr: DynProofExpr,
120        to_datatype: ColumnType,
121    ) -> AnalyzeResult<Self> {
122        ScalingCastExpr::try_new(Box::new(from_expr), to_datatype).map(DynProofExpr::ScalingCast)
123    }
124}