diff --git a/core/Cargo.toml b/core/Cargo.toml
index f78a1893af..4c378cbaa0 100644
--- a/core/Cargo.toml
+++ b/core/Cargo.toml
@@ -53,8 +53,8 @@ tempfile = "3.9.0"
 tracing = "0.1.40"
 tracing-forest = { version = "0.1.6", features = ["ansi", "smallvec"] }
 tracing-subscriber = { version = "0.3.17", features = ["std", "env-filter"] }
-strum_macros = "0.26.2"
-strum = "0.26.2"
+strum_macros = "0.26"
+strum = "0.26"
 web-time = "1.1.0"
 rayon-scan = "0.1.1"
 
diff --git a/recursion/circuit/src/challenger.rs b/recursion/circuit/src/challenger.rs
index fe1163cdbd..81a1910291 100644
--- a/recursion/circuit/src/challenger.rs
+++ b/recursion/circuit/src/challenger.rs
@@ -292,8 +292,8 @@ mod tests {
         challenger.observe(&mut builder, c);
         let result2 = challenger.sample_ext(&mut builder);
 
-        builder.assert_ext_eq(SymbolicExt::Const(gt1), result1);
-        builder.assert_ext_eq(SymbolicExt::Const(gt2), result2);
+        builder.assert_ext_eq(SymbolicExt::from_f(gt1), result1);
+        builder.assert_ext_eq(SymbolicExt::from_f(gt2), result2);
 
         let mut backend = ConstraintCompiler::<OuterConfig>::default();
         let constraints = backend.emit(builder.operations);
diff --git a/recursion/circuit/src/constraints.rs b/recursion/circuit/src/constraints.rs
index def14aa089..f922cd375c 100644
--- a/recursion/circuit/src/constraints.rs
+++ b/recursion/circuit/src/constraints.rs
@@ -8,8 +8,8 @@ use sp1_core::stark::AirOpenedValues;
 use sp1_core::stark::PROOF_MAX_NUM_PVS;
 use sp1_core::stark::{MachineChip, StarkGenericConfig};
 use sp1_recursion_compiler::ir::Array;
+use sp1_recursion_compiler::ir::ExtensionOperand;
 use sp1_recursion_compiler::ir::Felt;
-use sp1_recursion_compiler::ir::SymbolicFelt;
 use sp1_recursion_compiler::ir::{Builder, Config, Ext};
 use sp1_recursion_compiler::prelude::SymbolicExt;
 use sp1_recursion_program::commit::PolynomialSpaceVariable;
@@ -45,7 +45,7 @@ where
                             .iter()
                             .enumerate()
                             .map(|(e_i, &x)| {
-                                x * SymbolicExt::<C::F, C::EF>::Const(C::EF::monomial(e_i))
+                                x * SymbolicExt::<C::F, C::EF>::from_f(C::EF::monomial(e_i))
                             })
                             .sum::<SymbolicExt<_, _>>(),
                     )
@@ -101,8 +101,8 @@ where
                         // Calculate: other_domain.zp_at_point(zeta)
                         //     * other_domain.zp_at_point(domain.first_point()).inverse()
                         let first_point = domain.first_point(builder);
-                        let first_point: Ext<_, _> =
-                            builder.eval(SymbolicExt::Base(SymbolicFelt::Val(first_point).into()));
+                        let first_point_ext = first_point.to_operand().symbolic();
+                        let first_point: Ext<_, _> = builder.eval(first_point_ext);
                         let z = other_domain.zp_at_point(builder, first_point);
                         other_domain.zp_at_point(builder, zeta) * z.inverse()
                     })
diff --git a/recursion/circuit/src/fri.rs b/recursion/circuit/src/fri.rs
index ea4710e7ad..639f2c97c0 100644
--- a/recursion/circuit/src/fri.rs
+++ b/recursion/circuit/src/fri.rs
@@ -66,9 +66,9 @@ pub fn verify_two_adic_pcs<C: Config>(
         .zip(&fri_challenges.query_indices)
         .map(|(query_opening, &index)| {
             let mut ro: [Ext<C::F, C::EF>; 32] =
-                [builder.eval(SymbolicExt::Const(C::EF::zero())); 32];
+                [builder.eval(SymbolicExt::from_f(C::EF::zero())); 32];
             let mut alpha_pow: [Ext<C::F, C::EF>; 32] =
-                [builder.eval(SymbolicExt::Const(C::EF::one())); 32];
+                [builder.eval(SymbolicExt::from_f(C::EF::one())); 32];
 
             for (batch_opening, round) in izip!(query_opening.clone(), &rounds) {
                 let batch_commit = round.batch_commit;
@@ -174,8 +174,8 @@ pub fn verify_query<C: Config>(
     reduced_openings: [Ext<C::F, C::EF>; 32],
     log_max_height: usize,
 ) -> Ext<C::F, C::EF> {
-    let mut folded_eval: Ext<C::F, C::EF> = builder.eval(SymbolicExt::Const(C::EF::zero()));
-    let two_adic_generator = builder.eval(SymbolicExt::Const(C::EF::two_adic_generator(
+    let mut folded_eval: Ext<C::F, C::EF> = builder.eval(SymbolicExt::from_f(C::EF::zero()));
+    let two_adic_generator = builder.eval(SymbolicExt::from_f(C::EF::two_adic_generator(
         log_max_height,
     )));
     let index_bits = builder.num2bits_v_circuit(index, 256);
@@ -288,7 +288,7 @@ pub mod tests {
                     .iter()
                     .map(|commit_phase_opening| {
                         let sibling_value =
-                            builder.eval(SymbolicExt::Const(commit_phase_opening.sibling_value));
+                            builder.eval(SymbolicExt::from_f(commit_phase_opening.sibling_value));
                         let opening_proof = commit_phase_opening
                             .opening_proof
                             .iter()
@@ -313,7 +313,7 @@ pub mod tests {
         FriProofVariable {
             commit_phase_commits,
             query_proofs,
-            final_poly: builder.eval(SymbolicExt::Const(fri_proof.final_poly)),
+            final_poly: builder.eval(SymbolicExt::from_f(fri_proof.final_poly)),
             pow_witness: builder.eval(fri_proof.pow_witness),
         }
     }
@@ -372,14 +372,14 @@ pub mod tests {
         for (domain, poly) in os.into_iter() {
             let points: Vec<Ext<OuterVal, OuterChallenge>> = poly
                 .iter()
-                .map(|(p, _)| builder.eval(SymbolicExt::Const(*p)))
+                .map(|(p, _)| builder.eval(SymbolicExt::from_f(*p)))
                 .collect::<Vec<_>>();
             let values: Vec<Vec<Ext<OuterVal, OuterChallenge>>> = poly
                 .iter()
                 .map(|(_, v)| {
                     v.clone()
                         .iter()
-                        .map(|t| builder.eval(SymbolicExt::Const(*t)))
+                        .map(|t| builder.eval(SymbolicExt::from_f(*t)))
                         .collect::<Vec<_>>()
                 })
                 .collect::<Vec<_>>();
@@ -469,7 +469,7 @@ pub mod tests {
 
         for i in 0..fri_challenges_gt.betas.len() {
             builder.assert_ext_eq(
-                SymbolicExt::Const(fri_challenges_gt.betas[i]),
+                SymbolicExt::from_f(fri_challenges_gt.betas[i]),
                 fri_challenges.betas[i],
             );
         }
diff --git a/recursion/compiler/src/ir/builder.rs b/recursion/compiler/src/ir/builder.rs
index f3e555fe59..e608880e35 100644
--- a/recursion/compiler/src/ir/builder.rs
+++ b/recursion/compiler/src/ir/builder.rs
@@ -567,53 +567,59 @@ impl<'a, C: Config> IfBuilder<'a, C> {
 
     fn condition(&mut self) -> IfCondition<C::N> {
         match (self.lhs.clone(), self.rhs.clone(), self.is_eq) {
-            (SymbolicVar::Const(lhs), SymbolicVar::Const(rhs), true) => {
+            (SymbolicVar::Const(lhs, _), SymbolicVar::Const(rhs, _), true) => {
                 IfCondition::EqConst(lhs, rhs)
             }
-            (SymbolicVar::Const(lhs), SymbolicVar::Const(rhs), false) => {
+            (SymbolicVar::Const(lhs, _), SymbolicVar::Const(rhs, _), false) => {
                 IfCondition::NeConst(lhs, rhs)
             }
-            (SymbolicVar::Const(lhs), SymbolicVar::Val(rhs), true) => IfCondition::EqI(rhs, lhs),
-            (SymbolicVar::Const(lhs), SymbolicVar::Val(rhs), false) => IfCondition::NeI(rhs, lhs),
-            (SymbolicVar::Const(lhs), rhs, true) => {
+            (SymbolicVar::Const(lhs, _), SymbolicVar::Val(rhs, _), true) => {
+                IfCondition::EqI(rhs, lhs)
+            }
+            (SymbolicVar::Const(lhs, _), SymbolicVar::Val(rhs, _), false) => {
+                IfCondition::NeI(rhs, lhs)
+            }
+            (SymbolicVar::Const(lhs, _), rhs, true) => {
                 let rhs: Var<C::N> = self.builder.eval(rhs);
                 IfCondition::EqI(rhs, lhs)
             }
-            (SymbolicVar::Const(lhs), rhs, false) => {
+            (SymbolicVar::Const(lhs, _), rhs, false) => {
                 let rhs: Var<C::N> = self.builder.eval(rhs);
                 IfCondition::NeI(rhs, lhs)
             }
-            (SymbolicVar::Val(lhs), SymbolicVar::Const(rhs), true) => {
+            (SymbolicVar::Val(lhs, _), SymbolicVar::Const(rhs, _), true) => {
                 let lhs: Var<C::N> = self.builder.eval(lhs);
                 IfCondition::EqI(lhs, rhs)
             }
-            (SymbolicVar::Val(lhs), SymbolicVar::Const(rhs), false) => {
+            (SymbolicVar::Val(lhs, _), SymbolicVar::Const(rhs, _), false) => {
                 let lhs: Var<C::N> = self.builder.eval(lhs);
                 IfCondition::NeI(lhs, rhs)
             }
-            (lhs, SymbolicVar::Const(rhs), true) => {
+            (lhs, SymbolicVar::Const(rhs, _), true) => {
                 let lhs: Var<C::N> = self.builder.eval(lhs);
                 IfCondition::EqI(lhs, rhs)
             }
-            (lhs, SymbolicVar::Const(rhs), false) => {
+            (lhs, SymbolicVar::Const(rhs, _), false) => {
                 let lhs: Var<C::N> = self.builder.eval(lhs);
                 IfCondition::NeI(lhs, rhs)
             }
-            (SymbolicVar::Val(lhs), SymbolicVar::Val(rhs), true) => IfCondition::Eq(lhs, rhs),
-            (SymbolicVar::Val(lhs), SymbolicVar::Val(rhs), false) => IfCondition::Ne(lhs, rhs),
-            (SymbolicVar::Val(lhs), rhs, true) => {
+            (SymbolicVar::Val(lhs, _), SymbolicVar::Val(rhs, _), true) => IfCondition::Eq(lhs, rhs),
+            (SymbolicVar::Val(lhs, _), SymbolicVar::Val(rhs, _), false) => {
+                IfCondition::Ne(lhs, rhs)
+            }
+            (SymbolicVar::Val(lhs, _), rhs, true) => {
                 let rhs: Var<C::N> = self.builder.eval(rhs);
                 IfCondition::Eq(lhs, rhs)
             }
-            (SymbolicVar::Val(lhs), rhs, false) => {
+            (SymbolicVar::Val(lhs, _), rhs, false) => {
                 let rhs: Var<C::N> = self.builder.eval(rhs);
                 IfCondition::Ne(lhs, rhs)
             }
-            (lhs, SymbolicVar::Val(rhs), true) => {
+            (lhs, SymbolicVar::Val(rhs, _), true) => {
                 let lhs: Var<C::N> = self.builder.eval(lhs);
                 IfCondition::Eq(lhs, rhs)
             }
-            (lhs, SymbolicVar::Val(rhs), false) => {
+            (lhs, SymbolicVar::Val(rhs, _), false) => {
                 let lhs: Var<C::N> = self.builder.eval(lhs);
                 IfCondition::Ne(lhs, rhs)
             }
diff --git a/recursion/compiler/src/ir/ptr.rs b/recursion/compiler/src/ir/ptr.rs
index bf1dc9e22a..caa8012e1a 100644
--- a/recursion/compiler/src/ir/ptr.rs
+++ b/recursion/compiler/src/ir/ptr.rs
@@ -10,7 +10,7 @@ pub struct Ptr<N> {
     pub address: Var<N>,
 }
 
-pub struct SymbolicPtr<N> {
+pub struct SymbolicPtr<N: Field> {
     pub address: SymbolicVar<N>,
 }
 
@@ -77,15 +77,15 @@ impl<C: Config> MemVariable<C> for Ptr<C::N> {
     }
 }
 
-impl<N> From<Ptr<N>> for SymbolicPtr<N> {
+impl<N: Field> From<Ptr<N>> for SymbolicPtr<N> {
     fn from(ptr: Ptr<N>) -> Self {
         SymbolicPtr {
-            address: SymbolicVar::Val(ptr.address),
+            address: SymbolicVar::from(ptr.address),
         }
     }
 }
 
-impl<N> Add for Ptr<N> {
+impl<N: Field> Add for Ptr<N> {
     type Output = SymbolicPtr<N>;
 
     fn add(self, rhs: Self) -> Self::Output {
@@ -95,7 +95,7 @@ impl<N> Add for Ptr<N> {
     }
 }
 
-impl<N> Sub for Ptr<N> {
+impl<N: Field> Sub for Ptr<N> {
     type Output = SymbolicPtr<N>;
 
     fn sub(self, rhs: Self) -> Self::Output {
@@ -105,7 +105,7 @@ impl<N> Sub for Ptr<N> {
     }
 }
 
-impl<N> Add for SymbolicPtr<N> {
+impl<N: Field> Add for SymbolicPtr<N> {
     type Output = Self;
 
     fn add(self, rhs: Self) -> Self {
@@ -115,7 +115,7 @@ impl<N> Add for SymbolicPtr<N> {
     }
 }
 
-impl<N> Sub for SymbolicPtr<N> {
+impl<N: Field> Sub for SymbolicPtr<N> {
     type Output = Self;
 
     fn sub(self, rhs: Self) -> Self {
@@ -125,7 +125,7 @@ impl<N> Sub for SymbolicPtr<N> {
     }
 }
 
-impl<N> Add<Ptr<N>> for SymbolicPtr<N> {
+impl<N: Field> Add<Ptr<N>> for SymbolicPtr<N> {
     type Output = Self;
 
     fn add(self, rhs: Ptr<N>) -> Self {
@@ -135,7 +135,7 @@ impl<N> Add<Ptr<N>> for SymbolicPtr<N> {
     }
 }
 
-impl<N> Sub<Ptr<N>> for SymbolicPtr<N> {
+impl<N: Field> Sub<Ptr<N>> for SymbolicPtr<N> {
     type Output = Self;
 
     fn sub(self, rhs: Ptr<N>) -> Self {
@@ -145,7 +145,7 @@ impl<N> Sub<Ptr<N>> for SymbolicPtr<N> {
     }
 }
 
-impl<N> Add<SymbolicPtr<N>> for Ptr<N> {
+impl<N: Field> Add<SymbolicPtr<N>> for Ptr<N> {
     type Output = SymbolicPtr<N>;
 
     fn add(self, rhs: SymbolicPtr<N>) -> SymbolicPtr<N> {
@@ -155,7 +155,7 @@ impl<N> Add<SymbolicPtr<N>> for Ptr<N> {
     }
 }
 
-impl<N> Add<SymbolicVar<N>> for Ptr<N> {
+impl<N: Field> Add<SymbolicVar<N>> for Ptr<N> {
     type Output = SymbolicPtr<N>;
 
     fn add(self, rhs: SymbolicVar<N>) -> SymbolicPtr<N> {
@@ -165,7 +165,7 @@ impl<N> Add<SymbolicVar<N>> for Ptr<N> {
     }
 }
 
-impl<N> Sub<SymbolicVar<N>> for Ptr<N> {
+impl<N: Field> Sub<SymbolicVar<N>> for Ptr<N> {
     type Output = SymbolicPtr<N>;
 
     fn sub(self, rhs: SymbolicVar<N>) -> SymbolicPtr<N> {
@@ -175,7 +175,7 @@ impl<N> Sub<SymbolicVar<N>> for Ptr<N> {
     }
 }
 
-impl<N> Sub<SymbolicPtr<N>> for Ptr<N> {
+impl<N: Field> Sub<SymbolicPtr<N>> for Ptr<N> {
     type Output = SymbolicPtr<N>;
 
     fn sub(self, rhs: SymbolicPtr<N>) -> SymbolicPtr<N> {
diff --git a/recursion/compiler/src/ir/symbolic.rs b/recursion/compiler/src/ir/symbolic.rs
index cded3d2550..37beac2a8e 100644
--- a/recursion/compiler/src/ir/symbolic.rs
+++ b/recursion/compiler/src/ir/symbolic.rs
@@ -2,57 +2,188 @@ use alloc::rc::Rc;
 use core::any::Any;
 use core::ops::{Add, Div, Mul, Neg, Sub};
 use std::any::TypeId;
+use std::hash::Hash;
 use std::iter::{Product, Sum};
 use std::mem;
 use std::ops::{AddAssign, DivAssign, MulAssign, SubAssign};
 
-use p3_field::Field;
 use p3_field::{AbstractField, ExtensionField};
+use p3_field::{Field, FieldArray};
 
 use super::Usize;
 use super::{Ext, Felt, Var};
 
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum SymbolicVar<N> {
-    Const(N),
-    Val(Var<N>),
-    Add(Rc<SymbolicVar<N>>, Rc<SymbolicVar<N>>),
-    Mul(Rc<SymbolicVar<N>>, Rc<SymbolicVar<N>>),
-    Sub(Rc<SymbolicVar<N>>, Rc<SymbolicVar<N>>),
-    Neg(Rc<SymbolicVar<N>>),
-}
-
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum SymbolicFelt<F> {
-    Const(F),
-    Val(Felt<F>),
-    Add(Rc<SymbolicFelt<F>>, Rc<SymbolicFelt<F>>),
-    Mul(Rc<SymbolicFelt<F>>, Rc<SymbolicFelt<F>>),
-    Sub(Rc<SymbolicFelt<F>>, Rc<SymbolicFelt<F>>),
-    Div(Rc<SymbolicFelt<F>>, Rc<SymbolicFelt<F>>),
-    Neg(Rc<SymbolicFelt<F>>),
-}
-
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum SymbolicExt<F, EF> {
-    Const(EF),
-    Base(Rc<SymbolicFelt<F>>),
-    Val(Ext<F, EF>),
-    Add(Rc<SymbolicExt<F, EF>>, Rc<SymbolicExt<F, EF>>),
-    Mul(Rc<SymbolicExt<F, EF>>, Rc<SymbolicExt<F, EF>>),
-    Sub(Rc<SymbolicExt<F, EF>>, Rc<SymbolicExt<F, EF>>),
-    Div(Rc<SymbolicExt<F, EF>>, Rc<SymbolicExt<F, EF>>),
-    Neg(Rc<SymbolicExt<F, EF>>),
+const NUM_RANDOM_ELEMENTS: usize = 4;
+
+pub type Digest<T> = FieldArray<T, NUM_RANDOM_ELEMENTS>;
+
+pub fn elements<F: Field>() -> Digest<F> {
+    let powers = [1671541671, 1254988180, 442438744, 1716490559];
+    let generator = F::generator();
+
+    Digest::from(powers.map(|p| generator.exp_u64(p)))
+}
+
+pub fn ext_elements<F: Field, EF: ExtensionField<F>>() -> Digest<EF> {
+    let powers = [1021539871, 1430550064, 447478069, 1248903325];
+    let generator = EF::generator();
+
+    Digest::from(powers.map(|p| generator.exp_u64(p)))
+}
+
+fn digest_id<F: Field>(id: u32) -> Digest<F> {
+    let elements = elements();
+    Digest::from(elements.0.map(|e: F| {
+        (e + F::from_canonical_u32(id))
+            .try_inverse()
+            .unwrap_or(F::one())
+    }))
+}
+
+fn digest_id_ext<F: Field, EF: ExtensionField<F>>(id: u32) -> Digest<EF> {
+    let elements = ext_elements();
+    Digest::from(elements.0.map(|e: EF| {
+        (e + EF::from_canonical_u32(id))
+            .try_inverse()
+            .unwrap_or(EF::one())
+    }))
+}
+
+fn div_digests<F: Field>(a: Digest<F>, b: Digest<F>) -> Digest<F> {
+    Digest::from(core::array::from_fn(|i| a.0[i] / b.0[i]))
+}
+
+#[derive(Debug, Clone)]
+pub enum SymbolicVar<N: Field> {
+    Const(N, Digest<N>),
+    Val(Var<N>, Digest<N>),
+    Add(Rc<SymbolicVar<N>>, Rc<SymbolicVar<N>>, Digest<N>),
+    Mul(Rc<SymbolicVar<N>>, Rc<SymbolicVar<N>>, Digest<N>),
+    Sub(Rc<SymbolicVar<N>>, Rc<SymbolicVar<N>>, Digest<N>),
+    Neg(Rc<SymbolicVar<N>>, Digest<N>),
+}
+
+#[derive(Debug, Clone)]
+pub enum SymbolicFelt<F: Field> {
+    Const(F, Digest<F>),
+    Val(Felt<F>, Digest<F>),
+    Add(Rc<SymbolicFelt<F>>, Rc<SymbolicFelt<F>>, Digest<F>),
+    Mul(Rc<SymbolicFelt<F>>, Rc<SymbolicFelt<F>>, Digest<F>),
+    Sub(Rc<SymbolicFelt<F>>, Rc<SymbolicFelt<F>>, Digest<F>),
+    Div(Rc<SymbolicFelt<F>>, Rc<SymbolicFelt<F>>, Digest<F>),
+    Neg(Rc<SymbolicFelt<F>>, Digest<F>),
+}
+
+#[derive(Debug, Clone)]
+pub enum SymbolicExt<F: Field, EF: Field> {
+    Const(EF, Digest<EF>),
+    Base(Rc<SymbolicFelt<F>>, Digest<EF>),
+    Val(Ext<F, EF>, Digest<EF>),
+    Add(Rc<SymbolicExt<F, EF>>, Rc<SymbolicExt<F, EF>>, Digest<EF>),
+    Mul(Rc<SymbolicExt<F, EF>>, Rc<SymbolicExt<F, EF>>, Digest<EF>),
+    Sub(Rc<SymbolicExt<F, EF>>, Rc<SymbolicExt<F, EF>>, Digest<EF>),
+    Div(Rc<SymbolicExt<F, EF>>, Rc<SymbolicExt<F, EF>>, Digest<EF>),
+    Neg(Rc<SymbolicExt<F, EF>>, Digest<EF>),
+}
+
+impl<N: Field> Hash for SymbolicVar<N> {
+    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+        for elem in self.digest().0.iter() {
+            elem.hash(state);
+        }
+    }
+}
+
+impl<N: Field> PartialEq for SymbolicVar<N> {
+    fn eq(&self, other: &Self) -> bool {
+        self.digest() == other.digest()
+    }
+}
+
+impl<N: Field> Eq for SymbolicVar<N> {}
+
+impl<F: Field> Hash for SymbolicFelt<F> {
+    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+        for elem in self.digest().0.iter() {
+            elem.hash(state);
+        }
+    }
+}
+
+impl<F: Field> PartialEq for SymbolicFelt<F> {
+    fn eq(&self, other: &Self) -> bool {
+        self.digest() == other.digest()
+    }
+}
+
+impl<F: Field> Eq for SymbolicFelt<F> {}
+
+impl<F: Field, EF: Field> Hash for SymbolicExt<F, EF> {
+    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+        for elem in self.digest().0.iter() {
+            elem.hash(state);
+        }
+    }
+}
+
+impl<F: Field, EF: Field> PartialEq for SymbolicExt<F, EF> {
+    fn eq(&self, other: &Self) -> bool {
+        self.digest() == other.digest()
+    }
+}
+
+impl<F: Field, EF: Field> Eq for SymbolicExt<F, EF> {}
+
+impl<N: Field> SymbolicVar<N> {
+    pub(crate) fn digest(&self) -> Digest<N> {
+        match self {
+            SymbolicVar::Const(_, d) => *d,
+            SymbolicVar::Val(_, d) => *d,
+            SymbolicVar::Add(_, _, d) => *d,
+            SymbolicVar::Mul(_, _, d) => *d,
+            SymbolicVar::Sub(_, _, d) => *d,
+            SymbolicVar::Neg(_, d) => *d,
+        }
+    }
+}
+
+impl<F: Field> SymbolicFelt<F> {
+    pub(crate) fn digest(&self) -> Digest<F> {
+        match self {
+            SymbolicFelt::Const(_, d) => *d,
+            SymbolicFelt::Val(_, d) => *d,
+            SymbolicFelt::Add(_, _, d) => *d,
+            SymbolicFelt::Mul(_, _, d) => *d,
+            SymbolicFelt::Sub(_, _, d) => *d,
+            SymbolicFelt::Div(_, _, d) => *d,
+            SymbolicFelt::Neg(_, d) => *d,
+        }
+    }
 }
 
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum SymbolicUsize<N> {
+impl<F: Field, EF: Field> SymbolicExt<F, EF> {
+    pub(crate) fn digest(&self) -> Digest<EF> {
+        match self {
+            SymbolicExt::Const(_, d) => *d,
+            SymbolicExt::Base(_, d) => *d,
+            SymbolicExt::Val(_, d) => *d,
+            SymbolicExt::Add(_, _, d) => *d,
+            SymbolicExt::Mul(_, _, d) => *d,
+            SymbolicExt::Sub(_, _, d) => *d,
+            SymbolicExt::Div(_, _, d) => *d,
+            SymbolicExt::Neg(_, d) => *d,
+        }
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum SymbolicUsize<N: Field> {
     Const(usize),
     Var(SymbolicVar<N>),
 }
 
 #[derive(Debug, Clone)]
-pub enum ExtOperand<F, EF> {
+pub enum ExtOperand<F: Field, EF: ExtensionField<F>> {
     Base(F),
     Const(EF),
     Felt(Felt<F>),
@@ -61,17 +192,42 @@ pub enum ExtOperand<F, EF> {
     Sym(SymbolicExt<F, EF>),
 }
 
+impl<F: Field, EF: ExtensionField<F>> ExtOperand<F, EF> {
+    pub fn digest(&self) -> Digest<EF> {
+        match self {
+            ExtOperand::Base(f) => SymbolicFelt::from(*f).digest().0.map(EF::from_base).into(),
+            ExtOperand::Const(ef) => (*ef).into(),
+            ExtOperand::Felt(f) => SymbolicFelt::from(*f).digest().0.map(EF::from_base).into(),
+            ExtOperand::Ext(e) => digest_id_ext::<F, EF>(e.0),
+            ExtOperand::SymFelt(f) => f.digest().0.map(EF::from_base).into(),
+            ExtOperand::Sym(e) => e.digest(),
+        }
+    }
+
+    pub fn symbolic(self) -> SymbolicExt<F, EF> {
+        let digest = self.digest();
+        match self {
+            ExtOperand::Base(f) => SymbolicExt::Base(Rc::new(SymbolicFelt::from(f)), digest),
+            ExtOperand::Const(ef) => SymbolicExt::Const(ef, digest),
+            ExtOperand::Felt(f) => SymbolicExt::Base(Rc::new(SymbolicFelt::from(f)), digest),
+            ExtOperand::Ext(e) => SymbolicExt::Val(e, digest),
+            ExtOperand::SymFelt(f) => SymbolicExt::Base(Rc::new(f), digest),
+            ExtOperand::Sym(e) => e,
+        }
+    }
+}
+
 pub trait ExtConst<F: Field, EF: ExtensionField<F>> {
     fn cons(self) -> SymbolicExt<F, EF>;
 }
 
 impl<F: Field, EF: ExtensionField<F>> ExtConst<F, EF> for EF {
     fn cons(self) -> SymbolicExt<F, EF> {
-        SymbolicExt::Const(self)
+        SymbolicExt::Const(self, self.into())
     }
 }
 
-pub trait ExtensionOperand<F: Field, EF: ExtensionField<EF>> {
+pub trait ExtensionOperand<F: Field, EF: ExtensionField<F>> {
     fn to_operand(self) -> ExtOperand<F, EF>;
 }
 
@@ -79,53 +235,53 @@ impl<N: Field> AbstractField for SymbolicVar<N> {
     type F = N;
 
     fn zero() -> Self {
-        SymbolicVar::Const(N::zero())
+        SymbolicVar::from(N::zero())
     }
 
     fn one() -> Self {
-        SymbolicVar::Const(N::one())
+        SymbolicVar::from(N::one())
     }
 
     fn two() -> Self {
-        SymbolicVar::Const(N::two())
+        SymbolicVar::from(N::two())
     }
 
     fn neg_one() -> Self {
-        SymbolicVar::Const(N::neg_one())
+        SymbolicVar::from(N::neg_one())
     }
 
     fn from_f(f: Self::F) -> Self {
-        SymbolicVar::Const(f)
+        SymbolicVar::from(f)
     }
     fn from_bool(b: bool) -> Self {
-        SymbolicVar::Const(N::from_bool(b))
+        SymbolicVar::from(N::from_bool(b))
     }
     fn from_canonical_u8(n: u8) -> Self {
-        SymbolicVar::Const(N::from_canonical_u8(n))
+        SymbolicVar::from(N::from_canonical_u8(n))
     }
     fn from_canonical_u16(n: u16) -> Self {
-        SymbolicVar::Const(N::from_canonical_u16(n))
+        SymbolicVar::from(N::from_canonical_u16(n))
     }
     fn from_canonical_u32(n: u32) -> Self {
-        SymbolicVar::Const(N::from_canonical_u32(n))
+        SymbolicVar::from(N::from_canonical_u32(n))
     }
     fn from_canonical_u64(n: u64) -> Self {
-        SymbolicVar::Const(N::from_canonical_u64(n))
+        SymbolicVar::from(N::from_canonical_u64(n))
     }
     fn from_canonical_usize(n: usize) -> Self {
-        SymbolicVar::Const(N::from_canonical_usize(n))
+        SymbolicVar::from(N::from_canonical_usize(n))
     }
 
     fn from_wrapped_u32(n: u32) -> Self {
-        SymbolicVar::Const(N::from_wrapped_u32(n))
+        SymbolicVar::from(N::from_wrapped_u32(n))
     }
     fn from_wrapped_u64(n: u64) -> Self {
-        SymbolicVar::Const(N::from_wrapped_u64(n))
+        SymbolicVar::from(N::from_wrapped_u64(n))
     }
 
     /// A generator of this field's entire multiplicative group.
     fn generator() -> Self {
-        SymbolicVar::Const(N::generator())
+        SymbolicVar::from(N::generator())
     }
 }
 
@@ -133,53 +289,53 @@ impl<F: Field> AbstractField for SymbolicFelt<F> {
     type F = F;
 
     fn zero() -> Self {
-        SymbolicFelt::Const(F::zero())
+        SymbolicFelt::from(F::zero())
     }
 
     fn one() -> Self {
-        SymbolicFelt::Const(F::one())
+        SymbolicFelt::from(F::one())
     }
 
     fn two() -> Self {
-        SymbolicFelt::Const(F::two())
+        SymbolicFelt::from(F::two())
     }
 
     fn neg_one() -> Self {
-        SymbolicFelt::Const(F::neg_one())
+        SymbolicFelt::from(F::neg_one())
     }
 
     fn from_f(f: Self::F) -> Self {
-        SymbolicFelt::Const(f)
+        SymbolicFelt::from(f)
     }
     fn from_bool(b: bool) -> Self {
-        SymbolicFelt::Const(F::from_bool(b))
+        SymbolicFelt::from(F::from_bool(b))
     }
     fn from_canonical_u8(n: u8) -> Self {
-        SymbolicFelt::Const(F::from_canonical_u8(n))
+        SymbolicFelt::from(F::from_canonical_u8(n))
     }
     fn from_canonical_u16(n: u16) -> Self {
-        SymbolicFelt::Const(F::from_canonical_u16(n))
+        SymbolicFelt::from(F::from_canonical_u16(n))
     }
     fn from_canonical_u32(n: u32) -> Self {
-        SymbolicFelt::Const(F::from_canonical_u32(n))
+        SymbolicFelt::from(F::from_canonical_u32(n))
     }
     fn from_canonical_u64(n: u64) -> Self {
-        SymbolicFelt::Const(F::from_canonical_u64(n))
+        SymbolicFelt::from(F::from_canonical_u64(n))
     }
     fn from_canonical_usize(n: usize) -> Self {
-        SymbolicFelt::Const(F::from_canonical_usize(n))
+        SymbolicFelt::from(F::from_canonical_usize(n))
     }
 
     fn from_wrapped_u32(n: u32) -> Self {
-        SymbolicFelt::Const(F::from_wrapped_u32(n))
+        SymbolicFelt::from(F::from_wrapped_u32(n))
     }
     fn from_wrapped_u64(n: u64) -> Self {
-        SymbolicFelt::Const(F::from_wrapped_u64(n))
+        SymbolicFelt::from(F::from_wrapped_u64(n))
     }
 
     /// A generator of this field's entire multiplicative group.
     fn generator() -> Self {
-        SymbolicFelt::Const(F::generator())
+        SymbolicFelt::from(F::generator())
     }
 }
 
@@ -187,111 +343,113 @@ impl<F: Field, EF: ExtensionField<F>> AbstractField for SymbolicExt<F, EF> {
     type F = EF;
 
     fn zero() -> Self {
-        SymbolicExt::Const(EF::zero())
+        SymbolicExt::from_f(EF::zero())
     }
 
     fn one() -> Self {
-        SymbolicExt::Const(EF::one())
+        SymbolicExt::from_f(EF::one())
     }
 
     fn two() -> Self {
-        SymbolicExt::Const(EF::two())
+        SymbolicExt::from_f(EF::two())
     }
 
     fn neg_one() -> Self {
-        SymbolicExt::Const(EF::neg_one())
+        SymbolicExt::from_f(EF::neg_one())
     }
 
     fn from_f(f: Self::F) -> Self {
-        SymbolicExt::Const(f)
+        SymbolicExt::Const(f, f.into())
     }
     fn from_bool(b: bool) -> Self {
-        SymbolicExt::Const(EF::from_bool(b))
+        SymbolicExt::from_f(EF::from_bool(b))
     }
     fn from_canonical_u8(n: u8) -> Self {
-        SymbolicExt::Const(EF::from_canonical_u8(n))
+        SymbolicExt::from_f(EF::from_canonical_u8(n))
     }
     fn from_canonical_u16(n: u16) -> Self {
-        SymbolicExt::Const(EF::from_canonical_u16(n))
+        SymbolicExt::from_f(EF::from_canonical_u16(n))
     }
     fn from_canonical_u32(n: u32) -> Self {
-        SymbolicExt::Const(EF::from_canonical_u32(n))
+        SymbolicExt::from_f(EF::from_canonical_u32(n))
     }
     fn from_canonical_u64(n: u64) -> Self {
-        SymbolicExt::Const(EF::from_canonical_u64(n))
+        SymbolicExt::from_f(EF::from_canonical_u64(n))
     }
     fn from_canonical_usize(n: usize) -> Self {
-        SymbolicExt::Const(EF::from_canonical_usize(n))
+        SymbolicExt::from_f(EF::from_canonical_usize(n))
     }
 
     fn from_wrapped_u32(n: u32) -> Self {
-        SymbolicExt::Const(EF::from_wrapped_u32(n))
+        SymbolicExt::from_f(EF::from_wrapped_u32(n))
     }
     fn from_wrapped_u64(n: u64) -> Self {
-        SymbolicExt::Const(EF::from_wrapped_u64(n))
+        SymbolicExt::from_f(EF::from_wrapped_u64(n))
     }
 
     /// A generator of this field's entire multiplicative group.
     fn generator() -> Self {
-        SymbolicExt::Const(EF::generator())
+        SymbolicExt::from_f(EF::generator())
     }
 }
 
 // Implement all conversions from constants N, F, EF, to the corresponding symbolic types
 
-impl<N> From<N> for SymbolicVar<N> {
+impl<N: Field> From<N> for SymbolicVar<N> {
     fn from(n: N) -> Self {
-        SymbolicVar::Const(n)
+        SymbolicVar::Const(n, n.into())
     }
 }
 
-impl<F> From<F> for SymbolicFelt<F> {
+impl<F: Field> From<F> for SymbolicFelt<F> {
     fn from(f: F) -> Self {
-        SymbolicFelt::Const(f)
+        SymbolicFelt::Const(f, f.into())
     }
 }
 
 impl<F: Field, EF: ExtensionField<F>> From<F> for SymbolicExt<F, EF> {
     fn from(f: F) -> Self {
-        SymbolicExt::Base(Rc::new(SymbolicFelt::Const(f)))
+        f.to_operand().symbolic()
     }
 }
 
 // Implement all conversions from Var<N>, Felt<F>, Ext<F, EF> to the corresponding symbolic types
 
-impl<N> From<Var<N>> for SymbolicVar<N> {
+impl<N: Field> From<Var<N>> for SymbolicVar<N> {
     fn from(v: Var<N>) -> Self {
-        SymbolicVar::Val(v)
+        SymbolicVar::Val(v, digest_id(v.0))
     }
 }
 
-impl<F> From<Felt<F>> for SymbolicFelt<F> {
+impl<F: Field> From<Felt<F>> for SymbolicFelt<F> {
     fn from(f: Felt<F>) -> Self {
-        SymbolicFelt::Val(f)
+        SymbolicFelt::Val(f, digest_id(f.0))
     }
 }
 
 impl<F: Field, EF: ExtensionField<F>> From<Ext<F, EF>> for SymbolicExt<F, EF> {
     fn from(e: Ext<F, EF>) -> Self {
-        SymbolicExt::Val(e)
+        e.to_operand().symbolic()
     }
 }
 
 // Implement all operations for SymbolicVar<N>, SymbolicFelt<F>, SymbolicExt<F, EF>
 
-impl<N> Add for SymbolicVar<N> {
+impl<N: Field> Add for SymbolicVar<N> {
     type Output = Self;
 
     fn add(self, rhs: Self) -> Self::Output {
-        SymbolicVar::Add(Rc::new(self), Rc::new(rhs))
+        let digest = self.digest() + rhs.digest();
+        SymbolicVar::Add(Rc::new(self), Rc::new(rhs), digest)
     }
 }
 
-impl<F> Add for SymbolicFelt<F> {
+impl<F: Field> Add for SymbolicFelt<F> {
     type Output = Self;
 
     fn add(self, rhs: Self) -> Self::Output {
-        SymbolicFelt::Add(Rc::new(self), Rc::new(rhs))
+        let digest = self.digest() + rhs.digest();
+        SymbolicFelt::Add(Rc::new(self), Rc::new(rhs), digest)
     }
 }
 
@@ -299,41 +457,27 @@ impl<F: Field, EF: ExtensionField<F>, E: ExtensionOperand<F, EF>> Add<E> for Sym
     type Output = Self;
 
     fn add(self, rhs: E) -> Self::Output {
-        let rhs = rhs.to_operand();
-        match rhs {
-            ExtOperand::Base(f) => SymbolicExt::Add(
-                Rc::new(self),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Const(f)))),
-            ),
-            ExtOperand::Const(ef) => {
-                SymbolicExt::Add(Rc::new(self), Rc::new(SymbolicExt::Const(ef)))
-            }
-            ExtOperand::Felt(f) => SymbolicExt::Add(
-                Rc::new(self),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Val(f)))),
-            ),
-            ExtOperand::Ext(e) => SymbolicExt::Add(Rc::new(self), Rc::new(SymbolicExt::Val(e))),
-            ExtOperand::SymFelt(f) => {
-                SymbolicExt::Add(Rc::new(self), Rc::new(SymbolicExt::Base(Rc::new(f))))
-            }
-            ExtOperand::Sym(e) => SymbolicExt::Add(Rc::new(self), Rc::new(e)),
-        }
+        let rhs = rhs.to_operand().symbolic();
+        let digest = self.digest() + rhs.digest();
+        SymbolicExt::Add(Rc::new(self), Rc::new(rhs), digest)
     }
 }
 
-impl<N> Mul for SymbolicVar<N> {
+impl<N: Field> Mul for SymbolicVar<N> {
     type Output = Self;
 
     fn mul(self, rhs: Self) -> Self::Output {
-        SymbolicVar::Mul(Rc::new(self), Rc::new(rhs))
+        let digest = self.digest() * rhs.digest();
+        SymbolicVar::Mul(Rc::new(self), Rc::new(rhs), digest)
     }
 }
 
-impl<F> Mul for SymbolicFelt<F> {
+impl<F: Field> Mul for SymbolicFelt<F> {
     type Output = Self;
 
     fn mul(self, rhs: Self) -> Self::Output {
-        SymbolicFelt::Mul(Rc::new(self), Rc::new(rhs))
+        let digest = self.digest() * rhs.digest();
+        SymbolicFelt::Mul(Rc::new(self), Rc::new(rhs), digest)
     }
 }
 
@@ -342,40 +486,60 @@ impl<F: Field, EF: ExtensionField<F>, E: Any> Mul<E> for SymbolicExt<F, EF> {
 
     fn mul(self, rhs: E) -> Self::Output {
         let rhs = rhs.to_operand();
+        let rhs_digest = rhs.digest();
+        let prod_digest = self.digest() * rhs_digest;
         match rhs {
             ExtOperand::Base(f) => SymbolicExt::Mul(
                 Rc::new(self),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Const(f)))),
+                Rc::new(SymbolicExt::Base(
+                    Rc::new(SymbolicFelt::from(f)),
+                    rhs_digest,
+                )),
+                prod_digest,
+            ),
+            ExtOperand::Const(ef) => SymbolicExt::Mul(
+                Rc::new(self),
+                Rc::new(SymbolicExt::Const(ef, rhs_digest)),
+                prod_digest,
             ),
-            ExtOperand::Const(ef) => {
-                SymbolicExt::Mul(Rc::new(self), Rc::new(SymbolicExt::Const(ef)))
-            }
             ExtOperand::Felt(f) => SymbolicExt::Mul(
                 Rc::new(self),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Val(f)))),
+                Rc::new(SymbolicExt::Base(
+                    Rc::new(SymbolicFelt::from(f)),
+                    rhs_digest,
+                )),
+                prod_digest,
             ),
-            ExtOperand::Ext(e) => SymbolicExt::Mul(Rc::new(self), Rc::new(SymbolicExt::Val(e))),
-            ExtOperand::SymFelt(f) => {
-                SymbolicExt::Mul(Rc::new(self), Rc::new(SymbolicExt::Base(Rc::new(f))))
-            }
-            ExtOperand::Sym(e) => SymbolicExt::Mul(Rc::new(self), Rc::new(e)),
+            ExtOperand::Ext(e) => SymbolicExt::Mul(
+                Rc::new(self),
+                Rc::new(SymbolicExt::Val(e, rhs_digest)),
+                prod_digest,
+            ),
+            ExtOperand::SymFelt(f) => SymbolicExt::Mul(
+                Rc::new(self),
+                Rc::new(SymbolicExt::Base(Rc::new(f), rhs_digest)),
+                prod_digest,
+            ),
+            ExtOperand::Sym(e) => SymbolicExt::Mul(Rc::new(self), Rc::new(e), prod_digest),
         }
     }
 }
 
-impl<N> Sub for SymbolicVar<N> {
+impl<N: Field> Sub for SymbolicVar<N> {
     type Output = Self;
 
     fn sub(self, rhs: Self) -> Self::Output {
-        SymbolicVar::Sub(Rc::new(self), Rc::new(rhs))
+        let digest = self.digest() - rhs.digest();
+        SymbolicVar::Sub(Rc::new(self), Rc::new(rhs), digest)
     }
 }
 
-impl<F> Sub for SymbolicFelt<F> {
+impl<F: Field> Sub for SymbolicFelt<F> {
     type Output = Self;
 
     fn sub(self, rhs: Self) -> Self::Output {
-        SymbolicFelt::Sub(Rc::new(self), Rc::new(rhs))
+        let digest = self.digest() - rhs.digest();
+        SymbolicFelt::Sub(Rc::new(self), Rc::new(rhs), digest)
     }
 }
 
@@ -384,32 +548,53 @@ impl<F: Field, EF: ExtensionField<F>, E: Any> Sub<E> for SymbolicExt<F, EF> {
 
     fn sub(self, rhs: E) -> Self::Output {
         let rhs = rhs.to_operand();
+        let rhs_digest = rhs.digest();
+        let digest = self.digest() - rhs_digest;
         match rhs {
             ExtOperand::Base(f) => SymbolicExt::Sub(
                 Rc::new(self),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Const(f)))),
+                Rc::new(SymbolicExt::Base(
+                    Rc::new(SymbolicFelt::from(f)),
+                    rhs_digest,
+                )),
+                digest,
+            ),
+            ExtOperand::Const(ef) => SymbolicExt::Sub(
+                Rc::new(self),
+                Rc::new(SymbolicExt::Const(ef, rhs_digest)),
+                digest,
             ),
-            ExtOperand::Const(ef) => {
-                SymbolicExt::Sub(Rc::new(self), Rc::new(SymbolicExt::Const(ef)))
-            }
             ExtOperand::Felt(f) => SymbolicExt::Sub(
                 Rc::new(self),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Val(f)))),
+                Rc::new(SymbolicExt::Base(
+                    Rc::new(SymbolicFelt::from(f)),
+                    rhs_digest,
+                )),
+                digest,
             ),
-            ExtOperand::Ext(e) => SymbolicExt::Sub(Rc::new(self), Rc::new(SymbolicExt::Val(e))),
-            ExtOperand::SymFelt(f) => {
-                SymbolicExt::Sub(Rc::new(self), Rc::new(SymbolicExt::Base(Rc::new(f))))
-            }
-            ExtOperand::Sym(e) => SymbolicExt::Sub(Rc::new(self), Rc::new(e)),
+            ExtOperand::Ext(e) => SymbolicExt::Sub(
+                Rc::new(self),
+                Rc::new(SymbolicExt::Val(e, rhs_digest)),
+                digest,
+            ),
+            ExtOperand::SymFelt(f) => SymbolicExt::Sub(
+                Rc::new(self),
+                Rc::new(SymbolicExt::Base(Rc::new(f), rhs_digest)),
+                digest,
+            ),
+            ExtOperand::Sym(e) => SymbolicExt::Sub(Rc::new(self), Rc::new(e), digest),
         }
     }
 }
 
-impl<F> Div for SymbolicFelt<F> {
+impl<F: Field> Div for SymbolicFelt<F> {
     type Output = Self;
 
     fn div(self, rhs: Self) -> Self::Output {
-        SymbolicFelt::Div(Rc::new(self), Rc::new(rhs))
+        let self_digest = self.digest();
+        let rhs_digest = rhs.digest();
+        let digest = div_digests(self_digest, rhs_digest);
+        SymbolicFelt::Div(Rc::new(self), Rc::new(rhs), digest)
     }
 }
 
@@ -418,40 +603,60 @@ impl<F: Field, EF: ExtensionField<F>, E: Any> Div<E> for SymbolicExt<F, EF> {
 
     fn div(self, rhs: E) -> Self::Output {
         let rhs = rhs.to_operand();
+        let rhs_digest = rhs.digest();
+        let digest = div_digests(self.digest(), rhs_digest);
         match rhs {
             ExtOperand::Base(f) => SymbolicExt::Div(
                 Rc::new(self),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Const(f)))),
+                Rc::new(SymbolicExt::Base(
+                    Rc::new(SymbolicFelt::from(f)),
+                    rhs_digest,
+                )),
+                digest,
+            ),
+            ExtOperand::Const(ef) => SymbolicExt::Div(
+                Rc::new(self),
+                Rc::new(SymbolicExt::Const(ef, rhs_digest)),
+                digest,
             ),
-            ExtOperand::Const(ef) => {
-                SymbolicExt::Div(Rc::new(self), Rc::new(SymbolicExt::Const(ef)))
-            }
             ExtOperand::Felt(f) => SymbolicExt::Div(
                 Rc::new(self),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Val(f)))),
+                Rc::new(SymbolicExt::Base(
+                    Rc::new(SymbolicFelt::from(f)),
+                    rhs_digest,
+                )),
+                digest,
             ),
-            ExtOperand::Ext(e) => SymbolicExt::Div(Rc::new(self), Rc::new(SymbolicExt::Val(e))),
-            ExtOperand::SymFelt(f) => {
-                SymbolicExt::Div(Rc::new(self), Rc::new(SymbolicExt::Base(Rc::new(f))))
-            }
-            ExtOperand::Sym(e) => SymbolicExt::Div(Rc::new(self), Rc::new(e)),
+            ExtOperand::Ext(e) => SymbolicExt::Div(
+                Rc::new(self),
+                Rc::new(SymbolicExt::Val(e, rhs_digest)),
+                digest,
+            ),
+            ExtOperand::SymFelt(f) => SymbolicExt::Div(
+                Rc::new(self),
+                Rc::new(SymbolicExt::Base(Rc::new(f), rhs_digest)),
+                digest,
+            ),
+            ExtOperand::Sym(e) => SymbolicExt::Div(Rc::new(self), Rc::new(e), digest),
         }
     }
 }
 
-impl<N> Neg for SymbolicVar<N> {
+impl<N: Field> Neg for SymbolicVar<N> {
     type Output = Self;
 
     fn neg(self) -> Self::Output {
-        SymbolicVar::Neg(Rc::new(self))
+        let digest = -self.digest();
+        SymbolicVar::Neg(Rc::new(self), digest)
     }
 }
 
-impl<F> Neg for SymbolicFelt<F> {
+impl<F: Field> Neg for SymbolicFelt<F> {
     type Output = Self;
 
     fn neg(self) -> Self::Output {
-        SymbolicFelt::Neg(Rc::new(self))
+        let digest = -self.digest();
+        SymbolicFelt::Neg(Rc::new(self), digest)
     }
 }
 
@@ -459,64 +664,66 @@ impl<F: Field, EF: ExtensionField<F>> Neg for SymbolicExt<F, EF> {
     type Output = Self;
 
     fn neg(self) -> Self::Output {
-        SymbolicExt::Neg(Rc::new(self))
+        let digest = -self.digest();
+        SymbolicExt::Neg(Rc::new(self), digest)
     }
 }
 
 // Implement all operations between N, F, EF, and SymbolicVar<N>, SymbolicFelt<F>, SymbolicExt<F, EF>
 
-impl<N> Add<N> for SymbolicVar<N> {
+impl<N: Field> Add<N> for SymbolicVar<N> {
     type Output = Self;
 
     fn add(self, rhs: N) -> Self::Output {
-        SymbolicVar::Add(Rc::new(self), Rc::new(SymbolicVar::Const(rhs)))
+        self + SymbolicVar::from(rhs)
     }
 }
 
-impl<F> Add<F> for SymbolicFelt<F> {
+impl<F: Field> Add<F> for SymbolicFelt<F> {
     type Output = Self;
 
     fn add(self, rhs: F) -> Self::Output {
-        SymbolicFelt::Add(Rc::new(self), Rc::new(SymbolicFelt::Const(rhs)))
+        self + SymbolicFelt::from(rhs)
     }
 }
 
-impl<N> Mul<N> for SymbolicVar<N> {
+impl<N: Field> Mul<N> for SymbolicVar<N> {
     type Output = Self;
 
     fn mul(self, rhs: N) -> Self::Output {
-        SymbolicVar::Mul(Rc::new(self), Rc::new(SymbolicVar::Const(rhs)))
+        self * SymbolicVar::from(rhs)
     }
 }
 
-impl<F> Mul<F> for SymbolicFelt<F> {
+impl<F: Field> Mul<F> for SymbolicFelt<F> {
     type Output = Self;
 
     fn mul(self, rhs: F) -> Self::Output {
-        SymbolicFelt::Mul(Rc::new(self), Rc::new(SymbolicFelt::Const(rhs)))
+        self * SymbolicFelt::from(rhs)
     }
 }
 
-impl<N> Sub<N> for SymbolicVar<N> {
+impl<N: Field> Sub<N> for SymbolicVar<N> {
     type Output = Self;
 
     fn sub(self, rhs: N) -> Self::Output {
-        SymbolicVar::Sub(Rc::new(self), Rc::new(SymbolicVar::Const(rhs)))
+        let digest = self.digest() - rhs;
+        SymbolicVar::Sub(Rc::new(self), Rc::new(SymbolicVar::from_f(rhs)), digest)
     }
 }
 
-impl<F> Sub<F> for SymbolicFelt<F> {
+impl<F: Field> Sub<F> for SymbolicFelt<F> {
     type Output = Self;
 
     fn sub(self, rhs: F) -> Self::Output {
-        SymbolicFelt::Sub(Rc::new(self), Rc::new(SymbolicFelt::Const(rhs)))
+        self - SymbolicFelt::from(rhs)
     }
 }
 
 // Implement all operations between SymbolicVar<N>, SymbolicFelt<F>, SymbolicExt<F, EF>, and Var<N>,
 //  Felt<F>, Ext<F, EF>.
 
-impl<N> Add<Var<N>> for SymbolicVar<N> {
+impl<N: Field> Add<Var<N>> for SymbolicVar<N> {
     type Output = SymbolicVar<N>;
 
     fn add(self, rhs: Var<N>) -> Self::Output {
@@ -524,7 +731,7 @@ impl<N> Add<Var<N>> for SymbolicVar<N> {
     }
 }
 
-impl<F> Add<Felt<F>> for SymbolicFelt<F> {
+impl<F: Field> Add<Felt<F>> for SymbolicFelt<F> {
     type Output = SymbolicFelt<F>;
 
     fn add(self, rhs: Felt<F>) -> Self::Output {
@@ -532,7 +739,7 @@ impl<F> Add<Felt<F>> for SymbolicFelt<F> {
     }
 }
 
-impl<N> Mul<Var<N>> for SymbolicVar<N> {
+impl<N: Field> Mul<Var<N>> for SymbolicVar<N> {
     type Output = SymbolicVar<N>;
 
     fn mul(self, rhs: Var<N>) -> Self::Output {
@@ -540,7 +747,7 @@ impl<N> Mul<Var<N>> for SymbolicVar<N> {
     }
 }
 
-impl<F> Mul<Felt<F>> for SymbolicFelt<F> {
+impl<F: Field> Mul<Felt<F>> for SymbolicFelt<F> {
     type Output = SymbolicFelt<F>;
 
     fn mul(self, rhs: Felt<F>) -> Self::Output {
@@ -548,7 +755,7 @@ impl<F> Mul<Felt<F>> for SymbolicFelt<F> {
     }
 }
 
-impl<N> Sub<Var<N>> for SymbolicVar<N> {
+impl<N: Field> Sub<Var<N>> for SymbolicVar<N> {
     type Output = SymbolicVar<N>;
 
     fn sub(self, rhs: Var<N>) -> Self::Output {
@@ -556,7 +763,7 @@ impl<N> Sub<Var<N>> for SymbolicVar<N> {
     }
 }
 
-impl<F> Sub<Felt<F>> for SymbolicFelt<F> {
+impl<F: Field> Sub<Felt<F>> for SymbolicFelt<F> {
     type Output = SymbolicFelt<F>;
 
     fn sub(self, rhs: Felt<F>) -> Self::Output {
@@ -564,7 +771,7 @@ impl<F> Sub<Felt<F>> for SymbolicFelt<F> {
     }
 }
 
-impl<F> Div<SymbolicFelt<F>> for Felt<F> {
+impl<F: Field> Div<SymbolicFelt<F>> for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn div(self, rhs: SymbolicFelt<F>) -> Self::Output {
@@ -574,7 +781,7 @@ impl<F> Div<SymbolicFelt<F>> for Felt<F> {
 
 // Implement operations between constants N, F, EF, and Var<N>, Felt<F>, Ext<F, EF>.
 
-impl<N> Add for Var<N> {
+impl<N: Field> Add for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn add(self, rhs: Self) -> Self::Output {
@@ -582,7 +789,7 @@ impl<N> Add for Var<N> {
     }
 }
 
-impl<N> Add<N> for Var<N> {
+impl<N: Field> Add<N> for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn add(self, rhs: N) -> Self::Output {
@@ -590,7 +797,7 @@ impl<N> Add<N> for Var<N> {
     }
 }
 
-impl<F> Add for Felt<F> {
+impl<F: Field> Add for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn add(self, rhs: Self) -> Self::Output {
@@ -598,7 +805,7 @@ impl<F> Add for Felt<F> {
     }
 }
 
-impl<F> Add<F> for Felt<F> {
+impl<F: Field> Add<F> for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn add(self, rhs: F) -> Self::Output {
@@ -606,7 +813,7 @@ impl<F> Add<F> for Felt<F> {
     }
 }
 
-impl<N> Mul for Var<N> {
+impl<N: Field> Mul for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn mul(self, rhs: Self) -> Self::Output {
@@ -614,7 +821,7 @@ impl<N> Mul for Var<N> {
     }
 }
 
-impl<N> Mul<N> for Var<N> {
+impl<N: Field> Mul<N> for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn mul(self, rhs: N) -> Self::Output {
@@ -622,7 +829,7 @@ impl<N> Mul<N> for Var<N> {
     }
 }
 
-impl<F> Mul for Felt<F> {
+impl<F: Field> Mul for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn mul(self, rhs: Self) -> Self::Output {
@@ -630,7 +837,7 @@ impl<F> Mul for Felt<F> {
     }
 }
 
-impl<F> Mul<F> for Felt<F> {
+impl<F: Field> Mul<F> for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn mul(self, rhs: F) -> Self::Output {
@@ -638,7 +845,7 @@ impl<F> Mul<F> for Felt<F> {
     }
 }
 
-impl<N> Sub for Var<N> {
+impl<N: Field> Sub for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn sub(self, rhs: Self) -> Self::Output {
@@ -646,7 +853,7 @@ impl<N> Sub for Var<N> {
     }
 }
 
-impl<N> Sub<N> for Var<N> {
+impl<N: Field> Sub<N> for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn sub(self, rhs: N) -> Self::Output {
@@ -654,7 +861,7 @@ impl<N> Sub<N> for Var<N> {
     }
 }
 
-impl<F> Sub for Felt<F> {
+impl<F: Field> Sub for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn sub(self, rhs: Self) -> Self::Output {
@@ -662,7 +869,7 @@ impl<F> Sub for Felt<F> {
     }
 }
 
-impl<F> Sub<F> for Felt<F> {
+impl<F: Field> Sub<F> for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn sub(self, rhs: F) -> Self::Output {
@@ -675,14 +882,8 @@ impl<F: Field, EF: ExtensionField<F>, E: Any> Add<E> for Ext<F, EF> {
 
     fn add(self, rhs: E) -> Self::Output {
         let rhs: ExtOperand<F, EF> = rhs.to_operand();
-        match rhs {
-            ExtOperand::Base(f) => SymbolicExt::Base(Rc::new(SymbolicFelt::Const(f))) + self,
-            ExtOperand::Const(ef) => SymbolicExt::Const(ef) + self,
-            ExtOperand::Felt(f) => SymbolicExt::Base(Rc::new(SymbolicFelt::Val(f))) + self,
-            ExtOperand::Ext(e) => SymbolicExt::Val(e) + self,
-            ExtOperand::SymFelt(f) => SymbolicExt::Base(Rc::new(f)) + self,
-            ExtOperand::Sym(e) => e + self,
-        }
+        let self_sym = self.to_operand().symbolic();
+        self_sym + rhs
     }
 }
 
@@ -690,15 +891,8 @@ impl<F: Field, EF: ExtensionField<F>, E: Any> Mul<E> for Ext<F, EF> {
     type Output = SymbolicExt<F, EF>;
 
     fn mul(self, rhs: E) -> Self::Output {
-        let rhs: ExtOperand<F, EF> = rhs.to_operand();
-        match rhs {
-            ExtOperand::Base(f) => SymbolicExt::Base(Rc::new(SymbolicFelt::Const(f))) * self,
-            ExtOperand::Const(ef) => SymbolicExt::Const(ef) * self,
-            ExtOperand::Felt(f) => SymbolicExt::Base(Rc::new(SymbolicFelt::Val(f))) * self,
-            ExtOperand::Ext(e) => SymbolicExt::Val(e) * self,
-            ExtOperand::SymFelt(f) => SymbolicExt::Base(Rc::new(f)) * self,
-            ExtOperand::Sym(e) => e * self,
-        }
+        let self_sym = self.to_operand().symbolic();
+        self_sym * rhs
     }
 }
 
@@ -706,30 +900,8 @@ impl<F: Field, EF: ExtensionField<F>, E: Any> Sub<E> for Ext<F, EF> {
     type Output = SymbolicExt<F, EF>;
 
     fn sub(self, rhs: E) -> Self::Output {
-        let rhs: ExtOperand<F, EF> = rhs.to_operand();
-        match rhs {
-            ExtOperand::Base(f) => SymbolicExt::Sub(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Const(f)))),
-            ),
-            ExtOperand::Const(ef) => SymbolicExt::Sub(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Const(ef)),
-            ),
-            ExtOperand::Felt(f) => SymbolicExt::Sub(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Val(f)))),
-            ),
-            ExtOperand::Ext(e) => SymbolicExt::Sub(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Val(e)),
-            ),
-            ExtOperand::SymFelt(f) => SymbolicExt::Sub(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Base(Rc::new(f))),
-            ),
-            ExtOperand::Sym(e) => SymbolicExt::Sub(Rc::new(SymbolicExt::Val(self)), Rc::new(e)),
-        }
+        let self_sym = self.to_operand().symbolic();
+        self_sym - rhs
     }
 }
 
@@ -737,30 +909,8 @@ impl<F: Field, EF: ExtensionField<F>, E: Any> Div<E> for Ext<F, EF> {
     type Output = SymbolicExt<F, EF>;
 
     fn div(self, rhs: E) -> Self::Output {
-        let rhs: ExtOperand<F, EF> = rhs.to_operand();
-        match rhs {
-            ExtOperand::Base(f) => SymbolicExt::Div(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Const(f)))),
-            ),
-            ExtOperand::Const(ef) => SymbolicExt::Div(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Const(ef)),
-            ),
-            ExtOperand::Felt(f) => SymbolicExt::Div(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Base(Rc::new(SymbolicFelt::Val(f)))),
-            ),
-            ExtOperand::Ext(e) => SymbolicExt::Div(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Val(e)),
-            ),
-            ExtOperand::SymFelt(f) => SymbolicExt::Div(
-                Rc::new(SymbolicExt::Val(self)),
-                Rc::new(SymbolicExt::Base(Rc::new(f))),
-            ),
-            ExtOperand::Sym(e) => SymbolicExt::Div(Rc::new(SymbolicExt::Val(self)), Rc::new(e)),
-        }
+        let self_sym = self.to_operand().symbolic();
+        self_sym / rhs
     }
 }
 
@@ -768,7 +918,8 @@ impl<F: Field, EF: ExtensionField<F>> Add<SymbolicExt<F, EF>> for Felt<F> {
     type Output = SymbolicExt<F, EF>;
 
     fn add(self, rhs: SymbolicExt<F, EF>) -> Self::Output {
-        SymbolicExt::<F, EF>::Base(Rc::new(SymbolicFelt::Val(self))) + rhs
+        let self_sym = self.to_operand().symbolic();
+        self_sym + rhs
     }
 }
 
@@ -776,7 +927,8 @@ impl<F: Field, EF: ExtensionField<F>> Mul<SymbolicExt<F, EF>> for Felt<F> {
     type Output = SymbolicExt<F, EF>;
 
     fn mul(self, rhs: SymbolicExt<F, EF>) -> Self::Output {
-        SymbolicExt::<F, EF>::Base(Rc::new(SymbolicFelt::Val(self))) * rhs
+        let self_sym = self.to_operand().symbolic();
+        self_sym * rhs
     }
 }
 
@@ -784,7 +936,8 @@ impl<F: Field, EF: ExtensionField<F>> Sub<SymbolicExt<F, EF>> for Felt<F> {
     type Output = SymbolicExt<F, EF>;
 
     fn sub(self, rhs: SymbolicExt<F, EF>) -> Self::Output {
-        SymbolicExt::<F, EF>::Base(Rc::new(SymbolicFelt::Val(self))) - rhs
+        let self_sym = self.to_operand().symbolic();
+        self_sym - rhs
     }
 }
 
@@ -792,11 +945,12 @@ impl<F: Field, EF: ExtensionField<F>> Div<SymbolicExt<F, EF>> for Felt<F> {
     type Output = SymbolicExt<F, EF>;
 
     fn div(self, rhs: SymbolicExt<F, EF>) -> Self::Output {
-        SymbolicExt::<F, EF>::Base(Rc::new(SymbolicFelt::Val(self))) / rhs
+        let self_sym = self.to_operand().symbolic();
+        self_sym / rhs
     }
 }
 
-impl<F> Div for Felt<F> {
+impl<F: Field> Div for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn div(self, rhs: Self) -> Self::Output {
@@ -804,7 +958,7 @@ impl<F> Div for Felt<F> {
     }
 }
 
-impl<F> Div<F> for Felt<F> {
+impl<F: Field> Div<F> for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn div(self, rhs: F) -> Self::Output {
@@ -812,23 +966,23 @@ impl<F> Div<F> for Felt<F> {
     }
 }
 
-impl<F> Div<Felt<F>> for SymbolicFelt<F> {
+impl<F: Field> Div<Felt<F>> for SymbolicFelt<F> {
     type Output = SymbolicFelt<F>;
 
     fn div(self, rhs: Felt<F>) -> Self::Output {
-        SymbolicFelt::Div(Rc::new(self), Rc::new(SymbolicFelt::Val(rhs)))
+        self / SymbolicFelt::from(rhs)
     }
 }
 
-impl<F> Div<F> for SymbolicFelt<F> {
+impl<F: Field> Div<F> for SymbolicFelt<F> {
     type Output = SymbolicFelt<F>;
 
     fn div(self, rhs: F) -> Self::Output {
-        SymbolicFelt::Div(Rc::new(self), Rc::new(SymbolicFelt::Const(rhs)))
+        self / SymbolicFelt::from(rhs)
     }
 }
 
-impl<N> Sub<SymbolicVar<N>> for Var<N> {
+impl<N: Field> Sub<SymbolicVar<N>> for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn sub(self, rhs: SymbolicVar<N>) -> Self::Output {
@@ -836,7 +990,7 @@ impl<N> Sub<SymbolicVar<N>> for Var<N> {
     }
 }
 
-impl<N> Add<SymbolicVar<N>> for Var<N> {
+impl<N: Field> Add<SymbolicVar<N>> for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn add(self, rhs: SymbolicVar<N>) -> Self::Output {
@@ -849,8 +1003,8 @@ impl<N: Field> Mul<usize> for Usize<N> {
 
     fn mul(self, rhs: usize) -> Self::Output {
         match self {
-            Usize::Const(n) => SymbolicVar::Const(N::from_canonical_usize(n * rhs)),
-            Usize::Var(n) => SymbolicVar::Val(n) * N::from_canonical_usize(rhs),
+            Usize::Const(n) => SymbolicVar::from(N::from_canonical_usize(n * rhs)),
+            Usize::Var(n) => SymbolicVar::from(n) * N::from_canonical_usize(rhs),
         }
     }
 }
@@ -1029,14 +1183,14 @@ impl<F: Field> Add<SymbolicFelt<F>> for Felt<F> {
 
 impl<F: Field, EF: ExtensionField<F>> From<Felt<F>> for SymbolicExt<F, EF> {
     fn from(value: Felt<F>) -> Self {
-        SymbolicExt::Base(Rc::new(SymbolicFelt::Val(value)))
+        value.to_operand().symbolic()
     }
 }
 
 impl<F: Field, EF: ExtensionField<F>> Neg for Ext<F, EF> {
     type Output = SymbolicExt<F, EF>;
     fn neg(self) -> Self::Output {
-        SymbolicExt::Neg(Rc::new(SymbolicExt::Val(self)))
+        -SymbolicExt::from(self)
     }
 }
 
@@ -1044,7 +1198,7 @@ impl<F: Field> Neg for Felt<F> {
     type Output = SymbolicFelt<F>;
 
     fn neg(self) -> Self::Output {
-        SymbolicFelt::Neg(Rc::new(SymbolicFelt::Val(self)))
+        -SymbolicFelt::from(self)
     }
 }
 
@@ -1052,23 +1206,23 @@ impl<N: Field> Neg for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn neg(self) -> Self::Output {
-        SymbolicVar::Neg(Rc::new(SymbolicVar::Val(self)))
+        -SymbolicVar::from(self)
     }
 }
 
-impl<N> From<usize> for SymbolicUsize<N> {
+impl<N: Field> From<usize> for SymbolicUsize<N> {
     fn from(n: usize) -> Self {
         SymbolicUsize::Const(n)
     }
 }
 
-impl<N> From<SymbolicVar<N>> for SymbolicUsize<N> {
+impl<N: Field> From<SymbolicVar<N>> for SymbolicUsize<N> {
     fn from(n: SymbolicVar<N>) -> Self {
         SymbolicUsize::Var(n)
     }
 }
 
-impl<N> From<Var<N>> for SymbolicUsize<N> {
+impl<N: Field> From<Var<N>> for SymbolicUsize<N> {
     fn from(n: Var<N>) -> Self {
         SymbolicUsize::Var(SymbolicVar::from(n))
     }
@@ -1130,7 +1284,7 @@ impl<N: Field> Sub<usize> for SymbolicUsize<N> {
     }
 }
 
-impl<N> From<Usize<N>> for SymbolicUsize<N> {
+impl<N: Field> From<Usize<N>> for SymbolicUsize<N> {
     fn from(n: Usize<N>) -> Self {
         match n {
             Usize::Const(n) => SymbolicUsize::Const(n),
@@ -1201,7 +1355,7 @@ impl<F: Field> Mul<SymbolicFelt<F>> for Felt<F> {
     }
 }
 
-impl<N> Mul<SymbolicVar<N>> for Var<N> {
+impl<N: Field> Mul<SymbolicVar<N>> for Var<N> {
     type Output = SymbolicVar<N>;
 
     fn mul(self, rhs: SymbolicVar<N>) -> Self::Output {
@@ -1252,7 +1406,7 @@ impl<N: Field> Sub<SymbolicVar<N>> for Usize<N> {
 
     fn sub(self, rhs: SymbolicVar<N>) -> Self::Output {
         match self {
-            Usize::Const(n) => SymbolicVar::Const(N::from_canonical_usize(n)) - rhs,
+            Usize::Const(n) => SymbolicVar::from(N::from_canonical_usize(n)) - rhs,
             Usize::Var(n) => SymbolicVar::<N>::from(n) - rhs,
         }
     }
@@ -1263,7 +1417,7 @@ impl<N: Field> Add<SymbolicVar<N>> for Usize<N> {
 
     fn add(self, rhs: SymbolicVar<N>) -> Self::Output {
         match self {
-            Usize::Const(n) => SymbolicVar::Const(N::from_canonical_usize(n)) + rhs,
+            Usize::Const(n) => SymbolicVar::from(N::from_canonical_usize(n)) + rhs,
             Usize::Var(n) => SymbolicVar::<N>::from(n) + rhs,
         }
     }
@@ -1288,8 +1442,8 @@ impl<N: Field> Sub<Var<N>> for Usize<N> {
 impl<N: Field> From<Usize<N>> for SymbolicVar<N> {
     fn from(value: Usize<N>) -> Self {
         match value {
-            Usize::Const(n) => SymbolicVar::Const(N::from_canonical_usize(n)),
-            Usize::Var(n) => SymbolicVar::Val(n),
+            Usize::Const(n) => SymbolicVar::from(N::from_canonical_usize(n)),
+            Usize::Var(n) => SymbolicVar::from(n),
         }
     }
 }
diff --git a/recursion/compiler/src/ir/types.rs b/recursion/compiler/src/ir/types.rs
index 01f08aeef6..5aec6fa97d 100644
--- a/recursion/compiler/src/ir/types.rs
+++ b/recursion/compiler/src/ir/types.rs
@@ -61,7 +61,7 @@ impl<C: Config> Witness<C> {
     }
 }
 
-impl<N: AbstractField> Usize<N> {
+impl<N: Field> Usize<N> {
     pub fn value(&self) -> usize {
         match self {
             Usize::Const(c) => *c,
@@ -72,7 +72,7 @@ impl<N: AbstractField> Usize<N> {
     pub fn materialize<C: Config<N = N>>(&self, builder: &mut Builder<C>) -> Var<C::N> {
         match self {
             Usize::Const(c) => builder.eval(C::N::from_canonical_usize(*c)),
-            Usize::Var(v) => v.clone(),
+            Usize::Var(v) => *v,
         }
     }
 }
@@ -230,44 +230,44 @@ impl<N: Field> Var<N> {
             return;
         }
         match src {
-            SymbolicVar::Const(c) => {
+            SymbolicVar::Const(c, _) => {
                 builder.operations.push(DslIr::ImmV(*self, c));
             }
-            SymbolicVar::Val(v) => {
+            SymbolicVar::Val(v, _) => {
                 builder
                     .operations
                     .push(DslIr::AddVI(*self, v, C::N::zero()));
             }
-            SymbolicVar::Add(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicVar::Const(lhs), SymbolicVar::Const(rhs)) => {
+            SymbolicVar::Add(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicVar::Const(lhs, _), SymbolicVar::Const(rhs, _)) => {
                     let sum = *lhs + *rhs;
                     builder.operations.push(DslIr::ImmV(*self, sum));
                 }
-                (SymbolicVar::Const(lhs), SymbolicVar::Val(rhs)) => {
+                (SymbolicVar::Const(lhs, _), SymbolicVar::Val(rhs, _)) => {
                     builder.operations.push(DslIr::AddVI(*self, *rhs, *lhs));
                 }
-                (SymbolicVar::Const(lhs), rhs) => {
+                (SymbolicVar::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign(rhs.clone(), builder);
                     builder.push(DslIr::AddVI(*self, rhs_value, *lhs));
                 }
-                (SymbolicVar::Val(lhs), SymbolicVar::Const(rhs)) => {
+                (SymbolicVar::Val(lhs, _), SymbolicVar::Const(rhs, _)) => {
                     builder.push(DslIr::AddVI(*self, *lhs, *rhs));
                 }
-                (SymbolicVar::Val(lhs), SymbolicVar::Val(rhs)) => {
+                (SymbolicVar::Val(lhs, _), SymbolicVar::Val(rhs, _)) => {
                     builder.push(DslIr::AddV(*self, *lhs, *rhs));
                 }
-                (SymbolicVar::Val(lhs), rhs) => {
+                (SymbolicVar::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign(rhs.clone(), builder);
                     builder.push(DslIr::AddV(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicVar::Const(rhs)) => {
+                (lhs, SymbolicVar::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign(lhs.clone(), builder);
                     builder.push(DslIr::AddVI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicVar::Val(rhs)) => {
+                (lhs, SymbolicVar::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign(lhs.clone(), builder);
                     builder.push(DslIr::AddV(*self, lhs_value, *rhs));
@@ -282,39 +282,39 @@ impl<N: Field> Var<N> {
                     builder.push(DslIr::AddV(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicVar::Mul(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicVar::Const(lhs), SymbolicVar::Const(rhs)) => {
+            SymbolicVar::Mul(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicVar::Const(lhs, _), SymbolicVar::Const(rhs, _)) => {
                     let product = *lhs * *rhs;
                     builder.push(DslIr::ImmV(*self, product));
                 }
-                (SymbolicVar::Const(lhs), SymbolicVar::Val(rhs)) => {
+                (SymbolicVar::Const(lhs, _), SymbolicVar::Val(rhs, _)) => {
                     builder.push(DslIr::MulVI(*self, *rhs, *lhs));
                 }
-                (SymbolicVar::Const(lhs), rhs) => {
+                (SymbolicVar::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::MulVI(*self, rhs_value, *lhs));
                 }
-                (SymbolicVar::Val(lhs), SymbolicVar::Const(rhs)) => {
+                (SymbolicVar::Val(lhs, _), SymbolicVar::Const(rhs, _)) => {
                     builder.push(DslIr::MulVI(*self, *lhs, *rhs));
                 }
-                (SymbolicVar::Val(lhs), SymbolicVar::Val(rhs)) => {
+                (SymbolicVar::Val(lhs, _), SymbolicVar::Val(rhs, _)) => {
                     builder.push(DslIr::MulV(*self, *lhs, *rhs));
                 }
-                (SymbolicVar::Val(lhs), rhs) => {
+                (SymbolicVar::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::MulV(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicVar::Const(rhs)) => {
+                (lhs, SymbolicVar::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::MulVI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicVar::Val(rhs)) => {
+                (lhs, SymbolicVar::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
@@ -330,39 +330,39 @@ impl<N: Field> Var<N> {
                     builder.push(DslIr::MulV(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicVar::Sub(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicVar::Const(lhs), SymbolicVar::Const(rhs)) => {
+            SymbolicVar::Sub(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicVar::Const(lhs, _), SymbolicVar::Const(rhs, _)) => {
                     let difference = *lhs - *rhs;
                     builder.push(DslIr::ImmV(*self, difference));
                 }
-                (SymbolicVar::Const(lhs), SymbolicVar::Val(rhs)) => {
+                (SymbolicVar::Const(lhs, _), SymbolicVar::Val(rhs, _)) => {
                     builder.push(DslIr::SubVIN(*self, *lhs, *rhs));
                 }
-                (SymbolicVar::Const(lhs), rhs) => {
+                (SymbolicVar::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::SubVIN(*self, *lhs, rhs_value));
                 }
-                (SymbolicVar::Val(lhs), SymbolicVar::Const(rhs)) => {
+                (SymbolicVar::Val(lhs, _), SymbolicVar::Const(rhs, _)) => {
                     builder.push(DslIr::SubVI(*self, *lhs, *rhs));
                 }
-                (SymbolicVar::Val(lhs), SymbolicVar::Val(rhs)) => {
+                (SymbolicVar::Val(lhs, _), SymbolicVar::Val(rhs, _)) => {
                     builder.push(DslIr::SubV(*self, *lhs, *rhs));
                 }
-                (SymbolicVar::Val(lhs), rhs) => {
+                (SymbolicVar::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::SubV(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicVar::Const(rhs)) => {
+                (lhs, SymbolicVar::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::SubVI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicVar::Val(rhs)) => {
+                (lhs, SymbolicVar::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
@@ -378,12 +378,12 @@ impl<N: Field> Var<N> {
                     builder.push(DslIr::SubV(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicVar::Neg(operand) => match &*operand {
-                SymbolicVar::Const(operand) => {
+            SymbolicVar::Neg(operand, _) => match &*operand {
+                SymbolicVar::Const(operand, _) => {
                     let negated = -*operand;
                     builder.push(DslIr::ImmV(*self, negated));
                 }
-                SymbolicVar::Val(operand) => {
+                SymbolicVar::Val(operand, _) => {
                     builder.push(DslIr::SubVIN(*self, C::N::zero(), *operand));
                 }
                 operand => {
@@ -419,24 +419,24 @@ impl<C: Config> Variable<C> for Var<C::N> {
         let rhs = rhs.into();
 
         match (lhs, rhs) {
-            (SymbolicVar::Const(lhs), SymbolicVar::Const(rhs)) => {
+            (SymbolicVar::Const(lhs, _), SymbolicVar::Const(rhs, _)) => {
                 assert_eq!(lhs, rhs, "Assertion failed at compile time");
             }
-            (SymbolicVar::Const(lhs), SymbolicVar::Val(rhs)) => {
+            (SymbolicVar::Const(lhs, _), SymbolicVar::Val(rhs, _)) => {
                 builder.push(DslIr::AssertEqVI(rhs, lhs));
             }
-            (SymbolicVar::Const(lhs), rhs) => {
+            (SymbolicVar::Const(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertEqVI(rhs_value, lhs));
             }
-            (SymbolicVar::Val(lhs), SymbolicVar::Const(rhs)) => {
+            (SymbolicVar::Val(lhs, _), SymbolicVar::Const(rhs, _)) => {
                 builder.push(DslIr::AssertEqVI(lhs, rhs));
             }
-            (SymbolicVar::Val(lhs), SymbolicVar::Val(rhs)) => {
+            (SymbolicVar::Val(lhs, _), SymbolicVar::Val(rhs, _)) => {
                 builder.push(DslIr::AssertEqV(lhs, rhs));
             }
-            (SymbolicVar::Val(lhs), rhs) => {
+            (SymbolicVar::Val(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertEqV(lhs, rhs_value));
@@ -460,24 +460,24 @@ impl<C: Config> Variable<C> for Var<C::N> {
         let rhs = rhs.into();
 
         match (lhs, rhs) {
-            (SymbolicVar::Const(lhs), SymbolicVar::Const(rhs)) => {
+            (SymbolicVar::Const(lhs, _), SymbolicVar::Const(rhs, _)) => {
                 assert_ne!(lhs, rhs, "Assertion failed at compile time");
             }
-            (SymbolicVar::Const(lhs), SymbolicVar::Val(rhs)) => {
+            (SymbolicVar::Const(lhs, _), SymbolicVar::Val(rhs, _)) => {
                 builder.push(DslIr::AssertNeVI(rhs, lhs));
             }
-            (SymbolicVar::Const(lhs), rhs) => {
+            (SymbolicVar::Const(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertNeVI(rhs_value, lhs));
             }
-            (SymbolicVar::Val(lhs), SymbolicVar::Const(rhs)) => {
+            (SymbolicVar::Val(lhs, _), SymbolicVar::Const(rhs, _)) => {
                 builder.push(DslIr::AssertNeVI(lhs, rhs));
             }
-            (SymbolicVar::Val(lhs), SymbolicVar::Val(rhs)) => {
+            (SymbolicVar::Val(lhs, _), SymbolicVar::Val(rhs, _)) => {
                 builder.push(DslIr::AssertNeV(lhs, rhs));
             }
-            (SymbolicVar::Val(lhs), rhs) => {
+            (SymbolicVar::Val(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertNeV(lhs, rhs_value));
@@ -521,47 +521,47 @@ impl<F: Field> Felt<F> {
             return;
         }
         match src {
-            SymbolicFelt::Const(c) => {
+            SymbolicFelt::Const(c, _) => {
                 builder.operations.push(DslIr::ImmF(*self, c));
             }
-            SymbolicFelt::Val(v) => {
+            SymbolicFelt::Val(v, _) => {
                 builder
                     .operations
                     .push(DslIr::AddFI(*self, v, C::F::zero()));
             }
-            SymbolicFelt::Add(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicFelt::Const(lhs), SymbolicFelt::Const(rhs)) => {
+            SymbolicFelt::Add(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicFelt::Const(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                     let sum = *lhs + *rhs;
                     builder.operations.push(DslIr::ImmF(*self, sum));
                 }
-                (SymbolicFelt::Const(lhs), SymbolicFelt::Val(rhs)) => {
+                (SymbolicFelt::Const(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                     builder.operations.push(DslIr::AddFI(*self, *rhs, *lhs));
                 }
-                (SymbolicFelt::Const(lhs), rhs) => {
+                (SymbolicFelt::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::AddFI(*self, rhs_value, *lhs));
                 }
-                (SymbolicFelt::Val(lhs), SymbolicFelt::Const(rhs)) => {
+                (SymbolicFelt::Val(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                     builder.push(DslIr::AddFI(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Val(lhs), SymbolicFelt::Val(rhs)) => {
+                (SymbolicFelt::Val(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                     builder.push(DslIr::AddF(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Val(lhs), rhs) => {
+                (SymbolicFelt::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::AddF(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicFelt::Const(rhs)) => {
+                (lhs, SymbolicFelt::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::AddFI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicFelt::Val(rhs)) => {
+                (lhs, SymbolicFelt::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
@@ -577,39 +577,39 @@ impl<F: Field> Felt<F> {
                     builder.push(DslIr::AddF(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicFelt::Mul(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicFelt::Const(lhs), SymbolicFelt::Const(rhs)) => {
+            SymbolicFelt::Mul(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicFelt::Const(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                     let product = *lhs * *rhs;
                     builder.push(DslIr::ImmF(*self, product));
                 }
-                (SymbolicFelt::Const(lhs), SymbolicFelt::Val(rhs)) => {
+                (SymbolicFelt::Const(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                     builder.push(DslIr::MulFI(*self, *rhs, *lhs));
                 }
-                (SymbolicFelt::Const(lhs), rhs) => {
+                (SymbolicFelt::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::MulFI(*self, rhs_value, *lhs));
                 }
-                (SymbolicFelt::Val(lhs), SymbolicFelt::Const(rhs)) => {
+                (SymbolicFelt::Val(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                     builder.push(DslIr::MulFI(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Val(lhs), SymbolicFelt::Val(rhs)) => {
+                (SymbolicFelt::Val(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                     builder.push(DslIr::MulF(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Val(lhs), rhs) => {
+                (SymbolicFelt::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::MulF(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicFelt::Const(rhs)) => {
+                (lhs, SymbolicFelt::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::MulFI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicFelt::Val(rhs)) => {
+                (lhs, SymbolicFelt::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
@@ -625,39 +625,39 @@ impl<F: Field> Felt<F> {
                     builder.push(DslIr::MulF(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicFelt::Sub(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicFelt::Const(lhs), SymbolicFelt::Const(rhs)) => {
+            SymbolicFelt::Sub(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicFelt::Const(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                     let difference = *lhs - *rhs;
                     builder.push(DslIr::ImmF(*self, difference));
                 }
-                (SymbolicFelt::Const(lhs), SymbolicFelt::Val(rhs)) => {
+                (SymbolicFelt::Const(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                     builder.push(DslIr::SubFIN(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Const(lhs), rhs) => {
+                (SymbolicFelt::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::SubFIN(*self, *lhs, rhs_value));
                 }
-                (SymbolicFelt::Val(lhs), SymbolicFelt::Const(rhs)) => {
+                (SymbolicFelt::Val(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                     builder.push(DslIr::SubFI(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Val(lhs), SymbolicFelt::Val(rhs)) => {
+                (SymbolicFelt::Val(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                     builder.push(DslIr::SubF(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Val(lhs), rhs) => {
+                (SymbolicFelt::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::SubF(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicFelt::Const(rhs)) => {
+                (lhs, SymbolicFelt::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::SubFI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicFelt::Val(rhs)) => {
+                (lhs, SymbolicFelt::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
@@ -673,39 +673,39 @@ impl<F: Field> Felt<F> {
                     builder.push(DslIr::SubF(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicFelt::Div(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicFelt::Const(lhs), SymbolicFelt::Const(rhs)) => {
+            SymbolicFelt::Div(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicFelt::Const(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                     let quotient = *lhs / *rhs;
                     builder.push(DslIr::ImmF(*self, quotient));
                 }
-                (SymbolicFelt::Const(lhs), SymbolicFelt::Val(rhs)) => {
+                (SymbolicFelt::Const(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                     builder.push(DslIr::DivFIN(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Const(lhs), rhs) => {
+                (SymbolicFelt::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::DivFIN(*self, *lhs, rhs_value));
                 }
-                (SymbolicFelt::Val(lhs), SymbolicFelt::Const(rhs)) => {
+                (SymbolicFelt::Val(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                     builder.push(DslIr::DivFI(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Val(lhs), SymbolicFelt::Val(rhs)) => {
+                (SymbolicFelt::Val(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                     builder.push(DslIr::DivF(*self, *lhs, *rhs));
                 }
-                (SymbolicFelt::Val(lhs), rhs) => {
+                (SymbolicFelt::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_cache(rhs.clone(), builder, cache);
                     cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::DivF(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicFelt::Const(rhs)) => {
+                (lhs, SymbolicFelt::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::DivFI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicFelt::Val(rhs)) => {
+                (lhs, SymbolicFelt::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_cache(lhs.clone(), builder, cache);
                     cache.insert(lhs.clone(), lhs_value);
@@ -721,12 +721,12 @@ impl<F: Field> Felt<F> {
                     builder.push(DslIr::DivF(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicFelt::Neg(operand) => match &*operand {
-                SymbolicFelt::Const(operand) => {
+            SymbolicFelt::Neg(operand, _) => match &*operand {
+                SymbolicFelt::Const(operand, _) => {
                     let negated = -*operand;
                     builder.push(DslIr::ImmF(*self, negated));
                 }
-                SymbolicFelt::Val(operand) => {
+                SymbolicFelt::Val(operand, _) => {
                     builder.push(DslIr::SubFIN(*self, C::F::zero(), *operand));
                 }
                 operand => {
@@ -762,24 +762,24 @@ impl<C: Config> Variable<C> for Felt<C::F> {
         let rhs = rhs.into();
 
         match (lhs, rhs) {
-            (SymbolicFelt::Const(lhs), SymbolicFelt::Const(rhs)) => {
+            (SymbolicFelt::Const(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                 assert_eq!(lhs, rhs, "Assertion failed at compile time");
             }
-            (SymbolicFelt::Const(lhs), SymbolicFelt::Val(rhs)) => {
+            (SymbolicFelt::Const(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                 builder.push(DslIr::AssertEqFI(rhs, lhs));
             }
-            (SymbolicFelt::Const(lhs), rhs) => {
+            (SymbolicFelt::Const(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertEqFI(rhs_value, lhs));
             }
-            (SymbolicFelt::Val(lhs), SymbolicFelt::Const(rhs)) => {
+            (SymbolicFelt::Val(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                 builder.push(DslIr::AssertEqFI(lhs, rhs));
             }
-            (SymbolicFelt::Val(lhs), SymbolicFelt::Val(rhs)) => {
+            (SymbolicFelt::Val(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                 builder.push(DslIr::AssertEqF(lhs, rhs));
             }
-            (SymbolicFelt::Val(lhs), rhs) => {
+            (SymbolicFelt::Val(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertEqF(lhs, rhs_value));
@@ -803,24 +803,24 @@ impl<C: Config> Variable<C> for Felt<C::F> {
         let rhs = rhs.into();
 
         match (lhs, rhs) {
-            (SymbolicFelt::Const(lhs), SymbolicFelt::Const(rhs)) => {
+            (SymbolicFelt::Const(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                 assert_ne!(lhs, rhs, "Assertion failed at compile time");
             }
-            (SymbolicFelt::Const(lhs), SymbolicFelt::Val(rhs)) => {
+            (SymbolicFelt::Const(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                 builder.push(DslIr::AssertNeFI(rhs, lhs));
             }
-            (SymbolicFelt::Const(lhs), rhs) => {
+            (SymbolicFelt::Const(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertNeFI(rhs_value, lhs));
             }
-            (SymbolicFelt::Val(lhs), SymbolicFelt::Const(rhs)) => {
+            (SymbolicFelt::Val(lhs, _), SymbolicFelt::Const(rhs, _)) => {
                 builder.push(DslIr::AssertNeFI(lhs, rhs));
             }
-            (SymbolicFelt::Val(lhs), SymbolicFelt::Val(rhs)) => {
+            (SymbolicFelt::Val(lhs, _), SymbolicFelt::Val(rhs, _)) => {
                 builder.push(DslIr::AssertNeF(lhs, rhs));
             }
-            (SymbolicFelt::Val(lhs), rhs) => {
+            (SymbolicFelt::Val(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertNeF(lhs, rhs_value));
@@ -866,13 +866,13 @@ impl<F: Field, EF: ExtensionField<F>> Ext<F, EF> {
             return;
         }
         match src {
-            SymbolicExt::Base(v) => match &*v {
-                SymbolicFelt::Const(c) => {
+            SymbolicExt::Base(v, _) => match &*v {
+                SymbolicFelt::Const(c, _) => {
                     builder
                         .operations
                         .push(DslIr::ImmE(*self, C::EF::from_base(*c)));
                 }
-                SymbolicFelt::Val(v) => {
+                SymbolicFelt::Val(v, _) => {
                     builder
                         .operations
                         .push(DslIr::AddEFFI(*self, *v, C::EF::zero()));
@@ -883,56 +883,53 @@ impl<F: Field, EF: ExtensionField<F>> Ext<F, EF> {
                     builder.push(DslIr::AddEFFI(*self, v_value, C::EF::zero()));
                 }
             },
-            SymbolicExt::Const(c) => {
+            SymbolicExt::Const(c, _) => {
                 builder.operations.push(DslIr::ImmE(*self, c));
             }
-            SymbolicExt::Val(v) => {
+            SymbolicExt::Val(v, _) => {
                 builder
                     .operations
                     .push(DslIr::AddEI(*self, v, C::EF::zero()));
             }
-            SymbolicExt::Add(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicExt::Const(lhs), SymbolicExt::Const(rhs)) => {
+            SymbolicExt::Add(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicExt::Const(lhs, _), SymbolicExt::Const(rhs, _)) => {
                     let sum = *lhs + *rhs;
                     builder.operations.push(DslIr::ImmE(*self, sum));
                 }
-                (SymbolicExt::Const(lhs), SymbolicExt::Val(rhs)) => {
+                (SymbolicExt::Const(lhs, _), SymbolicExt::Val(rhs, _)) => {
                     builder.operations.push(DslIr::AddEI(*self, *rhs, *lhs));
                 }
-                (SymbolicExt::Const(lhs), SymbolicExt::Base(rhs)) => {
-                    match rhs.as_ref() {
-                        SymbolicFelt::Const(rhs) => {
-                            let sum = *lhs + C::EF::from_base(*rhs);
-                            builder.operations.push(DslIr::ImmE(*self, sum));
-                        }
-                        SymbolicFelt::Val(rhs) => {
-                            builder.operations.push(DslIr::AddEFFI(*self, *rhs, *lhs));
-                        }
-                        rhs => {
-                            let rhs_value: Felt<_> = Felt::uninit(builder);
-                            rhs_value.assign_with_cache(rhs.clone(), builder, base_cache);
-                            base_cache.insert(rhs.clone(), rhs_value);
-                            builder
-                                .operations
-                                .push(DslIr::AddEFFI(*self, rhs_value, *lhs));
-                        }
+                (SymbolicExt::Const(lhs, _), SymbolicExt::Base(rhs, _)) => match rhs.as_ref() {
+                    SymbolicFelt::Const(rhs, _) => {
+                        let sum = *lhs + C::EF::from_base(*rhs);
+                        builder.operations.push(DslIr::ImmE(*self, sum));
                     }
-                    // builder.operations.push(DslIR::AddEI(*self, *rhs, *lhs));
-                }
-                (SymbolicExt::Const(lhs), rhs) => {
+                    SymbolicFelt::Val(rhs, _) => {
+                        builder.operations.push(DslIr::AddEFFI(*self, *rhs, *lhs));
+                    }
+                    rhs => {
+                        let rhs_value: Felt<_> = Felt::uninit(builder);
+                        rhs_value.assign_with_cache(rhs.clone(), builder, base_cache);
+                        base_cache.insert(rhs.clone(), rhs_value);
+                        builder
+                            .operations
+                            .push(DslIr::AddEFFI(*self, rhs_value, *lhs));
+                    }
+                },
+                (SymbolicExt::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_caches(rhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::AddEI(*self, rhs_value, *lhs));
                 }
-                (SymbolicExt::Val(lhs), SymbolicExt::Const(rhs)) => {
+                (SymbolicExt::Val(lhs, _), SymbolicExt::Const(rhs, _)) => {
                     builder.push(DslIr::AddEI(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Val(lhs), SymbolicExt::Base(rhs)) => match rhs.as_ref() {
-                    SymbolicFelt::Const(rhs) => {
+                (SymbolicExt::Val(lhs, _), SymbolicExt::Base(rhs, _)) => match rhs.as_ref() {
+                    SymbolicFelt::Const(rhs, _) => {
                         builder.push(DslIr::AddEFI(*self, *lhs, *rhs));
                     }
-                    SymbolicFelt::Val(rhs) => {
+                    SymbolicFelt::Val(rhs, _) => {
                         builder.push(DslIr::AddEF(*self, *lhs, *rhs));
                     }
                     rhs => {
@@ -940,22 +937,22 @@ impl<F: Field, EF: ExtensionField<F>> Ext<F, EF> {
                         builder.push(DslIr::AddEF(*self, *lhs, rhs));
                     }
                 },
-                (SymbolicExt::Val(lhs), SymbolicExt::Val(rhs)) => {
+                (SymbolicExt::Val(lhs, _), SymbolicExt::Val(rhs, _)) => {
                     builder.push(DslIr::AddE(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Val(lhs), rhs) => {
+                (SymbolicExt::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_caches(rhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::AddE(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicExt::Const(rhs)) => {
+                (lhs, SymbolicExt::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_caches(lhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::AddEI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicExt::Val(rhs)) => {
+                (lhs, SymbolicExt::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_caches(lhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(lhs.clone(), lhs_value);
@@ -971,39 +968,39 @@ impl<F: Field, EF: ExtensionField<F>> Ext<F, EF> {
                     builder.push(DslIr::AddE(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicExt::Mul(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicExt::Const(lhs), SymbolicExt::Const(rhs)) => {
+            SymbolicExt::Mul(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicExt::Const(lhs, _), SymbolicExt::Const(rhs, _)) => {
                     let product = *lhs * *rhs;
                     builder.push(DslIr::ImmE(*self, product));
                 }
-                (SymbolicExt::Const(lhs), SymbolicExt::Val(rhs)) => {
+                (SymbolicExt::Const(lhs, _), SymbolicExt::Val(rhs, _)) => {
                     builder.push(DslIr::MulEI(*self, *rhs, *lhs));
                 }
-                (SymbolicExt::Const(lhs), rhs) => {
+                (SymbolicExt::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_caches(rhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::MulEI(*self, rhs_value, *lhs));
                 }
-                (SymbolicExt::Val(lhs), SymbolicExt::Const(rhs)) => {
+                (SymbolicExt::Val(lhs, _), SymbolicExt::Const(rhs, _)) => {
                     builder.push(DslIr::MulEI(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Val(lhs), SymbolicExt::Val(rhs)) => {
+                (SymbolicExt::Val(lhs, _), SymbolicExt::Val(rhs, _)) => {
                     builder.push(DslIr::MulE(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Val(lhs), rhs) => {
+                (SymbolicExt::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_caches(rhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::MulE(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicExt::Const(rhs)) => {
+                (lhs, SymbolicExt::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_caches(lhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::MulEI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicExt::Val(rhs)) => {
+                (lhs, SymbolicExt::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_caches(lhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(lhs.clone(), lhs_value);
@@ -1019,39 +1016,39 @@ impl<F: Field, EF: ExtensionField<F>> Ext<F, EF> {
                     builder.push(DslIr::MulE(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicExt::Sub(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicExt::Const(lhs), SymbolicExt::Const(rhs)) => {
+            SymbolicExt::Sub(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicExt::Const(lhs, _), SymbolicExt::Const(rhs, _)) => {
                     let difference = *lhs - *rhs;
                     builder.push(DslIr::ImmE(*self, difference));
                 }
-                (SymbolicExt::Const(lhs), SymbolicExt::Val(rhs)) => {
+                (SymbolicExt::Const(lhs, _), SymbolicExt::Val(rhs, _)) => {
                     builder.push(DslIr::SubEIN(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Const(lhs), rhs) => {
+                (SymbolicExt::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_caches(rhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::SubEIN(*self, *lhs, rhs_value));
                 }
-                (SymbolicExt::Val(lhs), SymbolicExt::Const(rhs)) => {
+                (SymbolicExt::Val(lhs, _), SymbolicExt::Const(rhs, _)) => {
                     builder.push(DslIr::SubEI(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Val(lhs), SymbolicExt::Val(rhs)) => {
+                (SymbolicExt::Val(lhs, _), SymbolicExt::Val(rhs, _)) => {
                     builder.push(DslIr::SubE(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Val(lhs), rhs) => {
+                (SymbolicExt::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_caches(rhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::SubE(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicExt::Const(rhs)) => {
+                (lhs, SymbolicExt::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_caches(lhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::SubEI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicExt::Val(rhs)) => {
+                (lhs, SymbolicExt::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_caches(lhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(lhs.clone(), lhs_value);
@@ -1066,39 +1063,39 @@ impl<F: Field, EF: ExtensionField<F>> Ext<F, EF> {
                     builder.push(DslIr::SubE(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicExt::Div(lhs, rhs) => match (&*lhs, &*rhs) {
-                (SymbolicExt::Const(lhs), SymbolicExt::Const(rhs)) => {
+            SymbolicExt::Div(lhs, rhs, _) => match (&*lhs, &*rhs) {
+                (SymbolicExt::Const(lhs, _), SymbolicExt::Const(rhs, _)) => {
                     let quotient = *lhs / *rhs;
                     builder.push(DslIr::ImmE(*self, quotient));
                 }
-                (SymbolicExt::Const(lhs), SymbolicExt::Val(rhs)) => {
+                (SymbolicExt::Const(lhs, _), SymbolicExt::Val(rhs, _)) => {
                     builder.push(DslIr::DivEIN(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Const(lhs), rhs) => {
+                (SymbolicExt::Const(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_caches(rhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::DivEIN(*self, *lhs, rhs_value));
                 }
-                (SymbolicExt::Val(lhs), SymbolicExt::Const(rhs)) => {
+                (SymbolicExt::Val(lhs, _), SymbolicExt::Const(rhs, _)) => {
                     builder.push(DslIr::DivEI(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Val(lhs), SymbolicExt::Val(rhs)) => {
+                (SymbolicExt::Val(lhs, _), SymbolicExt::Val(rhs, _)) => {
                     builder.push(DslIr::DivE(*self, *lhs, *rhs));
                 }
-                (SymbolicExt::Val(lhs), rhs) => {
+                (SymbolicExt::Val(lhs, _), rhs) => {
                     let rhs_value = Self::uninit(builder);
                     rhs_value.assign_with_caches(rhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(rhs.clone(), rhs_value);
                     builder.push(DslIr::DivE(*self, *lhs, rhs_value));
                 }
-                (lhs, SymbolicExt::Const(rhs)) => {
+                (lhs, SymbolicExt::Const(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_caches(lhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(lhs.clone(), lhs_value);
                     builder.push(DslIr::DivEI(*self, lhs_value, *rhs));
                 }
-                (lhs, SymbolicExt::Val(rhs)) => {
+                (lhs, SymbolicExt::Val(rhs, _)) => {
                     let lhs_value = Self::uninit(builder);
                     lhs_value.assign_with_caches(lhs.clone(), builder, ext_cache, base_cache);
                     ext_cache.insert(lhs.clone(), lhs_value);
@@ -1114,12 +1111,12 @@ impl<F: Field, EF: ExtensionField<F>> Ext<F, EF> {
                     builder.push(DslIr::DivE(*self, lhs_value, rhs_value));
                 }
             },
-            SymbolicExt::Neg(operand) => match &*operand {
-                SymbolicExt::Const(operand) => {
+            SymbolicExt::Neg(operand, _) => match &*operand {
+                SymbolicExt::Const(operand, _) => {
                     let negated = -*operand;
                     builder.push(DslIr::ImmE(*self, negated));
                 }
-                SymbolicExt::Val(operand) => {
+                SymbolicExt::Val(operand, _) => {
                     builder.push(DslIr::NegE(*self, *operand));
                 }
                 operand => {
@@ -1160,24 +1157,24 @@ impl<C: Config> Variable<C> for Ext<C::F, C::EF> {
         let rhs = rhs.into();
 
         match (lhs, rhs) {
-            (SymbolicExt::Const(lhs), SymbolicExt::Const(rhs)) => {
+            (SymbolicExt::Const(lhs, _), SymbolicExt::Const(rhs, _)) => {
                 assert_eq!(lhs, rhs, "Assertion failed at compile time");
             }
-            (SymbolicExt::Const(lhs), SymbolicExt::Val(rhs)) => {
+            (SymbolicExt::Const(lhs, _), SymbolicExt::Val(rhs, _)) => {
                 builder.push(DslIr::AssertEqEI(rhs, lhs));
             }
-            (SymbolicExt::Const(lhs), rhs) => {
+            (SymbolicExt::Const(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertEqEI(rhs_value, lhs));
             }
-            (SymbolicExt::Val(lhs), SymbolicExt::Const(rhs)) => {
+            (SymbolicExt::Val(lhs, _), SymbolicExt::Const(rhs, _)) => {
                 builder.push(DslIr::AssertEqEI(lhs, rhs));
             }
-            (SymbolicExt::Val(lhs), SymbolicExt::Val(rhs)) => {
+            (SymbolicExt::Val(lhs, _), SymbolicExt::Val(rhs, _)) => {
                 builder.push(DslIr::AssertEqE(lhs, rhs));
             }
-            (SymbolicExt::Val(lhs), rhs) => {
+            (SymbolicExt::Val(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertEqE(lhs, rhs_value));
@@ -1201,24 +1198,24 @@ impl<C: Config> Variable<C> for Ext<C::F, C::EF> {
         let rhs = rhs.into();
 
         match (lhs, rhs) {
-            (SymbolicExt::Const(lhs), SymbolicExt::Const(rhs)) => {
+            (SymbolicExt::Const(lhs, _), SymbolicExt::Const(rhs, _)) => {
                 assert_ne!(lhs, rhs, "Assertion failed at compile time");
             }
-            (SymbolicExt::Const(lhs), SymbolicExt::Val(rhs)) => {
+            (SymbolicExt::Const(lhs, _), SymbolicExt::Val(rhs, _)) => {
                 builder.push(DslIr::AssertNeEI(rhs, lhs));
             }
-            (SymbolicExt::Const(lhs), rhs) => {
+            (SymbolicExt::Const(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertNeEI(rhs_value, lhs));
             }
-            (SymbolicExt::Val(lhs), SymbolicExt::Const(rhs)) => {
+            (SymbolicExt::Val(lhs, _), SymbolicExt::Const(rhs, _)) => {
                 builder.push(DslIr::AssertNeEI(lhs, rhs));
             }
-            (SymbolicExt::Val(lhs), SymbolicExt::Val(rhs)) => {
+            (SymbolicExt::Val(lhs, _), SymbolicExt::Val(rhs, _)) => {
                 builder.push(DslIr::AssertNeE(lhs, rhs));
             }
-            (SymbolicExt::Val(lhs), rhs) => {
+            (SymbolicExt::Val(lhs, _), rhs) => {
                 let rhs_value = Self::uninit(builder);
                 rhs_value.assign(rhs, builder);
                 builder.push(DslIr::AssertNeE(lhs, rhs_value));
diff --git a/recursion/compiler/src/ir/utils.rs b/recursion/compiler/src/ir/utils.rs
index f5013d5ff9..29a7ac8316 100644
--- a/recursion/compiler/src/ir/utils.rs
+++ b/recursion/compiler/src/ir/utils.rs
@@ -90,7 +90,7 @@ impl<C: Config> Builder<C> {
         x: Ext<C::F, C::EF>,
         power_bits: Vec<Var<C::N>>,
     ) -> Ext<C::F, C::EF> {
-        let mut result = self.eval(SymbolicExt::Const(C::EF::one()));
+        let mut result = self.eval(SymbolicExt::from_f(C::EF::one()));
         let mut power_f: Ext<_, _> = self.eval(x);
         for i in 0..power_bits.len() {
             let bit = power_bits[i];
@@ -184,9 +184,9 @@ impl<C: Config> Builder<C> {
     /// Creates an ext from a slice of felts.
     pub fn ext_from_base_slice(&mut self, arr: &[Felt<C::F>]) -> Ext<C::F, C::EF> {
         assert!(arr.len() <= <C::EF as AbstractExtensionField::<C::F>>::D);
-        let mut res = SymbolicExt::Const(C::EF::zero());
+        let mut res = SymbolicExt::from_f(C::EF::zero());
         for i in 0..arr.len() {
-            res += arr[i] * SymbolicExt::Const(C::EF::monomial(i));
+            res += arr[i] * SymbolicExt::from_f(C::EF::monomial(i));
         }
         self.eval(res)
     }
diff --git a/recursion/compiler/tests/arithmetic.rs b/recursion/compiler/tests/arithmetic.rs
index c90b2a88ee..ce3f214ba1 100644
--- a/recursion/compiler/tests/arithmetic.rs
+++ b/recursion/compiler/tests/arithmetic.rs
@@ -4,7 +4,7 @@ use p3_field::AbstractField;
 use sp1_core::stark::StarkGenericConfig;
 use sp1_core::utils::BabyBearPoseidon2;
 use sp1_recursion_compiler::asm::AsmBuilder;
-use sp1_recursion_compiler::ir::{Ext, Felt};
+use sp1_recursion_compiler::ir::{Ext, Felt, SymbolicExt};
 use sp1_recursion_compiler::ir::{ExtConst, Var};
 use sp1_recursion_core::runtime::Runtime;
 
@@ -58,6 +58,17 @@ fn test_compiler_arithmetic() {
         let a_ext: Ext<_, _> = builder.eval(a_ext_val.cons());
         let b_ext: Ext<_, _> = builder.eval(b_ext_val.cons());
         builder.assert_ext_eq(a_ext + b_ext, (a_ext_val + b_ext_val).cons());
+        builder.assert_ext_eq(
+            -a_ext / b_ext + (a_ext * b_ext) * (a_ext * b_ext),
+            (-a_ext_val / b_ext_val + (a_ext_val * b_ext_val) * (a_ext_val * b_ext_val)).cons(),
+        );
+        let mut a_expr = SymbolicExt::from(a_ext);
+        let mut a_val = a_ext_val;
+        for _ in 0..10 {
+            a_expr += b_ext * a_val + EF::one();
+            a_val += b_ext_val * a_val + EF::one();
+            builder.assert_ext_eq(a_expr.clone(), a_val.cons())
+        }
         builder.assert_ext_eq(a_ext * b_ext, (a_ext_val * b_ext_val).cons());
         builder.assert_ext_eq(a_ext - b_ext, (a_ext_val - b_ext_val).cons());
         builder.assert_ext_eq(a_ext / b_ext, (a_ext_val / b_ext_val).cons());
diff --git a/recursion/core/src/poseidon2_wide/external.rs b/recursion/core/src/poseidon2_wide/external.rs
index 40a96890ae..3c9cf067d3 100644
--- a/recursion/core/src/poseidon2_wide/external.rs
+++ b/recursion/core/src/poseidon2_wide/external.rs
@@ -1,6 +1,6 @@
 use core::borrow::Borrow;
 use core::mem::size_of;
-use p3_air::{Air, BaseAir};
+use p3_air::{Air, AirBuilder, BaseAir};
 use p3_field::{AbstractField, PrimeField32};
 use p3_matrix::dense::RowMajorMatrix;
 use p3_matrix::Matrix;
@@ -36,6 +36,8 @@ pub struct Poseidon2WideCols<T> {
     pub output: [T; WIDTH],
     external_rounds: [Poseidon2WideExternalRoundCols<T>; NUM_EXTERNAL_ROUNDS],
     internal_rounds: Poseidon2WideInternalRoundsCols<T>,
+
+    pub is_real: T,
 }
 
 /// A grouping of columns for a single external round.
@@ -84,6 +86,7 @@ impl<F: PrimeField32> MachineAir<F> for Poseidon2WideChip {
             // Apply the initial round.
             cols.input = event.input;
             cols.external_rounds[0].state = event.input;
+            cols.is_real = F::one();
             external_linear_layer(&mut cols.external_rounds[0].state);
 
             // Apply the first half of external rounds.
@@ -213,6 +216,7 @@ fn eval_external_round<AB: SP1AirBuilder>(
     builder: &mut AB,
     cols: &Poseidon2WideCols<AB::Var>,
     r: usize,
+    is_real: AB::Var,
 ) {
     let round_cols = cols.external_rounds[r];
 
@@ -223,7 +227,7 @@ fn eval_external_round<AB: SP1AirBuilder>(
         r + NUM_INTERNAL_ROUNDS
     };
     let add_rc: [AB::Expr; WIDTH] = core::array::from_fn(|i| {
-        round_cols.state[i].into() + AB::Expr::from_wrapped_u32(RC_16_30_U32[round][i])
+        round_cols.state[i].into() + is_real * AB::F::from_wrapped_u32(RC_16_30_U32[round][i])
     });
 
     // Apply the sboxes.
@@ -253,7 +257,11 @@ fn eval_external_round<AB: SP1AirBuilder>(
     }
 }
 
-fn eval_internal_rounds<AB: SP1AirBuilder>(builder: &mut AB, cols: &Poseidon2WideCols<AB::Var>) {
+fn eval_internal_rounds<AB: SP1AirBuilder>(
+    builder: &mut AB,
+    cols: &Poseidon2WideCols<AB::Var>,
+    is_real: AB::Var,
+) {
     let round_cols = &cols.internal_rounds;
     let mut state: [AB::Expr; WIDTH] = core::array::from_fn(|i| round_cols.state[i].into());
     for r in 0..NUM_INTERNAL_ROUNDS {
@@ -263,7 +271,7 @@ fn eval_internal_rounds<AB: SP1AirBuilder>(builder: &mut AB, cols: &Poseidon2Wid
             state[0].clone()
         } else {
             round_cols.s0[r - 1].into()
-        } + AB::Expr::from_wrapped_u32(RC_16_30_U32[round][0]);
+        } + is_real * AB::Expr::from_wrapped_u32(RC_16_30_U32[round][0]);
 
         let sbox_deg_3 = add_rc.clone() * add_rc.clone() * add_rc.clone();
         builder.assert_eq(round_cols.sbox_deg_3[r], sbox_deg_3);
@@ -313,7 +321,7 @@ where
             initial_round_output
         };
         for i in 0..WIDTH {
-            builder.assert_eq(
+            builder.when(cols.is_real).assert_eq(
                 cols.external_rounds[0].state[i],
                 initial_round_output[i].clone(),
             );
@@ -321,15 +329,15 @@ where
 
         // Apply the first half of external rounds.
         for r in 0..NUM_EXTERNAL_ROUNDS / 2 {
-            eval_external_round(builder, cols, r);
+            eval_external_round(builder, cols, r, cols.is_real);
         }
 
         // Apply the internal rounds.
-        eval_internal_rounds(builder, cols);
+        eval_internal_rounds(builder, cols, cols.is_real);
 
         // Apply the second half of external rounds.
         for r in NUM_EXTERNAL_ROUNDS / 2..NUM_EXTERNAL_ROUNDS {
-            eval_external_round(builder, cols, r);
+            eval_external_round(builder, cols, r, cols.is_real);
         }
     }
 }
@@ -396,18 +404,18 @@ mod tests {
 
     /// A test proving 2^10 permuations
     #[test]
-    fn prove_babybear() {
+    fn poseidon2_wide_prove_babybear() {
         let config = BabyBearPoseidon2Inner::new();
         let mut challenger = config.challenger();
 
         let chip = Poseidon2WideChip;
 
-        let test_inputs = (0..1024)
+        let test_inputs = (0..1000)
             .map(|i| [BabyBear::from_canonical_u32(i); WIDTH])
             .collect_vec();
 
         let mut input_exec = ExecutionRecord::<BabyBear>::default();
-        for input in test_inputs.iter().cloned() {
+        for input in test_inputs {
             input_exec.poseidon2_events.push(Poseidon2Event { input });
         }
         let trace: RowMajorMatrix<BabyBear> =
diff --git a/recursion/program/src/constraints.rs b/recursion/program/src/constraints.rs
index 87033b621e..8a01700a65 100644
--- a/recursion/program/src/constraints.rs
+++ b/recursion/program/src/constraints.rs
@@ -273,7 +273,7 @@ mod tests {
     }
 
     #[test]
-    fn test_verify_constraints_whole() {
+    fn test_verify_constraints() {
         type SC = BabyBearPoseidon2;
         type F = <SC as StarkGenericConfig>::Val;
         type EF = <SC as StarkGenericConfig>::Challenge;
diff --git a/recursion/program/src/fri/mod.rs b/recursion/program/src/fri/mod.rs
index 56de5e3b93..a9d8682702 100644
--- a/recursion/program/src/fri/mod.rs
+++ b/recursion/program/src/fri/mod.rs
@@ -4,6 +4,7 @@ pub mod two_adic_pcs;
 pub mod types;
 
 pub use domain::*;
+use sp1_recursion_compiler::ir::ExtensionOperand;
 #[cfg(test)]
 pub(crate) use two_adic_pcs::tests::*;
 pub use two_adic_pcs::*;
@@ -17,8 +18,6 @@ use sp1_recursion_compiler::ir::Builder;
 use sp1_recursion_compiler::ir::Config;
 use sp1_recursion_compiler::ir::Ext;
 use sp1_recursion_compiler::ir::Felt;
-use sp1_recursion_compiler::ir::SymbolicExt;
-use sp1_recursion_compiler::ir::SymbolicFelt;
 use sp1_recursion_compiler::ir::SymbolicVar;
 use sp1_recursion_compiler::ir::Usize;
 use sp1_recursion_compiler::ir::Var;
@@ -142,9 +141,9 @@ where
     builder.cycle_tracker("verify-query");
     let folded_eval: Ext<C::F, C::EF> = builder.eval(C::F::zero());
     let two_adic_generator_f = config.get_two_adic_generator(builder, log_max_height);
-    let two_adic_generator_ef: Ext<_, _> = builder.eval(SymbolicExt::Base(
-        SymbolicFelt::Val(two_adic_generator_f).into(),
-    ));
+
+    let two_adic_gen_ext = two_adic_generator_f.to_operand().symbolic();
+    let two_adic_generator_ef: Ext<_, _> = builder.eval(two_adic_gen_ext);
 
     let x = builder.exp_reverse_bits_len(two_adic_generator_ef, index_bits, log_max_height);
 
@@ -163,7 +162,7 @@ where
 
             let index_bit = builder.get(index_bits, i);
             let index_sibling_mod_2: Var<C::N> =
-                builder.eval(SymbolicVar::Const(C::N::one()) - index_bit);
+                builder.eval(SymbolicVar::from(C::N::one()) - index_bit);
             let i_plus_one = builder.eval(i + C::N::one());
             let index_pair = index_bits.shift(builder, i_plus_one);