diff --git a/Cargo.lock b/Cargo.lock
index f49e227620..3a42ba8793 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -28,6 +28,19 @@ dependencies = [
  "cpufeatures",
 ]
 
+[[package]]
+name = "ahash"
+version = "0.8.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011"
+dependencies = [
+ "cfg-if",
+ "getrandom 0.2.15",
+ "once_cell",
+ "version_check",
+ "zerocopy",
+]
+
 [[package]]
 name = "aho-corasick"
 version = "1.1.3"
@@ -452,6 +465,7 @@ dependencies = [
  "lazy_static",
  "libc",
  "log",
+ "once_map",
  "pathdiff",
  "petgraph",
  "regex",
@@ -1375,6 +1389,16 @@ version = "0.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "4ee93343901ab17bd981295f2cf0026d4ad018c7c31ba84549a4ddbb47a45104"
 
+[[package]]
+name = "lock_api"
+version = "0.4.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "07af8b9cdd281b7915f413fa73f29ebd5d55d0d3f0155584dade1ff18cea1b17"
+dependencies = [
+ "autocfg",
+ "scopeguard",
+]
+
 [[package]]
 name = "lockfree-object-pool"
 version = "0.1.6"
@@ -1540,6 +1564,18 @@ version = "1.20.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775"
 
+[[package]]
+name = "once_map"
+version = "0.4.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7bd2cae3bec3936bbed1ccc5a3343b3738858182419f9c0522c7260c80c430b0"
+dependencies = [
+ "ahash",
+ "hashbrown",
+ "parking_lot",
+ "stable_deref_trait",
+]
+
 [[package]]
 name = "openssl"
 version = "0.10.69"
@@ -1590,6 +1626,29 @@ version = "0.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "04744f49eae99ab78e0d5c0b603ab218f515ea8cfe5a456d7629ad883a3b6e7d"
 
+[[package]]
+name = "parking_lot"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f1bf18183cf54e8d6059647fc3063646a1801cf30896933ec2311622cc4b9a27"
+dependencies = [
+ "lock_api",
+ "parking_lot_core",
+]
+
+[[package]]
+name = "parking_lot_core"
+version = "0.9.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1e401f977ab385c9e4e3ab30627d6f26d00e2c73eef317493c4ec6d468726cf8"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "redox_syscall",
+ "smallvec",
+ "windows-targets",
+]
+
 [[package]]
 name = "pathdiff"
 version = "0.2.3"
@@ -1843,6 +1902,15 @@ dependencies = [
  "rand_core 0.3.1",
 ]
 
+[[package]]
+name = "redox_syscall"
+version = "0.5.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "03a862b389f93e68874fbf580b9de08dd02facb9a788ebadaf4a3fd33cf58834"
+dependencies = [
+ "bitflags",
+]
+
 [[package]]
 name = "redox_users"
 version = "0.5.0"
@@ -2069,6 +2137,12 @@ dependencies = [
  "windows-sys 0.59.0",
 ]
 
+[[package]]
+name = "scopeguard"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
+
 [[package]]
 name = "security-framework"
 version = "2.11.1"
diff --git a/creusot/Cargo.toml b/creusot/Cargo.toml
index 9b8b9e122b..0e9c05ec09 100644
--- a/creusot/Cargo.toml
+++ b/creusot/Cargo.toml
@@ -22,6 +22,7 @@ tempdir = "0.3"
 serde_json = "1.0"
 lazy_static = "1.5"
 pathdiff = "0.2"
+once_map = "0.4"
 
 [dev-dependencies]
 clap = { version = "4.5", features = ["derive", "env"] }
diff --git a/creusot/src/backend.rs b/creusot/src/backend.rs
index 9a7e8b8dfe..57686f21d2 100644
--- a/creusot/src/backend.rs
+++ b/creusot/src/backend.rs
@@ -12,6 +12,7 @@ use crate::{
     util::path_of_span,
 };
 use std::{
+    cell::RefCell,
     ops::{Deref, DerefMut},
     path::PathBuf,
 };
@@ -33,9 +34,9 @@ pub(crate) mod ty_inv;
 pub(crate) mod wto;
 
 pub struct Why3Generator<'tcx> {
-    ctx: TranslationCtx<'tcx>,
+    pub ctx: TranslationCtx<'tcx>,
     functions: Vec<TranslatedItem>,
-    pub(crate) span_map: SpanMap,
+    pub(crate) span_map: RefCell<SpanMap>,
 }
 
 impl<'tcx> Deref for Why3Generator<'tcx> {
@@ -96,10 +97,10 @@ impl<'tcx> Why3Generator<'tcx> {
         matches!(self.item_type(item), ItemType::Logic { .. } | ItemType::Predicate { .. })
     }
 
-    pub(crate) fn span_attr(&mut self, span: Span) -> Option<why3::declaration::Attribute> {
+    pub(crate) fn span_attr(&self, span: Span) -> Option<why3::declaration::Attribute> {
         let path = path_of_span(self.tcx, span, &self.opts.span_mode)?;
 
-        if let Some(span) = self.span_map.encode_span(&self.ctx.opts, span) {
+        if let Some(span) = self.span_map.borrow_mut().encode_span(&self.ctx.opts, span) {
             return Some(span);
         };
 
diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs
index 38a9348d4e..8318ab8f23 100644
--- a/creusot/src/backend/clone_map.rs
+++ b/creusot/src/backend/clone_map.rs
@@ -1,3 +1,5 @@
+use std::cell::RefCell;
+
 use crate::{
     backend::{clone_map::elaborator::Expander, dependency::Dependency, Why3Generator},
     contracts_items::{get_builtin, get_inv_function},
@@ -7,6 +9,8 @@ use crate::{
 };
 use elaborator::Strength;
 use indexmap::{IndexMap, IndexSet};
+use itertools::Itertools;
+use once_map::unsync::OnceMap;
 use petgraph::prelude::DiGraphMap;
 use rustc_hir::{
     def::DefKind,
@@ -82,12 +86,12 @@ impl PreludeModule {
 }
 
 pub(crate) trait Namer<'tcx> {
-    fn value(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
+    fn item(&self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
         let node = Dependency::Item(def_id, subst);
-        self.insert(node).qname()
+        self.dependency(node).qname()
     }
 
-    fn ty(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
+    fn ty(&self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
         let ty = match self.tcx().def_kind(def_id) {
             DefKind::Enum | DefKind::Struct | DefKind::Union => {
                 Ty::new_adt(self.tcx(), self.tcx().adt_def(def_id), subst)
@@ -97,23 +101,23 @@ pub(crate) trait Namer<'tcx> {
             _ => unreachable!(),
         };
 
-        self.insert(Dependency::Type(ty)).qname()
+        self.dependency(Dependency::Type(ty)).qname()
     }
 
-    fn ty_param(&mut self, ty: Ty<'tcx>) -> QName {
+    fn ty_param(&self, ty: Ty<'tcx>) -> QName {
         assert!(matches!(ty.kind(), TyKind::Param(_)));
-        self.insert(Dependency::Type(ty)).qname()
+        self.dependency(Dependency::Type(ty)).qname()
     }
 
-    fn constructor(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
+    fn constructor(&self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
         let node = Dependency::Item(def_id, subst);
-        self.insert(node).qname()
+        self.dependency(node).qname()
     }
 
-    fn ty_inv(&mut self, ty: Ty<'tcx>) -> QName {
+    fn ty_inv(&self, ty: Ty<'tcx>) -> QName {
         let def_id = get_inv_function(self.tcx());
         let subst = self.tcx().mk_args(&[ty::GenericArg::from(ty)]);
-        self.value(def_id, subst)
+        self.item(def_id, subst)
     }
 
     /// Creates a name for a struct or closure projection ie: x.field1
@@ -121,7 +125,7 @@ pub(crate) trait Namer<'tcx> {
     /// * `def_id` - The id of the type or closure being projected
     /// * `subst` - Substitution that type is being accessed at
     /// * `ix` - The field in that constructor being accessed.
-    fn field(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>, ix: FieldIdx) -> QName {
+    fn field(&self, def_id: DefId, subst: GenericArgsRef<'tcx>, ix: FieldIdx) -> QName {
         let node = match self.tcx().def_kind(def_id) {
             DefKind::Closure => Dependency::ClosureAccessor(def_id, subst, ix.as_u32()),
             DefKind::Struct | DefKind::Union => {
@@ -132,15 +136,15 @@ pub(crate) trait Namer<'tcx> {
             _ => unreachable!(),
         };
 
-        self.insert(node).qname()
+        self.dependency(node).qname()
     }
 
-    fn eliminator(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
-        self.insert(Dependency::Eliminator(def_id, subst)).qname()
+    fn eliminator(&self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
+        self.dependency(Dependency::Eliminator(def_id, subst)).qname()
     }
 
-    fn promoted(&mut self, def_id: LocalDefId, prom: Promoted) -> QName {
-        self.insert(Dependency::Promoted(def_id, prom)).qname()
+    fn promoted(&self, def_id: LocalDefId, prom: Promoted) -> QName {
+        self.dependency(Dependency::Promoted(def_id, prom)).qname()
     }
 
     fn normalize<T: TypeFoldable<TyCtxt<'tcx>> + Copy>(
@@ -149,15 +153,15 @@ pub(crate) trait Namer<'tcx> {
         ty: T,
     ) -> T;
 
-    fn import_prelude_module(&mut self, module: PreludeModule) {
-        self.insert(Dependency::Builtin(module));
+    fn import_prelude_module(&self, module: PreludeModule) {
+        self.dependency(Dependency::Builtin(module));
     }
 
-    fn insert(&mut self, dep: Dependency<'tcx>) -> &Kind;
+    fn dependency(&self, dep: Dependency<'tcx>) -> &Kind;
 
     fn tcx(&self) -> TyCtxt<'tcx>;
 
-    fn span(&mut self, span: Span) -> Option<why3::declaration::Attribute>;
+    fn span(&self, span: Span) -> Option<why3::declaration::Attribute>;
 }
 
 impl<'tcx> Namer<'tcx> for CloneNames<'tcx> {
@@ -170,23 +174,47 @@ impl<'tcx> Namer<'tcx> for CloneNames<'tcx> {
         self.tcx().normalize_erasing_regions(self.typing_env, ty)
     }
 
-    fn insert(&mut self, key: Dependency<'tcx>) -> &Kind {
+    fn dependency(&self, key: Dependency<'tcx>) -> &Kind {
         let key = key.erase_regions(self.tcx);
-        CloneNames::insert(self, key)
+        self.insert(self.tcx, key)
     }
 
     fn tcx(&self) -> TyCtxt<'tcx> {
         self.tcx
     }
 
-    fn span(&mut self, span: Span) -> Option<why3::declaration::Attribute> {
+    fn span(&self, span: Span) -> Option<why3::declaration::Attribute> {
         let path = path_of_span(self.tcx, span, &self.span_mode)?;
-
         let cnt = self.spans.len();
-        let name = self.spans.entry(span).or_insert_with(|| {
-            Symbol::intern(&format!("s{}{cnt}", path.file_stem().unwrap().to_str().unwrap()))
+        let name = self.spans.insert(span, |_| {
+            Box::new((
+                Symbol::intern(&format!("s{}{cnt}", path.file_stem().unwrap().to_str().unwrap())),
+                cnt,
+            ))
         });
-        Some(Attribute::NamedSpan(name.to_string()))
+        Some(Attribute::NamedSpan(name.0.to_string()))
+    }
+}
+
+impl<'tcx> CloneNames<'tcx> {
+    fn insert(&self, tcx: TyCtxt<'tcx>, key: Dependency<'tcx>) -> &Kind {
+        self.names.insert(key, |_| {
+            if let Some((did, _)) = key.did()
+                && let Some(why3_modl) = get_builtin(tcx, did)
+            {
+                let qname = QName::from(why3_modl.as_str());
+                if qname.module.is_empty() {
+                    return Box::new(Kind::Named(Symbol::intern(&qname.name)));
+                } else {
+                    return Box::new(Kind::UsedBuiltin(qname));
+                }
+            }
+            Box::new(
+                key.base_ident(tcx).map_or(Kind::Unnamed, |base| {
+                    Kind::Named(self.counts.borrow_mut().freshen(base))
+                }),
+            )
+        })
     }
 }
 
@@ -203,25 +231,23 @@ impl<'tcx> Namer<'tcx> for Dependencies<'tcx> {
         self.tcx
     }
 
-    fn insert(&mut self, key: Dependency<'tcx>) -> &Kind {
+    fn dependency(&self, key: Dependency<'tcx>) -> &Kind {
         let key = key.erase_regions(self.tcx);
-        self.dep_set.insert(key);
-        self.names.insert(key)
+        self.dep_set.borrow_mut().insert(key);
+        self.names.dependency(key)
     }
 
-    fn span(&mut self, span: Span) -> Option<Attribute> {
+    fn span(&self, span: Span) -> Option<Attribute> {
         self.names.span(span)
     }
 }
 
-#[derive(Clone)]
 pub(crate) struct Dependencies<'tcx> {
     tcx: TyCtxt<'tcx>,
-
-    pub names: CloneNames<'tcx>,
+    names: CloneNames<'tcx>,
 
     // A hacky thing which is used to remember the dependncies we need to seed the expander with
-    dep_set: IndexSet<Dependency<'tcx>>,
+    dep_set: RefCell<IndexSet<Dependency<'tcx>>>,
 
     pub(crate) self_id: DefId,
     pub(crate) self_subst: GenericArgsRef<'tcx>,
@@ -232,60 +258,32 @@ pub(crate) struct NameSupply {
     name_counts: IndexMap<Symbol, usize>,
 }
 
-#[derive(Clone)]
-pub struct CloneNames<'tcx> {
+pub(crate) struct CloneNames<'tcx> {
     tcx: TyCtxt<'tcx>,
-    /// Freshens a symbol by appending a number to the end
-    counts: NameSupply,
-    /// Tracks the name given to each dependency
-    names: IndexMap<Dependency<'tcx>, Kind>,
-    /// Maps spans to a unique name
-    spans: IndexMap<Span, Symbol>,
     // To normalize during dependency stuff (deprecated)
     typing_env: TypingEnv<'tcx>,
-
     // Internal state, used to determine whether we should emit spans at all
     span_mode: SpanMode,
-}
-
-impl std::fmt::Debug for CloneNames<'_> {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        for (n, k) in &self.names {
-            writeln!(f, "{n:?} -> {k:?}")?;
-        }
 
-        Ok(())
-    }
+    /// Freshens a symbol by appending a number to the end
+    counts: RefCell<NameSupply>,
+    /// Tracks the name given to each dependency
+    names: OnceMap<Dependency<'tcx>, Box<Kind>>,
+    /// Maps spans to a unique name
+    spans: OnceMap<Span, Box<(Symbol, usize)>>,
 }
 
 impl<'tcx> CloneNames<'tcx> {
     fn new(tcx: TyCtxt<'tcx>, typing_env: TypingEnv<'tcx>, span_mode: SpanMode) -> Self {
         CloneNames {
             tcx,
+            typing_env,
+            span_mode,
             counts: Default::default(),
             names: Default::default(),
             spans: Default::default(),
-            typing_env,
-            span_mode,
         }
     }
-
-    fn insert(&mut self, key: Dependency<'tcx>) -> &Kind {
-        self.names.entry(key).or_insert_with(|| {
-            if let Some((did, _)) = key.did()
-                && let Some(why3_modl) = get_builtin(self.tcx, did)
-            {
-                let qname = QName::from(why3_modl.as_str());
-                if qname.module.is_empty() {
-                    return Kind::Named(Symbol::intern(&qname.name));
-                } else {
-                    return Kind::UsedBuiltin(qname);
-                }
-            }
-            key.base_ident(self.tcx)
-                .map_or(Kind::Unnamed, |base| Kind::Named(self.counts.freshen(base)))
-        })
-    }
 }
 
 impl NameSupply {
@@ -336,23 +334,27 @@ impl<'tcx> Dependencies<'tcx> {
         let names = CloneNames::new(ctx.tcx, ctx.typing_env(self_id), ctx.opts.span_mode.clone());
         debug!("cloning self: {:?}", self_id);
         let self_subst = erased_identity_for_item(ctx.tcx, self_id);
-        let mut deps =
+        let deps =
             Dependencies { tcx: ctx.tcx, self_id, self_subst, names, dep_set: Default::default() };
 
         let node = Dependency::Item(self_id, self_subst);
-        deps.names.insert(node);
+        deps.names.dependency(node);
         deps
     }
 
-    pub(crate) fn provide_deps(mut self, ctx: &mut Why3Generator<'tcx>) -> Vec<Decl> {
+    pub(crate) fn provide_deps(mut self, ctx: &Why3Generator<'tcx>) -> Vec<Decl> {
         trace!("emitting dependencies for {:?}", self.self_id);
         let mut decls = Vec::new();
 
         let typing_env = ctx.typing_env(self.self_id);
 
         let self_node = Dependency::Item(self.self_id, self.self_subst);
-        let graph =
-            Expander::new(&mut self.names, self_node, typing_env, self.dep_set.iter().copied());
+        let graph = Expander::new(
+            &mut self.names,
+            self_node,
+            typing_env,
+            self.dep_set.into_inner().into_iter(),
+        );
 
         // Update the clone graph with any new entries.
         let (graph, mut bodies) = graph.update_graph(ctx);
@@ -435,7 +437,8 @@ impl<'tcx> Dependencies<'tcx> {
             .names
             .spans
             .into_iter()
-            .filter_map(|(sp, name)| {
+            .sorted_by_key(|(_, b)| b.1)
+            .filter_map(|(sp, b)| {
                 let (path, start_line, start_column, end_line, end_column) =
                     if let Some(Attribute::Span(path, l1, c1, l2, c2)) = ctx.span_attr(sp) {
                         (path, l1, c1, l2, c2)
@@ -444,7 +447,7 @@ impl<'tcx> Dependencies<'tcx> {
                     };
 
                 Some(why3::declaration::Span {
-                    name: name.as_str().into(),
+                    name: b.0.as_str().into(),
                     path,
                     start_line,
                     start_column,
diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs
index fce10cb535..52d27929c7 100644
--- a/creusot/src/backend/clone_map/elaborator.rs
+++ b/creusot/src/backend/clone_map/elaborator.rs
@@ -1,4 +1,7 @@
-use std::collections::{HashMap, HashSet, VecDeque};
+use std::{
+    cell::RefCell,
+    collections::{HashMap, HashSet, VecDeque},
+};
 
 use crate::{
     backend::{
@@ -58,7 +61,7 @@ pub(super) struct Expander<'a, 'tcx> {
 
 struct ExpansionProxy<'a, 'tcx> {
     namer: &'a mut CloneNames<'tcx>,
-    expansion_queue: &'a mut VecDeque<(Dependency<'tcx>, Strength, Dependency<'tcx>)>,
+    expansion_queue: RefCell<&'a mut VecDeque<(Dependency<'tcx>, Strength, Dependency<'tcx>)>>,
     source: Dependency<'tcx>,
 }
 
@@ -71,17 +74,17 @@ impl<'a, 'tcx> Namer<'tcx> for ExpansionProxy<'a, 'tcx> {
         self.namer.normalize(ctx, ty)
     }
 
-    fn insert(&mut self, dep: Dependency<'tcx>) -> &Kind {
+    fn dependency(&self, dep: Dependency<'tcx>) -> &Kind {
         let dep = dep.erase_regions(self.tcx());
-        self.expansion_queue.push_back((self.source, Strength::Strong, dep));
-        self.namer.insert(dep)
+        self.expansion_queue.borrow_mut().push_back((self.source, Strength::Strong, dep));
+        self.namer.dependency(dep)
     }
 
     fn tcx(&self) -> TyCtxt<'tcx> {
         self.namer.tcx()
     }
 
-    fn span(&mut self, span: Span) -> Option<why3::declaration::Attribute> {
+    fn span(&self, span: Span) -> Option<why3::declaration::Attribute> {
         self.namer.span(span)
     }
 }
@@ -93,7 +96,7 @@ trait DepElab {
 
     fn expand<'tcx>(
         elab: &mut Expander<'_, 'tcx>,
-        ctx: &mut Why3Generator<'tcx>,
+        ctx: &Why3Generator<'tcx>,
         dep: Dependency<'tcx>,
     ) -> Vec<why3::declaration::Decl>;
 }
@@ -103,7 +106,7 @@ struct ProgElab;
 impl DepElab for ProgElab {
     fn expand<'tcx>(
         elab: &mut Expander<'_, 'tcx>,
-        ctx: &mut Why3Generator<'tcx>,
+        ctx: &Why3Generator<'tcx>,
         dep: Dependency<'tcx>,
     ) -> Vec<why3::declaration::Decl> {
         if let Dependency::Item(def_id, subst) = dep
@@ -118,7 +121,7 @@ impl DepElab for ProgElab {
 
         // Inline the body of closures and promoted
         let mut names = elab.namer(dep);
-        let name = names.insert(dep).ident();
+        let name = names.dependency(dep).ident();
 
         let bid = match dep {
             Dependency::Item(def_id, _) => BodyId { def_id: def_id.expect_local(), promoted: None },
@@ -133,15 +136,15 @@ impl DepElab for ProgElab {
 
 // What is the difference with `sig` below and `sigs` in logic?
 fn signature<'tcx>(
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     elab: &mut Expander<'_, 'tcx>,
     sig: PreSignature<'tcx>,
     dep: Dependency<'tcx>,
 ) -> Signature {
     let mut names = elab.namer(dep);
-    let name = names.insert(dep).ident();
     let (def_id, _) = dep.did().unwrap();
-    sig_to_why3(ctx, &mut names, name, sig, def_id)
+    let id = names.dependency(dep).ident();
+    sig_to_why3(ctx, &mut names, id, sig, def_id)
 }
 
 struct LogicElab;
@@ -149,7 +152,7 @@ struct LogicElab;
 impl DepElab for LogicElab {
     fn expand<'tcx>(
         elab: &mut Expander<'_, 'tcx>,
-        ctx: &mut Why3Generator<'tcx>,
+        ctx: &Why3Generator<'tcx>,
         dep: Dependency<'tcx>,
     ) -> Vec<why3::declaration::Decl> {
         assert!(matches!(dep, Dependency::Item(_, _) | Dependency::TyInvAxiom(_)));
@@ -178,7 +181,7 @@ impl DepElab for LogicElab {
         };
 
         if get_builtin(ctx.tcx, def_id).is_some() {
-            match elab.namer.insert(dep) {
+            match elab.namer.dependency(dep) {
                 Kind::Named(_) => return vec![],
                 Kind::UsedBuiltin(qname) => {
                     return vec![Decl::UseDecl(Use {
@@ -221,7 +224,7 @@ impl DepElab for LogicElab {
 // TODO Deprecate and fold into LogicElab
 fn expand_ty_inv_axiom<'tcx>(
     elab: &mut Expander<'_, 'tcx>,
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     ty: Ty<'tcx>,
 ) -> Vec<Decl> {
     let param_env = elab.typing_env;
@@ -232,7 +235,7 @@ fn expand_ty_inv_axiom<'tcx>(
     let rewrite = elab.rewrite;
     let exp = lower_pure(ctx, &mut names, &term);
     let axiom =
-        Axiom { name: names.insert(Dependency::TyInvAxiom(ty)).ident(), rewrite, axiom: exp };
+        Axiom { name: names.dependency(Dependency::TyInvAxiom(ty)).ident(), rewrite, axiom: exp };
     vec![Decl::Axiom(axiom)]
 }
 
@@ -241,7 +244,7 @@ struct TyElab;
 impl DepElab for TyElab {
     fn expand<'tcx>(
         elab: &mut Expander<'_, 'tcx>,
-        ctx: &mut Why3Generator<'tcx>,
+        ctx: &Why3Generator<'tcx>,
         dep: Dependency<'tcx>,
     ) -> Vec<why3::declaration::Decl> {
         let Dependency::Type(ty) = dep else { unreachable!() };
@@ -269,7 +272,7 @@ impl DepElab for TyElab {
                 for ty in subst.types() {
                     translate_ty(ctx, &mut names, DUMMY_SP, ty);
                 }
-                let Kind::UsedBuiltin(qname) = names.insert(dep) else { unreachable!() };
+                let Kind::UsedBuiltin(qname) = names.dependency(dep) else { unreachable!() };
                 vec![Decl::UseDecl(Use { as_: None, name: qname.module.clone(), export: false })]
             }
             TyKind::Adt(_, _) => {
@@ -299,13 +302,17 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
     }
 
     fn namer(&mut self, source: Dependency<'tcx>) -> ExpansionProxy<'_, 'tcx> {
-        ExpansionProxy { namer: self.namer, expansion_queue: &mut self.expansion_queue, source }
+        ExpansionProxy {
+            namer: self.namer,
+            expansion_queue: RefCell::new(&mut self.expansion_queue),
+            source,
+        }
     }
 
     /// Expand the graph with new entries
     pub fn update_graph(
         mut self,
-        ctx: &mut Why3Generator<'tcx>,
+        ctx: &Why3Generator<'tcx>,
     ) -> (DiGraphMap<Dependency<'tcx>, Strength>, HashMap<Dependency<'tcx>, Vec<Decl>>) {
         let mut visited = HashSet::new();
         while let Some((s, strength, mut t)) = self.expansion_queue.pop_front() {
@@ -332,7 +339,7 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
         (self.graph, self.dep_bodies)
     }
 
-    fn expand(&mut self, ctx: &mut Why3Generator<'tcx>, dep: Dependency<'tcx>) {
+    fn expand(&mut self, ctx: &Why3Generator<'tcx>, dep: Dependency<'tcx>) {
         expand_laws(self, ctx, dep);
 
         let decls = match dep {
@@ -341,8 +348,7 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
                 if ctx.is_logical(def_id) || matches!(ctx.item_type(def_id), ItemType::Constant) {
                     LogicElab::expand(self, ctx, dep)
                 } else if matches!(ctx.def_kind(def_id), DefKind::Field | DefKind::Variant) {
-                    let mut namer = self.namer(dep);
-                    namer.ty(ctx.parent(def_id), subst);
+                    self.namer(dep).ty(ctx.parent(def_id), subst);
                     vec![]
                 } else {
                     ProgElab::expand(self, ctx, dep)
@@ -383,7 +389,7 @@ fn traitref_of_item<'tcx>(
 
 fn expand_laws<'tcx>(
     elab: &mut Expander<'_, 'tcx>,
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     dep: Dependency<'tcx>,
 ) {
     let (self_did, self_subst) = elab.self_key.did().unwrap();
@@ -415,7 +421,7 @@ fn expand_laws<'tcx>(
     }
 }
 
-fn val(ctx: &mut Why3Generator, mut sig: Signature, kind: Option<DeclKind>) -> Vec<Decl> {
+fn val(ctx: &Why3Generator, mut sig: Signature, kind: Option<DeclKind>) -> Vec<Decl> {
     sig.contract.variant = Vec::new();
     if let Some(k) = kind {
         let ax = if !sig.contract.is_empty() { Some(spec_axiom(&sig)) } else { None };
@@ -441,7 +447,7 @@ fn val(ctx: &mut Why3Generator, mut sig: Signature, kind: Option<DeclKind>) -> V
 }
 
 fn resolve_term<'tcx>(
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     typing_env: TypingEnv<'tcx>,
     def_id: DefId,
     subst: GenericArgsRef<'tcx>,
@@ -474,7 +480,7 @@ fn resolve_term<'tcx>(
 }
 
 fn fn_once_postcond_term<'tcx>(
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     typing_env: TypingEnv<'tcx>,
     subst: GenericArgsRef<'tcx>,
 ) -> Option<Term<'tcx>> {
@@ -509,7 +515,7 @@ fn fn_once_postcond_term<'tcx>(
 }
 
 fn fn_mut_postcond_term<'tcx>(
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     typing_env: TypingEnv<'tcx>,
     subst: GenericArgsRef<'tcx>,
 ) -> Option<Term<'tcx>> {
@@ -551,7 +557,7 @@ fn fn_mut_postcond_term<'tcx>(
 }
 
 fn fn_postcond_term<'tcx>(
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     typing_env: TypingEnv<'tcx>,
     subst: GenericArgsRef<'tcx>,
 ) -> Option<Term<'tcx>> {
@@ -581,7 +587,7 @@ fn fn_postcond_term<'tcx>(
 // Returns a resolved and normalized term for a dependency.
 // Currently, it does not handle invariant axioms but otherwise returns all logical terms.
 fn term<'tcx>(
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     typing_env: TypingEnv<'tcx>,
     dep: Dependency<'tcx>,
 ) -> Option<Term<'tcx>> {
diff --git a/creusot/src/backend/logic.rs b/creusot/src/backend/logic.rs
index b2f3b30206..918898d43a 100644
--- a/creusot/src/backend/logic.rs
+++ b/creusot/src/backend/logic.rs
@@ -43,7 +43,7 @@ pub(crate) fn binders_to_args(binders: Vec<Binder>) -> (Vec<Ident>, Vec<Binder>)
 }
 
 pub(crate) fn translate_logic_or_predicate(
-    ctx: &mut Why3Generator,
+    ctx: &Why3Generator,
     def_id: DefId,
 ) -> Result<Option<FileModule>, CannotFetchThir> {
     let mut names = Dependencies::new(ctx, def_id);
@@ -60,7 +60,7 @@ pub(crate) fn translate_logic_or_predicate(
         );
     }
 
-    let name = names.value(names.self_id, names.self_subst).as_ident();
+    let name = names.item(names.self_id, names.self_subst).as_ident();
     let mut sig = signature_of(ctx, &mut names, name, def_id);
 
     if sig.contract.is_empty()
@@ -132,8 +132,8 @@ pub(crate) fn translate_logic_or_predicate(
 }
 
 pub(crate) fn lower_logical_defn<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     mut sig: Signature,
     kind: Option<DeclKind>,
     body: Term<'tcx>,
diff --git a/creusot/src/backend/logic/vcgen.rs b/creusot/src/backend/logic/vcgen.rs
index ab7ec870b4..bbb3a1f961 100644
--- a/creusot/src/backend/logic/vcgen.rs
+++ b/creusot/src/backend/logic/vcgen.rs
@@ -41,8 +41,8 @@ use why3::{
 /// 1. Conjunction: 2. Exists & Forall: 3. Function calls:
 
 struct VCGen<'a, 'tcx> {
-    ctx: RefCell<&'a mut Why3Generator<'tcx>>,
-    names: RefCell<&'a mut Dependencies<'tcx>>,
+    ctx: &'a Why3Generator<'tcx>,
+    names: &'a Dependencies<'tcx>,
     self_id: DefId,
     structurally_recursive: bool,
     typing_env: TypingEnv<'tcx>,
@@ -50,7 +50,7 @@ struct VCGen<'a, 'tcx> {
 }
 
 pub(super) fn vc<'tcx>(
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     names: &mut Dependencies<'tcx>,
     self_id: DefId,
     t: Term<'tcx>,
@@ -66,11 +66,11 @@ pub(super) fn vc<'tcx>(
         .collect();
     let gen = VCGen {
         typing_env: ctx.typing_env(self_id),
-        ctx: RefCell::new(ctx),
-        names: RefCell::new(names),
+        ctx,
+        names,
         self_id,
         structurally_recursive,
-        subst: RefCell::new(Default::default()),
+        subst: Default::default(),
     };
     gen.add_bounds(bounds);
     gen.build_vc(&t, &|exp| Ok(Exp::let_(dest.clone(), exp, post.clone())))
@@ -88,7 +88,7 @@ pub(super) fn vc<'tcx>(
 /// ``` match x { Cons(_, tl) => recursive((tl, 0).0) } ```
 ///
 /// This check can be extended in the future
-fn is_structurally_recursive(ctx: &mut Why3Generator<'_>, self_id: DefId, t: &Term<'_>) -> bool {
+fn is_structurally_recursive(ctx: &Why3Generator<'_>, self_id: DefId, t: &Term<'_>) -> bool {
     struct StructuralRecursion {
         smaller_than: HashMap<Symbol, Symbol>,
         self_id: DefId,
@@ -215,11 +215,11 @@ type PostCont<'a, 'tcx, A, R = Exp> = &'a dyn Fn(A) -> Result<R, VCError<'tcx>>;
 
 impl<'a, 'tcx> VCGen<'a, 'tcx> {
     fn lower_literal(&self, lit: &Literal<'tcx>) -> Exp {
-        lower_literal(*self.ctx.borrow_mut(), *self.names.borrow_mut(), lit)
+        lower_literal(self.ctx, self.names, lit)
     }
 
     fn lower_pure(&self, lit: &Term<'tcx>) -> Exp {
-        lower_pure(*self.ctx.borrow_mut(), *self.names.borrow_mut(), lit)
+        lower_pure(self.ctx, self.names, lit)
     }
 
     fn build_vc(&self, t: &Term<'tcx>, k: PostCont<'_, 'tcx, Exp>) -> Result<Exp, VCError<'tcx>> {
@@ -236,9 +236,9 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             // Items are just global names so
             // VC(i, Q) = Q(i)
             TermKind::Item(id, sub) => {
-                let item_name = self.names.borrow_mut().value(*id, sub);
+                let item_name = self.names.item(*id, sub);
 
-                if get_builtin(self.ctx.borrow().tcx, *id).is_some() {
+                if get_builtin(self.ctx.tcx, *id).is_some() {
                     // Builtins can leverage Why3 polymorphism and sometimes can cause typeck errors in why3 due to ambiguous type variables so lets fix the type now.
                     k(Exp::qvar(item_name).ascribe(self.ty(t.ty)))
                 } else {
@@ -253,25 +253,18 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             //  pre(f)(a0..an) /\ variant(f)(a0..an) /\ (post(f)(a0..an, F(a0..an)) -> Q(F a0..an))
             // ))
             TermKind::Call { id, subst, args } => self.build_vc_slice(args, &|args| {
-                let tcx = self.ctx.borrow().tcx;
-                let pre_sig = EarlyBinder::bind(self.ctx.borrow_mut().sig(*id).clone())
-                    .instantiate(tcx, subst);
+                let pre_sig =
+                    EarlyBinder::bind(self.ctx.sig(*id).clone()).instantiate(self.ctx.tcx, subst);
 
-                let pre_sig = pre_sig.normalize(tcx, self.typing_env);
+                let pre_sig = pre_sig.normalize(self.ctx.tcx, self.typing_env);
                 let arg_subst = pre_sig
                     .inputs
                     .iter()
                     .zip(args.clone())
                     .map(|(nm, res)| (ident_of(nm.0), res))
                     .collect();
-                let fname = self.names.borrow_mut().value(*id, subst);
-                let mut sig = sig_to_why3(
-                    *self.ctx.borrow_mut(),
-                    *self.names.borrow_mut(),
-                    "".into(),
-                    pre_sig,
-                    *id,
-                );
+                let fname = self.names.item(*id, subst);
+                let mut sig = sig_to_why3(self.ctx, self.names, "".into(), pre_sig, *id);
                 sig.contract.subst(&arg_subst);
                 let variant =
                     if *id == self.self_id { self.build_variant(&args)? } else { Exp::mk_true() };
@@ -349,16 +342,10 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             TermKind::Tuple { fields } => self.build_vc_slice(fields, &|flds| k(Exp::Tuple(flds))),
             // Same as for tuples
             TermKind::Constructor { variant, fields, .. } => {
-                let ty =
-                    self.ctx.borrow().normalize_erasing_regions(self.typing_env, t.creusot_ty());
+                let ty = self.ctx.normalize_erasing_regions(self.typing_env, t.creusot_ty());
                 let TyKind::Adt(adt, subst) = ty.kind() else { unreachable!() };
                 self.build_vc_slice(fields, &|fields| {
-                    let ctor = constructor(
-                        *self.names.borrow_mut(),
-                        fields,
-                        adt.variant(*variant).def_id,
-                        subst,
-                    );
+                    let ctor = constructor(self.names, fields, adt.variant(*variant).def_id, subst);
                     k(ctor)
                 })
             }
@@ -410,14 +397,13 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             }),
             // VC(A.f, Q) = VC(A, |a| Q(a.f))
             TermKind::Projection { lhs, name } => {
-                let ty =
-                    self.ctx.borrow().normalize_erasing_regions(self.typing_env, lhs.creusot_ty());
+                let ty = self.ctx.normalize_erasing_regions(self.typing_env, lhs.creusot_ty());
                 let field = match ty.kind() {
                     TyKind::Closure(did, substs) => {
-                        self.names.borrow_mut().field(*did, substs, *name).as_ident()
+                        self.names.field(*did, substs, *name).as_ident()
                     }
                     TyKind::Adt(def, substs) => {
-                        self.names.borrow_mut().field(def.did(), substs, *name).as_ident()
+                        self.names.field(def.did(), substs, *name).as_ident()
                     }
                     TyKind::Tuple(f) => {
                         let mut fields = vec![why3::exp::Pattern::Wildcard; f.len()];
@@ -468,9 +454,9 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             Pattern::Constructor { variant, fields, substs } => {
                 let fields =
                     fields.iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect();
-                let substs = self.ctx.borrow().normalize_erasing_regions(self.typing_env, *substs);
-                if self.ctx.borrow().def_kind(variant) == DefKind::Variant {
-                    Pat::ConsP(self.names.borrow_mut().constructor(*variant, substs), fields)
+                let substs = self.ctx.normalize_erasing_regions(self.typing_env, *substs);
+                if self.ctx.def_kind(variant) == DefKind::Variant {
+                    Pat::ConsP(self.names.constructor(*variant, substs), fields)
                 } else if fields.is_empty() {
                     Pat::TupleP(vec![])
                 } else {
@@ -479,13 +465,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
                             .into_iter()
                             .enumerate()
                             .map(|(i, f)| {
-                                (
-                                    self.names
-                                        .borrow_mut()
-                                        .field(*variant, substs, i.into())
-                                        .as_ident(),
-                                    f,
-                                )
+                                (self.names.field(*variant, substs, i.into()).as_ident(), f)
                             })
                             .filter(|(_, f)| !matches!(f, Pat::Wildcard))
                             .collect(),
@@ -557,11 +537,11 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
     }
 
     fn ty(&self, ty: Ty<'tcx>) -> Type {
-        translate_ty(*self.ctx.borrow_mut(), *self.names.borrow_mut(), rustc_span::DUMMY_SP, ty)
+        translate_ty(self.ctx, self.names, rustc_span::DUMMY_SP, ty)
     }
 
     fn self_sig(&self) -> Signature {
-        signature_of(*self.ctx.borrow_mut(), *self.names.borrow_mut(), "".into(), self.self_id)
+        signature_of(self.ctx, self.names, "".into(), self.self_id)
     }
 
     // Generates the expression to test the validity of the variant for a recursive call.
@@ -574,7 +554,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
         if self.structurally_recursive {
             return Ok(Exp::mk_true());
         }
-        let variant = self.ctx.borrow_mut().sig(self.self_id).contract.variant.clone();
+        let variant = self.ctx.sig(self.self_id).contract.variant.clone();
         let Some(variant) = variant else { return Ok(Exp::mk_false()) };
 
         let top_level_args = self.top_level_args();
@@ -584,8 +564,8 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
         let orig_variant = self.self_sig().contract.variant.remove(0);
         let mut rec_var_exp = orig_variant.clone();
         rec_var_exp.subst(&mut subst);
-        if is_int(self.ctx.borrow().tcx, variant.creusot_ty()) {
-            self.names.borrow_mut().import_prelude_module(PreludeModule::Int);
+        if is_int(self.ctx.tcx, variant.creusot_ty()) {
+            self.names.import_prelude_module(PreludeModule::Int);
             Ok(Exp::BinaryOp(BinOp::Le, Box::new(Exp::int(0)), Box::new(orig_variant.clone()))
                 .log_and(Exp::BinaryOp(BinOp::Lt, Box::new(rec_var_exp), Box::new(orig_variant))))
         } else {
diff --git a/creusot/src/backend/optimization/invariants.rs b/creusot/src/backend/optimization/invariants.rs
index f50dbf8456..8d7ca2dc07 100644
--- a/creusot/src/backend/optimization/invariants.rs
+++ b/creusot/src/backend/optimization/invariants.rs
@@ -27,7 +27,7 @@ use crate::translation::fmir::{Block, FmirVisitor, Place, RValue, Statement, Ter
 /// (1) types with invariants being mutated inside of a loop
 /// (2) mutable borrows being mutated inside of a loop.
 
-pub fn infer_proph_invariants<'tcx>(ctx: &mut TranslationCtx<'tcx>, body: &mut fmir::Body<'tcx>) {
+pub fn infer_proph_invariants<'tcx>(ctx: &TranslationCtx<'tcx>, body: &mut fmir::Body<'tcx>) {
     let graph = node_graph(body);
 
     let wto = weak_topological_order(&graph, START_BLOCK);
diff --git a/creusot/src/backend/place.rs b/creusot/src/backend/place.rs
index e8bc344109..98b2b1dfdb 100644
--- a/creusot/src/backend/place.rs
+++ b/creusot/src/backend/place.rs
@@ -28,7 +28,7 @@ use super::program::{IntermediateStmt, LoweringState};
 /// [(_1 as Some).0] = X   ---> let _1 = (let Some(a) = _1 in Some(X))
 /// (* (* _1).2) = X ---> let _1 = { _1 with current = { * _1 with current = [(**_1).2 = X] }}
 pub(crate) fn create_assign_inner<'tcx, N: Namer<'tcx>>(
-    lower: &mut LoweringState<'_, 'tcx, N>,
+    lower: &LoweringState<'_, 'tcx, N>,
     lhs: &Place<'tcx>,
     rhs: Exp,
     istmts: &mut Vec<IntermediateStmt>,
@@ -56,7 +56,7 @@ impl<'a> Focus<'a> {
 type Constructor<'a> = Box<dyn FnOnce(&mut Vec<IntermediateStmt>, Exp) -> Exp + 'a>;
 
 pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
-    lower: &'a RefCell<&'a mut LoweringState<'_, 'tcx, N>>,
+    lower: &'a LoweringState<'_, 'tcx, N>,
     istmts: &mut Vec<IntermediateStmt>,
     mut place_ty: PlaceTy<'tcx>,
     // The term holding the currently 'focused' portion of the place
@@ -87,15 +87,14 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
                         .fields
                         .iter()
                         .map(|f| {
-                            let low = &mut *lower.borrow_mut();
                             Param::Term(
-                                low.fresh_from(format!("r{}", f.name)),
-                                low.ty(f.ty(low.ctx.tcx, subst)),
+                                lower.fresh_from(format!("r{}", f.name)),
+                                lower.ty(f.ty(lower.ctx.tcx, subst)),
                             )
                         })
                         .collect();
 
-                    let acc_name = lower.borrow_mut().names.eliminator(variant.def_id, subst);
+                    let acc_name = lower.names.eliminator(variant.def_id, subst);
                     let args = vec![Arg::Term(focus.call(istmts))];
                     istmts.push(IntermediateStmt::Call(
                         fields.clone(),
@@ -107,8 +106,7 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
                     focus = Focus::new(|_| foc);
 
                     constructor = Box::new(|is, t| {
-                        let constr =
-                            Exp::qvar(lower.borrow_mut().names.constructor(variant.def_id, subst));
+                        let constr = Exp::qvar(lower.names.constructor(variant.def_id, subst));
                         let mut fields: Vec<_> =
                             fields.into_iter().map(|f| Exp::var(f.as_term().0.clone())).collect();
                         fields[ix.as_usize()] = t;
@@ -121,19 +119,12 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
                     let focus1 = focus.clone();
 
                     focus = Focus::new(move |is| {
-                        focus.call(is).field(
-                            &lower.borrow_mut().names.field(def.did(), subst, *ix).as_ident(),
-                        )
+                        focus.call(is).field(&lower.names.field(def.did(), subst, *ix).as_ident())
                     });
 
                     constructor = Box::new(move |is, t| {
                         let updates = vec![(
-                            lower
-                                .borrow_mut()
-                                .names
-                                .field(def.did(), subst, *ix)
-                                .as_ident()
-                                .to_string(),
+                            lower.names.field(def.did(), subst, *ix).as_ident().to_string(),
                             t,
                         )];
                         if def.all_fields().count() == 1 {
@@ -148,7 +139,7 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
                     let focus1 = focus.clone();
 
                     focus = Focus::new(move |is| {
-                        let var = lower.borrow_mut().fresh_from("r");
+                        let var = lower.fresh_from("r");
                         let mut pat = vec![Wildcard; fields.len()];
                         pat[ix.as_usize()] = VarP(var.clone());
                         Let {
@@ -160,7 +151,7 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
 
                     constructor = Box::new(move |is, t| {
                         let var_names: Vec<_> =
-                            fields.iter().map(|_| lower.borrow_mut().fresh_from("r")).collect();
+                            fields.iter().map(|_| lower.fresh_from("r")).collect();
 
                         let mut field_pats =
                             var_names.clone().into_iter().map(VarP).collect::<Vec<_>>();
@@ -182,16 +173,12 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
                     let focus1 = focus.clone();
 
                     focus = Focus::new(move |is| {
-                        focus
-                            .call(is)
-                            .field(&lower.borrow_mut().names.field(*id, subst, *ix).as_ident())
+                        focus.call(is).field(&lower.names.field(*id, subst, *ix).as_ident())
                     });
 
                     constructor = Box::new(move |is, t| {
-                        let updates = vec![(
-                            lower.borrow_mut().names.field(*id, subst, *ix).as_ident().to_string(),
-                            t,
-                        )];
+                        let updates =
+                            vec![(lower.names.field(*id, subst, *ix).as_ident().to_string(), t)];
 
                         if subst.as_closure().upvar_tys().len() == 1 {
                             constructor(is, Exp::Record { fields: updates })
@@ -204,9 +191,9 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
                 _ => todo!("place: {:?}", place_ty.ty.kind()),
             },
             Index(ix) => {
-                let elt_ty = projection_ty(place_ty, lower.borrow().ctx.tcx, *elem);
-                let elt_ty = lower.borrow_mut().ty(elt_ty.ty);
-                let ty = lower.borrow_mut().ty(place_ty.ty);
+                let elt_ty = projection_ty(place_ty, lower.ctx.tcx, *elem);
+                let elt_ty = lower.ty(elt_ty.ty);
+                let ty = lower.ty(place_ty.ty);
                 // TODO: Use [_] syntax
                 let ix_exp = Exp::var(Ident::build(ix.as_str()));
 
@@ -214,7 +201,7 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
                 let elt_ty1 = elt_ty.clone();
                 let ix_exp1 = ix_exp.clone();
                 focus = Focus::new(move |is| {
-                    let result = lower.borrow_mut().fresh_from("r");
+                    let result = lower.fresh_from("r");
                     let foc = focus.call(is);
                     is.push(IntermediateStmt::Call(
                         vec![Param::Term(result.clone(), elt_ty1.clone())],
@@ -226,7 +213,7 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
                 });
 
                 constructor = Box::new(move |is, t| {
-                    let out = lower.borrow_mut().fresh_from("r");
+                    let out = lower.fresh_from("r");
                     let rhs = t;
                     let foc = focus1.call(is);
 
@@ -245,7 +232,7 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
             OpaqueCast(_) => todo!(),
             Subtype(_) => todo!(),
         }
-        place_ty = projection_ty(place_ty, lower.borrow().ctx.tcx, *elem);
+        place_ty = projection_ty(place_ty, lower.ctx.tcx, *elem);
     }
 
     (place_ty, focus, constructor)
@@ -257,9 +244,8 @@ pub(crate) fn rplace_to_expr<'tcx, N: Namer<'tcx>>(
     istmts: &mut Vec<IntermediateStmt>,
 ) -> Exp {
     let place_ty = PlaceTy::from_ty(lower.locals[&pl.local].ty);
-    let lower = RefCell::new(lower);
     let (_, rhs, _) = projections_to_expr(
-        &lower,
+        lower,
         istmts,
         place_ty,
         Focus::new(|_| Exp::var(ident_of(pl.local))),
@@ -270,15 +256,14 @@ pub(crate) fn rplace_to_expr<'tcx, N: Namer<'tcx>>(
 }
 
 fn lplace_to_expr<'tcx, N: Namer<'tcx>>(
-    lower: &mut LoweringState<'_, 'tcx, N>,
+    lower: &LoweringState<'_, 'tcx, N>,
     pl: &Place<'tcx>,
     rhs: Exp,
     istmts: &mut Vec<IntermediateStmt>,
 ) -> Exp {
     let place_ty = PlaceTy::from_ty(lower.locals[&pl.local].ty);
-    let lower = RefCell::new(lower);
     let (_, _, constructor) = projections_to_expr(
-        &lower,
+        lower,
         istmts,
         place_ty,
         Focus::new(|_| Exp::var(ident_of(pl.local))),
diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs
index 4a9a0d1dfa..f3356ef5aa 100644
--- a/creusot/src/backend/program.rs
+++ b/creusot/src/backend/program.rs
@@ -46,7 +46,7 @@ use why3::{
 };
 
 pub(crate) fn translate_function<'tcx, 'sess>(
-    ctx: &mut Why3Generator<'tcx>,
+    ctx: &Why3Generator<'tcx>,
     def_id: DefId,
 ) -> Option<FileModule> {
     let mut names = Dependencies::new(ctx, def_id);
@@ -55,7 +55,7 @@ pub(crate) fn translate_function<'tcx, 'sess>(
         return None;
     }
 
-    let name = names.value(names.self_id, names.self_subst).as_ident();
+    let name = names.item(names.self_id, names.self_subst).as_ident();
     let body = Decl::Coma(to_why(ctx, &mut names, name, BodyId::new(def_id.expect_local(), None)));
 
     let mut decls = names.provide_deps(ctx);
@@ -72,7 +72,7 @@ pub(crate) fn translate_function<'tcx, 'sess>(
     Some(FileModule { path, modl: Module { name, decls, attrs, meta } })
 }
 
-pub fn val<'tcx>(_: &mut Why3Generator<'tcx>, sig: Signature) -> Decl {
+pub fn val<'tcx>(_: &Why3Generator<'tcx>, sig: Signature) -> Decl {
     let params = sig
         .args
         .into_iter()
@@ -129,8 +129,8 @@ pub(crate) fn node_graph(x: &Body) -> petgraph::graphmap::DiGraphMap<BasicBlock,
 }
 
 pub fn to_why<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     name: Ident,
     body_id: BodyId,
 ) -> coma::Defn {
@@ -241,8 +241,8 @@ pub fn to_why<'tcx, N: Namer<'tcx>>(
 
 fn component_to_defn<'tcx, N: Namer<'tcx>>(
     body: &mut Body<'tcx>,
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     def_id: LocalDefId,
     c: Component<BasicBlock>,
 ) -> coma::Defn {
@@ -275,29 +275,27 @@ fn component_to_defn<'tcx, N: Namer<'tcx>>(
 }
 
 pub(crate) struct LoweringState<'a, 'tcx, N: Namer<'tcx>> {
-    pub(super) ctx: &'a mut Why3Generator<'tcx>,
-    pub(super) names: &'a mut N,
+    pub(super) ctx: &'a Why3Generator<'tcx>,
+    pub(super) names: &'a N,
     pub(super) locals: &'a LocalDecls<'tcx>,
-    pub(super) name_supply: NameSupply,
+    pub(super) name_supply: RefCell<NameSupply>,
     pub(super) def_id: LocalDefId,
 }
 
 impl<'a, 'tcx, N: Namer<'tcx>> LoweringState<'a, 'tcx, N> {
-    pub(super) fn ty(&mut self, ty: Ty<'tcx>) -> Type {
+    pub(super) fn ty(&self, ty: Ty<'tcx>) -> Type {
         translate_ty(self.ctx, self.names, DUMMY_SP, ty)
     }
 
-    fn assignment(&mut self, lhs: &Place<'tcx>, rhs: Term, istmts: &mut Vec<IntermediateStmt>) {
+    fn assignment(&self, lhs: &Place<'tcx>, rhs: Term, istmts: &mut Vec<IntermediateStmt>) {
         place::create_assign_inner(self, lhs, rhs, istmts)
     }
 
-    fn reset_names(&mut self) {}
-
-    pub(super) fn fresh_sym_from(&mut self, base: impl AsRef<str>) -> Symbol {
-        self.name_supply.freshen(Symbol::intern(base.as_ref()))
+    pub(super) fn fresh_sym_from(&self, base: impl AsRef<str>) -> Symbol {
+        self.name_supply.borrow_mut().freshen(Symbol::intern(base.as_ref()))
     }
 
-    pub(super) fn fresh_from(&mut self, base: impl AsRef<str>) -> Ident {
+    pub(super) fn fresh_from(&self, base: impl AsRef<str>) -> Ident {
         self.fresh_sym_from(base).to_string().into()
     }
 }
@@ -390,7 +388,7 @@ impl<'tcx> RValue<'tcx> {
             }
             RValue::Constructor(id, subst, args) => {
                 if lower.ctx.def_kind(id) == DefKind::Closure {
-                    lower.names.insert(Dependency::Item(id, subst));
+                    lower.names.dependency(Dependency::Item(id, subst));
                 }
                 let args = args.into_iter().map(|a| a.to_why(lower, istmts)).collect();
                 constructor(lower.names, args, id, subst)
@@ -618,8 +616,8 @@ impl<'tcx> Terminator<'tcx> {
 impl<'tcx> Branches<'tcx> {
     fn to_why<N: Namer<'tcx>>(
         self,
-        ctx: &mut Why3Generator<'tcx>,
-        names: &mut N,
+        ctx: &Why3Generator<'tcx>,
+        names: &N,
         discr: Exp,
     ) -> coma::Expr {
         match self {
@@ -662,8 +660,8 @@ fn mk_goto(bb: BasicBlock) -> coma::Expr {
 }
 
 fn mk_adt_switch<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     adt: AdtDef<'tcx>,
     subst: GenericArgsRef<'tcx>,
     discr: Exp,
@@ -740,7 +738,6 @@ impl<'tcx> Block<'tcx> {
         let mut statements = vec![];
 
         for (ix, s) in self.stmts.into_iter().enumerate() {
-            lower.reset_names();
             let stmt = s.to_why(lower);
 
             let body = assemble_intermediates(
@@ -887,8 +884,6 @@ impl<'tcx> Statement<'tcx> {
                     None
                 };
 
-                let lower = RefCell::new(lower);
-
                 let func = match bor_kind {
                     BorrowKind::Mut => coma::Expr::Symbol("Borrow.borrow_mut".into()),
                     BorrowKind::Final(_) => coma::Expr::Symbol("Borrow.borrow_final".into()),
@@ -901,7 +896,7 @@ impl<'tcx> Statement<'tcx> {
                 if let BorrowKind::Final(deref_index) = bor_kind {
                     let (original_borrow_ty, original_borrow, original_borrow_constr) =
                         place::projections_to_expr(
-                            &lower,
+                            lower,
                             &mut istmts,
                             rhs_local_ty,
                             place::Focus::new(|_| Exp::var(ident_of(rhs.local))),
@@ -909,7 +904,7 @@ impl<'tcx> Statement<'tcx> {
                             &rhs.projection[..deref_index],
                         );
                     let (_, foc, constr) = place::projections_to_expr(
-                        &lower,
+                        lower,
                         &mut istmts,
                         original_borrow_ty,
                         original_borrow.clone(),
@@ -954,7 +949,7 @@ impl<'tcx> Statement<'tcx> {
 
                 let borrow_call = IntermediateStmt::call("_ret'".into(), lhs_ty_low, func, args);
                 istmts.push(borrow_call);
-                lower.borrow_mut().assignment(&lhs, Exp::var("_ret'"), &mut istmts);
+                lower.assignment(&lhs, Exp::var("_ret'"), &mut istmts);
 
                 let reassign = Exp::var("_ret'").field("final");
 
@@ -978,7 +973,7 @@ impl<'tcx> Statement<'tcx> {
                 lower.assignment(&dest, Exp::var("_ret'"), &mut istmts);
             }
             Statement::Resolve { did, subst, pl } => {
-                let rp = Exp::qvar(lower.names.value(did, subst));
+                let rp = Exp::qvar(lower.names.item(did, subst));
                 let loc = pl.local;
 
                 let bound = lower.fresh_sym_from("x");
@@ -1145,12 +1140,12 @@ fn func_call_to_why3<'tcx, N: Namer<'tcx>>(
         args.into_iter().map(|a| a.to_why(lower, istmts)).map(|a| coma::Arg::Term(a)).collect()
     };
 
-    let fname = lower.names.value(id, subst);
+    let fname = lower.names.item(id, subst);
 
     (coma::Expr::Symbol(fname), args)
 }
 
-pub(crate) fn binop_to_binop<'tcx, N: Namer<'tcx>>(names: &mut N, ty: Ty, op: mir::BinOp) -> QName {
+pub(crate) fn binop_to_binop<'tcx, N: Namer<'tcx>>(names: &N, ty: Ty, op: mir::BinOp) -> QName {
     let prelude: PreludeModule = match ty.kind() {
         TyKind::Int(ity) => int_to_prelude(*ity),
         TyKind::Uint(uty) => uint_to_prelude(*uty),
diff --git a/creusot/src/backend/signature.rs b/creusot/src/backend/signature.rs
index d424a70d83..e2445888a1 100644
--- a/creusot/src/backend/signature.rs
+++ b/creusot/src/backend/signature.rs
@@ -16,8 +16,8 @@ use crate::{
 use super::{logic::function_call, term::lower_pure, Namer, Why3Generator};
 
 pub(crate) fn signature_of<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     name: Ident,
     def_id: DefId,
 ) -> Signature {
@@ -27,8 +27,8 @@ pub(crate) fn signature_of<'tcx, N: Namer<'tcx>>(
 }
 
 pub(crate) fn sig_to_why3<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     name: Ident,
     pre_sig: PreSignature<'tcx>,
     // FIXME: Get rid of this def id
@@ -74,8 +74,8 @@ pub(crate) fn sig_to_why3<'tcx, N: Namer<'tcx>>(
 }
 
 fn lower_condition<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     cond: Condition<'tcx>,
 ) -> why3::declaration::Condition {
     why3::declaration::Condition { exp: lower_pure(ctx, names, &cond.term), expl: cond.expl }
@@ -83,8 +83,8 @@ fn lower_condition<'tcx, N: Namer<'tcx>>(
 
 fn contract_to_why3<'tcx, N: Namer<'tcx>>(
     pre: PreContract<'tcx>,
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
 ) -> Contract {
     let mut out = Contract::new();
     for cond in pre.requires.into_iter() {
diff --git a/creusot/src/backend/term.rs b/creusot/src/backend/term.rs
index 3a9a6bf98d..2e777f732a 100644
--- a/creusot/src/backend/term.rs
+++ b/creusot/src/backend/term.rs
@@ -19,8 +19,8 @@ use why3::{
 };
 
 pub(crate) fn lower_pure<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     term: &Term<'tcx>,
 ) -> Exp {
     let span = term.span;
@@ -34,16 +34,16 @@ pub(crate) fn lower_pure<'tcx, N: Namer<'tcx>>(
 }
 
 pub(crate) fn lower_pat<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     pat: &Pattern<'tcx>,
 ) -> Pat {
     Lower { ctx, names }.lower_pat(pat)
 }
 
 struct Lower<'a, 'tcx, N: Namer<'tcx>> {
-    ctx: &'a mut Why3Generator<'tcx>,
-    names: &'a mut N,
+    ctx: &'a Why3Generator<'tcx>,
+    names: &'a N,
 }
 impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
     fn lower_term(&mut self, term: &Term<'tcx>) -> Exp {
@@ -53,7 +53,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
             TermKind::Item(id, subst) => {
                 let method = (*id, *subst);
                 debug!("resolved_method={:?}", method);
-                let clone = self.names.value(*id, subst);
+                let clone = self.names.item(*id, subst);
                 let item = match self.ctx.type_of(id).instantiate_identity().kind() {
                     TyKind::FnDef(_, _) => Exp::Tuple(Vec::new()),
                     _ => Exp::qvar(clone),
@@ -103,7 +103,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 }
 
                 self.lookup_builtin(method, &mut args).unwrap_or_else(|| {
-                    let clone = self.names.value(method.0, method.1);
+                    let clone = self.names.item(method.0, method.1);
                     Exp::qvar(clone).app(args)
                 })
             }
@@ -222,14 +222,14 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
             }
             TermKind::Precondition { item, args, params } => {
                 let params: Vec<_> = params.iter().map(|p| self.lower_term(p)).collect();
-                let mut sym = self.names.value(*item, args);
+                let mut sym = self.names.item(*item, args);
                 sym.name = format!("{}'pre", &*sym.name).into();
 
                 Exp::qvar(sym).app(params)
             }
             TermKind::Postcondition { item, args, params } => {
                 let params: Vec<_> = params.iter().map(|p| self.lower_term(p)).collect();
-                let mut sym = self.names.value(*item, args);
+                let mut sym = self.names.item(*item, args);
                 sym.name = format!("{}'post'return'", &*sym.name).into();
                 Exp::qvar(sym).app(params)
             }
@@ -289,7 +289,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
         let substs = method.1;
 
         if get_builtin(self.ctx.tcx, def_id).is_some() {
-            return Some(Exp::qvar(self.names.value(def_id, substs)).app(args.clone()));
+            return Some(Exp::qvar(self.names.item(def_id, substs)).app(args.clone()));
         }
         None
     }
@@ -303,8 +303,8 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
 }
 
 pub(crate) fn lower_literal<'tcx, N: Namer<'tcx>>(
-    _: &mut TranslationCtx<'tcx>,
-    names: &mut N,
+    _: &TranslationCtx<'tcx>,
+    names: &N,
     lit: &Literal<'tcx>,
 ) -> Exp {
     match *lit {
@@ -321,7 +321,7 @@ pub(crate) fn lower_literal<'tcx, N: Namer<'tcx>>(
         Literal::Bool(true) => Constant::const_true().into(),
         Literal::Bool(false) => Constant::const_false().into(),
         Literal::Function(id, subst) => {
-            names.value(id, subst);
+            names.item(id, subst);
             Exp::Tuple(Vec::new())
         }
         Literal::Float(ref f, fty) => {
diff --git a/creusot/src/backend/traits.rs b/creusot/src/backend/traits.rs
index fec336fbda..2b8e41b72b 100644
--- a/creusot/src/backend/traits.rs
+++ b/creusot/src/backend/traits.rs
@@ -6,7 +6,7 @@ use crate::{
 use rustc_hir::def_id::DefId;
 use why3::declaration::{Decl, Goal, Module};
 
-pub(crate) fn lower_impl<'tcx>(ctx: &mut Why3Generator<'tcx>, def_id: DefId) -> Vec<FileModule> {
+pub(crate) fn lower_impl<'tcx>(ctx: &Why3Generator<'tcx>, def_id: DefId) -> Vec<FileModule> {
     let data = ctx.trait_impl(def_id).clone();
     let mut res = vec![];
 
diff --git a/creusot/src/backend/ty.rs b/creusot/src/backend/ty.rs
index d87b0908ef..5e21630fe3 100644
--- a/creusot/src/backend/ty.rs
+++ b/creusot/src/backend/ty.rs
@@ -19,8 +19,8 @@ use why3::{
 };
 
 pub(crate) fn translate_ty<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     span: Span,
     ty: Ty<'tcx>,
 ) -> MlT {
@@ -127,8 +127,8 @@ pub(crate) fn translate_ty<'tcx, N: Namer<'tcx>>(
 }
 
 fn translate_projection_ty<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     pty: &AliasTy<'tcx>,
 ) -> MlT {
     let ty = Ty::new_alias(ctx.tcx, AliasTyKind::Projection, *pty);
@@ -140,8 +140,8 @@ fn translate_projection_ty<'tcx, N: Namer<'tcx>>(
 }
 
 pub(crate) fn translate_closure_ty<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     did: DefId,
     subst: GenericArgsRef<'tcx>,
 ) -> Option<TyDecl> {
@@ -172,8 +172,8 @@ pub(crate) fn translate_closure_ty<'tcx, N: Namer<'tcx>>(
 //
 // Mutually recursive types are translated separately, are later merged by the elaborator
 pub(crate) fn translate_tydecl<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     (did, subst): (DefId, GenericArgsRef<'tcx>),
     typing_env: TypingEnv<'tcx>,
 ) -> Vec<Decl> {
@@ -228,8 +228,8 @@ pub(crate) fn translate_tydecl<'tcx, N: Namer<'tcx>>(
 }
 
 pub(crate) fn eliminator<'tcx, N: Namer<'tcx>>(
-    ctx: &mut Why3Generator<'tcx>,
-    names: &mut N,
+    ctx: &Why3Generator<'tcx>,
+    names: &N,
     variant_id: DefId,
     subst: GenericArgsRef<'tcx>,
 ) -> Decl {
@@ -317,7 +317,7 @@ pub(crate) fn eliminator<'tcx, N: Namer<'tcx>>(
 }
 
 pub(crate) fn constructor<'tcx, N: Namer<'tcx>>(
-    names: &mut N,
+    names: &N,
     fields: Vec<Exp>,
     did: DefId,
     subst: GenericArgsRef<'tcx>,
@@ -343,7 +343,7 @@ pub(crate) fn constructor<'tcx, N: Namer<'tcx>>(
     }
 }
 
-pub(crate) fn intty_to_ty<'tcx, N: Namer<'tcx>>(names: &mut N, ity: IntTy) -> MlT {
+pub(crate) fn intty_to_ty<'tcx, N: Namer<'tcx>>(names: &N, ity: IntTy) -> MlT {
     names.import_prelude_module(int_to_prelude(ity));
     match ity {
         IntTy::Isize => MlT::TConstructor("isize".into()),
@@ -355,7 +355,7 @@ pub(crate) fn intty_to_ty<'tcx, N: Namer<'tcx>>(names: &mut N, ity: IntTy) -> Ml
     }
 }
 
-pub(crate) fn uintty_to_ty<'tcx, N: Namer<'tcx>>(names: &mut N, uty: UintTy) -> MlT {
+pub(crate) fn uintty_to_ty<'tcx, N: Namer<'tcx>>(names: &N, uty: UintTy) -> MlT {
     names.import_prelude_module(uint_to_prelude(uty));
     match uty {
         UintTy::Usize => MlT::TConstructor("usize".into()),
@@ -367,7 +367,7 @@ pub(crate) fn uintty_to_ty<'tcx, N: Namer<'tcx>>(names: &mut N, uty: UintTy) ->
     }
 }
 
-pub(crate) fn floatty_to_ty<'tcx, N: Namer<'tcx>>(names: &mut N, fty: FloatTy) -> MlT {
+pub(crate) fn floatty_to_ty<'tcx, N: Namer<'tcx>>(names: &N, fty: FloatTy) -> MlT {
     names.import_prelude_module(floatty_to_prelude(fty));
     match fty {
         FloatTy::F32 => MlT::TConstructor("Float32.t".into()),
@@ -384,7 +384,7 @@ pub fn is_int(tcx: TyCtxt, ty: Ty) -> bool {
     }
 }
 
-pub fn int_ty<'tcx, N: Namer<'tcx>>(ctx: &mut Why3Generator<'tcx>, names: &mut N) -> MlT {
+pub fn int_ty<'tcx, N: Namer<'tcx>>(ctx: &Why3Generator<'tcx>, names: &N) -> MlT {
     let int_id = get_int_ty(ctx.tcx);
     let ty = ctx.type_of(int_id).skip_binder();
     translate_ty(ctx, names, DUMMY_SP, ty)
diff --git a/creusot/src/backend/ty_inv.rs b/creusot/src/backend/ty_inv.rs
index bb5c896f80..16d0a61193 100644
--- a/creusot/src/backend/ty_inv.rs
+++ b/creusot/src/backend/ty_inv.rs
@@ -74,12 +74,12 @@ pub(crate) fn is_tyinv_trivial<'tcx>(
 
 pub struct InvariantElaborator<'a, 'tcx> {
     typing_env: TypingEnv<'tcx>,
-    ctx: &'a mut Why3Generator<'tcx>,
+    ctx: &'a Why3Generator<'tcx>,
     pub rewrite: bool,
 }
 
 impl<'a, 'tcx> InvariantElaborator<'a, 'tcx> {
-    pub(crate) fn new(typing_env: TypingEnv<'tcx>, ctx: &'a mut Why3Generator<'tcx>) -> Self {
+    pub(crate) fn new(typing_env: TypingEnv<'tcx>, ctx: &'a Why3Generator<'tcx>) -> Self {
         InvariantElaborator { typing_env, ctx, rewrite: false }
     }
 
diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs
index 0d6ca28461..bd62cceb05 100644
--- a/creusot/src/ctx.rs
+++ b/creusot/src/ctx.rs
@@ -21,7 +21,7 @@ use crate::{
     },
     util::{erased_identity_for_item, parent_module},
 };
-use indexmap::IndexMap;
+use once_map::unsync::OnceMap;
 use rustc_ast::{
     visit::{walk_fn, FnKind, Visitor},
     Fn, FnSig, NodeId,
@@ -44,29 +44,19 @@ use rustc_middle::{
 };
 use rustc_span::{Span, Symbol};
 use rustc_trait_selection::traits::normalize_param_env_or_error;
-use std::{collections::HashMap, ops::Deref, rc::Rc};
+use std::{collections::HashMap, ops::Deref};
 
 pub(crate) use crate::{backend::clone_map::*, translated_item::*};
 
 macro_rules! queryish {
-    ($name:ident, $res:ty, $builder:ident) => {
-        pub(crate) fn $name(&mut self, item: DefId) -> $res {
-            if self.$name.get(&item).is_none() {
-                let res = self.$builder(item);
-                self.$name.insert(item, res);
-            };
-
-            &self.$name[&item]
+    ($name:ident, $key:ty, $res:ty, $builder:ident) => {
+        pub(crate) fn $name(&self, item: $key) -> &$res {
+            self.$name.insert(item, |&item| Box::new(self.$builder(item)))
         }
     };
-    ($name:ident, $res:ty, $builder:expr) => {
-        pub(crate) fn $name(&mut self, item: DefId) -> $res {
-            if self.$name.get(&item).is_none() {
-                let res = ($builder)(self, item);
-                self.$name.insert(item, res);
-            };
-
-            &self.$name[&item]
+    ($name:ident, $key:ty, $res:ty, $builder:expr) => {
+        pub(crate) fn $name(&self, item: $key) -> &$res {
+            self.$name.insert(item, |&item| Box::new(($builder)(self, item)))
         }
     };
 }
@@ -149,20 +139,21 @@ impl ItemType {
 // TODO: The state in here should be as opaque as possible...
 pub struct TranslationCtx<'tcx> {
     pub tcx: TyCtxt<'tcx>,
-    laws: IndexMap<DefId, Vec<DefId>>,
-    fmir_body: IndexMap<BodyId, fmir::Body<'tcx>>,
-    terms: IndexMap<DefId, Term<'tcx>>,
+
     pub externs: Metadata<'tcx>,
     pub(crate) opts: Options,
     creusot_items: CreusotItems,
     extern_specs: HashMap<DefId, ExternSpec<'tcx>>,
     extern_spec_items: HashMap<LocalDefId, DefId>,
-    trait_impl: HashMap<DefId, TraitImpl<'tcx>>,
-    sig: HashMap<DefId, PreSignature<'tcx>>,
-    bodies: HashMap<LocalDefId, Rc<BodyWithBorrowckFacts<'tcx>>>,
-    opacity: HashMap<DefId, Opacity>,
-    closure_contract: HashMap<DefId, ClosureContract<'tcx>>,
     params_open_inv: HashMap<DefId, Vec<usize>>,
+    laws: OnceMap<DefId, Box<Vec<DefId>>>,
+    fmir_body: OnceMap<BodyId, Box<fmir::Body<'tcx>>>,
+    terms: OnceMap<DefId, Box<Option<Term<'tcx>>>>,
+    trait_impl: OnceMap<DefId, Box<TraitImpl<'tcx>>>,
+    sig: OnceMap<DefId, Box<PreSignature<'tcx>>>,
+    bodies: OnceMap<LocalDefId, Box<BodyWithBorrowckFacts<'tcx>>>,
+    opacity: OnceMap<DefId, Box<Opacity>>,
+    closure_contract: OnceMap<DefId, Box<ClosureContract<'tcx>>>,
 }
 
 impl<'tcx> Deref for TranslationCtx<'tcx> {
@@ -245,17 +236,11 @@ impl<'tcx> TranslationCtx<'tcx> {
         }
     }
 
-    queryish!(trait_impl, &TraitImpl<'tcx>, translate_impl);
+    queryish!(trait_impl, DefId, TraitImpl<'tcx>, translate_impl);
 
-    queryish!(closure_contract, &ClosureContract<'tcx>, build_closure_contract);
+    queryish!(closure_contract, DefId, ClosureContract<'tcx>, build_closure_contract);
 
-    pub(crate) fn fmir_body(&mut self, body_id: BodyId) -> &fmir::Body<'tcx> {
-        if !self.fmir_body.contains_key(&body_id) {
-            let fmir = translation::function::fmir(self, body_id);
-            self.fmir_body.insert(body_id, fmir);
-        }
-        self.fmir_body.get(&body_id).unwrap()
-    }
+    queryish!(fmir_body, BodyId, fmir::Body<'tcx>, translation::function::fmir);
 
     /// Compute the pearlite term associated with `def_id`.
     ///
@@ -263,31 +248,35 @@ impl<'tcx> TranslationCtx<'tcx> {
     /// - `Ok(None)` if `def_id` does not have a body
     /// - `Ok(Some(term))` if `def_id` has a body, in this crate or in a dependency.
     /// - `Err(CannotFetchThir)` if typechecking the body of `def_id` failed.
-    pub(crate) fn term(&mut self, def_id: DefId) -> Result<Option<&Term<'tcx>>, CannotFetchThir> {
-        let Some(local_id) = def_id.as_local() else { return Ok(self.externs.term(def_id)) };
-
-        if self.tcx.hir().maybe_body_owned_by(local_id).is_some() {
-            if !self.terms.contains_key(&def_id) {
-                let mut term = match pearlite::pearlite(self, local_id) {
-                    Ok(t) => t,
-                    Err(Error::MustPrint(msg)) => msg.emit(self.tcx),
-                    Err(Error::TypeCheck(thir)) => return Err(thir),
-                };
-                term = pearlite::normalize(self.tcx, self.typing_env(def_id), term);
+    pub(crate) fn term<'a>(
+        &'a self,
+        def_id: DefId,
+    ) -> Result<Option<&'a Term<'tcx>>, CannotFetchThir> {
+        let Some(local_id) = def_id.as_local() else {
+            return Ok(self.externs.term(def_id));
+        };
 
-                self.terms.insert(def_id, term);
-            };
-            Ok(self.terms.get(&def_id))
-        } else {
-            Ok(None)
-        }
+        self.terms
+            .try_insert(def_id, |_| {
+                if self.tcx.hir().maybe_body_owned_by(local_id).is_some() {
+                    let term = match pearlite::pearlite(self, local_id) {
+                        Ok(t) => t,
+                        Err(Error::MustPrint(msg)) => msg.emit(self.tcx),
+                        Err(Error::TypeCheck(thir)) => return Err(thir),
+                    };
+                    Ok(Box::new(Some(pearlite::normalize(self.tcx, self.typing_env(def_id), term))))
+                } else {
+                    Ok(Box::new(None))
+                }
+            })
+            .map(|x| x.as_ref())
     }
 
     /// Same as [`Self::term`], but aborts if an error was found.
     ///
     /// This should only be used in [`after_analysis`](crate::translation::after_analysis),
     /// where we are confident that typechecking errors have already been reported.
-    pub(crate) fn term_fail_fast(&mut self, def_id: DefId) -> Option<&Term<'tcx>> {
+    pub(crate) fn term_fail_fast(&self, def_id: DefId) -> Option<&Term<'tcx>> {
         let tcx = self.tcx;
         self.term(def_id).unwrap_or_else(|_| {
             tcx.dcx().abort_if_errors();
@@ -302,14 +291,10 @@ impl<'tcx> TranslationCtx<'tcx> {
         self.params_open_inv.get(&def_id)
     }
 
-    queryish!(sig, &PreSignature<'tcx>, |ctx: &mut Self, key| { pre_sig_of(&mut *ctx, key) });
+    queryish!(sig, DefId, PreSignature<'tcx>, (pre_sig_of));
 
-    pub(crate) fn body_with_facts(
-        &mut self,
-        def_id: LocalDefId,
-    ) -> &Rc<BodyWithBorrowckFacts<'tcx>> {
-        let entry = self.bodies.entry(def_id);
-        entry.or_insert_with(|| {
+    pub(crate) fn body_with_facts(&self, def_id: LocalDefId) -> &BodyWithBorrowckFacts<'tcx> {
+        self.bodies.insert(def_id, |_| {
             let mut body = callbacks::get_body(self.tcx, def_id)
                 .unwrap_or_else(|| panic!("did not find body for {def_id:?}"));
 
@@ -325,7 +310,7 @@ impl<'tcx> TranslationCtx<'tcx> {
                 }
             }
 
-            Rc::new(body)
+            Box::new(body)
         })
     }
 
@@ -362,7 +347,7 @@ impl<'tcx> TranslationCtx<'tcx> {
         self.tcx.dcx().span_warn(span, msg.into())
     }
 
-    queryish!(laws, &[DefId], laws_inner);
+    queryish!(laws, DefId, [DefId], laws_inner);
 
     // TODO Make private
     pub(crate) fn extern_spec(&self, def_id: DefId) -> Option<&ExternSpec<'tcx>> {
@@ -377,16 +362,10 @@ impl<'tcx> TranslationCtx<'tcx> {
         self.opts.should_output
     }
 
+    queryish!(opacity, DefId, Opacity, mk_opacity);
+
     /// We encodes the opacity of functions using 'witnesses', funcitons that have the target opacity
     /// set as their *visibility*.
-    pub(crate) fn opacity(&mut self, item: DefId) -> &Opacity {
-        if !self.opacity.contains_key(&item) {
-            self.opacity.insert(item, self.mk_opacity(item));
-        }
-
-        &self.opacity[&item]
-    }
-
     fn mk_opacity(&self, item: DefId) -> Opacity {
         if !matches!(self.item_type(item), ItemType::Predicate { .. } | ItemType::Logic { .. }) {
             return Opacity(Visibility::Public);
@@ -401,13 +380,13 @@ impl<'tcx> TranslationCtx<'tcx> {
 
     /// Checks if `item` is transparent in the scope of `modl`.
     /// This will determine whether the solvers are allowed to unfold the body's definition.
-    pub(crate) fn is_transparent_from(&mut self, item: DefId, modl: DefId) -> bool {
+    pub(crate) fn is_transparent_from(&self, item: DefId, modl: DefId) -> bool {
         self.opacity(item).0.is_accessible_from(modl, self.tcx)
     }
 
-    pub(crate) fn metadata(&self) -> BinaryMetadata<'tcx> {
+    pub(crate) fn metadata(&mut self) -> BinaryMetadata<'tcx> {
         BinaryMetadata::from_parts(
-            &self.terms,
+            &mut self.terms,
             &self.creusot_items,
             &self.extern_specs,
             &self.params_open_inv,
@@ -447,7 +426,7 @@ impl<'tcx> TranslationCtx<'tcx> {
         TypingEnv { typing_mode: TypingMode::non_body_analysis(), param_env }
     }
 
-    pub(crate) fn has_body(&mut self, def_id: DefId) -> bool {
+    pub(crate) fn has_body(&self, def_id: DefId) -> bool {
         if let Some(local_id) = def_id.as_local() {
             self.tcx.hir().maybe_body_owned_by(local_id).is_some()
         } else {
diff --git a/creusot/src/gather_spec_closures.rs b/creusot/src/gather_spec_closures.rs
index 6e14e3dfaa..71e479c990 100644
--- a/creusot/src/gather_spec_closures.rs
+++ b/creusot/src/gather_spec_closures.rs
@@ -27,7 +27,7 @@ pub(crate) struct SpecClosures<'tcx> {
 }
 
 impl<'tcx> SpecClosures<'tcx> {
-    pub(crate) fn collect(ctx: &mut TranslationCtx<'tcx>, body: &Body<'tcx>) -> Self {
+    pub(crate) fn collect(ctx: &TranslationCtx<'tcx>, body: &Body<'tcx>) -> Self {
         let mut visitor = Closures::new(ctx.tcx);
         visitor.visit_body(body);
 
@@ -91,7 +91,7 @@ pub(crate) struct Invariants<'tcx> {
 }
 
 struct InvariantsVisitor<'a, 'tcx> {
-    ctx: &'a mut TranslationCtx<'tcx>,
+    ctx: &'a TranslationCtx<'tcx>,
     body: &'a Body<'tcx>,
     before_loop: IndexSet<BasicBlock>,
     invariants: Invariants<'tcx>,
@@ -166,7 +166,7 @@ impl<'a, 'tcx> Visitor<'tcx> for InvariantsVisitor<'a, 'tcx> {
 
 // Calculate the *actual* location of invariants in MIR
 pub(crate) fn corrected_invariant_names_and_locations<'tcx>(
-    ctx: &mut TranslationCtx<'tcx>,
+    ctx: &TranslationCtx<'tcx>,
     body: &Body<'tcx>,
 ) -> Invariants<'tcx> {
     let mut invs_gather = InvariantsVisitor {
diff --git a/creusot/src/metadata.rs b/creusot/src/metadata.rs
index 7e21abe2f2..881879c911 100644
--- a/creusot/src/metadata.rs
+++ b/creusot/src/metadata.rs
@@ -3,6 +3,7 @@ use crate::{
 };
 use creusot_metadata::{decode_metadata, encode_metadata};
 use indexmap::IndexMap;
+use once_map::unsync::OnceMap;
 use rustc_hir::def_id::{CrateNum, DefId};
 use rustc_macros::{TyDecodable, TyEncodable};
 use rustc_middle::ty::TyCtxt;
@@ -140,15 +141,15 @@ pub(crate) struct BinaryMetadata<'tcx> {
 
 impl<'tcx> BinaryMetadata<'tcx> {
     pub(crate) fn from_parts(
-        terms: &IndexMap<DefId, Term<'tcx>>,
+        terms: &mut OnceMap<DefId, Box<Option<Term<'tcx>>>>,
         items: &CreusotItems,
         extern_specs: &HashMap<DefId, ExternSpec<'tcx>>,
         params_open_inv: &HashMap<DefId, Vec<usize>>,
     ) -> Self {
         let terms = terms
-            .iter()
-            .filter(|(def_id, _)| def_id.is_local())
-            .map(|(id, t)| (*id, t.clone()))
+            .iter_mut()
+            .filter(|(def_id, t)| def_id.is_local() && t.is_some())
+            .map(|(id, t)| (*id, t.clone().unwrap()))
             .collect();
 
         BinaryMetadata {
@@ -170,8 +171,8 @@ fn export_file(ctx: &TranslationCtx, out: &Option<String>) -> PathBuf {
     })
 }
 
-pub(crate) fn dump_exports(ctx: &TranslationCtx, out: &Option<String>) {
-    let out_filename = export_file(ctx, out);
+pub(crate) fn dump_exports(ctx: &mut TranslationCtx) {
+    let out_filename = export_file(ctx, &ctx.opts.metadata_path);
     debug!("dump_exports={:?}", out_filename);
 
     dump_binary_metadata(ctx.tcx, &out_filename, ctx.metadata()).unwrap_or_else(|err| {
diff --git a/creusot/src/run_why3.rs b/creusot/src/run_why3.rs
index d70dcd9d87..73fde229f9 100644
--- a/creusot/src/run_why3.rs
+++ b/creusot/src/run_why3.rs
@@ -69,7 +69,7 @@ pub(super) fn run_why3<'tcx>(ctx: &Why3Generator<'tcx>, file: Option<PathBuf>) {
 
     if matches!(why3_cmd.sub, Why3Sub::Prove) {
         command.arg("--json");
-        let span_map = &ctx.span_map;
+        let span_map = &ctx.span_map.borrow();
         let mut child = command.stdout(Stdio::piped()).spawn().expect("could not run why3");
         let mut stdout = BufReader::new(child.stdout.take().unwrap());
         let de = Deserializer::from_reader(&mut stdout);
diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs
index 2eadabb831..99609e4a8d 100644
--- a/creusot/src/translation.rs
+++ b/creusot/src/translation.rs
@@ -138,7 +138,7 @@ pub(crate) fn after_analysis(ctx: TranslationCtx) -> Result<(), Box<dyn std::err
     }
 
     if why3.should_export() {
-        metadata::dump_exports(&why3, &why3.opts.metadata_path);
+        metadata::dump_exports(&mut why3);
     }
 
     if why3.should_compile() {
diff --git a/creusot/src/translation/external.rs b/creusot/src/translation/external.rs
index 0ec9810e01..0f199fbefa 100644
--- a/creusot/src/translation/external.rs
+++ b/creusot/src/translation/external.rs
@@ -36,7 +36,7 @@ impl<'tcx> ExternSpec<'tcx> {
 
 // Must be run before MIR generation.
 pub(crate) fn extract_extern_specs_from_item<'tcx>(
-    ctx: &mut TranslationCtx<'tcx>,
+    ctx: &TranslationCtx<'tcx>,
     def_id: LocalDefId,
 ) -> CreusotResult<(DefId, ExternSpec<'tcx>)> {
     // Handle error gracefully
diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs
index 5f0edfcdab..c42a8165b0 100644
--- a/creusot/src/translation/function.rs
+++ b/creusot/src/translation/function.rs
@@ -52,7 +52,7 @@ use terminator::discriminator_for_switch;
 use self::pearlite::BinOp;
 
 /// Translate a function from rustc's MIR to fMIR.
-pub(crate) fn fmir<'tcx>(ctx: &mut TranslationCtx<'tcx>, body_id: BodyId) -> fmir::Body<'tcx> {
+pub(crate) fn fmir<'tcx>(ctx: &TranslationCtx<'tcx>, body_id: BodyId) -> fmir::Body<'tcx> {
     BodyTranslator::with_context(ctx, body_id, |func_translator| func_translator.translate())
 }
 
@@ -78,7 +78,7 @@ struct BodyTranslator<'a, 'tcx> {
     past_blocks: IndexMap<BasicBlock, fmir::Block<'tcx>>,
 
     // Type translation context
-    ctx: &'a mut TranslationCtx<'tcx>,
+    ctx: &'a TranslationCtx<'tcx>,
 
     // Fresh BlockId
     fresh_id: usize,
@@ -113,13 +113,13 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
     }
 
     fn with_context<R, F: for<'b> FnOnce(BodyTranslator<'b, 'tcx>) -> R>(
-        ctx: &'body mut TranslationCtx<'tcx>,
+        ctx: &'body TranslationCtx<'tcx>,
         body_id: BodyId,
         f: F,
     ) -> R {
         let tcx = ctx.tcx;
 
-        let body_with_facts = ctx.body_with_facts(body_id.def_id).clone();
+        let body_with_facts = ctx.body_with_facts(body_id.def_id);
         let (body, move_data, resolver, borrows);
         match body_id.promoted {
             None => {
@@ -801,7 +801,7 @@ pub(crate) struct ClosureContract<'tcx> {
 }
 
 impl<'tcx> TranslationCtx<'tcx> {
-    pub(crate) fn build_closure_contract(&mut self, def_id: DefId) -> ClosureContract<'tcx> {
+    pub(crate) fn build_closure_contract(&self, def_id: DefId) -> ClosureContract<'tcx> {
         let TyKind::Closure(_, subst) = self.type_of(def_id).instantiate_identity().kind() else {
             unreachable!()
         };
@@ -1076,7 +1076,7 @@ impl<'tcx> TranslationCtx<'tcx> {
 }
 
 pub(crate) fn closure_resolve<'tcx>(
-    ctx: &mut TranslationCtx<'tcx>,
+    ctx: &TranslationCtx<'tcx>,
     def_id: DefId,
     subst: GenericArgsRef<'tcx>,
 ) -> Term<'tcx> {
@@ -1290,7 +1290,7 @@ pub(crate) fn closure_capture_subst<'a, 'tcx>(
 }
 
 fn resolve_predicate_of<'tcx>(
-    ctx: &mut TranslationCtx<'tcx>,
+    ctx: &TranslationCtx<'tcx>,
     typing_env: TypingEnv<'tcx>,
     ty: Ty<'tcx>,
 ) -> Option<(DefId, GenericArgsRef<'tcx>)> {
diff --git a/creusot/src/translation/function/promoted.rs b/creusot/src/translation/function/promoted.rs
index 0f13310f1b..86d781015f 100644
--- a/creusot/src/translation/function/promoted.rs
+++ b/creusot/src/translation/function/promoted.rs
@@ -22,7 +22,7 @@ pub(crate) fn promoted_signature<'tcx>(body: &Body<'tcx>) -> PreSignature<'tcx>
 }
 
 pub(crate) fn translate_promoted<'tcx>(
-    ctx: &mut TranslationCtx<'tcx>,
+    ctx: &TranslationCtx<'tcx>,
     body_id: BodyId,
 ) -> CreusotResult<(PreSignature<'tcx>, fmir::Body<'tcx>)> {
     let body = ctx.body(body_id).clone();
diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs
index 15bdb91e58..0e2d33e583 100644
--- a/creusot/src/translation/function/terminator.rs
+++ b/creusot/src/translation/function/terminator.rs
@@ -400,7 +400,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
 ///
 /// - `report_location`: used to emit an eventual warning.
 fn resolve_function<'tcx>(
-    ctx: &mut TranslationCtx<'tcx>,
+    ctx: &TranslationCtx<'tcx>,
     typing_env: TypingEnv<'tcx>,
     def_id: DefId,
     subst: GenericArgsRef<'tcx>,
diff --git a/creusot/src/translation/specification.rs b/creusot/src/translation/specification.rs
index ca18b7e93b..f221a74f16 100644
--- a/creusot/src/translation/specification.rs
+++ b/creusot/src/translation/specification.rs
@@ -131,7 +131,7 @@ impl ContractClauses {
 
     fn get_pre<'tcx>(
         self,
-        ctx: &mut TranslationCtx<'tcx>,
+        ctx: &TranslationCtx<'tcx>,
         fn_name: &str,
     ) -> EarlyBinder<'tcx, PreContract<'tcx>> {
         let mut out = PreContract::default();
@@ -374,10 +374,7 @@ pub(crate) fn inherited_extern_spec<'tcx>(
     }
 }
 
-pub(crate) fn contract_of<'tcx>(
-    ctx: &mut TranslationCtx<'tcx>,
-    def_id: DefId,
-) -> PreContract<'tcx> {
+pub(crate) fn contract_of<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> PreContract<'tcx> {
     let fn_name = ctx.opt_item_name(def_id);
     let fn_name = match &fn_name {
         Some(fn_name) => fn_name.as_str(),
@@ -438,10 +435,7 @@ impl<'tcx> PreSignature<'tcx> {
     }
 }
 
-pub(crate) fn pre_sig_of<'tcx>(
-    ctx: &mut TranslationCtx<'tcx>,
-    def_id: DefId,
-) -> PreSignature<'tcx> {
+pub(crate) fn pre_sig_of<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> PreSignature<'tcx> {
     let (inputs, output) = inputs_and_output(ctx.tcx, def_id);
 
     let mut contract = crate::specification::contract_of(ctx, def_id);
diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs
index 6dba929985..876c797364 100644
--- a/creusot/src/translation/traits.rs
+++ b/creusot/src/translation/traits.rs
@@ -54,7 +54,7 @@ impl<'tcx> TranslationCtx<'tcx> {
         laws
     }
 
-    pub(crate) fn translate_impl(&mut self, impl_id: DefId) -> TraitImpl<'tcx> {
+    pub(crate) fn translate_impl(&self, impl_id: DefId) -> TraitImpl<'tcx> {
         assert!(self.trait_id_of_impl(impl_id).is_some(), "{impl_id:?} is not a trait impl");
         let trait_ref = self.tcx.impl_trait_ref(impl_id).unwrap();
 
@@ -122,7 +122,7 @@ impl<'tcx> TranslationCtx<'tcx> {
 }
 
 fn logic_refinement_term<'tcx>(
-    ctx: &mut TranslationCtx<'tcx>,
+    ctx: &TranslationCtx<'tcx>,
     impl_item_id: DefId,
     trait_item_id: DefId,
     refn_subst: GenericArgsRef<'tcx>,
diff --git a/creusot/src/validate.rs b/creusot/src/validate.rs
index cfefaac429..525e908ae4 100644
--- a/creusot/src/validate.rs
+++ b/creusot/src/validate.rs
@@ -23,7 +23,7 @@ use crate::{
     util::parent_module,
 };
 
-pub(crate) fn validate_trusted(ctx: &mut TranslationCtx) {
+pub(crate) fn validate_trusted(ctx: &TranslationCtx) {
     for def_id in ctx.hir_crate_items(()).definitions() {
         let def_id = def_id.to_def_id();
         if get_builtin(ctx.tcx, def_id).is_some() && !is_trusted(ctx.tcx, def_id) {
@@ -36,10 +36,7 @@ pub(crate) fn validate_trusted(ctx: &mut TranslationCtx) {
     }
 }
 
-pub(crate) fn validate_opacity(
-    ctx: &mut TranslationCtx,
-    item: DefId,
-) -> Result<(), CannotFetchThir> {
+pub(crate) fn validate_opacity(ctx: &TranslationCtx, item: DefId) -> Result<(), CannotFetchThir> {
     struct OpacityVisitor<'a, 'tcx> {
         ctx: &'a TranslationCtx<'tcx>,
         opacity: Option<DefId>,
@@ -108,7 +105,7 @@ pub(crate) fn validate_opacity(
 
 // Validate that laws have no additional generic parameters.
 // This is because laws are auto-loaded, and we do not want to generate polymorphic WhyML code
-pub(crate) fn validate_traits(ctx: &mut TranslationCtx) {
+pub(crate) fn validate_traits(ctx: &TranslationCtx) {
     let mut law_violations = Vec::new();
 
     for trait_item_id in ctx.hir_crate_items(()).trait_items() {
@@ -142,7 +139,7 @@ fn is_overloaded_item(tcx: TyCtxt, def_id: DefId) -> bool {
     }
 }
 
-pub(crate) fn validate_impls(ctx: &mut TranslationCtx) {
+pub(crate) fn validate_impls(ctx: &TranslationCtx) {
     for impl_id in ctx.all_local_trait_impls(()).values().flat_map(|i| i.iter()) {
         if !matches!(ctx.def_kind(*impl_id), DefKind::Impl { .. }) {
             continue;
@@ -246,7 +243,7 @@ pub(crate) enum Purity {
 }
 
 impl Purity {
-    pub(crate) fn of_def_id(ctx: &mut TranslationCtx, def_id: DefId) -> Self {
+    pub(crate) fn of_def_id(ctx: &TranslationCtx, def_id: DefId) -> Self {
         let is_snapshot = is_snapshot_closure(ctx.tcx, def_id);
         if is_predicate(ctx.tcx, def_id) && is_prophetic(ctx.tcx, def_id)
             || is_logic(ctx.tcx, def_id) && is_prophetic(ctx.tcx, def_id)
@@ -291,7 +288,7 @@ impl Purity {
 }
 
 pub(crate) fn validate_purity(
-    ctx: &mut TranslationCtx,
+    ctx: &TranslationCtx,
     def_id: LocalDefId,
 ) -> Result<(), CannotFetchThir> {
     let (thir, expr) = ctx.fetch_thir(def_id)?;
@@ -319,7 +316,7 @@ pub(crate) fn validate_purity(
 }
 
 struct PurityVisitor<'a, 'tcx> {
-    ctx: &'a mut TranslationCtx<'tcx>,
+    ctx: &'a TranslationCtx<'tcx>,
     thir: &'a Thir<'tcx>,
     context: Purity,
     /// Typing environment of the caller function
@@ -329,7 +326,7 @@ struct PurityVisitor<'a, 'tcx> {
 }
 
 impl<'a, 'tcx> PurityVisitor<'a, 'tcx> {
-    fn purity(&mut self, fun: thir::ExprId, func_did: DefId) -> Purity {
+    fn purity(&self, fun: thir::ExprId, func_did: DefId) -> Purity {
         let stub = pearlite_stub(self.ctx.tcx, self.thir[fun].ty);
 
         if matches!(stub, Some(Stub::Fin))
diff --git a/creusot/src/validate_terminates.rs b/creusot/src/validate_terminates.rs
index 3e760fa370..daef9bf0fb 100644
--- a/creusot/src/validate_terminates.rs
+++ b/creusot/src/validate_terminates.rs
@@ -63,7 +63,7 @@ use rustc_trait_selection::traits::normalize_param_env_or_error;
 ///
 /// Note that for logical functions, these are relaxed: we don't check loops, nor simple
 /// recursion, because why3 will handle it for us.
-pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) -> Result<(), CannotFetchThir> {
+pub(crate) fn validate_terminates(ctx: &TranslationCtx) -> Result<(), CannotFetchThir> {
     ctx.tcx.dcx().abort_if_errors(); // There may have been errors before, if a `#[terminates]` calls a non-`#[terminates]`.
 
     let CallGraph { graph: mut call_graph, additional_data } = CallGraph::build(ctx)?;
@@ -312,7 +312,7 @@ impl<'tcx> BuildFunctionsGraph<'tcx> {
     /// Process the call from `node` to `called_id`.
     fn function_call(
         &mut self,
-        ctx: &mut TranslationCtx<'tcx>,
+        ctx: &TranslationCtx<'tcx>,
         node: graph::NodeIndex,
         typing_env: TypingEnv<'tcx>,
         called_id: DefId,
@@ -436,7 +436,7 @@ impl<'tcx> BuildFunctionsGraph<'tcx> {
     /// We use this function, so that only those specialization that are actually called are visited.
     fn visit_specialized_default_function(
         &mut self,
-        ctx: &mut TranslationCtx<'tcx>,
+        ctx: &TranslationCtx<'tcx>,
         graph_node: ImplDefaultTransparent,
     ) -> Result<Option<graph::NodeIndex>, CannotFetchThir> {
         let Some(&node) =
@@ -501,7 +501,7 @@ impl CallGraph {
     /// exclusively for the purpose of termination checking.
     ///
     /// In particular, this means it only contains `#[terminates]` functions.
-    fn build(ctx: &mut TranslationCtx) -> Result<Self, CannotFetchThir> {
+    fn build(ctx: &TranslationCtx) -> Result<Self, CannotFetchThir> {
         let tcx = ctx.tcx;
         let mut build_call_graph = BuildFunctionsGraph::default();
 
diff --git a/why3/src/coma.rs b/why3/src/coma.rs
index 75b61b3439..8a6e3c9066 100644
--- a/why3/src/coma.rs
+++ b/why3/src/coma.rs
@@ -160,7 +160,7 @@ impl Expr {
         // If we have `x [ x = z ]` replace this by `z`
         if defs.len() == 1
             && !defs[0].body.occurs_cont(&defs[0].name)
-            && self.as_symbol().and_then(QName::ident) == Some(&defs[0].name)
+            && self.as_symbol().is_some_and(|qn| qn.is_ident(&defs[0].name))
         {
             defs.remove(0).body
         } else {
@@ -191,7 +191,7 @@ impl Expr {
     /// Checks whether a symbol of name `cont` occurs in `self`
     pub fn occurs_cont(&self, cont: &Ident) -> bool {
         match self {
-            Expr::Symbol(v) => v.ident() == Some(&cont),
+            Expr::Symbol(v) => v.is_ident(cont),
             Expr::App(e, arg) => {
                 let arg = if let Arg::Cont(e) = &**arg { e.occurs_cont(cont) } else { false };
                 arg || e.occurs_cont(cont)
diff --git a/why3/src/name.rs b/why3/src/name.rs
index 43dbe15ece..cb9449d7b9 100644
--- a/why3/src/name.rs
+++ b/why3/src/name.rs
@@ -100,14 +100,6 @@ impl QName {
         self.name.clone()
     }
 
-    pub fn ident(&self) -> Option<&Ident> {
-        if self.module.is_empty() {
-            Some(&self.name)
-        } else {
-            None
-        }
-    }
-
     pub fn without_search_path(mut self) -> QName {
         let mut i = 0;
         while i < self.module.len() {