diff --git a/verify/rust_verify/src/context.rs b/verify/rust_verify/src/context.rs
index 5df20fad1af73..a4271fd72e098 100644
--- a/verify/rust_verify/src/context.rs
+++ b/verify/rust_verify/src/context.rs
@@ -8,7 +8,7 @@ use vir::ast::Mode;
 pub struct ErasureInfo {
     pub(crate) resolved_calls: Vec<(SpanData, ResolvedCall)>,
     pub(crate) condition_modes: Vec<(SpanData, Mode)>,
-    pub(crate) external_functions: Vec<air::ast::Ident>,
+    pub(crate) external_functions: Vec<vir::ast::Path>,
 }
 
 type ErasureInfoRef = std::rc::Rc<std::cell::RefCell<ErasureInfo>>;
diff --git a/verify/rust_verify/src/erase.rs b/verify/rust_verify/src/erase.rs
index 4830d0c1f3321..3ee1eaf058477 100644
--- a/verify/rust_verify/src/erase.rs
+++ b/verify/rust_verify/src/erase.rs
@@ -39,7 +39,7 @@
 use crate::rust_to_vir_base::get_verifier_attrs;
 use crate::util::{from_raw_span, vec_map};
 use crate::{unsupported, unsupported_unless};
-use air::ast::Ident;
+
 use rustc_ast::ast::{
     Block, Crate, Expr, ExprKind, FnDecl, FnKind, FnSig, Item, ItemKind, Local, ModKind, Param,
     Stmt, StmtKind,
@@ -48,7 +48,8 @@ use rustc_ast::ptr::P;
 use rustc_interface::interface::Compiler;
 use rustc_span::{Span, SpanData};
 use std::collections::HashMap;
-use std::sync::Arc;
+use vir::ast::Path;
+
 use vir::ast::{Function, Krate, Mode};
 use vir::modes::ErasureModes;
 
@@ -60,7 +61,7 @@ pub enum ResolvedCall {
     /// The call is to an operator like == or + that should be compiled.
     CompilableOperator,
     /// The call is to a function, and we record the resolved name of the function here.
-    Call(Ident),
+    Call(Path),
 }
 
 #[derive(Clone)]
@@ -73,16 +74,18 @@ pub struct ErasureHints {
     pub erasure_modes: ErasureModes,
     /// List of #[verifier(external)] functions.  (These don't appear in vir_crate,
     /// so we need to record them separately here.)
-    pub external_functions: Vec<Ident>,
+    pub external_functions: Vec<Path>,
 }
 
 #[derive(Clone)]
 pub struct Ctxt {
     /// Copy of the entire VIR crate that was created in the first run's HIR -> VIR transformation
     vir_crate: Krate,
-    /// Map each function name to its VIR Function, or to None if it is a #[verifier(external)]
+    /// Map each function path to its VIR Function, or to None if it is a #[verifier(external)]
     /// function
-    functions: HashMap<Ident, Option<Function>>,
+    functions: HashMap<Path, Option<Function>>,
+    /// Map each function span to its VIR Function, excluding #[verifier(external)] functions
+    functions_by_span: HashMap<Span, Function>,
     /// Details of each call in the first run's HIR
     calls: HashMap<Span, ResolvedCall>,
     /// Mode of each if/else or match condition, used to decide how to erase if/else and match
@@ -181,8 +184,8 @@ fn erase_expr_opt(ctxt: &Ctxt, is_exec: bool, expr: &Expr) -> Option<Expr> {
                     f_expr.clone(),
                     vec_map(args, |e| P(erase_expr(ctxt, is_exec, e))),
                 ),
-                ResolvedCall::Call(f_name) => {
-                    let f = &ctxt.functions[f_name];
+                ResolvedCall::Call(f_path) => {
+                    let f = &ctxt.functions[f_path];
                     if let Some(f) = f {
                         match f.x.mode {
                             Mode::Spec | Mode::Proof => return None,
@@ -271,13 +274,13 @@ fn erase_block(ctxt: &Ctxt, is_exec: bool, block: &Block) -> Block {
     Block { stmts, id, rules, span, tokens: block.tokens.clone() }
 }
 
-fn erase_fn(ctxt: &Ctxt, f_name: &String, f: &FnKind) -> Option<FnKind> {
-    let f_vir = &ctxt.functions[&Arc::new(f_name.clone())].as_ref().expect("erase_fn");
+fn erase_fn(ctxt: &Ctxt, f: &FnKind) -> Option<FnKind> {
+    let FnKind(defaultness, sig, generics, body_opt) = f;
+    let f_vir = &ctxt.functions_by_span[&sig.span];
     match f_vir.x.mode {
         Mode::Spec | Mode::Proof => return None,
         Mode::Exec => {}
     }
-    let FnKind(defaultness, sig, generics, body_opt) = f;
     let FnSig { header: _, decl, span: _ } = sig;
     let FnDecl { inputs, output } = &**decl;
     let mut new_inputs: Vec<Param> = Vec::new();
@@ -315,7 +318,7 @@ fn erase_item(ctxt: &Ctxt, item: &Item) -> Vec<P<Item>> {
             if vattrs.external {
                 return vec![P(item.clone())];
             }
-            match erase_fn(ctxt, &item.ident.name.to_string(), kind) {
+            match erase_fn(ctxt, kind) {
                 None => return vec![],
                 Some(kind) => ItemKind::Fn(Box::new(kind)),
             }
@@ -364,9 +367,11 @@ pub struct CompilerCallbacks {
 
 fn mk_ctxt(erasure_hints: &ErasureHints) -> Ctxt {
     let mut functions = HashMap::new();
+    let mut functions_by_span = HashMap::new();
     let mut calls: HashMap<Span, ResolvedCall> = HashMap::new();
     for f in &erasure_hints.vir_crate.functions {
-        functions.insert(f.x.name.clone(), Some(f.clone()));
+        functions.insert(f.x.path.clone(), Some(f.clone()));
+        functions_by_span.insert(from_raw_span(&f.span.raw_span), f.clone());
     }
     for name in &erasure_hints.external_functions {
         functions.insert(name.clone(), None);
@@ -385,6 +390,7 @@ fn mk_ctxt(erasure_hints: &ErasureHints) -> Ctxt {
     Ctxt {
         vir_crate: erasure_hints.vir_crate.clone(),
         functions,
+        functions_by_span,
         calls,
         condition_modes,
         var_modes,
diff --git a/verify/rust_verify/src/rust_to_vir.rs b/verify/rust_verify/src/rust_to_vir.rs
index e672d6881c7e6..23a2da4177356 100644
--- a/verify/rust_verify/src/rust_to_vir.rs
+++ b/verify/rust_verify/src/rust_to_vir.rs
@@ -14,8 +14,8 @@ use crate::util::unsupported_err_span;
 use crate::{err_unless, unsupported_err, unsupported_err_unless, unsupported_unless};
 use rustc_ast::Attribute;
 use rustc_hir::{
-    Crate, ForeignItem, ForeignItemId, ForeignItemKind, HirId, Item, ItemId, ItemKind, ModuleItems,
-    QPath, TraitRef, TyKind,
+    Crate, ForeignItem, ForeignItemId, ForeignItemKind, HirId, Item,
+    ItemId, ItemKind, ModuleItems, QPath, TraitRef, TyKind,
 };
 use rustc_middle::ty::TyCtxt;
 use std::collections::HashMap;
@@ -35,7 +35,8 @@ fn check_item<'tcx>(
             check_item_fn(
                 ctxt,
                 vir,
-                item.ident,
+                None,
+                item.def_id.to_def_id(),
                 visibility,
                 ctxt.tcx.hir().attrs(item.hir_id()),
                 sig,
@@ -189,7 +190,7 @@ fn check_item<'tcx>(
 }
 
 fn check_module<'tcx>(
-    tcx: TyCtxt<'tcx>,
+    _tcx: TyCtxt<'tcx>,
     module_path: &Path,
     module_items: &'tcx ModuleItems,
     item_to_module: &mut HashMap<ItemId, Path>,
@@ -200,18 +201,8 @@ fn check_module<'tcx>(
                 item_to_module.insert(*item_id, module_path.clone());
             }
             unsupported_unless!(trait_items.len() == 0, "trait definitions", trait_items);
-            // TODO: deduplicate with crate_to_vir
-            for id in impl_items {
-                let def_name = hack_get_def_name(tcx, id.def_id.to_def_id());
-                // TODO: check whether these implement the correct trait
-                unsupported_unless!(
-                    def_name == "assert_receiver_is_total_eq"
-                        || def_name == "eq"
-                        || def_name == "ne"
-                        || def_name == "assert_receiver_is_structural",
-                    "impl definition in module",
-                    id
-                );
+            for _id in impl_items {
+                // TODO?
             }
             for _id in foreign_items {
                 // TODO
@@ -232,7 +223,7 @@ fn check_foreign_item<'tcx>(
             check_foreign_item_fn(
                 ctxt,
                 vir,
-                item.ident,
+                item.def_id.to_def_id(),
                 item.span,
                 mk_visibility(&None, &item.vis),
                 ctxt.tcx.hir().attrs(item.hir_id()),
diff --git a/verify/rust_verify/src/rust_to_vir_expr.rs b/verify/rust_verify/src/rust_to_vir_expr.rs
index d75c5c94a5fa7..38329f57af92b 100644
--- a/verify/rust_verify/src/rust_to_vir_expr.rs
+++ b/verify/rust_verify/src/rust_to_vir_expr.rs
@@ -9,7 +9,7 @@ use crate::util::{
     vec_map_result,
 };
 use crate::{unsupported, unsupported_err, unsupported_err_unless, unsupported_unless};
-use air::ast::{Binder, BinderX, Ident, Quant};
+use air::ast::{Binder, BinderX, Quant};
 use rustc_ast::{Attribute, BorrowKind, LitKind, Mutability};
 use rustc_hir::def::{DefKind, Res};
 use rustc_hir::{
@@ -181,17 +181,15 @@ fn record_fun(
     } else if is_compilable_operator {
         ResolvedCall::CompilableOperator
     } else {
-        ResolvedCall::Call(Arc::new(hack_get_def_name(ctxt.tcx, id)))
+        ResolvedCall::Call(def_id_to_vir_path(ctxt.tcx, id))
     };
     erasure_info.resolved_calls.push((span.data(), resolved_call));
 }
 
-fn get_fn_name<'tcx>(tcx: TyCtxt<'tcx>, expr: &Expr<'tcx>) -> Result<Ident, VirErr> {
+fn get_fn_path<'tcx>(tcx: TyCtxt<'tcx>, expr: &Expr<'tcx>) -> Result<vir::ast::Path, VirErr> {
     match &expr.kind {
         ExprKind::Path(QPath::Resolved(None, path)) => match path.res {
-            Res::Def(DefKind::Fn, id) => {
-                Ok(Arc::new(hack_get_def_name(tcx, id))) // TODO: proper handling of paths
-            }
+            Res::Def(DefKind::Fn, id) => Ok(def_id_to_vir_path(tcx, id)),
             res => unsupported_err!(expr.span, format!("Path {:?}", res)),
         },
         _ => unsupported_err!(expr.span, format!("{:?}", expr)),
@@ -273,7 +271,7 @@ fn fn_call_to_vir<'tcx>(
 
     if is_hide || is_reveal {
         unsupported_err_unless!(len == 1, expr.span, "expected hide/reveal", &args);
-        let x = get_fn_name(tcx, &args[0])?;
+        let x = get_fn_path(tcx, &args[0])?;
         if is_hide {
             let header = Arc::new(HeaderExprX::Hide(x));
             return Ok(mk_expr(ExprX::Header(header)));
@@ -283,7 +281,7 @@ fn fn_call_to_vir<'tcx>(
     }
     if is_reveal_fuel {
         unsupported_err_unless!(len == 2, expr.span, "expected reveal_fuel", &args);
-        let x = get_fn_name(tcx, &args[0])?;
+        let x = get_fn_path(tcx, &args[0])?;
         match &expr_to_vir(bctx, &args[1])?.x {
             ExprX::Const(Constant::Nat(s)) => {
                 let n = s.parse::<u32>().expect(&format!("internal error: parse {}", s));
@@ -396,11 +394,10 @@ fn fn_call_to_vir<'tcx>(
             },
         };
         // make call
-        let name = hack_get_def_name(tcx, f); // TODO: proper handling of paths
         let mut call = spanned_typed_new(
             expr.span,
             &possibly_boxed_ret_typ,
-            ExprX::Call(Arc::new(name), Arc::new(typ_args), Arc::new(vir_args)),
+            ExprX::Call(def_id_to_vir_path(tcx, f), Arc::new(typ_args), Arc::new(vir_args)),
         );
         // unbox result if necessary
         if let Some(ret_typ) = ret_typ {
diff --git a/verify/rust_verify/src/rust_to_vir_func.rs b/verify/rust_verify/src/rust_to_vir_func.rs
index 6e6815da7beb8..81cfd91b2a7c1 100644
--- a/verify/rust_verify/src/rust_to_vir_func.rs
+++ b/verify/rust_verify/src/rust_to_vir_func.rs
@@ -1,7 +1,7 @@
 use crate::context::Context;
 use crate::rust_to_vir_base::{
-    check_generics, get_fuel, get_mode, get_var_mode, get_verifier_attrs, ident_to_var, ty_to_vir,
-    BodyCtxt,
+    check_generics, def_id_to_vir_path, get_fuel, get_mode, get_var_mode, get_verifier_attrs,
+    ident_to_var, ty_to_vir, BodyCtxt,
 };
 use crate::rust_to_vir_expr::{expr_to_vir, pat_to_var};
 use crate::util::{err_span_str, err_span_string, spanned_new, unsupported_err_span};
@@ -50,14 +50,15 @@ fn check_fn_decl<'tcx>(
 pub(crate) fn check_item_fn<'tcx>(
     ctxt: &Context<'tcx>,
     vir: &mut KrateX,
-    id: Ident,
+    _self_path: Option<&'tcx rustc_hir::Path<'tcx>>,
+    id: rustc_span::def_id::DefId,
     visibility: vir::ast::Visibility,
     attrs: &[Attribute],
     sig: &'tcx FnSig<'tcx>,
     generics: &'tcx Generics,
     body_id: &BodyId,
 ) -> Result<(), VirErr> {
-    let name = Arc::new(ident_to_var(&id));
+    let path = def_id_to_vir_path(ctxt.tcx, id);
     let mode = get_mode(Mode::Exec, attrs);
     let ret_typ_mode = match sig {
         FnSig {
@@ -74,7 +75,7 @@ pub(crate) fn check_item_fn<'tcx>(
     let vattrs = get_verifier_attrs(attrs)?;
     if vattrs.external {
         let mut erasure_info = ctxt.erasure_info.borrow_mut();
-        erasure_info.external_functions.push(name);
+        erasure_info.external_functions.push(path);
         return Ok(());
     }
     let body = &ctxt.krate.bodies[body_id];
@@ -129,7 +130,7 @@ pub(crate) fn check_item_fn<'tcx>(
         _ => panic!("internal error: ret_typ"),
     };
     let func = FunctionX {
-        name,
+        path,
         visibility,
         mode,
         fuel,
@@ -152,7 +153,7 @@ pub(crate) fn check_item_fn<'tcx>(
 pub(crate) fn check_foreign_item_fn<'tcx>(
     ctxt: &Context<'tcx>,
     vir: &mut KrateX,
-    id: Ident,
+    id: rustc_span::def_id::DefId,
     span: Span,
     visibility: vir::ast::Visibility,
     attrs: &[Attribute],
@@ -172,10 +173,10 @@ pub(crate) fn check_foreign_item_fn<'tcx>(
         let vir_param = spanned_new(param.span, ParamX { name, typ, mode });
         vir_params.push(vir_param);
     }
-    let name = Arc::new(ident_to_var(&id));
+    let path = def_id_to_vir_path(ctxt.tcx, id);
     let params = Arc::new(vir_params);
     let func = FunctionX {
-        name,
+        path,
         visibility,
         fuel,
         mode,
diff --git a/verify/rust_verify/src/verifier.rs b/verify/rust_verify/src/verifier.rs
index 6dc6f000adc7a..376bab095f466 100644
--- a/verify/rust_verify/src/verifier.rs
+++ b/verify/rust_verify/src/verifier.rs
@@ -12,6 +12,7 @@ use rustc_span::{CharPos, FileName, MultiSpan, Span};
 use std::fs::File;
 use std::io::Write;
 use vir::ast::{Krate, Path, VirErr, VirErrX, Visibility};
+use vir::ast_util::path_to_string;
 use vir::def::SnapPos;
 use vir::model::Model as VModel;
 
@@ -247,7 +248,7 @@ impl Verifier {
             Self::run_commands(
                 air_context,
                 &commands,
-                &("Function-Decl ".to_string() + &function.x.name),
+                &("Function-Decl ".to_string() + &path_to_string(&function.x.path)),
             );
         }
 
@@ -264,7 +265,7 @@ impl Verifier {
             Self::run_commands(
                 air_context,
                 &decl_commands,
-                &("Function-Axioms ".to_string() + &function.x.name),
+                &("Function-Axioms ".to_string() + &path_to_string(&function.x.path)),
             );
 
             // Check termination
@@ -276,7 +277,7 @@ impl Verifier {
                 air_context,
                 &check_commands,
                 &vec![],
-                &("Function-Termination ".to_string() + &function.x.name),
+                &("Function-Termination ".to_string() + &path_to_string(&function.x.path)),
             );
         }
 
@@ -291,7 +292,7 @@ impl Verifier {
                 air_context,
                 &commands,
                 &snap_map,
-                &("Function-Def ".to_string() + &function.x.name),
+                &("Function-Def ".to_string() + &path_to_string(&function.x.path)),
             );
         }
 
@@ -399,7 +400,7 @@ impl Verifier {
                 writeln!(&mut file).expect("cannot write to vir file");
             }
             for func in vir_crate.functions.iter() {
-                writeln!(&mut file, "fn {} @ {:?}", func.x.name, func.span)
+                writeln!(&mut file, "fn {} @ {:?}", path_to_string(&func.x.path), func.span)
                     .expect("cannot write to vir file");
                 for param in func.x.params.iter() {
                     writeln!(
diff --git a/verify/vir/src/ast.rs b/verify/vir/src/ast.rs
index 2ea4133f11522..45b3ce947b72a 100644
--- a/verify/vir/src/ast.rs
+++ b/verify/vir/src/ast.rs
@@ -161,7 +161,7 @@ pub enum HeaderExprX {
     Decreases(Expr, Typ),
     /// Make a function f opaque (definition hidden) within the current function body.
     /// (The current function body can later reveal f in specific parts of the current function body if desired.)
-    Hide(Ident),
+    Hide(Path),
 }
 
 /// Primitive constant values
@@ -192,7 +192,7 @@ pub enum ExprX {
     /// Call to function with given name, passing some type arguments and some expression arguments
     /// TODO: should be Path, not Ident
     /// Note: higher-order functions aren't yet supported
-    Call(Ident, Typs, Exprs),
+    Call(Path, Typs, Exprs),
     /// Construct datatype value of type Path and variant Ident, with field initializers Binders<Expr>
     Ctor(Path, Ident, Binders<Expr>),
     /// Read field from datatype
@@ -208,7 +208,7 @@ pub enum ExprX {
     /// Assign to local variable
     Assign(Expr, Expr),
     /// Reveal definition of an opaque function with some integer fuel amount
-    Fuel(Ident, u32),
+    Fuel(Path, u32),
     /// Header, which must appear at the beginning of a function or while loop.
     /// Note: this only appears temporarily during rust_to_vir construction, and should not
     /// appear in the final Expr produced by rust_to_vir (see vir::headers::read_header).
@@ -248,8 +248,7 @@ pub struct ParamX {
 pub type Function = Arc<Spanned<FunctionX>>;
 #[derive(Debug, Clone)]
 pub struct FunctionX {
-    /// TODO: should be Path, not Ident
-    pub name: Ident,
+    pub path: Path,
     pub visibility: Visibility,
     /// exec functions are compiled, proof/spec are erased
     /// exec/proof functions can have requires/ensures, spec cannot
@@ -274,7 +273,7 @@ pub struct FunctionX {
     /// Custom error message to display when a pre-condition fails
     pub custom_req_err: Option<String>,
     /// List of functions that this function wants to view as opaque
-    pub hidden: Idents,
+    pub hidden: Arc<Vec<Path>>,
     /// For public spec functions, is_abstract == true means that the body is private
     /// even though the function is public
     pub is_abstract: bool,
diff --git a/verify/vir/src/ast_to_sst.rs b/verify/vir/src/ast_to_sst.rs
index 37290425cabc4..0c602bc6f9f50 100644
--- a/verify/vir/src/ast_to_sst.rs
+++ b/verify/vir/src/ast_to_sst.rs
@@ -1,5 +1,5 @@
 use crate::ast::{
-    BinaryOp, Constant, Expr, ExprX, Function, Ident, Mode, Stmt, StmtX, Typs, VirErr,
+    BinaryOp, Constant, Expr, ExprX, Function, Ident, Mode, Path, Stmt, StmtX, Typs, VirErr,
 };
 use crate::ast_util::{err_str, err_string};
 use crate::context::Ctx;
@@ -30,15 +30,15 @@ fn assume_var(span: &Span, x: &Ident, exp: &Exp) -> Stm {
     Spanned::new(span.clone(), StmX::Assume(eq))
 }
 
-fn get_function(ctx: &Ctx, expr: &Expr, name: &Ident) -> Result<Function, VirErr> {
+fn get_function(ctx: &Ctx, expr: &Expr, name: &Path) -> Result<Function, VirErr> {
     match ctx.func_map.get(name) {
-        None => err_string(&expr.span, format!("could not find function {}", &name)),
+        None => err_string(&expr.span, format!("could not find function {:?}", &name)),
         Some(func) => Ok(func.clone()),
     }
 }
 
-fn function_can_be_exp(ctx: &Ctx, expr: &Expr, name: &Ident) -> Result<bool, VirErr> {
-    match get_function(ctx, expr, name)?.x.mode {
+fn function_can_be_exp(ctx: &Ctx, expr: &Expr, path: &Path) -> Result<bool, VirErr> {
+    match get_function(ctx, expr, path)?.x.mode {
         Mode::Spec => Ok(true),
         Mode::Proof | Mode::Exec => Ok(false),
     }
@@ -48,7 +48,7 @@ fn expr_get_call(
     ctx: &Ctx,
     state: &mut State,
     expr: &Expr,
-) -> Result<Option<(Vec<Stm>, Ident, Typs, bool, Exps)>, VirErr> {
+) -> Result<Option<(Vec<Stm>, Path, Typs, bool, Exps)>, VirErr> {
     match &expr.x {
         ExprX::Call(x, typs, args) => {
             let mut stms: Vec<Stm> = Vec::new();
@@ -70,7 +70,7 @@ fn expr_must_be_call_stm(
     ctx: &Ctx,
     state: &mut State,
     expr: &Expr,
-) -> Result<Option<(Vec<Stm>, Ident, Typs, bool, Exps)>, VirErr> {
+) -> Result<Option<(Vec<Stm>, Path, Typs, bool, Exps)>, VirErr> {
     match &expr.x {
         ExprX::Call(x, _, _) if !function_can_be_exp(ctx, expr, x)? => {
             expr_get_call(ctx, state, expr)
@@ -163,10 +163,10 @@ pub(crate) fn expr_to_stm_opt(
                 _ => err_str(&expr1.span, "complex assignments not yet supported"),
             };
             match expr_must_be_call_stm(ctx, state, expr2)? {
-                Some((mut stms2, func_name, typs, _, args)) => {
+                Some((mut stms2, func_path, typs, _, args)) => {
                     // make a Call
                     let dest = Dest { var: dest_x?.clone(), mutable: true };
-                    let call = StmX::Call(func_name, typs, args, Some(dest));
+                    let call = StmX::Call(func_path, typs, args, Some(dest));
                     stms2.push(Spanned::new(expr.span.clone(), call));
                     Ok((stms2, None))
                 }
@@ -184,7 +184,7 @@ pub(crate) fn expr_to_stm_opt(
             let (mut stms, x, typs, ret, args) = expr_get_call(ctx, state, expr)?.expect("Call");
             if function_can_be_exp(ctx, expr, &x)? {
                 // ExpX::Call
-                let call = ExpX::Call(x.clone(), typs.clone(), args);
+                let call = ExpX::Call(false, x.clone(), typs.clone(), args);
                 Ok((stms, Some(Spanned::new(expr.span.clone(), call))))
             } else if ret {
                 let temp = state.next_temp();
diff --git a/verify/vir/src/context.rs b/verify/vir/src/context.rs
index 0b68c0a9a7e54..9d94e69192e18 100644
--- a/verify/vir/src/context.rs
+++ b/verify/vir/src/context.rs
@@ -1,6 +1,7 @@
-use crate::ast::{Function, Ident, Krate, Mode, Path, Variants, VirErr};
+use crate::ast::{Function, Krate, Mode, Path, Variants, VirErr};
 use crate::def::FUEL_ID;
 use crate::scc::Graph;
+use crate::sst_to_air::path_to_air_ident;
 use air::ast::{Command, CommandX, Commands, DeclX, MultiOp, Span};
 use air::ast_util::str_typ;
 use std::collections::HashMap;
@@ -9,8 +10,8 @@ use std::sync::Arc;
 pub struct Ctx {
     pub(crate) datatypes: HashMap<Path, Variants>,
     pub(crate) functions: Vec<Function>,
-    pub(crate) func_map: HashMap<Ident, Function>,
-    pub(crate) func_call_graph: Graph<Ident>,
+    pub(crate) func_map: HashMap<Path, Function>,
+    pub(crate) func_call_graph: Graph<Path>,
     pub(crate) chosen_triggers: std::cell::RefCell<Vec<(Span, Vec<Vec<String>>)>>, // diagnostics
     pub(crate) debug: bool,
 }
@@ -23,10 +24,10 @@ impl Ctx {
             .map(|d| (d.x.path.clone(), d.x.variants.clone()))
             .collect::<HashMap<_, _>>();
         let mut functions: Vec<Function> = Vec::new();
-        let mut func_map: HashMap<Ident, Function> = HashMap::new();
-        let mut func_call_graph: Graph<Ident> = Graph::new();
+        let mut func_map: HashMap<Path, Function> = HashMap::new();
+        let mut func_call_graph: Graph<Path> = Graph::new();
         for function in krate.functions.iter() {
-            func_map.insert(function.x.name.clone(), function.clone());
+            func_map.insert(function.x.path.clone(), function.clone());
             crate::recursion::expand_call_graph(&mut func_call_graph, function)?;
             functions.push(function.clone());
         }
@@ -47,7 +48,7 @@ impl Ctx {
         for function in &self.functions {
             match (function.x.mode, function.x.body.as_ref()) {
                 (Mode::Spec, Some(_)) => {
-                    let id = crate::def::prefix_fuel_id(&function.x.name);
+                    let id = crate::def::prefix_fuel_id(&path_to_air_ident(&function.x.path));
                     ids.push(air::ast_util::ident_var(&id));
                     let typ_fuel_id = str_typ(&FUEL_ID);
                     let decl = Arc::new(DeclX::Const(id, typ_fuel_id));
diff --git a/verify/vir/src/def.rs b/verify/vir/src/def.rs
index d1e457c1a05d4..2d73f71cdae47 100644
--- a/verify/vir/src/def.rs
+++ b/verify/vir/src/def.rs
@@ -1,3 +1,4 @@
+use crate::ast_util::str_ident;
 use air::ast::{Ident, Span};
 use std::fmt::Debug;
 use std::sync::Arc;
@@ -58,7 +59,6 @@ pub const NAT_CLIP: &str = "nClip";
 pub const U_INV: &str = "uInv";
 pub const I_INV: &str = "iInv";
 pub const ARCH_SIZE: &str = "SZ";
-pub const CHECK_DECREASE_INT: &str = "check_decrease_int";
 pub const DECREASE_AT_ENTRY: &str = "decrease%init";
 pub const SNAPSHOT_CALL: &str = "CALL";
 pub const UNIT: &str = "Unit";
@@ -82,6 +82,10 @@ pub const PREFIX_TYPE_ID: &str = "TYPE%";
 pub const HAS_TYPE: &str = "has_type";
 pub const VARIANT_FIELD_SEPARATOR: &str = "/";
 
+pub fn check_decrease_int() -> crate::ast::Path {
+    Arc::new(vec![str_ident("check_decrease_int")])
+}
+
 pub fn suffix_global_id(ident: &Ident) -> Ident {
     Arc::new(ident.to_string() + SUFFIX_GLOBAL)
 }
diff --git a/verify/vir/src/func_to_air.rs b/verify/vir/src/func_to_air.rs
index 3e46455651b4e..b6dcf007440f0 100644
--- a/verify/vir/src/func_to_air.rs
+++ b/verify/vir/src/func_to_air.rs
@@ -5,7 +5,7 @@ use crate::def::{
     suffix_global_id, suffix_local_id, suffix_typ_param_id, SnapPos, Spanned, FUEL_BOOL,
     FUEL_BOOL_DEFAULT, FUEL_LOCAL, FUEL_TYPE, SUCC, ZERO,
 };
-use crate::sst_to_air::{exp_to_expr, typ_invariant, typ_to_air};
+use crate::sst_to_air::{exp_to_expr, path_to_air_ident, typ_invariant, typ_to_air};
 use crate::util::{vec_map, vec_map_result};
 use air::ast::{
     BinaryOp, Bind, BindX, Command, CommandX, Commands, DeclX, Expr, ExprX, MultiOp, Quant, Span,
@@ -74,7 +74,7 @@ fn func_body_to_air(
     function: &Function,
     body: &crate::ast::Expr,
 ) -> Result<(), VirErr> {
-    let id_fuel = prefix_fuel_id(&function.x.name);
+    let id_fuel = prefix_fuel_id(&path_to_air_ident(&function.x.path));
 
     // ast --> sst
     let body_exp = crate::ast_to_sst::expr_to_exp(&ctx, &body)?;
@@ -103,8 +103,8 @@ fn func_body_to_air(
     let def_body = if !is_recursive {
         body_expr
     } else {
-        let rec_f = suffix_global_id(&prefix_recursive(&function.x.name));
-        let fuel_nat_f = prefix_fuel_nat(&function.x.name);
+        let rec_f = suffix_global_id(&prefix_recursive(&path_to_air_ident(&function.x.path)));
+        let fuel_nat_f = prefix_fuel_nat(&path_to_air_ident(&function.x.path));
         let args = func_def_args(&function.x.typ_params, &function.x.params);
         let mut args_zero = args.clone();
         let mut args_fuel = args.clone();
@@ -136,7 +136,7 @@ fn func_body_to_air(
     };
     let e_forall = func_def_quant(
         ctx,
-        &suffix_global_id(&function.x.name),
+        &suffix_global_id(&path_to_air_ident(&function.x.path)),
         &function.x.typ_params,
         &function.x.params,
         def_body,
@@ -202,15 +202,16 @@ pub fn func_name_to_air(ctx: &Ctx, function: &Function) -> Result<Commands, VirE
     if let (Mode::Spec, Some((_, ret, _))) = (function.x.mode, function.x.ret.as_ref()) {
         // Declare the function symbol itself
         let typ = typ_to_air(ctx, &ret);
-        let name = suffix_global_id(&function.x.name);
+        let name = suffix_global_id(&path_to_air_ident(&function.x.path));
         let decl = Arc::new(DeclX::Fun(name, Arc::new(all_typs), typ));
         commands.push(Arc::new(CommandX::Global(decl)));
 
         // Check whether we need to declare the recursive version too
         if let Some(body) = &function.x.body {
             let body_exp = crate::ast_to_sst::expr_to_exp(&ctx, &body)?;
-            if crate::recursion::is_recursive_exp(ctx, &function.x.name, &body_exp) {
-                let rec_f = suffix_global_id(&prefix_recursive(&function.x.name));
+            if crate::recursion::is_recursive_exp(ctx, &function.x.path, &body_exp) {
+                let rec_f =
+                    suffix_global_id(&prefix_recursive(&path_to_air_ident(&function.x.path)));
                 let mut rec_typs =
                     vec_map(&*function.x.params, |param| typ_to_air(ctx, &param.x.typ));
                 rec_typs.push(str_typ(FUEL_TYPE));
@@ -233,7 +234,7 @@ pub fn func_decl_to_air(ctx: &Ctx, function: &Function) -> Result<(Commands, Com
     let mut check_commands: Vec<Command> = Vec::new();
     match (function.x.mode, function.x.ret.as_ref()) {
         (Mode::Spec, Some((_, ret, _))) => {
-            let name = suffix_global_id(&function.x.name);
+            let name = suffix_global_id(&path_to_air_ident(&function.x.path));
 
             // Body
             if let Some(body) = &function.x.body {
@@ -274,7 +275,7 @@ pub fn func_decl_to_air(ctx: &Ctx, function: &Function) -> Result<(Commands, Com
                 &function.x.require,
                 &function.x.typ_params,
                 &param_typs,
-                &prefix_requires(&function.x.name),
+                &prefix_requires(&path_to_air_ident(&function.x.path)),
                 &msg,
             )?;
             let mut ens_typs = (*param_typs).clone();
@@ -296,7 +297,7 @@ pub fn func_decl_to_air(ctx: &Ctx, function: &Function) -> Result<(Commands, Com
                 &function.x.ensure,
                 &function.x.typ_params,
                 &Arc::new(ens_typs),
-                &prefix_ensures(&function.x.name),
+                &prefix_ensures(&path_to_air_ident(&function.x.path)),
                 &None,
             )?;
         }
diff --git a/verify/vir/src/headers.rs b/verify/vir/src/headers.rs
index 9fb88c3d4d159..4f34fbb315805 100644
--- a/verify/vir/src/headers.rs
+++ b/verify/vir/src/headers.rs
@@ -1,10 +1,10 @@
-use crate::ast::{Expr, ExprX, Exprs, HeaderExprX, Ident, Stmt, StmtX, Typ, VirErr};
+use crate::ast::{Expr, ExprX, Exprs, HeaderExprX, Ident, Path, Stmt, StmtX, Typ, VirErr};
 use crate::ast_util::err_str;
 use std::sync::Arc;
 
 #[derive(Clone, Debug)]
 pub struct Header {
-    pub hidden: Vec<Ident>,
+    pub hidden: Vec<Path>,
     pub require: Exprs,
     pub ensure_id_typ: Option<(Ident, Typ)>,
     pub ensure: Exprs,
@@ -13,7 +13,7 @@ pub struct Header {
 }
 
 fn read_header_block(block: &mut Vec<Stmt>) -> Result<Header, VirErr> {
-    let mut hidden: Vec<Ident> = Vec::new();
+    let mut hidden: Vec<Path> = Vec::new();
     let mut require: Option<Exprs> = None;
     let mut ensure: Option<(Option<(Ident, Typ)>, Exprs)> = None;
     let mut invariant: Option<Exprs> = None;
diff --git a/verify/vir/src/modes.rs b/verify/vir/src/modes.rs
index 683e607282908..363bea8b481fc 100644
--- a/verify/vir/src/modes.rs
+++ b/verify/vir/src/modes.rs
@@ -34,7 +34,7 @@ pub struct ErasureModes {
 }
 
 struct Typing {
-    pub(crate) funs: HashMap<Ident, Function>,
+    pub(crate) funs: HashMap<Path, Function>,
     pub(crate) datatypes: HashMap<Path, Datatype>,
     pub(crate) vars: ScopeMap<Ident, Mode>,
     pub(crate) erasure_modes: ErasureModes,
@@ -236,10 +236,10 @@ fn check_function(typing: &mut Typing, function: &Function) -> Result<(), VirErr
 }
 
 pub fn check_crate(krate: &Krate) -> Result<ErasureModes, VirErr> {
-    let mut funs: HashMap<Ident, Function> = HashMap::new();
+    let mut funs: HashMap<Path, Function> = HashMap::new();
     let mut datatypes: HashMap<Path, Datatype> = HashMap::new();
     for function in krate.functions.iter() {
-        funs.insert(function.x.name.clone(), function.clone());
+        funs.insert(function.x.path.clone(), function.clone());
     }
     for datatype in krate.datatypes.iter() {
         datatypes.insert(datatype.x.path.clone(), datatype.clone());
diff --git a/verify/vir/src/prelude.rs b/verify/vir/src/prelude.rs
index 069ec129a2075..4abc8199200b9 100644
--- a/verify/vir/src/prelude.rs
+++ b/verify/vir/src/prelude.rs
@@ -1,6 +1,6 @@
 use crate::def::*;
+use crate::sst_to_air::path_to_air_ident;
 use air::ast::Ident;
-use air::ast_util::str_ident;
 use air::printer::{macro_push_node, str_to_node};
 use air::{node, nodes_vec};
 use sise::Node;
@@ -24,7 +24,8 @@ pub(crate) fn prelude_nodes() -> Vec<Node> {
     let u_inv = str_to_node(U_INV);
     let i_inv = str_to_node(I_INV);
     let arch_size = str_to_node(ARCH_SIZE);
-    let check_decrease_int = str_to_node(&suffix_global_id(&str_ident(CHECK_DECREASE_INT)));
+    let check_decrease_int =
+        str_to_node(&suffix_global_id(&path_to_air_ident(&check_decrease_int())));
     #[allow(non_snake_case)]
     let Unit = str_to_node(UNIT);
     #[allow(non_snake_case)]
diff --git a/verify/vir/src/recursion.rs b/verify/vir/src/recursion.rs
index fa3b2089aa6f0..7ab3f0c3d9729 100644
--- a/verify/vir/src/recursion.rs
+++ b/verify/vir/src/recursion.rs
@@ -1,10 +1,8 @@
-use crate::ast::{BinaryOp, Constant, Function, Ident, Params, Typ, TypX, UnaryOp, VirErr};
+use crate::ast::{BinaryOp, Constant, Function, Ident, Params, Path, Typ, TypX, UnaryOp, VirErr};
 use crate::ast_util::err_str;
 use crate::ast_visitor::map_expr_visitor;
 use crate::context::Ctx;
-use crate::def::{
-    prefix_recursive, suffix_rename, Spanned, CHECK_DECREASE_INT, DECREASE_AT_ENTRY, FUEL_PARAM,
-};
+use crate::def::{check_decrease_int, suffix_rename, Spanned, DECREASE_AT_ENTRY, FUEL_PARAM};
 use crate::scc::Graph;
 use crate::sst::{BndX, Exp, ExpX, Exps, Stm, StmX};
 use crate::sst_visitor::{exp_rename_vars, map_exp_visitor, map_stm_visitor};
@@ -15,12 +13,12 @@ use std::sync::Arc;
 
 #[derive(Clone)]
 struct Ctxt<'a> {
-    recursive_function_name: Ident,
+    recursive_function_path: Path,
     params: Params,
     decreases_at_entry: Ident,
     decreases_exp: Exp,
     decreases_typ: Typ,
-    scc_rep: Ident,
+    scc_rep: Path,
     ctx: &'a Ctx,
 }
 
@@ -31,7 +29,8 @@ fn check_decrease(ctxt: &Ctxt, exp: &Exp) -> Exp {
         TypX::Int(_) => {
             // 0 <= decreases_exp < decreases_at_entry
             let call = ExpX::Call(
-                str_ident(CHECK_DECREASE_INT),
+                false,
+                check_decrease_int(),
                 Arc::new(vec![]),
                 Arc::new(vec![exp.clone(), decreases_at_entry]),
             );
@@ -62,7 +61,7 @@ fn check_decrease_rename(ctxt: &Ctxt, span: &Span, args: &Exps) -> Exp {
     check_decrease(ctxt, &e_dec)
 }
 
-fn update_decreases_exp<'a>(ctxt: &'a Ctxt, name: &Ident) -> Result<Ctxt<'a>, VirErr> {
+fn update_decreases_exp<'a>(ctxt: &'a Ctxt, name: &Path) -> Result<Ctxt<'a>, VirErr> {
     let function = ctxt.ctx.func_map.get(name).expect("func_map should hold all functions");
     let (new_decreases_expr, _) = function
         .x
@@ -80,8 +79,8 @@ fn terminates(ctxt: &Ctxt, exp: &Exp) -> Result<Exp, VirErr> {
         ExpX::Const(_) | ExpX::Var(_) | ExpX::Old(_, _) => {
             Ok(Spanned::new(exp.span.clone(), ExpX::Const(Constant::Bool(true))))
         }
-        ExpX::Call(x, _, args) => {
-            let mut e = if *x == ctxt.recursive_function_name
+        ExpX::Call(_, x, _, args) => {
+            let mut e = if *x == ctxt.recursive_function_path
                 || ctxt.ctx.func_call_graph.get_scc_rep(x) == ctxt.scc_rep
             {
                 let new_ctxt = update_decreases_exp(&ctxt, x)?;
@@ -167,7 +166,7 @@ fn terminates(ctxt: &Ctxt, exp: &Exp) -> Result<Exp, VirErr> {
     }
 }
 
-pub(crate) fn is_recursive_exp(ctx: &Ctx, name: &Ident, body: &Exp) -> bool {
+pub(crate) fn is_recursive_exp(ctx: &Ctx, name: &Path, body: &Exp) -> bool {
     if ctx.func_call_graph.get_scc_size(name) > 1 {
         // This function is part of a mutually recursive component
         true
@@ -175,7 +174,7 @@ pub(crate) fn is_recursive_exp(ctx: &Ctx, name: &Ident, body: &Exp) -> bool {
         // Check for self-recursion, which SCC computation does not account for
         let mut recurse = false;
         map_exp_visitor(body, &mut |exp| match &exp.x {
-            ExpX::Call(x, _, _) if x == name => {
+            ExpX::Call(_, x, _, _) if x == name => {
                 recurse = true;
                 exp.clone()
             }
@@ -185,7 +184,7 @@ pub(crate) fn is_recursive_exp(ctx: &Ctx, name: &Ident, body: &Exp) -> bool {
     }
 }
 
-pub(crate) fn is_recursive_stm(ctx: &Ctx, name: &Ident, body: &Stm) -> bool {
+pub(crate) fn is_recursive_stm(ctx: &Ctx, name: &Path, body: &Stm) -> bool {
     if ctx.func_call_graph.get_scc_size(name) > 1 {
         // This function is part of a mutually recursive component
         true
@@ -233,7 +232,7 @@ pub(crate) fn check_termination_exp(
     function: &Function,
     body: &Exp,
 ) -> Result<(bool, Commands, Exp), VirErr> {
-    if !is_recursive_exp(ctx, &function.x.name, body) {
+    if !is_recursive_exp(ctx, &function.x.path, body) {
         return Ok((false, Arc::new(vec![]), body.clone()));
     }
 
@@ -245,10 +244,10 @@ pub(crate) fn check_termination_exp(
     };
     let decreases_exp = crate::ast_to_sst::expr_to_exp(ctx, &decreases_expr)?;
     let decreases_at_entry = str_ident(DECREASE_AT_ENTRY);
-    let scc_rep = ctx.func_call_graph.get_scc_rep(&function.x.name);
+    let scc_rep = ctx.func_call_graph.get_scc_rep(&function.x.path);
     let scc_rep_clone = scc_rep.clone();
     let ctxt = Ctxt {
-        recursive_function_name: function.x.name.clone(),
+        recursive_function_path: function.x.path.clone(),
         params: function.x.params.clone(),
         decreases_at_entry,
         decreases_exp,
@@ -281,13 +280,15 @@ pub(crate) fn check_termination_exp(
 
     // New body: substitute rec%f(args, fuel) for f(args)
     let body = map_exp_visitor(&body, &mut |exp| match &exp.x {
-        ExpX::Call(x, typs, args)
-            if *x == function.x.name || ctx.func_call_graph.get_scc_rep(x) == scc_rep_clone =>
+        ExpX::Call(_, x, typs, args)
+            if *x == function.x.path || ctx.func_call_graph.get_scc_rep(x) == scc_rep_clone =>
         {
-            let rec_x = prefix_recursive(x);
             let mut args = (**args).clone();
             args.push(Spanned::new(exp.span.clone(), ExpX::Var(str_ident(FUEL_PARAM))));
-            Spanned::new(exp.span.clone(), ExpX::Call(rec_x, typs.clone(), Arc::new(args)))
+            Spanned::new(
+                exp.span.clone(),
+                ExpX::Call(true, x.clone(), typs.clone(), Arc::new(args)),
+            )
         }
         _ => exp.clone(),
     });
@@ -300,7 +301,7 @@ pub(crate) fn check_termination_stm(
     function: &Function,
     body: &Stm,
 ) -> Result<Stm, VirErr> {
-    if !is_recursive_stm(ctx, &function.x.name, body) {
+    if !is_recursive_stm(ctx, &function.x.path, body) {
         return Ok(body.clone());
     }
 
@@ -312,9 +313,9 @@ pub(crate) fn check_termination_stm(
     };
     let decreases_exp = crate::ast_to_sst::expr_to_exp(ctx, &decreases_expr)?;
     let decreases_at_entry = str_ident(DECREASE_AT_ENTRY);
-    let scc_rep = ctx.func_call_graph.get_scc_rep(&function.x.name);
+    let scc_rep = ctx.func_call_graph.get_scc_rep(&function.x.path);
     let ctxt = Ctxt {
-        recursive_function_name: function.x.name.clone(),
+        recursive_function_path: function.x.path.clone(),
         params: function.x.params.clone(),
         decreases_at_entry,
         decreases_exp,
@@ -324,7 +325,7 @@ pub(crate) fn check_termination_stm(
     };
     let stm = map_stm_visitor(body, &mut |s| match &s.x {
         StmX::Call(x, _, args, _)
-            if *x == function.x.name || ctx.func_call_graph.get_scc_rep(x) == ctxt.scc_rep =>
+            if *x == function.x.path || ctx.func_call_graph.get_scc_rep(x) == ctxt.scc_rep =>
         {
             let new_ctxt = update_decreases_exp(&ctxt, x)?;
             let check = check_decrease_rename(&new_ctxt, &s.span, &args);
@@ -348,8 +349,8 @@ pub(crate) fn check_termination_stm(
 }
 
 fn add_call_graph_edges(
-    call_graph: &mut Graph<Ident>,
-    src: &Ident,
+    call_graph: &mut Graph<Path>,
+    src: &Path,
     expr: &crate::ast::Expr,
 ) -> Result<crate::ast::Expr, VirErr> {
     use crate::ast::ExprX;
@@ -362,13 +363,13 @@ fn add_call_graph_edges(
 }
 
 pub(crate) fn expand_call_graph(
-    call_graph: &mut Graph<Ident>,
+    call_graph: &mut Graph<Path>,
     function: &Function,
 ) -> Result<(), VirErr> {
     // We only traverse expressions (not statements), since calls only appear in the former (see ast.rs)
     if let Some(body) = &function.x.body {
         map_expr_visitor(body, &mut |expr| {
-            add_call_graph_edges(call_graph, &function.x.name, expr)
+            add_call_graph_edges(call_graph, &function.x.path, expr)
         })?;
     }
     Ok(())
diff --git a/verify/vir/src/sst.rs b/verify/vir/src/sst.rs
index 59e1858814b82..0d4080b70fadc 100644
--- a/verify/vir/src/sst.rs
+++ b/verify/vir/src/sst.rs
@@ -27,8 +27,8 @@ pub type Exps = Arc<Vec<Exp>>;
 pub enum ExpX {
     Const(Constant),
     Var(Ident),
-    Old(Ident, Ident),       // used only during sst_to_air to generate AIR Old
-    Call(Ident, Typs, Exps), // call to spec function
+    Old(Ident, Ident), // used only during sst_to_air to generate AIR Old
+    Call(/* recursive: */ bool, Path, Typs, Exps), // call to spec function
     Ctor(Path, Ident, Binders<Exp>),
     Field { lhs: Exp, datatype: Path, field_name: Ident },
     Unary(UnaryOp, Exp),
@@ -48,7 +48,7 @@ pub type Stm = Arc<Spanned<StmX>>;
 pub type Stms = Arc<Vec<Stm>>;
 #[derive(Debug)]
 pub enum StmX {
-    Call(Ident, Typs, Exps, Option<Dest>), // call to exec/proof function
+    Call(Path, Typs, Exps, Option<Dest>), // call to exec/proof function
     Assert(Exp),
     Assume(Exp),
     Decl {
@@ -58,7 +58,7 @@ pub enum StmX {
         init: bool,
     },
     Assign(Exp, Exp),
-    Fuel(Ident, u32),
+    Fuel(Path, u32),
     If(Exp, Stm, Option<Stm>),
     While {
         cond: Exp,
diff --git a/verify/vir/src/sst_to_air.rs b/verify/vir/src/sst_to_air.rs
index b2187156cfa1a..a310b69ac9f9c 100644
--- a/verify/vir/src/sst_to_air.rs
+++ b/verify/vir/src/sst_to_air.rs
@@ -4,9 +4,10 @@ use crate::ast::{
 use crate::ast_util::path_to_string;
 use crate::context::Ctx;
 use crate::def::{
-    prefix_ensures, prefix_fuel_id, prefix_requires, prefix_type_id, suffix_global_id,
-    suffix_local_id, suffix_typ_param_id, SnapPos, Spanned, FUEL_BOOL, FUEL_BOOL_DEFAULT,
-    FUEL_DEFAULTS, FUEL_ID, FUEL_PARAM, FUEL_TYPE, POLY, SNAPSHOT_CALL, SUCC, UNIT,
+    prefix_ensures, prefix_fuel_id, prefix_recursive, prefix_requires, prefix_type_id,
+    suffix_global_id, suffix_local_id, suffix_typ_param_id, SnapPos, Spanned, FUEL_BOOL,
+    FUEL_BOOL_DEFAULT, FUEL_DEFAULTS, FUEL_ID, FUEL_PARAM, FUEL_TYPE, POLY, SNAPSHOT_CALL, SUCC,
+    UNIT,
 };
 use crate::sst::{BndX, Dest, Exp, ExpX, Stm, StmX};
 use crate::util::vec_map;
@@ -134,8 +135,10 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp) -> Expr {
         }
         ExpX::Var(x) => string_var(&suffix_local_id(x)),
         ExpX::Old(span, x) => Arc::new(ExprX::Old(span.clone(), suffix_local_id(x))),
-        ExpX::Call(x, typs, args) => {
-            let name = suffix_global_id(&x);
+        ExpX::Call(rec, x, typs, args) => {
+            let air_ident = path_to_air_ident(&x);
+            let name =
+                suffix_global_id(&if *rec { prefix_recursive(&air_ident) } else { air_ident });
             let mut exprs: Vec<Expr> = vec_map(typs, typ_to_id);
             for arg in args.iter() {
                 exprs.push(exp_to_expr(ctx, arg));
@@ -289,7 +292,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec<Stmt> {
             let mut stmts: Vec<Stmt> = Vec::new();
             let func = &ctx.func_map[x];
             if func.x.require.len() > 0 {
-                let f_req = prefix_requires(&func.x.name);
+                let f_req = prefix_requires(&path_to_air_ident(&func.x.path));
                 let mut req_args = vec_map(typs, typ_to_id);
                 for arg in args.iter() {
                     req_args.push(exp_to_expr(ctx, arg));
@@ -354,7 +357,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec<Stmt> {
                 }
             }
             if func.x.ensure.len() > 0 {
-                let f_ens = prefix_ensures(&func.x.name);
+                let f_ens = prefix_ensures(&path_to_air_ident(&func.x.path));
                 let e_ens = Arc::new(ExprX::Apply(f_ens, Arc::new(ens_args)));
                 stmts.push(Arc::new(StmtX::Assume(e_ens)));
             }
@@ -563,7 +566,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec<Stmt> {
             let mut stmts: Vec<Stmt> = Vec::new();
             if *fuel >= 1 {
                 // (assume (fuel_bool fuel%f))
-                let id_fuel = prefix_fuel_id(&x);
+                let id_fuel = prefix_fuel_id(&path_to_air_ident(&x));
                 let expr_fuel_bool = str_apply(&FUEL_BOOL, &vec![ident_var(&id_fuel)]);
                 stmts.push(Arc::new(StmtX::Assume(expr_fuel_bool)));
             }
@@ -573,7 +576,10 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec<Stmt> {
                 for _ in 0..*fuel - 1 {
                     added_fuel = str_apply(SUCC, &vec![added_fuel]);
                 }
-                let eq = mk_eq(&ident_var(&crate::def::prefix_fuel_nat(&x)), &added_fuel);
+                let eq = mk_eq(
+                    &ident_var(&crate::def::prefix_fuel_nat(&path_to_air_ident(&x))),
+                    &added_fuel,
+                );
                 let binder = ident_binder(&str_ident(FUEL_PARAM), &str_typ(FUEL_TYPE));
                 stmts.push(Arc::new(StmtX::Assume(mk_exists(&vec![binder], &vec![], &eq))));
             }
@@ -588,7 +594,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec<Stmt> {
     }
 }
 
-fn set_fuel(local: &mut Vec<Decl>, hidden: &Vec<Ident>) {
+fn set_fuel(local: &mut Vec<Decl>, hidden: &Vec<Path>) {
     let fuel_expr = if hidden.len() == 0 {
         str_var(&FUEL_DEFAULTS)
     } else {
@@ -604,7 +610,7 @@ fn set_fuel(local: &mut Vec<Decl>, hidden: &Vec<Ident>) {
 
         // ... || id == hidden1 || id == hidden2 || ...
         for hide in hidden {
-            let x_hide = ident_var(&prefix_fuel_id(&hide));
+            let x_hide = ident_var(&prefix_fuel_id(&path_to_air_ident(hide)));
             disjuncts.push(Arc::new(ExprX::Binary(air::ast::BinaryOp::Eq, x_id.clone(), x_hide)));
         }
 
@@ -624,7 +630,7 @@ pub fn body_stm_to_air(
     typ_params: &Idents,
     params: &Params,
     ret: &Option<(Ident, Typ, Mode)>,
-    hidden: &Vec<Ident>,
+    hidden: &Vec<Path>,
     reqs: &Vec<Exp>,
     enss: &Vec<Exp>,
     stm: &Stm,
diff --git a/verify/vir/src/sst_visitor.rs b/verify/vir/src/sst_visitor.rs
index a443400935d1f..8bf2592dc0f2d 100644
--- a/verify/vir/src/sst_visitor.rs
+++ b/verify/vir/src/sst_visitor.rs
@@ -18,13 +18,15 @@ where
         ExpX::Const(_) => f(exp, map),
         ExpX::Var(_) => f(exp, map),
         ExpX::Old(_, _) => f(exp, map),
-        ExpX::Call(x, typs, es) => {
+        ExpX::Call(rec, x, typs, es) => {
             let mut exps: Vec<Exp> = Vec::new();
             for e in es.iter() {
                 exps.push(map_exp_visitor_bind(e, map, f)?);
             }
-            let exp =
-                Spanned::new(exp.span.clone(), ExpX::Call(x.clone(), typs.clone(), Arc::new(exps)));
+            let exp = Spanned::new(
+                exp.span.clone(),
+                ExpX::Call(*rec, x.clone(), typs.clone(), Arc::new(exps)),
+            );
             f(&exp, map)
         }
         ExpX::Ctor(path, ident, binders) => {
diff --git a/verify/vir/src/triggers.rs b/verify/vir/src/triggers.rs
index 422598f4bf025..cac9f01e4c3eb 100644
--- a/verify/vir/src/triggers.rs
+++ b/verify/vir/src/triggers.rs
@@ -16,14 +16,14 @@ struct State {
 
 fn check_trigger_expr(exp: &Exp, free_vars: &mut HashSet<Ident>) -> Result<(), VirErr> {
     match &exp.x {
-        ExpX::Call(_, _, _) | ExpX::Field { .. } | ExpX::Unary(UnaryOp::Trigger(_), _) => {}
+        ExpX::Call(_, _, _, _) | ExpX::Field { .. } | ExpX::Unary(UnaryOp::Trigger(_), _) => {}
         // REVIEW: Z3 allows some arithmetic, but it's not clear we want to allow it
         _ => {
             return err_str(&exp.span, "trigger must be a function call or a field access");
         }
     }
     let mut f = |exp: &Exp, _: &mut _| match &exp.x {
-        ExpX::Const(_) | ExpX::Call(_, _, _) | ExpX::Field { .. } | ExpX::Ctor(_, _, _) => {
+        ExpX::Const(_) | ExpX::Call(_, _, _, _) | ExpX::Field { .. } | ExpX::Ctor(_, _, _) => {
             Ok(exp.clone())
         }
         ExpX::Var(x) => {
diff --git a/verify/vir/src/triggers_auto.rs b/verify/vir/src/triggers_auto.rs
index c5849df51bef1..13d7fa7e92890 100644
--- a/verify/vir/src/triggers_auto.rs
+++ b/verify/vir/src/triggers_auto.rs
@@ -1,6 +1,7 @@
 use crate::ast::{BinaryOp, Ident, Path, UnaryOp, UnaryOpr, VirErr};
 use crate::ast_util::err_str;
 use crate::context::Ctx;
+use crate::def::prefix_recursive;
 use crate::sst::{Exp, ExpX, Trig, Trigs};
 use crate::sst_to_air::path_to_air_ident;
 use crate::util::vec_map;
@@ -192,11 +193,18 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter
             return (true, Arc::new(TermX::Var(x.clone())));
         }
         ExpX::Old(_, _) => panic!("internal error: Old"),
-        ExpX::Call(x, _, args) => {
+        ExpX::Call(recursive, x, _, args) => {
             let (is_pures, terms): (Vec<bool>, Vec<Term>) =
                 args.iter().map(|e| gather_terms(ctxt, ctx, e, depth + 1)).unzip();
             let is_pure = is_pures.into_iter().all(|b| b);
-            (is_pure, Arc::new(TermX::App(App::Call(x.clone()), Arc::new(terms))))
+            let air_ident = path_to_air_ident(&x);
+            (
+                is_pure,
+                Arc::new(TermX::App(
+                    App::Call(if *recursive { prefix_recursive(&air_ident) } else { air_ident }),
+                    Arc::new(terms),
+                )),
+            )
         }
         ExpX::Ctor(path, variant, fields) => {
             let (variant, args) = crate::sst_to_air::ctor_to_apply(ctx, path, variant, fields);
diff --git a/verify/vir/src/well_formed.rs b/verify/vir/src/well_formed.rs
index d4c0ddd7cc3cc..260ab6a67240d 100644
--- a/verify/vir/src/well_formed.rs
+++ b/verify/vir/src/well_formed.rs
@@ -1,11 +1,11 @@
-use crate::ast::{Datatype, Expr, ExprX, Function, Ident, Krate, Mode, Path, VirErr};
+use crate::ast::{Datatype, Expr, ExprX, Function, Krate, Mode, Path, VirErr};
 use crate::ast_util::err_string;
 use crate::ast_visitor::map_expr_visitor;
 use crate::datatype_to_air::is_datatype_transparent;
 use std::collections::HashMap;
 
 struct Ctxt {
-    pub(crate) funs: HashMap<Ident, Function>,
+    pub(crate) funs: HashMap<Path, Function>,
     pub(crate) dts: HashMap<Path, Datatype>,
 }
 
@@ -71,7 +71,7 @@ pub fn check_crate(krate: &Krate) -> Result<(), VirErr> {
     let funs = krate
         .functions
         .iter()
-        .map(|function| (function.x.name.clone(), function.clone()))
+        .map(|function| (function.x.path.clone(), function.clone()))
         .collect();
     let dts = krate
         .datatypes