Skip to main content

sp1_hypercube/ir/
expr.rs

1use std::{borrow::Borrow, collections::HashMap, fmt::Display};
2
3use serde::{Deserialize, Serialize};
4use slop_algebra::Field;
5
6use crate::ir::{FuncCtx, IrVar};
7
8/// The `AB::Expr` of the constraint compiler. Note that for the constraint
9/// compiler, this is also `AB::Var`.
10#[derive(Debug, Clone, Copy, Serialize, Deserialize)]
11pub enum ExprRef<F> {
12    /// An [`IrVar`], usually this comes from the chip/inputs.
13    IrVar(IrVar<F>),
14    /// An expression where its value `i` means this expression represents the
15    /// value of the i-th assignment. For the constraint compiler, since it
16    /// uses an SSA-style IR, `i` also means this expression represents the
17    /// result of the i-th computation.
18    Expr(usize),
19}
20
21impl<F: Field> ExprRef<F> {
22    /// An expression representing a variable from public inputs.
23    #[must_use]
24    pub fn public(index: usize) -> Self {
25        ExprRef::IrVar(IrVar::Public(index))
26    }
27
28    /// An expression representing a variable from preprocessed trace.
29    #[must_use]
30    pub fn preprocessed(index: usize) -> Self {
31        ExprRef::IrVar(IrVar::Preprocessed(index))
32    }
33
34    /// An expression representing a variable from main trace.
35    #[must_use]
36    pub fn main(index: usize) -> Self {
37        ExprRef::IrVar(IrVar::Main(index))
38    }
39
40    /// An expression representing a constant value.
41    pub fn constant(value: F) -> Self {
42        ExprRef::IrVar(IrVar::Constant(value))
43    }
44
45    /// An expression representing a variable from input arguments.
46    pub fn input_arg(ctx: &mut FuncCtx) -> Self {
47        let index = ctx.input_idx;
48        ctx.input_idx += 1;
49        ExprRef::IrVar(IrVar::InputArg(index))
50    }
51
52    /// Get a struct with input arguments.
53    ///
54    /// Given a sized struct that can be flattened to a slice of `Self`, produce a new struct of
55    /// this type where all the fields are replaced with input arguments.
56    pub fn input_from_struct<T>(ctx: &mut FuncCtx) -> T
57    where
58        T: Copy,
59        [Self]: Borrow<T>,
60    {
61        let size = std::mem::size_of::<T>() / std::mem::size_of::<Self>();
62        let values = (0..size).map(|_| Self::input_arg(ctx)).collect::<Vec<_>>();
63        let value_ref: &T = values.as_slice().borrow();
64        *value_ref
65    }
66
67    /// An expression representing a variable from output arguments.
68    pub fn output_arg(ctx: &mut FuncCtx) -> Self {
69        let index = ctx.output_idx;
70        ctx.output_idx += 1;
71        ExprRef::IrVar(IrVar::OutputArg(index))
72    }
73
74    /// Get a struct with output arguments.
75    ///
76    /// Given a sized struct that can be flattened to a slice of `Self`, produce a new struct of
77    /// this type where all the fields are replaced with output arguments.
78    pub fn output_from_struct<T>(ctx: &mut FuncCtx) -> T
79    where
80        T: Copy,
81        [Self]: Borrow<T>,
82    {
83        let size = std::mem::size_of::<T>() / std::mem::size_of::<Self>();
84        let values = (0..size).map(|_| Self::output_arg(ctx)).collect::<Vec<_>>();
85        let value_ref: &T = values.as_slice().borrow();
86        *value_ref
87    }
88
89    /// Returns the value in Lean-syntax string
90    pub fn to_lean_string(&self, input_mapping: &HashMap<usize, String>) -> String {
91        match self {
92            ExprRef::Expr(idx) => format!("E{idx}"),
93            ExprRef::IrVar(IrVar::Main(idx)) => format!("Main[{idx}]"),
94            ExprRef::IrVar(IrVar::Constant(idx)) => format!("{idx}"),
95            ExprRef::IrVar(IrVar::InputArg(idx)) => input_mapping.get(idx).unwrap().clone(),
96            ExprRef::IrVar(IrVar::Public(idx)) => format!("public_value () {idx}"),
97            _ => todo!(),
98        }
99    }
100
101    /// Returns the value in Lean-syntax string, except that it must be an intermediate expression.
102    ///
103    /// Used for the LHS when assigning variables in steps
104    pub fn expr_to_lean_string(&self) -> String {
105        match self {
106            ExprRef::Expr(idx) => format!("E{idx}"),
107            _ => unimplemented!(),
108        }
109    }
110}
111
112impl<F: Field> Display for ExprRef<F> {
113    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
114        match self {
115            ExprRef::IrVar(ir_var) => write!(f, "{ir_var}"),
116            ExprRef::Expr(expr) => write!(f, "Expr({expr})"),
117        }
118    }
119}
120
121impl<F: Field> ExprRef<F> {
122    /// Convert to Lean syntax
123    pub fn to_lean(&self, is_operation: bool, input_mapping: &HashMap<usize, String>) -> String {
124        match self {
125            ExprRef::IrVar(var) => var.to_lean(is_operation, input_mapping),
126            ExprRef::Expr(i) => format!("E{i}"),
127        }
128    }
129}
130
131/// The [`ExtensionField`] for the constraint compiler.
132#[derive(Debug, Clone, Copy, Serialize, Deserialize)]
133pub enum ExprExtRef<EF> {
134    /// A constant in the extension field.
135    ExtConstant(EF),
136    /// An expression where its value `i` means this expression represents the
137    /// value of the i-th assignment. For the constraint compiler, since it
138    /// uses an SSA-style IR, `i` also means this expression represents the
139    /// result of the i-th computation.
140    Expr(usize),
141}
142
143impl<EF: Field> ExprExtRef<EF> {
144    /// An expression representing a variable from input arguments.
145    pub fn input_arg(ctx: &mut FuncCtx) -> Self {
146        let index = ctx.input_idx;
147        ctx.input_idx += 1;
148        ExprExtRef::Expr(index)
149    }
150
151    /// An expression representing a variable from output arguments.
152    pub fn output_arg(ctx: &mut FuncCtx) -> Self {
153        let index = ctx.output_idx;
154        ctx.output_idx += 1;
155        ExprExtRef::Expr(index)
156    }
157}
158
159impl<EF: Field> Display for ExprExtRef<EF> {
160    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
161        match self {
162            ExprExtRef::ExtConstant(ext_constant) => write!(f, "{ext_constant}"),
163            ExprExtRef::Expr(expr) => write!(f, "ExprExt({expr})"),
164        }
165    }
166}
167
168impl<EF: Field> ExprExtRef<EF> {
169    /// Convert to Lean syntax
170    pub fn to_lean(&self, _is_operation: bool, _input_mapping: &HashMap<usize, String>) -> String {
171        match self {
172            ExprExtRef::ExtConstant(c) => format!("{c}"),
173            ExprExtRef::Expr(i) => format!("EExt{i}"),
174        }
175    }
176}