proof_of_sql/sql/proof_exprs/
dyn_proof_expr.rs1use 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#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)]
25#[enum_dispatch::enum_dispatch]
26pub enum DynProofExpr {
27 Column(ColumnExpr),
29 And(AndExpr),
31 Or(OrExpr),
33 Not(NotExpr),
35 Literal(LiteralExpr),
37 Placeholder(PlaceholderExpr),
39 Equals(EqualsExpr),
41 Inequality(InequalityExpr),
43 Add(AddExpr),
45 Subtract(SubtractExpr),
47 Multiply(MultiplyExpr),
49 Cast(CastExpr),
51 ScalingCast(ScalingCastExpr),
53}
54impl DynProofExpr {
55 #[must_use]
57 pub fn new_column(column_ref: ColumnRef) -> Self {
58 Self::Column(ColumnExpr::new(column_ref))
59 }
60 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 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 pub fn try_new_not(expr: DynProofExpr) -> AnalyzeResult<Self> {
70 NotExpr::try_new(Box::new(expr)).map(DynProofExpr::Not)
71 }
72 #[must_use]
74 pub fn new_literal(value: LiteralValue) -> Self {
75 Self::Literal(LiteralExpr::new(value))
76 }
77 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 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 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 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 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 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 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 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}