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

proof_of_sql/sql/proof_exprs/
dyn_proof_expr.rs
