openvm_stark_backend/air_builders/symbolic/
dag.rs

1use std::sync::Arc;
2
3use p3_field::Field;
4use rustc_hash::FxHashMap;
5use serde::{Deserialize, Serialize};
6
7use super::SymbolicConstraints;
8use crate::{
9    air_builders::symbolic::{
10        symbolic_expression::SymbolicExpression, symbolic_variable::SymbolicVariable,
11    },
12    interaction::{Interaction, SymbolicInteraction},
13};
14
15/// A node in symbolic expression DAG.
16/// Basically replace `Arc`s in `SymbolicExpression` with node IDs.
17/// Intended to be serializable and deserializable.
18#[derive(Clone, Debug, Hash, Serialize, Deserialize, PartialEq, Eq)]
19#[serde(bound(serialize = "F: Serialize", deserialize = "F: Deserialize<'de>"))]
20#[repr(C)]
21pub enum SymbolicExpressionNode<F> {
22    Variable(SymbolicVariable<F>),
23    IsFirstRow,
24    IsLastRow,
25    IsTransition,
26    Constant(F),
27    Add {
28        left_idx: usize,
29        right_idx: usize,
30        degree_multiple: usize,
31    },
32    Sub {
33        left_idx: usize,
34        right_idx: usize,
35        degree_multiple: usize,
36    },
37    Neg {
38        idx: usize,
39        degree_multiple: usize,
40    },
41    Mul {
42        left_idx: usize,
43        right_idx: usize,
44        degree_multiple: usize,
45    },
46}
47
48#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
49#[serde(bound(serialize = "F: Serialize", deserialize = "F: Deserialize<'de>"))]
50#[repr(C)]
51pub struct SymbolicExpressionDag<F> {
52    /// Nodes in **topological** order.
53    pub nodes: Vec<SymbolicExpressionNode<F>>,
54    /// Node indices of expressions to assert equal zero.
55    pub constraint_idx: Vec<usize>,
56}
57
58impl<F> SymbolicExpressionDag<F> {
59    pub fn max_rotation(&self) -> usize {
60        let mut rotation = 0;
61        for node in &self.nodes {
62            if let SymbolicExpressionNode::Variable(var) = node {
63                rotation = rotation.max(var.entry.offset().unwrap_or(0));
64            }
65        }
66        rotation
67    }
68
69    pub fn num_constraints(&self) -> usize {
70        self.constraint_idx.len()
71    }
72}
73
74#[derive(Clone, Debug, Serialize, Deserialize)]
75#[serde(bound(serialize = "F: Serialize", deserialize = "F: Deserialize<'de>"))]
76#[repr(C)]
77pub struct SymbolicConstraintsDag<F> {
78    /// DAG with all symbolic expressions as nodes.
79    /// These nodes include expressions for plain AIR constraints as well as symbolic expressions
80    /// used for `interactions`.
81    pub constraints: SymbolicExpressionDag<F>,
82    /// List of all interactions, where expressions in the interactions
83    /// are referenced by node idx as `usize`.
84    ///
85    /// These expressions are converted into a LogUp fractional sum
86    /// which must be proven using GKR.
87    pub interactions: Vec<Interaction<usize>>,
88}
89
90pub(crate) fn build_symbolic_constraints_dag<F: Field>(
91    constraints: &[SymbolicExpression<F>],
92    interactions: &[SymbolicInteraction<F>],
93) -> SymbolicConstraintsDag<F> {
94    let mut builder = SymbolicDagBuilder::new();
95    let mut constraint_idx: Vec<usize> = constraints
96        .iter()
97        .map(|expr| builder.add_expr(expr))
98        .collect();
99    constraint_idx.sort();
100    constraint_idx.dedup();
101    let interactions: Vec<Interaction<usize>> = interactions
102        .iter()
103        .map(|interaction| {
104            let fields: Vec<usize> = interaction
105                .message
106                .iter()
107                .map(|field_expr| builder.add_expr(field_expr))
108                .collect();
109            let count = builder.add_expr(&interaction.count);
110            Interaction {
111                message: fields,
112                count,
113                bus_index: interaction.bus_index,
114                count_weight: interaction.count_weight,
115            }
116        })
117        .collect();
118    let constraints = SymbolicExpressionDag {
119        nodes: builder.nodes,
120        constraint_idx,
121    };
122    SymbolicConstraintsDag {
123        constraints,
124        interactions,
125    }
126}
127
128/// Builder for constructing a symbolic expression DAG with structural deduplication
129/// and algebraic simplifications.
130///
131/// Two caches are used:
132/// - `expr_to_idx`: Fast path for expressions with the same Arc pointer
133/// - `node_to_idx`: Structural deduplication - catches identical nodes with different Arc pointers
134///
135/// Algebraic simplifications performed:
136/// - Constant folding: `a + b` → `c`, `a - b` → `c`, `a * b` → `c`, `-a` → `c` (for constants a,b)
137/// - `x + 0` → `x`, `0 + x` → `x`
138/// - `x - 0` → `x`
139/// - `x * 1` → `x`, `1 * x` → `x`
140/// - `x * 0` → `0`, `0 * x` → `0`
141/// - `x + (-y)` → `x - y`
142/// - `x - (-y)` → `x + y`
143pub struct SymbolicDagBuilder<F: Field> {
144    /// Cache: Arc pointer -> node index (fast path for same Arc)
145    pub expr_to_idx: FxHashMap<*const SymbolicExpression<F>, usize>,
146    /// Cache: node structure -> node index (structural deduplication)
147    pub node_to_idx: FxHashMap<SymbolicExpressionNode<F>, usize>,
148    /// Nodes in topological order
149    pub nodes: Vec<SymbolicExpressionNode<F>>,
150}
151
152impl<F: Field> Default for SymbolicDagBuilder<F> {
153    fn default() -> Self {
154        Self::new()
155    }
156}
157
158impl<F: Field> SymbolicDagBuilder<F> {
159    pub fn new() -> Self {
160        Self {
161            expr_to_idx: FxHashMap::default(),
162            node_to_idx: FxHashMap::default(),
163            nodes: Vec::new(),
164        }
165    }
166
167    /// Add a symbolic expression to the DAG, returning its node index.
168    /// Performs structural deduplication and algebraic simplifications.
169    pub fn add_expr(&mut self, expr: &SymbolicExpression<F>) -> usize {
170        // Fast path: check if we've seen this exact Arc pointer before
171        let ptr = expr as *const SymbolicExpression<F>;
172        if let Some(&idx) = self.expr_to_idx.get(&ptr) {
173            return idx;
174        }
175
176        let idx = match expr {
177            SymbolicExpression::Variable(var) => {
178                self.intern_node(SymbolicExpressionNode::Variable(*var))
179            }
180            SymbolicExpression::IsFirstRow => self.intern_node(SymbolicExpressionNode::IsFirstRow),
181            SymbolicExpression::IsLastRow => self.intern_node(SymbolicExpressionNode::IsLastRow),
182            SymbolicExpression::IsTransition => {
183                self.intern_node(SymbolicExpressionNode::IsTransition)
184            }
185            SymbolicExpression::Constant(cons) => {
186                self.intern_node(SymbolicExpressionNode::Constant(*cons))
187            }
188            SymbolicExpression::Add {
189                x,
190                y,
191                degree_multiple,
192            } => {
193                let left_idx = self.add_expr(x.as_ref());
194                let right_idx = self.add_expr(y.as_ref());
195
196                // Constant folding: const + const = const
197                if let (Some(a), Some(b)) = (self.get_const(left_idx), self.get_const(right_idx)) {
198                    self.intern_node(SymbolicExpressionNode::Constant(a + b))
199                }
200                // Simplify: 0 + x = x, x + 0 = x
201                else if self.is_const(left_idx, F::ZERO) {
202                    right_idx
203                } else if self.is_const(right_idx, F::ZERO) {
204                    left_idx
205                }
206                // Normalize: x + (-y) = x - y
207                else if let Some(neg_child_idx) = self.get_neg_child(right_idx) {
208                    self.intern_node(SymbolicExpressionNode::Sub {
209                        left_idx,
210                        right_idx: neg_child_idx,
211                        degree_multiple: *degree_multiple,
212                    })
213                } else {
214                    self.intern_node(SymbolicExpressionNode::Add {
215                        left_idx,
216                        right_idx,
217                        degree_multiple: *degree_multiple,
218                    })
219                }
220            }
221            SymbolicExpression::Sub {
222                x,
223                y,
224                degree_multiple,
225            } => {
226                let left_idx = self.add_expr(x.as_ref());
227                let right_idx = self.add_expr(y.as_ref());
228
229                // Constant folding: const - const = const
230                if let (Some(a), Some(b)) = (self.get_const(left_idx), self.get_const(right_idx)) {
231                    self.intern_node(SymbolicExpressionNode::Constant(a - b))
232                }
233                // Simplify: x - 0 = x
234                else if self.is_const(right_idx, F::ZERO) {
235                    left_idx
236                }
237                // Simplify: x - (-y) = x + y (double negation)
238                else if let Some(neg_child_idx) = self.get_neg_child(right_idx) {
239                    self.intern_node(SymbolicExpressionNode::Add {
240                        left_idx,
241                        right_idx: neg_child_idx,
242                        degree_multiple: *degree_multiple,
243                    })
244                } else {
245                    self.intern_node(SymbolicExpressionNode::Sub {
246                        left_idx,
247                        right_idx,
248                        degree_multiple: *degree_multiple,
249                    })
250                }
251            }
252            SymbolicExpression::Neg { x, degree_multiple } => {
253                let child_idx = self.add_expr(x.as_ref());
254
255                // Constant folding: -const = const
256                if let Some(c) = self.get_const(child_idx) {
257                    self.intern_node(SymbolicExpressionNode::Constant(-c))
258                } else {
259                    self.intern_node(SymbolicExpressionNode::Neg {
260                        idx: child_idx,
261                        degree_multiple: *degree_multiple,
262                    })
263                }
264            }
265            SymbolicExpression::Mul {
266                x,
267                y,
268                degree_multiple,
269            } => {
270                // An important case to remember: square will have Arc::as_ptr(&x) ==
271                // Arc::as_ptr(&y) The `expr_to_idx` will ensure only one recursive
272                // call is done to prevent exponential behavior.
273                let left_idx = self.add_expr(x.as_ref());
274                let right_idx = self.add_expr(y.as_ref());
275
276                // Constant folding: const * const = const
277                if let (Some(a), Some(b)) = (self.get_const(left_idx), self.get_const(right_idx)) {
278                    self.intern_node(SymbolicExpressionNode::Constant(a * b))
279                }
280                // Simplify: 0 * x = 0, x * 1 = x (return left_idx)
281                // Simplify: x * 0 = 0, 1 * x = x (return right_idx)
282                else if self.is_const(left_idx, F::ZERO) || self.is_const(right_idx, F::ONE) {
283                    left_idx
284                } else if self.is_const(right_idx, F::ZERO) || self.is_const(left_idx, F::ONE) {
285                    right_idx
286                } else {
287                    self.intern_node(SymbolicExpressionNode::Mul {
288                        left_idx,
289                        right_idx,
290                        degree_multiple: *degree_multiple,
291                    })
292                }
293            }
294        };
295
296        self.expr_to_idx.insert(ptr, idx);
297        idx
298    }
299
300    /// Intern a node: return existing index if the node already exists, otherwise add it.
301    fn intern_node(&mut self, node: SymbolicExpressionNode<F>) -> usize {
302        *self.node_to_idx.entry(node.clone()).or_insert_with(|| {
303            let idx = self.nodes.len();
304            self.nodes.push(node);
305            idx
306        })
307    }
308
309    /// Check if a node at given index is a constant with specific value.
310    fn is_const(&self, idx: usize, val: F) -> bool {
311        matches!(&self.nodes[idx], SymbolicExpressionNode::Constant(c) if *c == val)
312    }
313
314    /// Get constant value from a node, if it is a constant.
315    fn get_const(&self, idx: usize) -> Option<F> {
316        match &self.nodes[idx] {
317            SymbolicExpressionNode::Constant(c) => Some(*c),
318            _ => None,
319        }
320    }
321
322    /// If a node is a Neg, return its child index.
323    fn get_neg_child(&self, idx: usize) -> Option<usize> {
324        match &self.nodes[idx] {
325            SymbolicExpressionNode::Neg { idx, .. } => Some(*idx),
326            _ => None,
327        }
328    }
329}
330
331impl<F: Field> SymbolicExpressionDag<F> {
332    /// Convert each node to a [`SymbolicExpression<F>`] reference and return
333    /// the full list.
334    fn to_symbolic_expressions(&self) -> Vec<Arc<SymbolicExpression<F>>> {
335        let mut exprs: Vec<Arc<SymbolicExpression<_>>> = Vec::with_capacity(self.nodes.len());
336        for node in &self.nodes {
337            let expr = match *node {
338                SymbolicExpressionNode::Variable(var) => SymbolicExpression::Variable(var),
339                SymbolicExpressionNode::IsFirstRow => SymbolicExpression::IsFirstRow,
340                SymbolicExpressionNode::IsLastRow => SymbolicExpression::IsLastRow,
341                SymbolicExpressionNode::IsTransition => SymbolicExpression::IsTransition,
342                SymbolicExpressionNode::Constant(f) => SymbolicExpression::Constant(f),
343                SymbolicExpressionNode::Add {
344                    left_idx,
345                    right_idx,
346                    degree_multiple,
347                } => SymbolicExpression::Add {
348                    x: exprs[left_idx].clone(),
349                    y: exprs[right_idx].clone(),
350                    degree_multiple,
351                },
352                SymbolicExpressionNode::Sub {
353                    left_idx,
354                    right_idx,
355                    degree_multiple,
356                } => SymbolicExpression::Sub {
357                    x: exprs[left_idx].clone(),
358                    y: exprs[right_idx].clone(),
359                    degree_multiple,
360                },
361                SymbolicExpressionNode::Neg {
362                    idx,
363                    degree_multiple,
364                } => SymbolicExpression::Neg {
365                    x: exprs[idx].clone(),
366                    degree_multiple,
367                },
368                SymbolicExpressionNode::Mul {
369                    left_idx,
370                    right_idx,
371                    degree_multiple,
372                } => SymbolicExpression::Mul {
373                    x: exprs[left_idx].clone(),
374                    y: exprs[right_idx].clone(),
375                    degree_multiple,
376                },
377            };
378            exprs.push(Arc::new(expr));
379        }
380        exprs
381    }
382}
383
384// TEMPORARY conversions until we switch main interfaces to use SymbolicConstraintsDag
385impl<'a, F: Field> From<&'a SymbolicConstraintsDag<F>> for SymbolicConstraints<F> {
386    fn from(dag: &'a SymbolicConstraintsDag<F>) -> Self {
387        let exprs = dag.constraints.to_symbolic_expressions();
388        let constraints = dag
389            .constraints
390            .constraint_idx
391            .iter()
392            .map(|&idx| exprs[idx].as_ref().clone())
393            .collect::<Vec<_>>();
394        let interactions = dag
395            .interactions
396            .iter()
397            .map(|interaction| {
398                let fields = interaction
399                    .message
400                    .iter()
401                    .map(|&idx| exprs[idx].as_ref().clone())
402                    .collect();
403                let count = exprs[interaction.count].as_ref().clone();
404                Interaction {
405                    message: fields,
406                    count,
407                    bus_index: interaction.bus_index,
408                    count_weight: interaction.count_weight,
409                }
410            })
411            .collect::<Vec<_>>();
412        SymbolicConstraints {
413            constraints,
414            interactions,
415        }
416    }
417}
418
419impl<F: Field> From<SymbolicConstraintsDag<F>> for SymbolicConstraints<F> {
420    fn from(dag: SymbolicConstraintsDag<F>) -> Self {
421        (&dag).into()
422    }
423}
424
425impl<F: Field> From<SymbolicConstraints<F>> for SymbolicConstraintsDag<F> {
426    fn from(sc: SymbolicConstraints<F>) -> Self {
427        build_symbolic_constraints_dag(&sc.constraints, &sc.interactions)
428    }
429}
430
431#[cfg(test)]
432mod tests {
433    use p3_baby_bear::BabyBear;
434    use p3_field::PrimeCharacteristicRing;
435
436    use crate::{
437        air_builders::symbolic::{
438            dag::{build_symbolic_constraints_dag, SymbolicExpressionDag, SymbolicExpressionNode},
439            symbolic_expression::SymbolicExpression,
440            symbolic_variable::{Entry, SymbolicVariable},
441        },
442        interaction::Interaction,
443    };
444
445    type F = BabyBear;
446
447    #[test]
448    fn test_duplicate_constraints_are_deduplicated() {
449        // Create a simple expression
450        let expr: SymbolicExpression<F> = SymbolicExpression::Variable(SymbolicVariable::new(
451            Entry::Main {
452                part_index: 0,
453                offset: 0,
454            },
455            0,
456        ));
457
458        // Simulate calling assert_zero twice on the same expression
459        let constraints = vec![expr.clone(), expr.clone()];
460        let interactions = vec![];
461
462        let dag = build_symbolic_constraints_dag(&constraints, &interactions);
463
464        // Nodes are deduplicated - there's only 1 node in the DAG
465        assert_eq!(
466            dag.constraints.nodes.len(),
467            1,
468            "Nodes should be deduplicated"
469        );
470
471        // constraint_idx should also be deduplicated
472        assert_eq!(
473            dag.constraints.constraint_idx,
474            vec![0],
475            "constraint_idx should be deduplicated"
476        );
477
478        // Only 1 constraint
479        assert_eq!(
480            dag.constraints.num_constraints(),
481            1,
482            "Duplicate constraints should be deduplicated"
483        );
484    }
485
486    #[test]
487    fn test_structural_deduplication() {
488        // Create two structurally identical expressions with different Arc pointers
489        // This simulates: builder.assert_zero(x - ONE); builder.assert_zero(x - ONE);
490        let var = SymbolicVariable::<F>::new(
491            Entry::Main {
492                part_index: 0,
493                offset: 0,
494            },
495            0,
496        );
497        let expr1 = SymbolicExpression::from(var) - SymbolicExpression::Constant(F::ONE);
498        let expr2 = SymbolicExpression::from(var) - SymbolicExpression::Constant(F::ONE);
499
500        // These are different Arc allocations
501        assert!(!std::ptr::eq(&expr1, &expr2));
502
503        let constraints = vec![expr1, expr2];
504        let dag = build_symbolic_constraints_dag(&constraints, &[]);
505
506        // With structural deduplication, both expressions should map to the same node
507        // Nodes: Variable(0), Constant(1), Sub(0,1)
508        assert_eq!(dag.constraints.nodes.len(), 3);
509        assert_eq!(dag.constraints.constraint_idx, vec![2]);
510    }
511
512    #[test]
513    fn test_algebraic_simplifications() {
514        let var = SymbolicVariable::<F>::new(
515            Entry::Main {
516                part_index: 0,
517                offset: 0,
518            },
519            0,
520        );
521        let x = SymbolicExpression::from(var);
522        let zero = SymbolicExpression::Constant(F::ZERO);
523        let one = SymbolicExpression::Constant(F::ONE);
524
525        // Test x + 0 = x
526        let expr_add_zero = x.clone() + zero.clone();
527        let dag = build_symbolic_constraints_dag(&[expr_add_zero], &[]);
528        // Should only have Variable node, no Add node
529        assert_eq!(dag.constraints.nodes.len(), 2); // Variable + Constant(0) interned but Add simplified away
530        assert!(matches!(
531            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
532            SymbolicExpressionNode::Variable(_)
533        ));
534
535        // Test 0 + x = x
536        let expr_zero_add = zero.clone() + x.clone();
537        let dag = build_symbolic_constraints_dag(&[expr_zero_add], &[]);
538        assert!(matches!(
539            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
540            SymbolicExpressionNode::Variable(_)
541        ));
542
543        // Test x * 1 = x
544        let expr_mul_one = x.clone() * one.clone();
545        let dag = build_symbolic_constraints_dag(&[expr_mul_one], &[]);
546        assert!(matches!(
547            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
548            SymbolicExpressionNode::Variable(_)
549        ));
550
551        // Test 1 * x = x
552        let expr_one_mul = one.clone() * x.clone();
553        let dag = build_symbolic_constraints_dag(&[expr_one_mul], &[]);
554        assert!(matches!(
555            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
556            SymbolicExpressionNode::Variable(_)
557        ));
558
559        // Test x * 0 = 0
560        let expr_mul_zero = x.clone() * zero.clone();
561        let dag = build_symbolic_constraints_dag(&[expr_mul_zero], &[]);
562        assert!(matches!(
563            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
564            SymbolicExpressionNode::Constant(c) if c == F::ZERO
565        ));
566
567        // Test x - 0 = x
568        let expr_sub_zero = x.clone() - zero.clone();
569        let dag = build_symbolic_constraints_dag(&[expr_sub_zero], &[]);
570        assert!(matches!(
571            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
572            SymbolicExpressionNode::Variable(_)
573        ));
574
575        // Test x + (-y) normalizes to x - y (same as Sub)
576        let y = SymbolicExpression::from(SymbolicVariable::<F>::new(
577            Entry::Main {
578                part_index: 0,
579                offset: 0,
580            },
581            1,
582        ));
583        let expr_add_neg = x.clone() + (-y.clone());
584        let expr_sub = x.clone() - y.clone();
585        let dag1 = build_symbolic_constraints_dag(&[expr_add_neg], &[]);
586        let dag2 = build_symbolic_constraints_dag(&[expr_sub], &[]);
587        // Both should produce the same constraint node (Sub)
588        assert!(matches!(
589            dag1.constraints.nodes[dag1.constraints.constraint_idx[0]],
590            SymbolicExpressionNode::Sub { .. }
591        ));
592        assert_eq!(
593            dag1.constraints.nodes[dag1.constraints.constraint_idx[0]],
594            dag2.constraints.nodes[dag2.constraints.constraint_idx[0]]
595        );
596
597        // Test x - (-y) = x + y
598        let expr_sub_neg = x.clone() - (-y.clone());
599        let dag = build_symbolic_constraints_dag(&[expr_sub_neg], &[]);
600        assert!(matches!(
601            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
602            SymbolicExpressionNode::Add { .. }
603        ));
604    }
605
606    #[test]
607    fn test_constant_folding() {
608        let two = SymbolicExpression::<F>::Constant(F::TWO);
609        let three = SymbolicExpression::<F>::Constant(F::from_u32(3));
610        let five = F::from_u32(5);
611        let six = F::from_u32(6);
612        let neg_three = -F::from_u32(3);
613
614        // Test 2 + 3 = 5
615        let expr_add = two.clone() + three.clone();
616        let dag = build_symbolic_constraints_dag(&[expr_add], &[]);
617        assert!(matches!(
618            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
619            SymbolicExpressionNode::Constant(c) if c == five
620        ));
621
622        // Test 3 - 2 = 1
623        let expr_sub = three.clone() - two.clone();
624        let dag = build_symbolic_constraints_dag(&[expr_sub], &[]);
625        assert!(matches!(
626            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
627            SymbolicExpressionNode::Constant(c) if c == F::ONE
628        ));
629
630        // Test 2 * 3 = 6
631        let expr_mul = two.clone() * three.clone();
632        let dag = build_symbolic_constraints_dag(&[expr_mul], &[]);
633        assert!(matches!(
634            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
635            SymbolicExpressionNode::Constant(c) if c == six
636        ));
637
638        // Test -3 = neg_three
639        let expr_neg = -three.clone();
640        let dag = build_symbolic_constraints_dag(&[expr_neg], &[]);
641        assert!(matches!(
642            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
643            SymbolicExpressionNode::Constant(c) if c == neg_three
644        ));
645
646        // Test chained: (2 + 3) * 2 = 10
647        let expr_chain = (two.clone() + three.clone()) * two.clone();
648        let dag = build_symbolic_constraints_dag(&[expr_chain], &[]);
649        assert!(matches!(
650            dag.constraints.nodes[dag.constraints.constraint_idx[0]],
651            SymbolicExpressionNode::Constant(c) if c == F::from_u32(10)
652        ));
653    }
654
655    #[test]
656    fn test_symbolic_constraints_dag() {
657        // expr = Constant(1) * Variable, which simplifies to just Variable
658        let expr = SymbolicExpression::Constant(F::ONE)
659            * SymbolicVariable::new(
660                Entry::Main {
661                    part_index: 1,
662                    offset: 2,
663                },
664                3,
665            );
666        let constraints = vec![
667            SymbolicExpression::IsFirstRow * SymbolicExpression::IsLastRow
668                + SymbolicExpression::Constant(F::ONE)
669                + SymbolicExpression::IsFirstRow * SymbolicExpression::IsLastRow
670                + expr.clone(),
671            expr.clone() * expr.clone(),
672        ];
673        let interactions = vec![Interaction {
674            bus_index: 0,
675            message: vec![expr.clone(), SymbolicExpression::Constant(F::TWO)],
676            count: SymbolicExpression::Constant(F::ONE),
677            count_weight: 1,
678        }];
679        let dag = build_symbolic_constraints_dag(&constraints, &interactions);
680        assert_eq!(
681            dag.constraints,
682            SymbolicExpressionDag::<F> {
683                nodes: vec![
684                    SymbolicExpressionNode::IsFirstRow,
685                    SymbolicExpressionNode::IsLastRow,
686                    SymbolicExpressionNode::Mul {
687                        left_idx: 0,
688                        right_idx: 1,
689                        degree_multiple: 2
690                    },
691                    SymbolicExpressionNode::Constant(F::ONE),
692                    SymbolicExpressionNode::Add {
693                        left_idx: 2,
694                        right_idx: 3,
695                        degree_multiple: 2
696                    },
697                    // With structural deduplication, IsFirstRow * IsLastRow is now reused
698                    // instead of duplicated. The second occurrence reuses node index 2.
699                    SymbolicExpressionNode::Add {
700                        left_idx: 4,
701                        right_idx: 2,
702                        degree_multiple: 2
703                    },
704                    // expr = Constant(1) * Variable simplifies to just Variable (1 * x = x)
705                    SymbolicExpressionNode::Variable(SymbolicVariable::new(
706                        Entry::Main {
707                            part_index: 1,
708                            offset: 2
709                        },
710                        3
711                    )),
712                    // First constraint: ... + expr (which is Variable at index 6)
713                    SymbolicExpressionNode::Add {
714                        left_idx: 5,
715                        right_idx: 6,
716                        degree_multiple: 2
717                    },
718                    // Second constraint: expr * expr = Variable * Variable
719                    SymbolicExpressionNode::Mul {
720                        left_idx: 6,
721                        right_idx: 6,
722                        degree_multiple: 2
723                    },
724                    SymbolicExpressionNode::Constant(F::TWO),
725                ],
726                constraint_idx: vec![7, 8],
727            }
728        );
729        assert_eq!(
730            dag.interactions,
731            vec![Interaction {
732                bus_index: 0,
733                // expr simplified to Variable at index 6, Constant(2) at index 9
734                message: vec![6, 9],
735                count: 3,
736                count_weight: 1,
737            }]
738        );
739    }
740}
openvm_stark_backend/air_builders/symbolic/dag.rs

openvm_stark_backend/air_builders/symbolic/
dag.rs
