diff --git a/src/analyze.rs b/src/analyze.rs
index a4ffa5f4..5c9cf9bc 100644
--- a/src/analyze.rs
+++ b/src/analyze.rs
@@ -8,6 +8,7 @@
 
 use std::cell::RefCell;
 use std::collections::HashMap;
+use std::hash::Hash;
 use std::rc::Rc;
 
 use rustc_hir::lang_items::LangItem;
@@ -19,7 +20,7 @@ use rustc_span::Symbol;
 
 use crate::analyze;
 use crate::annot::{AnnotFormula, AnnotParser, Resolver};
-use crate::chc;
+use crate::chc::{self, ForallSortIdx};
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{self, BasicBlockType, TypeBuilder};
 use crate::rty;
@@ -163,9 +164,18 @@ struct DeferredDefTy<'tcx> {
     mode: DeferredDefMode,
 }
 
+#[derive(Debug, Clone)]
+struct GenericDefTy<'tcx> {
+    // this is different from a key in defs when the def is extern_spec_fn
+    local_def_id: LocalDefId,
+    cache: Rc<RefCell<HashMap<mir_ty::GenericArgsRef<'tcx>, rty::RefinedType>>>,
+    rty: Option<rty::RefinedType>,
+}
+
 #[derive(Debug, Clone)]
 enum DefTy<'tcx> {
     Concrete(rty::RefinedType),
+    Generic(GenericDefTy<'tcx>),
     Deferred(DeferredDefTy<'tcx>),
 }
 
@@ -201,6 +211,13 @@ impl refine::EnumDefProvider for Rc<RefCell<EnumDefs>> {
 }
 
 pub type Env = refine::Env<Rc<RefCell<EnumDefs>>>;
+pub type TypeParamMap<'tcx> = HashMap<TypeParam, ForallSortIdx>;
+
+#[derive(Eq, PartialEq, Hash, Debug, Clone)]
+pub enum TypeParam {
+    GenericType(DefId, u32),
+    AssocType(DefId, Vec<rty::Type<rty::Closed>>),
+}
 
 #[derive(Debug, Clone)]
 struct DeferredFormulaFnDef<'tcx> {
@@ -228,6 +245,9 @@ pub struct Analyzer<'tcx> {
     def_ids: did_cache::DefIdCache<'tcx>,
 
     enum_defs: Rc<RefCell<EnumDefs>>,
+
+    type_params: Rc<RefCell<TypeParamMap<'tcx>>>,
+    closure_type_params: Rc<RefCell<HashMap<TypeParam, rty::FunctionType>>>,
 }
 
 impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> {
@@ -255,6 +275,8 @@ impl<'tcx> Analyzer<'tcx> {
         let system = Default::default();
         let basic_blocks = Default::default();
         let enum_defs = Default::default();
+        let type_params = Default::default();
+        let closure_type_params = Default::default();
         Self {
             tcx,
             defs,
@@ -263,6 +285,8 @@ impl<'tcx> Analyzer<'tcx> {
             basic_blocks,
             def_ids: did_cache::DefIdCache::new(tcx),
             enum_defs,
+            type_params,
+            closure_type_params,
         }
     }
 
@@ -296,7 +320,7 @@ impl<'tcx> Analyzer<'tcx> {
                     .iter()
                     .map(|field| {
                         let field_ty = self.tcx.type_of(field.did).instantiate_identity();
-                        TypeBuilder::new(self.tcx, self.def_ids(), def_id).build(field_ty)
+                        self.type_builder(self.def_ids(), def_id).build(field_ty)
                     })
                     .collect();
                 rty::EnumVariantDef {
@@ -391,19 +415,40 @@ impl<'tcx> Analyzer<'tcx> {
             ?mode,
             "register_deferred_def"
         );
-        self.defs.insert(
-            target_def_id,
+        self.defs.entry(target_def_id).or_insert_with(|| {
             DefTy::Deferred(DeferredDefTy {
                 local_def_id,
                 cache: Rc::new(RefCell::new(HashMap::new())),
                 mode,
+            })
+        });
+    }
+
+    pub fn register_generic_def(
+        &mut self,
+        target_def_id: DefId,
+        local_def_id: LocalDefId,
+        rty: Option<rty::RefinedType>,
+    ) {
+        tracing::info!(?target_def_id, ?local_def_id, ?rty, "register_generic_def");
+        self.defs.insert(
+            target_def_id,
+            DefTy::Generic(GenericDefTy {
+                rty,
+                local_def_id,
+                cache: Rc::new(RefCell::new(HashMap::new())),
             }),
         );
     }
 
+    pub fn get_closure_type(&self, type_param: TypeParam) -> Option<rty::FunctionType> {
+        self.closure_type_params.borrow().get(&type_param).cloned()
+    }
+
     pub fn concrete_def_ty(&self, def_id: DefId) -> Option<&rty::RefinedType> {
         self.defs.get(&def_id).and_then(|def_ty| match def_ty {
             DefTy::Concrete(rty) => Some(rty),
+            DefTy::Generic(GenericDefTy { rty, .. }) => rty.as_ref(),
             DefTy::Deferred(_) => None,
         })
     }
@@ -416,9 +461,17 @@ impl<'tcx> Analyzer<'tcx> {
         def_id: DefId,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
     ) -> Option<rty::FunctionType> {
-        let type_builder = TypeBuilder::new(self.tcx, self.def_ids(), def_id);
+        let type_builder = TypeBuilder::new(
+            self.tcx,
+            self.def_ids(),
+            def_id,
+            self.type_params.clone(),
+            self.closure_type_params.clone(),
+            self.system.clone(),
+        );
         let mut def_ty = match self.defs.get(&def_id)? {
             DefTy::Concrete(rty) => rty.clone(),
+            DefTy::Generic(generic) => generic.cache.borrow().get(&generic_args)?.clone(),
             DefTy::Deferred(deferred) => deferred.cache.borrow().get(&generic_args)?.clone(),
         };
         def_ty.instantiate_ty_params(
@@ -435,6 +488,7 @@ impl<'tcx> Analyzer<'tcx> {
         &self,
         local_def_id: LocalDefId,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        owner_fn_id: DefId,
     ) -> Option<annot_fn::FormulaFn<'tcx>> {
         let deferred_formula_fn = self.formula_fns.get(&local_def_id)?;
 
@@ -443,8 +497,9 @@ impl<'tcx> Analyzer<'tcx> {
             return Some(formula_fn.clone());
         }
 
-        let translator = annot_fn::AnnotFnTranslator::new(self, local_def_id, generic_args)
-            .with_def_id_cache(self.def_ids());
+        let translator =
+            annot_fn::AnnotFnTranslator::new(self, local_def_id, generic_args, owner_fn_id)
+                .with_def_id_cache(self.def_ids());
         let formula_fn = translator.to_formula_fn();
         deferred_formula_fn_cache
             .borrow_mut()
@@ -454,53 +509,62 @@ impl<'tcx> Analyzer<'tcx> {
         Some(formula_fn)
     }
 
+    fn instantiate_generic_args(
+        ty: &mut rty::RefinedType,
+        generic_args: mir_ty::GenericArgsRef<'tcx>,
+        type_builder: &TypeBuilder<'tcx>,
+    ) {
+        ty.instantiate_ty_params(
+            generic_args
+                .types()
+                .map(|ty| type_builder.build(ty))
+                .map(rty::RefinedType::unrefined)
+                .collect(),
+        );
+    }
+
     pub fn def_ty_with_args(
         &mut self,
         def_id: DefId,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        caller_def_id: DefId,
     ) -> Option<rty::RefinedType> {
-        let type_builder = TypeBuilder::new(self.tcx, self.def_ids(), def_id);
-
-        let deferred_ty = match self.defs.get(&def_id)? {
-            DefTy::Concrete(rty) => {
-                let mut def_ty = rty.clone();
-                def_ty.instantiate_ty_params(
-                    generic_args
-                        .types()
-                        .map(|ty| type_builder.build(ty))
-                        .map(rty::RefinedType::unrefined)
-                        .collect(),
-                );
-                return Some(def_ty);
-            }
-            DefTy::Deferred(deferred) => deferred,
-        };
+        let type_builder = self.type_builder(self.def_ids(), caller_def_id);
+
+        let (local_def_id, instantiated_ty_cache, deferred_ty_mode) =
+            match self.defs.get(&def_id)? {
+                DefTy::Concrete(rty) => {
+                    let mut def_ty = rty.clone();
+                    Self::instantiate_generic_args(&mut def_ty, generic_args, &type_builder);
+                    return Some(def_ty);
+                }
+                DefTy::Generic(generic) => (generic.local_def_id, Rc::clone(&generic.cache), None),
+                DefTy::Deferred(deferred) => (
+                    deferred.local_def_id,
+                    Rc::clone(&deferred.cache),
+                    Some(deferred.mode),
+                ),
+            };
 
-        let deferred_ty_cache = Rc::clone(&deferred_ty.cache); // to cut reference to allow &mut self
-        if let Some(rty) = deferred_ty_cache.borrow().get(&generic_args) {
+        if let Some(rty) = instantiated_ty_cache.borrow().get(&generic_args) {
             return Some(rty.clone());
         }
-        let deferred_ty_mode = deferred_ty.mode;
 
-        let mut analyzer = self.local_def_analyzer(deferred_ty.local_def_id);
-        analyzer.generic_args(generic_args);
+        let mut analyzer = self.local_def_analyzer(local_def_id);
+        analyzer
+            .owner_fn_id(caller_def_id)
+            .generic_args(generic_args);
 
         let mut expected = analyzer.expected_ty();
         // parameters in annotations are left as params
         // TODO: remove this after annotation V2
-        expected.instantiate_ty_params(
-            generic_args
-                .types()
-                .map(|ty| type_builder.build(ty))
-                .map(rty::RefinedType::unrefined)
-                .collect(),
-        );
-        deferred_ty_cache
+        Self::instantiate_generic_args(&mut expected, generic_args, &type_builder);
+        instantiated_ty_cache
             .borrow_mut()
             .insert(generic_args, expected.clone());
         tracing::info!(?def_id, rty = %expected.display(), ?generic_args, "deferred def");
 
-        if deferred_ty_mode.should_analyze() {
+        if deferred_ty_mode.is_some_and(|mode| mode.should_analyze()) {
             let mut body_analyzer = if analyzer.local_def_id().to_def_id() == def_id {
                 analyzer
             } else {
@@ -640,8 +704,20 @@ impl<'tcx> Analyzer<'tcx> {
         &mut self,
         local_def_id: LocalDefId,
         bb: BasicBlock,
+        owner_fn_id: DefId,
     ) -> basic_block::Analyzer<'tcx, '_> {
-        basic_block::Analyzer::new(self, local_def_id, bb)
+        basic_block::Analyzer::new(self, local_def_id, bb, owner_fn_id)
+    }
+
+    pub fn type_builder(&self, def_ids: DefIdCache<'tcx>, owner_fn_id: DefId) -> TypeBuilder<'tcx> {
+        TypeBuilder::new(
+            self.tcx,
+            def_ids,
+            owner_fn_id,
+            self.type_params.clone(),
+            self.closure_type_params.clone(),
+            self.system.clone(),
+        )
     }
 
     pub fn solve(&mut self) {
@@ -735,6 +811,7 @@ impl<'tcx> Analyzer<'tcx> {
         resolver: T,
         self_type_name: Option<String>,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        owner_fn_id: DefId,
     ) -> Option<AnnotFormula<T::Output>>
     where
         T: Resolver<Output = rty::FunctionParamIdx>,
@@ -765,7 +842,9 @@ impl<'tcx> Analyzer<'tcx> {
             if require_annot.is_some() {
                 unimplemented!();
             }
-            let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else {
+            let Some(formula_fn) =
+                self.formula_fn_with_args(formula_def_id, generic_args, owner_fn_id)
+            else {
                 panic!(
                     "require annotation {:?} is not a formula function",
                     formula_def_id
@@ -784,6 +863,7 @@ impl<'tcx> Analyzer<'tcx> {
         resolver: T,
         self_type_name: Option<String>,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        owner_fn_id: DefId,
     ) -> Option<AnnotFormula<T::Output>>
     where
         T: Resolver<Output = rty::RefinedTypeVar<rty::FunctionParamIdx>>,
@@ -815,7 +895,9 @@ impl<'tcx> Analyzer<'tcx> {
             if ensure_annot.is_some() {
                 unimplemented!();
             }
-            let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else {
+            let Some(formula_fn) =
+                self.formula_fn_with_args(formula_def_id, generic_args, owner_fn_id)
+            else {
                 panic!(
                     "ensure annotation {:?} is not a formula function",
                     formula_def_id
@@ -886,6 +968,7 @@ impl<'tcx> Analyzer<'tcx> {
         &self,
         local_def_id: LocalDefId,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        owner_fn_id: DefId,
     ) -> Vec<(rty::TypePosition, rty::Refinement<rty::FunctionParamIdx>)> {
         let mut out = Vec::new();
         for (position, def_id) in self.extract_refinement_paths(local_def_id) {
@@ -895,7 +978,9 @@ impl<'tcx> Analyzer<'tcx> {
                     def_id
                 );
             };
-            let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else {
+            let Some(formula_fn) =
+                self.formula_fn_with_args(formula_def_id, generic_args, owner_fn_id)
+            else {
                 panic!(
                     "refinement_path annotation {:?} is not a formula function",
                     formula_def_id
diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs
index 0249e4aa..ce9dcb7a 100644
--- a/src/analyze/annot_fn.rs
+++ b/src/analyze/annot_fn.rs
@@ -1,13 +1,16 @@
 use std::collections::HashMap;
 
 use pretty::{termcolor, Pretty};
-use rustc_hir::{def_id::LocalDefId, HirId};
+use rustc_hir::{
+    def_id::{DefId, LocalDefId},
+    HirId,
+};
 use rustc_index::IndexVec;
-use rustc_middle::ty::{self as mir_ty, TyCtxt};
+use rustc_middle::ty::{self as mir_ty, TyCtxt, TypeFoldable};
 
 use crate::analyze::{self, did_cache::DefIdCache};
 use crate::annot::AnnotFormula;
-use crate::chc;
+use crate::chc::{self};
 use crate::refine::{self, TypeBuilder};
 use crate::rty;
 
@@ -178,12 +181,20 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
         analyzer: &'a analyze::Analyzer<'tcx>,
         local_def_id: LocalDefId,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        owner_fn_id: DefId,
     ) -> Self {
         let tcx = analyzer.tcx();
         let body = tcx.hir_body_owned_by(local_def_id);
         let typeck = tcx.typeck(local_def_id);
         let def_ids = analyzer.def_ids();
-        let type_builder = TypeBuilder::new(tcx, def_ids.clone(), local_def_id.to_def_id());
+        let type_builder = TypeBuilder::new(
+            tcx,
+            def_ids.clone(),
+            owner_fn_id,
+            analyzer.type_params.clone(),
+            analyzer.closure_type_params.clone(),
+            analyzer.system.clone(),
+        );
         let mut translator = Self {
             tcx,
             local_def_id,
@@ -201,11 +212,6 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
 
     pub fn with_def_id_cache(mut self, def_ids: DefIdCache<'tcx>) -> Self {
         self.def_ids = def_ids;
-        self.type_builder = TypeBuilder::new(
-            self.tcx,
-            self.def_ids.clone(),
-            self.local_def_id.to_def_id(),
-        );
         self
     }
 
@@ -285,29 +291,52 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
         }
     }
 
+    fn instantiate_generics<T>(
+        &self,
+        ty: T,
+        generic_args: mir_ty::GenericArgsRef<'tcx>,
+    ) -> Option<T>
+    where
+        T: TypeFoldable<TyCtxt<'tcx>>,
+    {
+        if !self.generic_args.is_empty() {
+            Some(mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, generic_args))
+        } else {
+            None
+        }
+    }
+
     fn expr_ty(&self, expr: &'tcx rustc_hir::Expr<'tcx>) -> mir_ty::Ty<'tcx> {
         let ty = self.typeck.expr_ty(expr);
-        let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args);
+        let instantiated = self
+            .instantiate_generics(ty, self.generic_args)
+            .unwrap_or(ty);
         let typing_env = mir_ty::TypingEnv::fully_monomorphized();
-        self.tcx.normalize_erasing_regions(typing_env, instantiated)
+        self.tcx
+            .try_normalize_erasing_regions(typing_env, instantiated)
+            .unwrap_or(instantiated)
     }
 
     fn pat_ty(&self, pat: &'tcx rustc_hir::Pat<'tcx>) -> mir_ty::Ty<'tcx> {
         let ty = self.typeck.pat_ty(pat);
-        let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args);
+        let instantiated = self
+            .instantiate_generics(ty, self.generic_args)
+            .unwrap_or(ty);
         let typing_env = mir_ty::TypingEnv::fully_monomorphized();
-        self.tcx.normalize_erasing_regions(typing_env, instantiated)
+        self.tcx
+            .try_normalize_erasing_regions(typing_env, instantiated)
+            .unwrap_or(instantiated)
     }
 
     pub fn to_formula_fn(&self) -> FormulaFn<'tcx> {
         let formula = self.to_formula(self.body.value);
-        let params = self
-            .tcx
-            .fn_sig(self.local_def_id.to_def_id())
-            .instantiate(self.tcx, self.generic_args)
-            .skip_binder()
-            .inputs()
-            .to_vec();
+        let fn_sig = self.tcx.fn_sig(self.local_def_id.to_def_id());
+        let binder = if self.generic_args.is_empty() {
+            fn_sig.skip_binder()
+        } else {
+            fn_sig.instantiate(self.tcx, self.generic_args)
+        };
+        let params = binder.skip_binder().inputs().to_vec();
         FormulaFn {
             params: IndexVec::from_raw(params),
             formula,
@@ -349,12 +378,164 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
     fn receiver_closure_fn_type(&self, receiver_ty: mir_ty::Ty<'tcx>) -> Option<rty::FunctionType> {
         let closure_ty = self.receiver_closure_ty(receiver_ty)?;
         let mir_ty::TyKind::Closure(def_id, args) = closure_ty.kind() else {
+            if let mir_ty::TyKind::Param(ty) = closure_ty.kind() {
+                tracing::debug!("ParamTy is found: {ty:?}");
+                let closure_fun_ty = self.type_param_as_callable_sig(*ty);
+                tracing::debug!(
+                    "the obtained FunctionType for the closure {ty:?}: {closure_fun_ty:#?}"
+                );
+                if let Some(closure_fun_ty) = closure_fun_ty.clone() {
+                    self.type_builder.register_closure_type_param(
+                        analyze::TypeParam::GenericType(self.type_builder.owner_fn_id(), ty.index),
+                        closure_fun_ty,
+                    );
+                };
+                return closure_fun_ty;
+            }
             return None;
         };
         self.analyzer
             .known_function_ty_with_args(*def_id, self.tcx.mk_args(args.as_closure().parent_args()))
     }
 
+    #[tracing::instrument(skip(self))]
+    fn closure_trait_args(
+        &self,
+        param_ty: mir_ty::ParamTy,
+        pred: mir_ty::TraitPredicate<'tcx>,
+    ) -> Option<IndexVec<rty::FunctionParamIdx, rty::RefinedType<rty::FunctionParamIdx>>> {
+        let trait_ref = pred.trait_ref;
+        if trait_ref.self_ty() != param_ty.to_ty(self.tcx) {
+            return None;
+        }
+        tracing::debug!(?trait_ref.args);
+
+        let receiver_type = self.type_builder.build(trait_ref.args.type_at(0));
+
+        use mir_ty::ClosureKind::*;
+        let receiver_type = match self.tcx.fn_trait_kind_from_def_id(trait_ref.def_id)? {
+            Fn => rty::PointerType::immut_to(receiver_type).into(),
+            FnMut => rty::PointerType::mut_to(receiver_type).into(),
+            FnOnce => receiver_type,
+        };
+
+        let mir_ty::Tuple(other_params) = trait_ref.args.type_at(1).kind() else {
+            panic!()
+        };
+
+        let other_params = other_params
+            .iter()
+            .map(|ty| self.type_builder.build(ty).vacuous());
+        let params = std::iter::once(receiver_type.vacuous())
+            .chain(other_params)
+            .map(rty::RefinedType::unrefined)
+            .collect();
+
+        tracing::debug!("found the signature for closure trait: {params:#?}");
+        Some(params)
+    }
+
+    #[tracing::instrument(skip(self))]
+    fn closure_trait_ret(
+        &self,
+        param_ty: mir_ty::ParamTy,
+        pred: mir_ty::ProjectionPredicate<'tcx>,
+    ) -> Option<rty::RefinedType<rty::FunctionParamIdx>> {
+        let projection = pred.projection_term;
+        if projection.def_id != self.tcx.lang_items().fn_once_output()?
+            || projection.args.type_at(0) != param_ty.to_ty(self.tcx)
+        {
+            return None;
+        }
+
+        let ret_ty = self.type_builder.build(pred.term.expect_type()).vacuous();
+        tracing::debug!(?ret_ty);
+        Some(rty::RefinedType::unrefined(ret_ty))
+    }
+
+    fn register_forall_pred(&self, forall_pred: chc::ForallPred) {
+        self.analyzer
+            .system
+            .borrow_mut()
+            .register_forall_pred(forall_pred.clone());
+    }
+
+    fn type_param_as_callable_sig(&self, param_ty: mir_ty::ParamTy) -> Option<rty::FunctionType> {
+        let param_ty = self
+            .instantiate_generics(param_ty, self.generic_args)
+            .unwrap_or(param_ty);
+        let mut predicates = self
+            .tcx
+            .predicates_of(self.local_def_id)
+            .predicates
+            .iter()
+            .map(|(clause, _)| {
+                self.instantiate_generics(*clause, self.generic_args)
+                    .unwrap_or(*clause)
+            });
+
+        let mut params = predicates.clone().find_map(|clause| {
+            self.closure_trait_args(param_ty, clause.as_trait_clause()?.skip_binder())
+        })?;
+        let mut ret = predicates.find_map(|clause| {
+            self.closure_trait_ret(param_ty, clause.as_projection_clause()?.skip_binder())
+        })?;
+
+        let free = |idx| chc::Term::var(rty::RefinedTypeVar::Free(idx));
+        let value = chc::Term::var(rty::RefinedTypeVar::Value);
+
+        let receiver = rty::FunctionParamIdx::from_usize(0);
+        let args: Vec<_> = params
+            .iter()
+            .enumerate()
+            .skip(1)
+            .map(|(idx, _)| free(rty::FunctionParamIdx::from_usize(idx)))
+            .collect();
+
+        let type_params = vec![self.type_builder.build(param_ty.to_ty(self.tcx)).to_sort()];
+        let mut params_sort: Vec<chc::Sort> = params.iter().map(|rty| rty.ty.to_sort()).collect();
+        let ret_sort = ret.ty.to_sort();
+
+        let pre_pred = refine::closure_pre_forall_pred(
+            self.tcx,
+            self.type_builder.owner_fn_id(),
+            type_params.clone(),
+            params_sort.clone(),
+        );
+        self.register_forall_pred(pre_pred.clone());
+        params_sort.push(ret_sort);
+        let post_pred = refine::closure_post_forall_pred(
+            self.tcx,
+            self.type_builder.owner_fn_id(),
+            type_params,
+            params_sort,
+        );
+        self.register_forall_pred(post_pred.clone());
+
+        params[receiver].extend_refinement(
+            chc::Atom::new(
+                pre_pred.into(),
+                [vec![value.clone()], args.clone()].concat(),
+            )
+            .into(),
+        );
+
+        ret.extend_refinement(
+            chc::Atom::new(
+                post_pred.into(),
+                [vec![free(receiver)], args, vec![value.clone()]].concat(),
+            )
+            .into(),
+        );
+        let ret = Box::new(ret);
+
+        Some(rty::FunctionType {
+            params,
+            ret,
+            abi: rty::FunctionAbi::RustCall,
+        })
+    }
+
     /// Extracts the logical argument terms passed to `closure_precondition`/
     /// `closure_postcondition`. The arguments are supplied as a single tuple (e.g. `(x,)` or
     /// `()`), whose elements are the logical arguments of the closure.
@@ -749,8 +930,12 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                                 outer_generic_args = ?self.generic_args,
                                 "resolving predicate call in formula"
                             );
-                            let generic_args = mir_ty::EarlyBinder::bind(generic_args)
-                                .instantiate(self.tcx, self.generic_args);
+                            let (mut is_unresolved_args, generic_args) =
+                                match self.instantiate_generics(generic_args, self.generic_args) {
+                                    Some(args) => (false, args),
+                                    None => (true, generic_args),
+                                };
+
                             let instance = mir_ty::Instance::try_resolve(
                                 self.tcx,
                                 typing_env,
@@ -761,11 +946,40 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                             let pred_def_id = if let Some(instance) = instance {
                                 instance.def_id()
                             } else {
+                                is_unresolved_args = true;
                                 def_id
                             };
-                            let pred = refine::user_defined_pred(self.tcx, pred_def_id);
+
+                            let pred = if is_unresolved_args {
+                                tracing::debug!(?self.local_def_id, ?generic_args, "owner_fn_id={:?}", self.type_builder.owner_fn_id());
+                                let type_params = generic_args
+                                    .types()
+                                    .map(|ty| self.type_builder.build(ty).to_sort())
+                                    .collect();
+
+                                let typeck_result = self.tcx.typeck(self.local_def_id);
+                                let params = args
+                                    .iter()
+                                    .map(|expr| {
+                                        let ty = typeck_result.expr_ty(expr);
+                                        self.type_builder.build(ty).to_sort()
+                                    })
+                                    .collect();
+
+                                let pred = refine::trait_forall_pred(
+                                    self.tcx,
+                                    pred_def_id,
+                                    type_params,
+                                    params,
+                                );
+                                self.register_forall_pred(pred.clone());
+                                pred.into()
+                            } else {
+                                refine::user_defined_pred(self.tcx, pred_def_id).into()
+                            };
+                            tracing::debug!("resolved predicate call in formula: {:?}", pred);
                             let arg_terms = args.iter().map(|e| self.to_term(e)).collect();
-                            let atom = chc::Atom::new(pred.into(), arg_terms);
+                            let atom = chc::Atom::new(pred, arg_terms);
                             return FormulaOrTerm::Formula(chc::Formula::Atom(atom));
                         }
                     }
diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
index 835a6623..1f8aeed3 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -9,7 +9,7 @@ use rustc_middle::mir::{
 use rustc_middle::ty::{self as mir_ty, TyCtxt};
 use rustc_span::def_id::{DefId, LocalDefId};
 
-use crate::analyze;
+use crate::analyze::{self, TypeParam};
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{
@@ -131,6 +131,11 @@ impl PrecondCapture {
     }
 }
 
+enum ResolvedCallable<'tcx> {
+    Closure(DefId, mir_ty::GenericArgsRef<'tcx>),
+    Generic(TypeParam),
+}
+
 pub struct Analyzer<'tcx, 'ctx> {
     ctx: &'ctx mut analyze::Analyzer<'tcx>,
     tcx: TyCtxt<'tcx>,
@@ -603,7 +608,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 _ty,
             ) => {
                 let func_ty = match operand.const_fn_def() {
-                    Some((def_id, args)) => self.fn_def_ty(def_id, args),
+                    Some((def_id, args)) => self.callable_ty(def_id, args),
                     _ => unimplemented!(),
                 };
                 PlaceType::with_ty_and_term(func_ty.vacuous(), chc::Term::null())
@@ -830,49 +835,67 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         });
     }
 
-    fn resolve_fn_def(
+    fn resolve_callable(
         &self,
         def_id: DefId,
         args: mir_ty::GenericArgsRef<'tcx>,
-    ) -> (DefId, mir_ty::GenericArgsRef<'tcx>) {
+    ) -> ResolvedCallable<'tcx> {
         if self.ctx.is_fn_trait_method(def_id) {
             // When calling a closure via `Fn`/`FnMut`/`FnOnce` trait,
             // we simply replace the def_id with the closure's function def_id.
             // This skips shims, and makes self arguments mismatch. visitor::RustCallVisitor
             // adjusts the arguments accordingly.
-            let mir_ty::TyKind::Closure(closure_def_id, closure_args) = args.type_at(0).kind()
-            else {
-                panic!("expected closure arg for fn trait");
-            };
-            tracing::debug!(?closure_def_id, "closure instance");
-            // closure_args contains [parent_generics..., upvars, return_ty, fn_sig_binder, ...].
-            // Only the parent generics are meaningful to def_ty_with_args; the rest are internal
-            // closure encoding that type_builder.build() cannot handle.
-            let parent_count = self.tcx.generics_of(*closure_def_id).parent_count;
-            let parent_args = self.tcx.mk_args(&closure_args[..parent_count]);
-            (*closure_def_id, parent_args)
+            match args.type_at(0).kind() {
+                mir_ty::TyKind::Closure(closure_def_id, closure_args) => {
+                    tracing::debug!(?closure_def_id, "closure instance");
+                    // closure_args contains [parent_generics..., upvars, return_ty, fn_sig_binder, ...].
+                    // Only the parent generics are meaningful to def_ty_with_args; the rest are internal
+                    // closure encoding that type_builder.build() cannot handle.
+                    let parent_count = self.tcx.generics_of(*closure_def_id).parent_count;
+                    let parent_args = self.tcx.mk_args(&closure_args[..parent_count]);
+                    ResolvedCallable::Closure(*closure_def_id, parent_args)
+                }
+                mir_ty::TyKind::Param(ty) => ResolvedCallable::Generic(TypeParam::GenericType(
+                    self.type_builder.owner_fn_id(),
+                    ty.index,
+                )),
+                kind => {
+                    panic!("expected closure arg for fn trait, got: {kind:?}");
+                }
+            }
         } else {
             let typing_env = self.body.typing_env(self.tcx);
             let instance =
                 mir_ty::Instance::try_resolve(self.tcx, typing_env, def_id, args).unwrap();
             if let Some(instance) = instance {
-                (instance.def_id(), instance.args)
+                ResolvedCallable::Closure(instance.def_id(), instance.args)
             } else {
-                (def_id, args)
+                ResolvedCallable::Closure(def_id, args)
             }
         }
     }
 
-    fn fn_def_ty(
+    fn callable_ty(
         &mut self,
         def_id: DefId,
         args: mir_ty::GenericArgsRef<'tcx>,
     ) -> rty::Type<rty::Closed> {
-        if let Some(def_ty) = self.ctx.def_ty_with_args(def_id, args) {
+        let caller_def_id = self.type_builder.owner_fn_id();
+        if let Some(def_ty) = self.ctx.def_ty_with_args(def_id, args, caller_def_id) {
             return def_ty.ty;
         }
 
-        let (resolved_def_id, resolved_args) = self.resolve_fn_def(def_id, args);
+        let (resolved_def_id, resolved_args) = match self.resolve_callable(def_id, args) {
+            ResolvedCallable::Closure(def_id, args) => (def_id, args),
+            ResolvedCallable::Generic(type_param) => {
+                tracing::debug!(?type_param, ?self.ctx.closure_type_params);
+                return self
+                    .ctx
+                    .get_closure_type(type_param)
+                    .expect("unknown closure type")
+                    .into();
+            }
+        };
         if resolved_def_id == def_id {
             panic!(
                 "unknown def (and not resolved): {:?}, args: {:?}",
@@ -880,7 +903,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             );
         }
         tracing::info!(?def_id, ?resolved_def_id, ?resolved_args, "resolved");
-        let Some(def_ty) = self.ctx.def_ty_with_args(resolved_def_id, resolved_args) else {
+        let Some(def_ty) = self
+            .ctx
+            .def_ty_with_args(resolved_def_id, resolved_args, caller_def_id)
+        else {
             panic!(
                 "unknown def (resolved): {:?}, args: {:?}",
                 resolved_def_id, resolved_args
@@ -895,7 +921,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     {
         // TODO: handle const_fn_def on Env side
         let func_ty = if let Some((def_id, args)) = func.const_fn_def() {
-            self.fn_def_ty(def_id, args).vacuous()
+            self.callable_ty(def_id, args).vacuous()
         } else {
             self.operand_type(func.clone()).ty
         };
@@ -1333,6 +1359,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         ctx: &'ctx mut analyze::Analyzer<'tcx>,
         local_def_id: LocalDefId,
         basic_block: BasicBlock,
+        owner_fn_id: DefId,
     ) -> Self {
         let tcx = ctx.tcx;
         let drop_points = DropPoints::default();
@@ -1340,7 +1367,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let env = ctx.new_env();
         let local_decls = body.local_decls.clone();
         let prophecy_vars = Default::default();
-        let type_builder = TypeBuilder::new(tcx, ctx.def_ids(), local_def_id.to_def_id());
+        let type_builder = ctx.type_builder(ctx.def_ids(), owner_fn_id);
         Self {
             ctx,
             tcx,
diff --git a/src/analyze/basic_block/visitor/rust_call.rs b/src/analyze/basic_block/visitor/rust_call.rs
index b46c0467..16feb1bb 100644
--- a/src/analyze/basic_block/visitor/rust_call.rs
+++ b/src/analyze/basic_block/visitor/rust_call.rs
@@ -70,7 +70,7 @@ impl<'a, 'tcx, 'ctx> mir::visit::MutVisitor<'tcx> for RustCallVisitor<'a, 'tcx,
                 // RustCallVisitor expects all generic args to be already instantiated
                 let mir_ty::TyKind::Closure(resolved_def_id, _) = generic_args.type_at(0).kind()
                 else {
-                    panic!("expected closure arg for fn trait");
+                    return;
                 };
                 let fn_sig = self.analyzer.ctx().fn_sig(*resolved_def_id);
                 if !matches!(fn_sig.abi, rustc_abi::ExternAbi::RustCall) {
diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs
index 74198f18..e1e66b30 100644
--- a/src/analyze/crate_.rs
+++ b/src/analyze/crate_.rs
@@ -8,7 +8,7 @@ use rustc_span::def_id::LocalDefId;
 
 use crate::analyze;
 use crate::chc;
-use crate::rty::{self, ClauseBuilderExt as _};
+use crate::rty::ClauseBuilderExt as _;
 
 /// An implementation of local crate analysis.
 ///
@@ -70,7 +70,6 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(local_def_id)))]
     fn refine_fn_def(&mut self, local_def_id: LocalDefId) {
         let sig = self.ctx.fn_sig(local_def_id.to_def_id());
-
         let mut analyzer = self.ctx.local_def_analyzer(local_def_id);
 
         if analyzer.is_annotated_as_trusted() {
@@ -113,26 +112,24 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             }
         }
 
-        let target_def_id = if analyzer.is_annotated_as_extern_spec_fn() {
-            analyzer.extern_spec_fn_target_def_id()
-        } else {
-            local_def_id.to_def_id()
-        };
-
+        let owner_fn_id = analyzer.owner_fn_id;
         use mir_ty::TypeVisitableExt as _;
         if sig.has_param() {
-            // TODO: needs clear criteria on whether extern_spec'ed target fn is analyzed or not
-            if target_def_id.as_local().is_none_or(|def_id| {
+            if owner_fn_id.as_local().is_none_or(|def_id| {
                 self.skip_analysis.contains(&def_id) || !self.tcx.is_mir_available(def_id)
             }) {
                 self.ctx
-                    .register_deferred_def_without_analysis(target_def_id, local_def_id);
+                    .register_deferred_def_without_analysis(owner_fn_id, local_def_id);
+            } else if analyzer.is_fully_annotated() {
+                let expected = analyzer.expected_ty();
+                self.ctx
+                    .register_generic_def(owner_fn_id, local_def_id, Some(expected));
             } else {
-                self.ctx.register_deferred_def(target_def_id, local_def_id);
+                self.ctx.register_deferred_def(owner_fn_id, local_def_id);
             }
         } else {
             let expected = analyzer.expected_ty();
-            self.ctx.register_def(target_def_id, expected);
+            self.ctx.register_def(owner_fn_id, expected);
         }
     }
 
@@ -142,25 +139,19 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 continue;
             };
             if self.skip_analysis.contains(local_def_id) {
+                tracing::debug!("this is marked as skip analysis: {:?}", local_def_id);
                 continue;
             }
 
             let Some(expected) = self.ctx.concrete_def_ty(local_def_id.to_def_id()) else {
                 // when the local_def_id is deferred it would be skipped
+                tracing::debug!("this is marked as deferred type: {:?}", local_def_id);
                 continue;
             };
 
             // check polymorphic function def by replacing type params with some opaque type
             // (and this is no-op if the function is mono)
-            let mut expected = expected.clone();
-            let subst = rty::TypeParamSubst::new(
-                expected
-                    .free_ty_params()
-                    .into_iter()
-                    .map(|ty_param| (ty_param, rty::RefinedType::unrefined(rty::Type::int())))
-                    .collect(),
-            );
-            expected.subst_ty_params(&subst);
+            let expected = expected.clone();
             let generic_args = self.placeholder_generic_args(*local_def_id);
             self.ctx
                 .local_def_analyzer(*local_def_id)
@@ -198,13 +189,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             let param = generics.param_at(idx, self.tcx);
             let arg = match param.kind {
                 mir_ty::GenericParamDefKind::Type { .. } => {
-                    if constrained_params.contains(&param.index) {
-                        panic!(
-                            "unable to check generic function with constrained type parameter: {}",
-                            self.tcx.def_path_str(local_def_id)
-                        );
-                    }
-                    self.tcx.types.i32.into()
+                    let new_param = mir_ty::Ty::new_param(self.tcx, param.index, param.name).into();
+                    tracing::debug!(
+                        "replace the cosnstrained param {:#?} with the new param {:#?}.",
+                        param,
+                        new_param
+                    );
+                    new_param
                 }
                 mir_ty::GenericParamDefKind::Const { .. } => {
                     unimplemented!()
diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs
index 15149120..b7da0aa4 100644
--- a/src/analyze/did_cache.rs
+++ b/src/analyze/did_cache.rs
@@ -58,6 +58,10 @@ impl<'tcx> DefIdCache<'tcx> {
         self.tcx.lang_items().owned_box()
     }
 
+    pub fn vec(&self) -> Option<DefId> {
+        self.tcx.get_diagnostic_item(Symbol::intern("Vec"))
+    }
+
     pub fn unique(&self) -> Option<DefId> {
         *self.def_ids.unique.get_or_init(|| {
             let box_did = self.box_()?;
diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs
index 3938e071..51678f00 100644
--- a/src/analyze/local_def.rs
+++ b/src/analyze/local_def.rs
@@ -36,6 +36,82 @@ fn stmt_str_literal(stmt: &rustc_hir::Stmt) -> Option<String> {
     }
 }
 
+fn is_annotated_as_extern_spec_fn_impl(tcx: &TyCtxt, local_def_id: &LocalDefId) -> bool {
+    tcx.get_attrs_by_path(
+        local_def_id.to_def_id(),
+        &analyze::annot::extern_spec_fn_path(),
+    )
+    .next()
+    .is_some()
+}
+
+/// Extract the target DefId from `#[thrust::extern_spec_fn]` function.
+///
+/// The target is identified as the tail call expression (last expression without
+/// semicolon) in the function body block.
+fn extern_spec_fn_target_def_id_impl<'tcx>(
+    tcx: &TyCtxt<'tcx>,
+    local_def_id: &LocalDefId,
+    mir_body: &Body<'tcx>,
+) -> DefId {
+    let hir_node = tcx.hir_node_by_def_id(*local_def_id);
+    let hir_body_id = match hir_node {
+        rustc_hir::Node::Item(item) => {
+            let rustc_hir::ItemKind::Fn { body: body_id, .. } = item.kind else {
+                panic!("extern_spec_fn must be a function");
+            };
+            body_id
+        }
+        rustc_hir::Node::ImplItem(impl_item) => {
+            let rustc_hir::ImplItemKind::Fn(_, body_id) = impl_item.kind else {
+                panic!("extern_spec_fn must be a function");
+            };
+            body_id
+        }
+        rustc_hir::Node::TraitItem(trait_item) => {
+            let rustc_hir::TraitItemKind::Fn(_, rustc_hir::TraitFn::Provided(body_id)) =
+                trait_item.kind
+            else {
+                panic!("extern_spec_fn must be a function with a body");
+            };
+            body_id
+        }
+        _ => panic!("extern_spec_fn must be a function item or impl item"),
+    };
+
+    let hir_body = tcx.hir_body(hir_body_id);
+
+    // The body is a block; the tail expression is the function call to the target.
+    let rustc_hir::ExprKind::Block(block, _) = &hir_body.value.kind else {
+        panic!("extern_spec_fn body must be a block");
+    };
+    let tail_expr = block
+        .expr
+        .expect("extern_spec_fn block must end with a tail call expression");
+
+    let rustc_hir::ExprKind::Call(func_expr, _) = &tail_expr.kind else {
+        panic!("extern_spec_fn tail expression must be a function call");
+    };
+    let rustc_hir::ExprKind::Path(qpath) = &func_expr.kind else {
+        panic!("extern_spec_fn call must be a path expression");
+    };
+
+    let typeck_result = tcx.typeck(local_def_id);
+    let hir_id = func_expr.hir_id;
+    let rustc_hir::def::Res::Def(_, def_id) = typeck_result.qpath_res(qpath, hir_id) else {
+        panic!("extern_spec_fn call must resolve to a definition");
+    };
+
+    let args = typeck_result.node_args(hir_id);
+    let typing_env = mir_body.typing_env(*tcx);
+    let instance = mir_ty::Instance::try_resolve(*tcx, typing_env, def_id, args).unwrap();
+    if let Some(instance) = instance {
+        instance.def_id()
+    } else {
+        def_id
+    }
+}
+
 /// An implementation of the typing of local definitions.
 ///
 /// The current implementation only applies to function definitions. The entry point is
@@ -45,6 +121,7 @@ pub struct Analyzer<'tcx, 'ctx> {
     tcx: TyCtxt<'tcx>,
 
     local_def_id: LocalDefId,
+    pub owner_fn_id: DefId,
 
     body: Body<'tcx>,
     /// to substitute HIR types during translation in [`crate::analyze::annot_fn`]
@@ -200,13 +277,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     }
 
     pub fn is_annotated_as_extern_spec_fn(&self) -> bool {
-        self.tcx
-            .get_attrs_by_path(
-                self.local_def_id.to_def_id(),
-                &analyze::annot::extern_spec_fn_path(),
-            )
-            .next()
-            .is_some()
+        is_annotated_as_extern_spec_fn_impl(&self.tcx, &self.local_def_id)
     }
 
     pub fn is_annotated_as_predicate(&self) -> bool {
@@ -317,7 +388,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             .associated_item(self.local_def_id.to_def_id())
             .trait_item_def_id
             .unwrap();
-        self.ctx.def_ty_with_args(trait_item_did, trait_ref.args)
+        self.ctx
+            .def_ty_with_args(trait_item_did, trait_ref.args, trait_ref.def_id)
     }
 
     // TODO: Remove this eager precompute together with
@@ -325,11 +397,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     // `def_ty_with_args` directly.
     fn precompute_callable_param_contracts(&mut self, sig: &mir_ty::FnSig<'tcx>) {
         for input_ty in sig.inputs() {
-            let inst =
-                mir_ty::EarlyBinder::bind(*input_ty).instantiate(self.tcx, self.generic_args);
             let inst = self
                 .tcx
-                .normalize_erasing_regions(mir_ty::TypingEnv::fully_monomorphized(), inst);
+                .try_normalize_erasing_regions(mir_ty::TypingEnv::fully_monomorphized(), *input_ty)
+                .unwrap_or(*input_ty);
             let (fn_def_id, fn_args) = match inst.kind() {
                 mir_ty::TyKind::Closure(def_id, args) => {
                     (*def_id, self.tcx.mk_args(args.as_closure().parent_args()))
@@ -340,7 +411,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             if fn_def_id == self.local_def_id.to_def_id() {
                 continue;
             }
-            let _ = self.ctx.def_ty_with_args(fn_def_id, fn_args);
+            let _ = self
+                .ctx
+                .def_ty_with_args(fn_def_id, fn_args, self.owner_fn_id);
         }
     }
 
@@ -386,6 +459,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             &param_resolver,
             self_type_name.clone(),
             self.generic_args,
+            self.owner_fn_id,
         );
 
         let mut ensure_annot = self.ctx.extract_ensure_annot(
@@ -393,6 +467,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             &result_param_resolver,
             self_type_name.clone(),
             self.generic_args,
+            self.owner_fn_id,
         );
 
         if let Some(trait_item_id) = self.local_trait_item_id() {
@@ -402,12 +477,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 &param_resolver,
                 self_type_name.clone(),
                 self.generic_args,
+                self.owner_fn_id,
             );
             let trait_ensure_annot = self.ctx.extract_ensure_annot(
                 trait_item_id,
                 &result_param_resolver,
                 self_type_name.clone(),
                 self.generic_args,
+                self.owner_fn_id,
             );
 
             assert!(require_annot.is_none() || trait_require_annot.is_none());
@@ -435,9 +512,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         assert!(require_annot.is_none() || param_annots.is_empty());
         assert!(ensure_annot.is_none() || ret_annot.is_none());
 
-        let refinement_annots = self
-            .ctx
-            .extract_refinement_annots(self.local_def_id, self.generic_args);
+        let refinement_annots = self.ctx.extract_refinement_annots(
+            self.local_def_id,
+            self.generic_args,
+            self.owner_fn_id,
+        );
 
         let trait_item_ty = self.trait_item_ty();
         let is_fully_annotated = self.is_fully_annotated();
@@ -482,62 +561,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     /// The target is identified as the tail call expression (last expression without
     /// semicolon) in the function body block.
     pub fn extern_spec_fn_target_def_id(&self) -> DefId {
-        let node = self.tcx.hir_node_by_def_id(self.local_def_id);
-        let body_id = match node {
-            rustc_hir::Node::Item(item) => {
-                let rustc_hir::ItemKind::Fn { body: body_id, .. } = item.kind else {
-                    panic!("extern_spec_fn must be a function");
-                };
-                body_id
-            }
-            rustc_hir::Node::ImplItem(impl_item) => {
-                let rustc_hir::ImplItemKind::Fn(_, body_id) = impl_item.kind else {
-                    panic!("extern_spec_fn must be a function");
-                };
-                body_id
-            }
-            rustc_hir::Node::TraitItem(trait_item) => {
-                let rustc_hir::TraitItemKind::Fn(_, rustc_hir::TraitFn::Provided(body_id)) =
-                    trait_item.kind
-                else {
-                    panic!("extern_spec_fn must be a function with a body");
-                };
-                body_id
-            }
-            _ => panic!("extern_spec_fn must be a function item or impl item"),
-        };
-
-        let body = self.tcx.hir_body(body_id);
-
-        // The body is a block; the tail expression is the function call to the target.
-        let rustc_hir::ExprKind::Block(block, _) = &body.value.kind else {
-            panic!("extern_spec_fn body must be a block");
-        };
-        let tail_expr = block
-            .expr
-            .expect("extern_spec_fn block must end with a tail call expression");
-
-        let rustc_hir::ExprKind::Call(func_expr, _) = &tail_expr.kind else {
-            panic!("extern_spec_fn tail expression must be a function call");
-        };
-        let rustc_hir::ExprKind::Path(qpath) = &func_expr.kind else {
-            panic!("extern_spec_fn call must be a path expression");
-        };
-
-        let typeck_result = self.tcx.typeck(self.local_def_id);
-        let hir_id = func_expr.hir_id;
-        let rustc_hir::def::Res::Def(_, def_id) = typeck_result.qpath_res(qpath, hir_id) else {
-            panic!("extern_spec_fn call must resolve to a definition");
-        };
-
-        let args = typeck_result.node_args(hir_id);
-        let typing_env = self.body.typing_env(self.tcx);
-        let instance = mir_ty::Instance::try_resolve(self.tcx, typing_env, def_id, args).unwrap();
-        if let Some(instance) = instance {
-            instance.def_id()
-        } else {
-            def_id
-        }
+        extern_spec_fn_target_def_id_impl(&self.tcx, &self.local_def_id, &self.body)
     }
 
     fn is_mut_param(&self, param_idx: rty::FunctionParamIdx) -> bool {
@@ -939,18 +963,24 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     fn local_of_name_in_bb(&self, name: rustc_span::Symbol, bty: &BasicBlockType) -> Option<Local> {
         let mut found: Option<Local> = None;
         for vdi in &self.body.var_debug_info {
+            tracing::debug!("comparing {name:?} with {vdi:?}...");
             if vdi.name != name {
+                tracing::debug!("different name, skip.");
                 continue;
             }
             let mir::VarDebugInfoContents::Place(place) = vdi.value else {
+                tracing::debug!("place, skip.");
                 continue;
             };
             if !place.projection.is_empty() {
+                tracing::debug!("empty projection, skip.");
                 continue;
             }
             if bty.param_of_local(place.local).is_none() {
+                tracing::debug!("not param of local, skip.");
                 continue;
             }
+            tracing::debug!("found.");
             match found {
                 None => found = Some(place.local),
                 Some(prev) if prev == place.local => {}
@@ -967,19 +997,25 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     fn function_param_local_of_name(&self, name: rustc_span::Symbol) -> Option<Local> {
         let mut found: Option<Local> = None;
         for vdi in &self.body.var_debug_info {
+            tracing::debug!("comparing {name:?} with {vdi:?}...");
             if vdi.name != name {
+                tracing::debug!("different name, skip.");
                 continue;
             }
             let mir::VarDebugInfoContents::Place(place) = vdi.value else {
+                tracing::debug!("place, skip.");
                 continue;
             };
             if !place.projection.is_empty() {
+                tracing::debug!("empty projection, skip.");
                 continue;
             }
             let local = place.local;
             if local.index() == 0 || local.index() > self.body.arg_count {
+                tracing::debug!("not param of local, skip.");
                 continue;
             }
+            tracing::debug!("found.");
             match found {
                 None => found = Some(local),
                 Some(prev) if prev == local => {}
@@ -989,6 +1025,19 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         found
     }
 
+    fn expand_model_projection(&self, ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> {
+        if let mir_ty::Alias(mir_ty::AliasTyKind::Projection, ty) = ty.kind() {
+            if let Some(model_ty_def_id) = self.ctx.def_ids.model_ty() {
+                let arg_ty = ty.args.type_at(0);
+
+                if ty.def_id == model_ty_def_id {
+                    return arg_ty;
+                }
+            }
+        }
+        ty
+    }
+
     /// Translates a user-provided loop invariant (a formula function over named
     /// live variables) into a precondition refinement over `bty`'s parameters.
     /// Each formula parameter names a live variable at the loop header and is
@@ -1001,7 +1050,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     ) -> rty::Refinement<rty::FunctionParamIdx> {
         let formula_fn = self
             .ctx
-            .formula_fn_with_args(formula_def_id, generic_args)
+            .formula_fn_with_args(formula_def_id, generic_args, self.owner_fn_id)
             .expect("invariant formula function is not registered");
         let idents = self.tcx.fn_arg_idents(formula_def_id.to_def_id());
         let sig = self
@@ -1020,6 +1069,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                     .unwrap_or(*input_ty)
             };
 
+            let input_ty = self.expand_model_projection(input_ty);
+            tracing::debug!(?ident_opt, ?input_ty, "resolving");
+
             // The synthetic `__thrust_self` parameter (emitted when an invariant refers to the receiver
             // `self`) maps to the loop-carried receiver, which appears as `self` in debug info.
             let name = if name.as_str() == "__thrust_self" {
@@ -1027,11 +1079,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             } else {
                 name
             };
-
+            tracing::debug!("{:?}", input_ty.ty_adt_def());
             if input_ty
                 .ty_adt_def()
                 .is_some_and(|def| Some(def.did()) == self.ctx.def_ids().fn_param_wrapper())
             {
+                tracing::debug!("fn_param_local: {input_ty:?}");
                 let local = self.function_param_local_of_name(name).unwrap_or_else(|| {
                     self.tcx.dcx().fatal(format!(
                         "loop invariant refers to `{name}` via FnParam, but it is not a function parameter"
@@ -1040,6 +1093,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 let param_idx = crate::analyze::function_param_of_local(local);
                 mapping.push(bty.param_of_outer_fn_param(param_idx).unwrap());
             } else {
+                tracing::debug!("local: {input_ty:?}");
                 let local = self.local_of_name_in_bb(name, bty).unwrap_or_else(|| {
                     self.tcx.dcx().fatal(format!(
                         "loop invariant refers to `{name}`, which is not a live variable at the loop header"
@@ -1153,7 +1207,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 .clone();
             let drop_points = self.drop_points[&bb].clone();
             self.ctx
-                .basic_block_analyzer(self.local_def_id, bb)
+                .basic_block_analyzer(self.local_def_id, bb, self.owner_fn_id)
                 .body(self.body.clone())
                 .drop_points(drop_points)
                 .run(&rty, expected_fn_ty);
@@ -1281,12 +1335,18 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let tcx = ctx.tcx;
         let body = tcx.optimized_mir(local_def_id.to_def_id()).clone();
         let drop_points = Default::default();
-        let type_builder = TypeBuilder::new(tcx, ctx.def_ids(), local_def_id.to_def_id());
+        let owner_fn_id = if is_annotated_as_extern_spec_fn_impl(&tcx, &local_def_id) {
+            extern_spec_fn_target_def_id_impl(&tcx, &local_def_id, &body)
+        } else {
+            local_def_id.to_def_id()
+        };
+        let type_builder = ctx.type_builder(ctx.def_ids(), owner_fn_id);
         let generic_args = tcx.mk_args(&[]);
         Self {
             ctx,
             tcx,
             local_def_id,
+            owner_fn_id,
             body,
             generic_args,
             drop_points,
@@ -1298,6 +1358,17 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         self.local_def_id
     }
 
+    pub fn owner_fn_id(&mut self, owner_fn_id: DefId) -> &mut Self {
+        tracing::debug!(
+            "change owner_fn_id from {:?} to {:?}.",
+            self.owner_fn_id,
+            owner_fn_id
+        );
+        self.owner_fn_id = owner_fn_id;
+        self.type_builder = self.ctx.type_builder(self.ctx.def_ids(), owner_fn_id);
+        self
+    }
+
     pub fn generic_args(&mut self, generic_args: mir_ty::GenericArgsRef<'tcx>) -> &mut Self {
         self.generic_args = generic_args;
         self.body =
diff --git a/src/chc.rs b/src/chc.rs
index 2a61f375..eb610ab1 100644
--- a/src/chc.rs
+++ b/src/chc.rs
@@ -1,5 +1,8 @@
 //! A multi-sorted CHC system with tuples.
 
+use std::collections::{HashMap, HashSet};
+use std::hash::Hash;
+
 use pretty::{termcolor, Pretty};
 use rustc_index::IndexVec;
 
@@ -84,6 +87,45 @@ impl DatatypeSort {
     }
 }
 
+rustc_index::newtype_index! {
+    /// An index representing sort-level variable.
+    ///
+    /// We manage sort-level variables using indices that are unique in the whole CHC system.
+    /// [`System`] contains `Vec<ForallSortIdx>` that manages the indices of the variables.
+    #[orderable]
+    #[debug_format = "a{}"]
+    pub struct ForallSortIdx { }
+}
+
+impl Default for ForallSortIdx {
+    fn default() -> Self {
+        0_usize.into()
+    }
+}
+
+impl std::fmt::Display for ForallSortIdx {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        write!(f, "a{}", self.index())
+    }
+}
+
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ForallSortIdx
+where
+    D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
+{
+    fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
+        allocator
+            .as_string(self)
+            .annotate(ForallSortIdx::color_spec())
+    }
+}
+
+impl ForallSortIdx {
+    fn color_spec() -> termcolor::ColorSpec {
+        termcolor::ColorSpec::new()
+    }
+}
+
 /// A sort is the type of a logical term.
 #[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
 pub enum Sort {
@@ -97,6 +139,7 @@ pub enum Sort {
     Tuple(Vec<Sort>),
     Array(Box<Sort>, Box<Sort>),
     Datatype(DatatypeSort),
+    Forall(ForallSortIdx),
 }
 
 impl From<DatatypeSort> for Sort {
@@ -154,6 +197,7 @@ where
                 }
             }
             Sort::Datatype(sort) => sort.pretty(allocator),
+            Sort::Forall(idx) => idx.pretty(allocator),
         }
     }
 }
@@ -180,7 +224,12 @@ impl Sort {
     fn walk_impl<'a, 'b>(&'a self, mut f: Box<dyn FnMut(&'a Sort) + 'b>) {
         f(self);
         match self {
-            Sort::Null | Sort::Int | Sort::Bool | Sort::String | Sort::Param(_) => {}
+            Sort::Null
+            | Sort::Int
+            | Sort::Bool
+            | Sort::String
+            | Sort::Param(_)
+            | Sort::Forall(_) => {}
             Sort::Box(s) | Sort::Mut(s) => s.walk(Box::new(&mut f)),
             Sort::Tuple(ss) => {
                 for s in ss {
@@ -261,6 +310,10 @@ impl Sort {
         Sort::Datatype(DatatypeSort { symbol, args })
     }
 
+    pub fn forall(index: ForallSortIdx) -> Self {
+        Sort::Forall(index)
+    }
+
     pub fn into_datatype(self) -> Option<DatatypeSort> {
         match self {
             Sort::Datatype(sort) => Some(sort),
@@ -435,7 +488,7 @@ impl Function {
 }
 
 /// A logical term.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Term<V = TermVarIdx> {
     Null,
     Var(V),
@@ -994,6 +1047,51 @@ impl UserDefinedPred {
     }
 }
 
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub struct ForallPred {
+    inner: String,
+    type_parameters: Vec<Sort>,
+    params: Vec<Sort>,
+}
+
+impl std::fmt::Display for ForallPred {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        self.inner.fmt(f)
+    }
+}
+
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ForallPred
+where
+    D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
+    D::Doc: Clone,
+{
+    fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
+        let args = allocator.intersperse(
+            self.type_parameters.iter().map(|a| a.pretty(allocator)),
+            allocator.text(", "),
+        );
+        allocator
+            .text("forall_pred")
+            .append(
+                allocator
+                    .as_string(&self.inner)
+                    .append(args.angles())
+                    .angles(),
+            )
+            .group()
+    }
+}
+
+impl ForallPred {
+    pub fn new(inner: String, type_parameters: Vec<Sort>, params: Vec<Sort>) -> Self {
+        Self {
+            inner,
+            type_parameters,
+            params,
+        }
+    }
+}
+
 /// A predicate.
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Pred {
@@ -1001,6 +1099,7 @@ pub enum Pred {
     Var(PredVarId),
     Matcher(MatcherPred),
     UserDefined(UserDefinedPred),
+    ForallPred(ForallPred),
 }
 
 impl std::fmt::Display for Pred {
@@ -1010,6 +1109,7 @@ impl std::fmt::Display for Pred {
             Pred::Var(p) => p.fmt(f),
             Pred::Matcher(p) => p.fmt(f),
             Pred::UserDefined(p) => p.fmt(f),
+            Pred::ForallPred(p) => p.fmt(f),
         }
     }
 }
@@ -1025,6 +1125,7 @@ where
             Pred::Var(p) => p.pretty(allocator),
             Pred::Matcher(p) => p.pretty(allocator),
             Pred::UserDefined(p) => p.pretty(allocator),
+            Pred::ForallPred(p) => p.pretty(allocator),
         }
     }
 }
@@ -1053,6 +1154,12 @@ impl From<UserDefinedPred> for Pred {
     }
 }
 
+impl From<ForallPred> for Pred {
+    fn from(p: ForallPred) -> Self {
+        Pred::ForallPred(p)
+    }
+}
+
 impl Pred {
     pub fn name(&self) -> std::borrow::Cow<'static, str> {
         match self {
@@ -1060,6 +1167,7 @@ impl Pred {
             Pred::Var(p) => p.to_string().into(),
             Pred::Matcher(p) => p.name().into(),
             Pred::UserDefined(p) => p.to_string().into(),
+            Pred::ForallPred(p) => p.to_string().into(),
         }
     }
 
@@ -1069,6 +1177,7 @@ impl Pred {
             Pred::Var(_) => false,
             Pred::Matcher(_) => false,
             Pred::UserDefined(_) => false,
+            Pred::ForallPred(_) => false,
         }
     }
 
@@ -1078,6 +1187,7 @@ impl Pred {
             Pred::Var(_) => false,
             Pred::Matcher(_) => false,
             Pred::UserDefined(_) => false,
+            Pred::ForallPred(_) => false,
         }
     }
 
@@ -1087,6 +1197,7 @@ impl Pred {
             Pred::Var(_) => false,
             Pred::Matcher(_) => false,
             Pred::UserDefined(_) => false,
+            Pred::ForallPred(_) => false,
         }
     }
 
@@ -1096,12 +1207,26 @@ impl Pred {
             Pred::Var(_) => false,
             Pred::Matcher(_) => false,
             Pred::UserDefined(_) => false,
+            Pred::ForallPred(_) => false,
+        }
+    }
+}
+
+impl TryFrom<Pred> for ForallPred {
+    type Error = String;
+    fn try_from(value: Pred) -> Result<Self, Self::Error> {
+        if let Pred::ForallPred(forall_pred) = value {
+            Ok(forall_pred)
+        } else {
+            Err(format!(
+                "expected the variant `Pred::ForallPred`, got {value:#?}."
+            ))
         }
     }
 }
 
 /// An atom is a predicate applied to a list of terms.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct Atom<V = TermVarIdx> {
     /// With `guard`, this represents `guard => pred(args)`.
     ///
@@ -1245,7 +1370,7 @@ impl<V> Atom<V> {
 /// While it allows arbitrary [`Atom`] in its `Atom` variant, we only expect atoms with known
 /// predicates (i.e., predicates other than `Pred::Var`) to appear in formulas. It is our TODO to
 /// enforce this restriction statically. Also see the definition of [`Body`].
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Formula<V = TermVarIdx> {
     Atom(Atom<V>),
     Not(Box<Formula<V>>),
@@ -1567,7 +1692,7 @@ impl<V> Formula<V> {
 }
 
 /// The body part of a clause, consisting of atoms and a formula.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct Body<V = TermVarIdx> {
     pub atoms: Vec<Atom<V>>,
     /// NOTE: This doesn't contain predicate variables. Also see [`Formula`].
@@ -1843,6 +1968,33 @@ pub struct UserDefinedPredDef {
     body: String,
 }
 
+pub fn compute_transitive_closure<T>(direct_deps: &HashMap<T, HashSet<T>>) -> HashMap<T, HashSet<T>>
+where
+    T: Clone + Eq + Hash,
+{
+    let mut closure = HashMap::new();
+
+    for start_id in direct_deps.keys() {
+        let mut visited = HashSet::new();
+        let mut stack = vec![start_id.clone()];
+
+        // Search by DFS
+        while let Some(current_id) = stack.pop() {
+            if let Some(deps) = direct_deps.get(&current_id) {
+                for next_id in deps {
+                    if visited.insert(next_id.clone()) {
+                        stack.push(next_id.clone());
+                    }
+                }
+            }
+        }
+
+        closure.insert(start_id.clone(), visited);
+    }
+
+    closure
+}
+
 /// A CHC system.
 #[derive(Debug, Clone, Default)]
 pub struct System {
@@ -1851,6 +2003,9 @@ pub struct System {
     pub user_defined_pred_defs: Vec<UserDefinedPredDef>,
     pub clauses: IndexVec<ClauseId, Clause>,
     pub pred_vars: IndexVec<PredVarId, PredVarDef>,
+    pub forall_sorts: Vec<ForallSortIdx>,
+    pub num_forall_sort_idx: ForallSortIdx,
+    forall_pred_vars: HashSet<ForallPred>,
 }
 
 impl System {
@@ -1858,6 +2013,17 @@ impl System {
         self.pred_vars.push(PredVarDef { sig, debug_info })
     }
 
+    pub fn register_forall_pred(&mut self, pred: ForallPred) {
+        self.forall_pred_vars.insert(pred);
+    }
+
+    pub fn new_forall_sort(&mut self) -> ForallSortIdx {
+        let new_idx = self.num_forall_sort_idx;
+        self.num_forall_sort_idx += 1;
+        self.forall_sorts.push(new_idx);
+        new_idx
+    }
+
     pub fn push_raw_command(&mut self, raw_command: RawCommand) {
         self.raw_commands.push(raw_command)
     }
@@ -1880,6 +2046,70 @@ impl System {
         Some(self.clauses.push(clause))
     }
 
+    fn compute_forall_dependency(clause: &Clause) -> HashSet<ForallPred> {
+        clause
+            .body
+            .iter_atoms()
+            .filter_map(|atom| atom.pred.clone().try_into().ok())
+            .collect()
+    }
+
+    fn compute_exists_dependency(clause: &Clause) -> HashSet<PredVarId> {
+        clause
+            .body
+            .iter_atoms()
+            .filter_map(|atom| match atom.pred {
+                Pred::Var(id) => Some(id),
+                _ => None,
+            })
+            .collect()
+    }
+
+    fn compute_dependency(&self) -> HashMap<PredVarId, HashSet<ForallPred>> {
+        let mut exists_deps: HashMap<PredVarId, HashSet<PredVarId>> = HashMap::new();
+        let mut forall_deps: HashMap<PredVarId, HashSet<ForallPred>> = HashMap::new();
+
+        for (clause_idx, clause) in self.clauses.iter_enumerated() {
+            let Pred::Var(head_id) = clause.head.pred else {
+                continue;
+            };
+
+            let exists = Self::compute_exists_dependency(clause);
+            let forall = Self::compute_forall_dependency(clause);
+
+            tracing::debug!(
+                "exists deps for {:?} at {:?}: {:?}",
+                head_id,
+                clause_idx,
+                exists
+            );
+
+            exists_deps.entry(head_id).or_default().extend(exists);
+            forall_deps.entry(head_id).or_default().extend(forall);
+        }
+        tracing::debug!("direct forall dependencies: {:#?}", forall_deps);
+        tracing::debug!("direct exists dependencies: {:#?}", exists_deps);
+
+        let transitive_exists_deps = compute_transitive_closure(&exists_deps);
+        tracing::debug!("transitive exists dependencies: {:#?}", exists_deps);
+
+        let mut propagated_forall_deps = HashMap::new();
+
+        for (pred, reachable_preds) in transitive_exists_deps {
+            let mut deps = forall_deps.get(&pred).cloned().unwrap_or_default();
+
+            for reachable in reachable_preds {
+                if let Some(foralls) = forall_deps.get(&reachable) {
+                    deps.extend(foralls.iter().cloned());
+                }
+            }
+
+            propagated_forall_deps.insert(pred, deps);
+        }
+
+        propagated_forall_deps
+    }
+
     pub fn smtlib2(&self) -> smtlib2::System<'_> {
         smtlib2::System::new(self)
     }
diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs
index f4a79fd4..00e6e208 100644
--- a/src/chc/format_context.rs
+++ b/src/chc/format_context.rs
@@ -87,6 +87,7 @@ impl<'a> std::fmt::Display for SortSymbol<'a> {
                 write!(f, "Array{}", SortSymbols::new(&[*s1.clone(), *s2.clone()]))
             }
             chc::Sort::Datatype(s) => write!(f, "{}{}", s.symbol, SortSymbols::new(&s.args)),
+            chc::Sort::Forall(i) => write!(f, "{}", i),
         }
     }
 }
@@ -347,6 +348,11 @@ impl FormatContext {
         format!("matcher_pred<{}>", self.fmt_datatype_symbol(sym))
     }
 
+    pub fn forall_pred(&self, p: &chc::ForallPred) -> impl std::fmt::Display {
+        let ss = SortSymbols::new(&p.type_parameters);
+        format!("{}{}", p.inner, ss)
+    }
+
     fn fmt_sort_impl(&self, sort: &chc::Sort) -> Box<dyn std::fmt::Display> {
         match sort {
             chc::Sort::Array(s1, s2) => {
diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs
index 7904d58d..1acdac2f 100644
--- a/src/chc/smtlib2.rs
+++ b/src/chc/smtlib2.rs
@@ -6,6 +6,8 @@
 //! such as naming convention and solver-specific workarounds.
 //! The output of this module is what gets passed to the external CHC solver.
 
+use std::collections::HashSet;
+
 use crate::chc::{self, format_context::FormatContext};
 
 /// A helper struct to display a list of items.
@@ -232,6 +234,7 @@ impl<'ctx, 'a> std::fmt::Display for Atom<'ctx, 'a> {
         }
         let pred = match &self.inner.pred {
             chc::Pred::Matcher(p) => self.ctx.matcher_pred(p).to_string(),
+            chc::Pred::ForallPred(p) => self.ctx.forall_pred(p).to_string(),
             p => p.name().into_owned(),
         };
         if self.inner.args.is_empty() {
@@ -602,6 +605,68 @@ impl<'ctx, 'a> UserDefinedPredDef<'ctx, 'a> {
         Self { ctx, inner }
     }
 }
+
+pub struct ForallPredDef<'ctx, 'a> {
+    ctx: &'ctx FormatContext,
+    pred: &'a chc::ForallPred,
+}
+
+impl<'ctx, 'a> std::fmt::Display for ForallPredDef<'ctx, 'a> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let params = self.pred.params.iter().map(|sort| self.ctx.fmt_sort(sort));
+        let params = List::closed(params);
+        write!(
+            f,
+            "(declare-forall-fun {name} {params} Bool)",
+            name = self.ctx.forall_pred(self.pred),
+        )
+    }
+}
+
+impl<'ctx, 'a> ForallPredDef<'ctx, 'a> {
+    pub fn new(ctx: &'ctx FormatContext, pred: &'a chc::ForallPred) -> Self {
+        Self { ctx, pred }
+    }
+}
+
+pub struct DepExistsPredVarDef<'ctx, 'a> {
+    ctx: &'ctx FormatContext,
+    id: &'a chc::PredVarId,
+    def: &'a chc::PredVarDef,
+    dependencies: &'a HashSet<chc::ForallPred>,
+}
+
+impl<'ctx, 'a> std::fmt::Display for DepExistsPredVarDef<'ctx, 'a> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        if !self.def.debug_info.is_empty() {
+            writeln!(f, "{}", self.def.debug_info.display("; "))?;
+        }
+        writeln!(
+            f,
+            "(declare-dep-exists-fun {} {} {} Bool)",
+            self.id,
+            List::closed(self.dependencies.iter().map(|p| self.ctx.forall_pred(p))),
+            List::closed(self.def.sig.iter().map(|s| self.ctx.fmt_sort(s))),
+        )
+    }
+}
+
+impl<'ctx, 'a> DepExistsPredVarDef<'ctx, 'a> {
+    pub fn new(
+        ctx: &'ctx FormatContext,
+        id: &'a chc::PredVarId,
+        def: &'a chc::PredVarDef,
+        dependencies: &'a HashSet<chc::ForallPred>,
+    ) -> Self {
+        Self {
+            ctx,
+            id,
+            def,
+            dependencies,
+        }
+    }
+}
+
 /// A wrapper around a [`chc::System`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct System<'a> {
@@ -613,6 +678,14 @@ impl<'a> std::fmt::Display for System<'a> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         writeln!(f, "(set-logic HORN)\n")?;
 
+        for forall_sort_idx in &self.inner.forall_sorts {
+            writeln!(f, "(declare-forall-sort {})\n", forall_sort_idx)?;
+        }
+
+        for pred in &self.inner.forall_pred_vars {
+            writeln!(f, "{}\n", ForallPredDef::new(&self.ctx, pred))?;
+        }
+
         writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?;
         for datatype in self.ctx.datatypes() {
             writeln!(f, "{}", DatatypeDiscrFun::new(&self.ctx, datatype))?;
@@ -633,16 +706,25 @@ impl<'a> std::fmt::Display for System<'a> {
         }
 
         writeln!(f)?;
+        let dependencies = self.inner.compute_dependency();
         for (p, def) in self.inner.pred_vars.iter_enumerated() {
-            if !def.debug_info.is_empty() {
-                writeln!(f, "{}", def.debug_info.display("; "))?;
+            if dependencies.contains_key(&p) && !dependencies[&p].is_empty() {
+                writeln!(
+                    f,
+                    "{}\n",
+                    DepExistsPredVarDef::new(&self.ctx, &p, def, &dependencies[&p])
+                )?;
+            } else {
+                if !def.debug_info.is_empty() {
+                    writeln!(f, "{}", def.debug_info.display("; "))?;
+                }
+                writeln!(
+                    f,
+                    "(declare-fun {} {} Bool)\n",
+                    p,
+                    List::closed(def.sig.iter().map(|s| self.ctx.fmt_sort(s)))
+                )?;
             }
-            writeln!(
-                f,
-                "(declare-fun {} {} Bool)\n",
-                p,
-                List::closed(def.sig.iter().map(|s| self.ctx.fmt_sort(s)))
-            )?;
         }
         for (id, clause) in self.inner.clauses.iter_enumerated() {
             writeln!(
diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs
index bfb782eb..5d1c140f 100644
--- a/src/chc/unbox.rs
+++ b/src/chc/unbox.rs
@@ -43,6 +43,7 @@ fn unbox_pred(pred: Pred) -> Pred {
         Pred::Var(pred) => Pred::Var(pred),
         Pred::Matcher(pred) => unbox_matcher_pred(pred),
         Pred::UserDefined(pred) => Pred::UserDefined(pred),
+        Pred::ForallPred(pred) => Pred::ForallPred(pred),
     }
 }
 
@@ -72,6 +73,7 @@ fn unbox_sort(sort: Sort) -> Sort {
         Sort::Tuple(sorts) => Sort::Tuple(sorts.into_iter().map(unbox_sort).collect()),
         Sort::Array(s1, s2) => Sort::Array(Box::new(unbox_sort(*s1)), Box::new(unbox_sort(*s2))),
         Sort::Datatype(sort) => Sort::Datatype(unbox_datatype_sort(sort)),
+        Sort::Forall(i) => Sort::Forall(i),
     }
 }
 
@@ -169,6 +171,14 @@ fn unbox_user_defined_pred_def(user_defined_pred_def: UserDefinedPredDef) -> Use
     UserDefinedPredDef { symbol, sig, body }
 }
 
+fn unbox_forall_pred_var_def(pred: ForallPred) -> ForallPred {
+    let args = pred.type_parameters.into_iter().map(unbox_sort).collect();
+    ForallPred {
+        type_parameters: args,
+        ..pred
+    }
+}
+
 /// Remove all `Box` sorts and `Box`/`BoxCurrent` terms from the system.
 ///
 /// The box values in Thrust represent an owned pointer, but are logically equivalent to the inner type.
@@ -181,6 +191,9 @@ pub fn unbox(system: System) -> System {
         user_defined_pred_defs,
         clauses,
         pred_vars,
+        forall_sorts,
+        num_forall_sort_idx,
+        forall_pred_vars,
     } = system;
     let datatypes = datatypes.into_iter().map(unbox_datatype).collect();
     let clauses = clauses.into_iter().map(unbox_clause).collect();
@@ -189,11 +202,18 @@ pub fn unbox(system: System) -> System {
         .into_iter()
         .map(unbox_user_defined_pred_def)
         .collect();
+    let forall_pred_vars = forall_pred_vars
+        .into_iter()
+        .map(unbox_forall_pred_var_def)
+        .collect();
     System {
         raw_commands,
         datatypes,
         user_defined_pred_defs,
         clauses,
         pred_vars,
+        forall_sorts,
+        num_forall_sort_idx,
+        forall_pred_vars,
     }
 }
diff --git a/src/refine.rs b/src/refine.rs
index 5a1fd8d3..afa14054 100644
--- a/src/refine.rs
+++ b/src/refine.rs
@@ -18,15 +18,16 @@ pub use env::{
     Assumption, EnumDefProvider, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, Var,
 };
 
-use crate::chc::{DatatypeSymbol, UserDefinedPred};
+use crate::chc::{DatatypeSymbol, ForallPred, Sort, UserDefinedPred};
 use rustc_middle::ty as mir_ty;
 use rustc_span::def_id::DefId;
 
-fn stable_def_id_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> String {
+fn stable_def_id_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId, prefix: &str) -> String {
     let hash = tcx.def_path_hash(did);
     let path = tcx.def_path(did);
     if let Some(name) = path.data.last().and_then(|d| d.data.get_opt_name()) {
-        format!("{}_{}", name, hash.0.to_hex())
+        tracing::debug!("stable_def_id_symbol: name={}", name);
+        format!("{}_{}_{}", prefix, name, hash.0.to_hex())
     } else {
         hash.0.to_hex()
     }
@@ -37,5 +38,40 @@ pub fn datatype_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> DatatypeSymbol {
 }
 
 pub fn user_defined_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> UserDefinedPred {
-    UserDefinedPred::new(stable_def_id_symbol(tcx, did))
+    UserDefinedPred::new(stable_def_id_symbol(tcx, did, "p"))
+}
+
+pub fn trait_forall_pred(
+    tcx: mir_ty::TyCtxt<'_>,
+    did: DefId,
+    type_parameters: Vec<Sort>,
+    params: Vec<Sort>,
+) -> ForallPred {
+    ForallPred::new(stable_def_id_symbol(tcx, did, "q"), type_parameters, params)
+}
+
+pub fn closure_pre_forall_pred(
+    tcx: mir_ty::TyCtxt<'_>,
+    did: DefId,
+    type_parameters: Vec<Sort>,
+    params: Vec<Sort>,
+) -> ForallPred {
+    ForallPred::new(
+        stable_def_id_symbol(tcx, did, "q_pre"),
+        type_parameters,
+        params,
+    )
+}
+
+pub fn closure_post_forall_pred(
+    tcx: mir_ty::TyCtxt<'_>,
+    did: DefId,
+    type_parameters: Vec<Sort>,
+    params: Vec<Sort>,
+) -> ForallPred {
+    ForallPred::new(
+        stable_def_id_symbol(tcx, did, "q_post"),
+        type_parameters,
+        params,
+    )
 }
diff --git a/src/refine/template.rs b/src/refine/template.rs
index fe200bda..a79a40e6 100644
--- a/src/refine/template.rs
+++ b/src/refine/template.rs
@@ -1,4 +1,6 @@
+use std::cell::RefCell;
 use std::collections::HashMap;
+use std::rc::Rc;
 
 use rustc_index::IndexVec;
 use rustc_middle::mir::{Local, Mutability};
@@ -6,7 +8,7 @@ use rustc_middle::ty as mir_ty;
 use rustc_span::def_id::DefId;
 
 use super::basic_block::BasicBlockType;
-use crate::analyze::DefIdCache;
+use crate::analyze::{DefIdCache, TypeParam, TypeParamMap};
 use crate::chc;
 use crate::refine;
 use crate::rty;
@@ -71,17 +73,28 @@ where
 pub struct TypeBuilder<'tcx> {
     tcx: mir_ty::TyCtxt<'tcx>,
     def_ids: DefIdCache<'tcx>,
+    owner_fn_id: DefId,
     typing_env: mir_ty::TypingEnv<'tcx>,
     /// Maps index in [`mir_ty::ParamTy`] to [`rty::TypeParamIdx`].
     /// These indices may differ because we skip lifetime parameters and they always need to be
     /// mapped when we translate a [`mir_ty::ParamTy`] to [`rty::ParamType`].
     /// See [`rty::TypeParamIdx`] for more details.
     param_idx_mapping: HashMap<u32, rty::TypeParamIdx>,
+    type_params: Rc<RefCell<TypeParamMap<'tcx>>>,
+    closure_type_params: Rc<RefCell<HashMap<TypeParam, rty::FunctionType>>>,
+    system: Rc<RefCell<chc::System>>,
 }
 
 impl<'tcx> TypeBuilder<'tcx> {
-    pub fn new(tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, def_id: DefId) -> Self {
-        let generics = tcx.generics_of(def_id);
+    pub fn new(
+        tcx: mir_ty::TyCtxt<'tcx>,
+        def_ids: DefIdCache<'tcx>,
+        owner_fn_id: DefId,
+        type_params: Rc<RefCell<TypeParamMap<'tcx>>>,
+        closure_type_params: Rc<RefCell<HashMap<TypeParam, rty::FunctionType>>>,
+        system: Rc<RefCell<chc::System>>,
+    ) -> Self {
+        let generics = tcx.generics_of(owner_fn_id);
         let mut param_idx_mapping: HashMap<u32, rty::TypeParamIdx> = Default::default();
         for i in 0..generics.count() {
             let generic_param = generics.param_at(i, tcx);
@@ -93,21 +106,90 @@ impl<'tcx> TypeBuilder<'tcx> {
                 mir_ty::GenericParamDefKind::Const { .. } => {}
             }
         }
-        let typing_env = mir_ty::TypingEnv::post_analysis(tcx, def_id);
+
+        tracing::debug!("TypeBuilder is created for {owner_fn_id:?} with param_idx_mapping {param_idx_mapping:#?}.");
+        let typing_env = mir_ty::TypingEnv::post_analysis(tcx, owner_fn_id);
         Self {
             tcx,
             def_ids,
+            owner_fn_id,
             typing_env,
             param_idx_mapping,
+            type_params,
+            closure_type_params,
+            system,
         }
     }
 
+    pub fn owner_fn_id(&self) -> DefId {
+        self.owner_fn_id
+    }
+
     fn translate_param_type(&self, ty: &mir_ty::ParamTy) -> rty::Type<rty::Closed> {
-        let index = *self
+        // FIXME:
+        // `__ThrustSelf` is currently treated as a distinct `ParamTy` from `Self`,
+        // which can lead to cache/key mismatches (e.g. in `TypeParamMap`).
+        //
+        // We currently normalize it here as a workaround, but this should be done
+        // earlier during type translation/analysis so that all internal
+        // representations consistently use the canonical `Self` parameter.
+        if ty.name.as_str() == "__ThrustSelf" {
+            let parent_def_id = self.tcx.parent(self.owner_fn_id);
+            let self_ty_def = self
+                .tcx
+                .generics_of(parent_def_id)
+                .own_params
+                .iter()
+                .find(|ty| ty.name.as_str() == "Self")
+                .expect("Type parameter `Self` is not found.");
+
+            let self_ty = mir_ty::ParamTy::new(self_ty_def.index, self_ty_def.name);
+            tracing::debug!("replace {ty:?} with {self_ty:?}.");
+            return self.translate_param_type(&self_ty);
+        }
+        let param_local_idx = *self
             .param_idx_mapping
             .get(&ty.index)
             .expect("unknown type param idx");
-        rty::ParamType::new(index).into()
+
+        tracing::debug!("translating ParamTy {ty:?}...");
+
+        let mut type_params = self.type_params.borrow_mut();
+        let forall_sort_idx = type_params
+            .entry(TypeParam::GenericType(self.owner_fn_id, ty.index))
+            .or_insert_with(|| {
+                let idx = self.system.borrow_mut().new_forall_sort();
+                tracing::debug!(
+                    "issue the new ForallSortIdx {} for ParamTy {:?} at {:?}.",
+                    idx,
+                    ty,
+                    self.owner_fn_id
+                );
+                idx
+            });
+        rty::ParamType::new(param_local_idx, *forall_sort_idx).into()
+    }
+
+    fn translate_alias_type(&self, ty: &mir_ty::AliasTy<'tcx>) -> rty::Type<rty::Closed> {
+        let args: Vec<rty::Type<rty::Closed>> = ty.args.types().map(|t| self.build(t)).collect();
+        let mut type_params = self.type_params.borrow_mut();
+        tracing::debug!(?type_params);
+        let index = type_params
+            .entry(TypeParam::AssocType(ty.def_id, args.clone()))
+            .or_insert_with(|| {
+                let idx = self.system.borrow_mut().new_forall_sort();
+                tracing::debug!("issue the new ForallSortIdx {} for AliasTy {:?} with (def_id = {:?}, args = {:?}).", idx, ty, ty.def_id, args);
+                idx
+            });
+
+        rty::AliasType::new(*index, args).into()
+    }
+
+    pub fn register_closure_type_param(&self, type_param: TypeParam, fun_type: rty::FunctionType) {
+        tracing::info!(?type_param, ?fun_type, "register_closure_type_param");
+        self.closure_type_params
+            .borrow_mut()
+            .insert(type_param, fun_type);
     }
 
     /// Replaces {closure} types with thrust_models::Closure<{closure}>.
@@ -152,19 +234,36 @@ impl<'tcx> TypeBuilder<'tcx> {
     }
 
     fn resolve_model_ty(&self, orig_ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> {
+        tracing::debug!("attempting to resolve the type {:#?}.", orig_ty);
         let ty = self.replace_closure_model(orig_ty);
 
         let Some(model_ty_def_id) = self.def_ids.model_ty() else {
             return ty;
         };
         let args = self.tcx.mk_args(&[ty.into()]);
+        tracing::debug!("generic args are {:#?}.", args);
         let projection_ty = mir_ty::Ty::new_projection(self.tcx, model_ty_def_id, args);
         if let Ok(normalized_ty) = self
             .tcx
             .try_normalize_erasing_regions(self.typing_env, projection_ty)
         {
-            return normalized_ty;
+            tracing::debug!(
+                "the type {:#?} is normalized as the type {:#?}.",
+                orig_ty,
+                normalized_ty
+            );
+            let contains_model_ty_alias = normalized_ty.walk().any(|arg| {
+                if let mir_ty::GenericArgKind::Type(t) = arg.kind() {
+                    matches!(t.kind(), mir_ty::TyKind::Alias(_, alias_ty) if alias_ty.def_id == model_ty_def_id)
+                } else {
+                    false
+                }
+            });
+            if !contains_model_ty_alias {
+                return normalized_ty;
+            }
         }
+        tracing::debug!("the type {:#?} is replaced as the {:#?}.", orig_ty, ty);
         ty
     }
 
@@ -212,6 +311,10 @@ impl<'tcx> TypeBuilder<'tcx> {
                 let elem_ty = self.build(*elem_ty);
                 rty::PointerType::immut_to(elem_ty).into()
             }
+            mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Mut) => {
+                let elem_ty = self.build(*elem_ty);
+                rty::PointerType::mut_to(elem_ty).into()
+            }
             mir_ty::TyKind::Tuple(ts) => {
                 // elaboration: all fields are boxed
                 let elems = ts
@@ -237,6 +340,23 @@ impl<'tcx> TypeBuilder<'tcx> {
                 if let Some(model_ty) = self.model_adt(def, params) {
                     return model_ty;
                 }
+                // Treat Box and Vec as opaque types to avoid traversing internal structure
+                if Some(def.did()) == self.def_ids.box_() {
+                    let elem_ty = self.build(params.type_at(0));
+                    return rty::PointerType::own(elem_ty).into();
+                }
+                if Some(def.did()) == self.def_ids.vec() {
+                    let elem_ty = self.build(params.type_at(0));
+                    // Vec is represented as a tuple of (Array<Int, T>, Int) in the model
+                    let idx_ty = rty::Type::int();
+                    let array_ty = rty::ArrayType::new(idx_ty, elem_ty.clone());
+                    let len_ty = rty::Type::int();
+                    return rty::TupleType::new(vec![
+                        rty::PointerType::own(rty::Type::Array(array_ty)).into(),
+                        rty::PointerType::own(len_ty).into(),
+                    ])
+                    .into();
+                }
                 if def.is_enum() {
                     let sym = refine::datatype_symbol(self.tcx, def.did());
                     let args: IndexVec<_, _> = params
@@ -258,6 +378,25 @@ impl<'tcx> TypeBuilder<'tcx> {
                     unimplemented!("unsupported ADT: {:?}", ty);
                 }
             }
+            mir_ty::TyKind::Alias(mir_ty::AliasTyKind::Projection, ty) => {
+                if let Some(model_ty_def_id) = self.def_ids.model_ty() {
+                    let arg_ty = ty.args.type_at(0);
+
+                    if ty.def_id == model_ty_def_id
+                        && (matches!(
+                            arg_ty.kind(),
+                            mir_ty::TyKind::Param(_) | mir_ty::TyKind::Alias(..)
+                        ))
+                    {
+                        tracing::debug!(
+                            "expanding projection to thrust_models::Model::Ty for {arg_ty:?}."
+                        );
+                        return self.build(arg_ty);
+                    }
+                }
+
+                self.translate_alias_type(ty)
+            }
             kind => unimplemented!("unrefined_ty: {:?}", kind),
         }
     }
@@ -398,6 +537,10 @@ where
                 let elem_ty = self.build(*elem_ty);
                 rty::PointerType::immut_to(elem_ty).into()
             }
+            mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Mut) => {
+                let elem_ty = self.build(*elem_ty);
+                rty::PointerType::mut_to(elem_ty).into()
+            }
             mir_ty::TyKind::Tuple(ts) => {
                 // elaboration: all fields are boxed
                 let elems = ts
@@ -418,6 +561,23 @@ where
                 if let Some(model_ty) = self.model_adt(def, params) {
                     return model_ty;
                 }
+                // Treat Box and Vec as opaque types to avoid traversing internal structure
+                if Some(def.did()) == self.inner.def_ids.box_() {
+                    let elem_ty = self.build(params.type_at(0));
+                    return rty::PointerType::own(elem_ty).into();
+                }
+                if Some(def.did()) == self.inner.def_ids.vec() {
+                    let elem_ty = self.build(params.type_at(0));
+                    // Vec is represented as a tuple of (Array<Int, T>, Int) in the model
+                    let idx_ty = rty::Type::int();
+                    let array_ty = rty::ArrayType::new(idx_ty, elem_ty.clone());
+                    let len_ty = rty::Type::int();
+                    return rty::TupleType::new(vec![
+                        rty::PointerType::own(rty::Type::Array(array_ty)).into(),
+                        rty::PointerType::own(len_ty).into(),
+                    ])
+                    .into();
+                }
                 if def.is_enum() {
                     let sym = refine::datatype_symbol(self.inner.tcx, def.did());
                     let args: IndexVec<_, _> =
@@ -437,6 +597,25 @@ where
                     unimplemented!("unsupported ADT: {:?}", ty);
                 }
             }
+            mir_ty::TyKind::Alias(mir_ty::AliasTyKind::Projection, ty) => {
+                if let Some(model_ty_def_id) = self.inner.def_ids.model_ty() {
+                    let arg_ty = ty.args.type_at(0);
+
+                    if ty.def_id == model_ty_def_id
+                        && (matches!(
+                            arg_ty.kind(),
+                            mir_ty::TyKind::Param(_) | mir_ty::TyKind::Alias(..)
+                        ))
+                    {
+                        tracing::debug!(
+                            "expanding projection to thrust_models::Model::Ty for {arg_ty:?}."
+                        );
+                        return self.build(arg_ty);
+                    }
+                }
+
+                self.inner.translate_alias_type(ty).vacuous()
+            }
             kind => unimplemented!("ty: {:?}", kind),
         }
     }
diff --git a/src/rty.rs b/src/rty.rs
index 28209bb4..85de6e42 100644
--- a/src/rty.rs
+++ b/src/rty.rs
@@ -43,7 +43,7 @@ use pretty::{termcolor, Pretty};
 use rustc_abi::VariantIdx;
 use rustc_index::IndexVec;
 
-use crate::chc;
+use crate::chc::{self, ForallSortIdx};
 
 mod template;
 pub use template::{Template, TemplateBuilder};
@@ -192,7 +192,7 @@ impl FunctionAbi {
 /// In Thrust, function types are closed. Because of that, function types, thus its parameters and
 /// return type only refer to the parameters of the function itself using [`FunctionParamIdx`] and
 /// do not accept other type of variables from the environment.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct FunctionType {
     pub params: IndexVec<FunctionParamIdx, RefinedType<FunctionParamIdx>>,
     pub ret: Box<RefinedType<FunctionParamIdx>>,
@@ -397,7 +397,7 @@ where
 }
 
 /// The kind of a reference, which is either mutable or immutable.
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 pub enum RefKind {
     Mut,
     Immut,
@@ -422,7 +422,7 @@ where
 }
 
 /// The kind of a pointer, which is either a reference or an owned pointer.
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 pub enum PointerKind {
     Ref(RefKind),
     Own,
@@ -462,7 +462,7 @@ impl PointerKind {
 }
 
 /// A pointer type.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct PointerType<T> {
     pub kind: PointerKind,
     pub elem: Box<RefinedType<T>>,
@@ -575,7 +575,7 @@ impl<T> PointerType<T> {
 /// Note that the current implementation uses tuples to represent structs. See
 /// implementation in `crate::refine::template` module for details.
 /// It is our TODO to improve the struct representation.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct TupleType<T> {
     pub elems: Vec<RefinedType<T>>,
 }
@@ -699,7 +699,7 @@ impl EnumDatatypeDef {
 /// An enum type.
 ///
 /// An enum type includes its type arguments and the argument types can refer to outer variables `T`.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct EnumType<T> {
     pub symbol: chc::DatatypeSymbol,
     pub args: IndexVec<TypeParamIdx, RefinedType<T>>,
@@ -801,9 +801,10 @@ impl<T> EnumType<T> {
 }
 
 /// A type parameter.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct ParamType {
-    pub idx: TypeParamIdx,
+    type_param_idx: TypeParamIdx,
+    forall_sort_idx: ForallSortIdx,
 }
 
 impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ParamType
@@ -811,17 +812,24 @@ where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
     fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
-        self.idx.pretty(allocator)
+        self.type_param_idx.pretty(allocator)
     }
 }
 
 impl ParamType {
-    pub fn new(idx: TypeParamIdx) -> Self {
-        ParamType { idx }
+    pub fn new(type_param_idx: TypeParamIdx, forall_sort_idx: ForallSortIdx) -> Self {
+        ParamType {
+            type_param_idx,
+            forall_sort_idx,
+        }
+    }
+
+    pub fn type_param_index(&self) -> TypeParamIdx {
+        self.type_param_idx
     }
 
-    pub fn index(&self) -> TypeParamIdx {
-        self.idx
+    pub fn forall_sort_index(&self) -> ForallSortIdx {
+        self.forall_sort_idx
     }
 
     pub fn into_closed_ty(self) -> Type<Closed> {
@@ -829,8 +837,60 @@ impl ParamType {
     }
 }
 
+/// A projection type representing an unresolved associated type.
+///
+/// This preserves the structural identity of projections like `<T as Iterator>::Item`
+/// or `<Map<I, F> as Iterator>::Item`, keeping them distinct even before normalization.
+///
+/// The `args` field stores the generic arguments (Self type + other args), which can
+/// recursively contain other types including params, ADTs, and other projections.
+/// For example, `<Map<I, F> as Iterator>::Item` would have `args = [Map<I, F>]`.
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub struct AliasType {
+    forall_sort_idx: ForallSortIdx,
+    args: Vec<Type<Closed>>,
+}
+
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &AliasType
+where
+    D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
+    D::Doc: Clone,
+{
+    fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
+        let sort = self.forall_sort_idx.pretty(allocator);
+        if self.args.is_empty() {
+            sort
+        } else {
+            let args = allocator.intersperse(
+                self.args.iter().map(|ty| ty.pretty(allocator)),
+                allocator.text(",").append(allocator.line()),
+            );
+            sort.append(allocator.line())
+                .append(args.nest(2).angles())
+                .group()
+        }
+    }
+}
+
+impl AliasType {
+    pub fn new(forall_sort_idx: ForallSortIdx, args: Vec<Type<Closed>>) -> Self {
+        AliasType {
+            forall_sort_idx,
+            args,
+        }
+    }
+
+    pub fn forall_sort_index(&self) -> ForallSortIdx {
+        self.forall_sort_idx
+    }
+
+    pub fn args(&self) -> &[Type<Closed>] {
+        &self.args
+    }
+}
+
 /// An array type.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct ArrayType<T> {
     pub index: Box<RefinedType<T>>,
     pub elem: Box<RefinedType<T>>,
@@ -913,13 +973,14 @@ impl<T> ArrayType<T> {
 }
 
 /// An underlying type of a refinement type.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Type<T> {
     Int,
     Bool,
     String,
     Never,
     Param(ParamType),
+    Alias(AliasType),
     Pointer(PointerType<T>),
     Function(FunctionType),
     Tuple(TupleType<T>),
@@ -933,6 +994,12 @@ impl<T> From<ParamType> for Type<T> {
     }
 }
 
+impl<T> From<AliasType> for Type<T> {
+    fn from(t: AliasType) -> Type<T> {
+        Type::Alias(t)
+    }
+}
+
 impl<T> From<FunctionType> for Type<T> {
     fn from(t: FunctionType) -> Type<T> {
         Type::Function(t)
@@ -976,6 +1043,7 @@ where
             Type::String => allocator.text("string"),
             Type::Never => allocator.text("!"),
             Type::Param(ty) => ty.pretty(allocator),
+            Type::Alias(ty) => ty.pretty(allocator),
             Type::Pointer(ty) => ty.pretty(allocator),
             Type::Function(ty) => ty.pretty(allocator),
             Type::Tuple(ty) => ty.pretty(allocator),
@@ -1108,7 +1176,8 @@ impl<T> Type<T> {
             //       currently String sort seems not available in HORN logic of Z3
             Type::String => chc::Sort::null(),
             Type::Never => chc::Sort::null(),
-            Type::Param(ty) => chc::Sort::param(ty.index().into()),
+            Type::Param(ty) => chc::Sort::forall(ty.forall_sort_index()),
+            Type::Alias(ty) => chc::Sort::Forall(ty.forall_sort_index()),
             Type::Pointer(ty) => {
                 let elem_sort = ty.elem.ty.to_sort();
 
@@ -1146,6 +1215,7 @@ impl<T> Type<T> {
             Type::String => Type::String,
             Type::Never => Type::Never,
             Type::Param(ty) => Type::Param(ty),
+            Type::Alias(ty) => Type::Alias(ty),
             Type::Pointer(ty) => Type::Pointer(ty.subst_var(f)),
             Type::Function(ty) => Type::Function(ty),
             Type::Tuple(ty) => Type::Tuple(ty.subst_var(f)),
@@ -1164,6 +1234,7 @@ impl<T> Type<T> {
             Type::String => Type::String,
             Type::Never => Type::Never,
             Type::Param(ty) => Type::Param(ty),
+            Type::Alias(ty) => Type::Alias(ty),
             Type::Pointer(ty) => Type::Pointer(ty.map_var(f)),
             Type::Function(ty) => Type::Function(ty),
             Type::Tuple(ty) => Type::Tuple(ty.map_var(f)),
@@ -1183,6 +1254,7 @@ impl<T> Type<T> {
             Type::String => Type::String,
             Type::Never => Type::Never,
             Type::Param(ty) => Type::Param(ty),
+            Type::Alias(ty) => Type::Alias(ty),
             Type::Pointer(ty) => Type::Pointer(ty.strip_refinement()),
             Type::Function(ty) => Type::Function(ty),
             Type::Tuple(ty) => Type::Tuple(ty.strip_refinement()),
@@ -1194,7 +1266,12 @@ impl<T> Type<T> {
     pub fn free_ty_params(&self) -> HashSet<TypeParamIdx> {
         match self {
             Type::Int | Type::Bool | Type::String | Type::Never => Default::default(),
-            Type::Param(ty) => std::iter::once(ty.index()).collect(),
+            Type::Param(ty) => std::iter::once(ty.type_param_index()).collect(),
+            Type::Alias(ty) => ty
+                .args()
+                .iter()
+                .flat_map(|ty| ty.free_ty_params())
+                .collect(),
             Type::Pointer(ty) => ty.free_ty_params(),
             Type::Function(ty) => ty.free_ty_params(),
             Type::Tuple(ty) => ty.free_ty_params(),
@@ -1336,7 +1413,7 @@ impl<T> ShiftExistential for RefinedTypeVar<T> {
 /// A formula, potentially equipped with an existential quantifier.
 ///
 /// Note: This is not to be confused with [`crate::chc::Formula`] in the [`crate::chc`] module, which is a different notion.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct Formula<V> {
     pub existentials: IndexVec<ExistentialVarIdx, chc::Sort>,
     pub body: chc::Body<V>,
@@ -1608,7 +1685,7 @@ impl<T> Instantiator<T> {
 }
 
 /// A refinement type.
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct RefinedType<FV = Closed> {
     pub ty: Type<FV>,
     pub refinement: Refinement<FV>,
@@ -1805,7 +1882,7 @@ impl<FV> RefinedType<FV> {
         match &mut self.ty {
             Type::Int | Type::Bool | Type::String | Type::Never => {}
             Type::Param(ty) => {
-                if let Some(rty) = subst.get(ty.index()) {
+                if let Some(rty) = subst.get(ty.type_param_index()) {
                     let RefinedType {
                         ty: replacement_ty,
                         refinement,
@@ -1814,6 +1891,19 @@ impl<FV> RefinedType<FV> {
                     self.ty = replacement_ty;
                 }
             }
+            Type::Alias(alias) => {
+                let subst_closed = subst.clone().strip_refinement();
+                let new_args: Vec<Type<Closed>> = alias
+                    .args()
+                    .iter()
+                    .map(|arg| {
+                        let mut arg_rty = RefinedType::unrefined(arg.clone());
+                        arg_rty.subst_ty_params(&subst_closed);
+                        arg_rty.ty
+                    })
+                    .collect();
+                self.ty = Type::Alias(AliasType::new(alias.forall_sort_index(), new_args));
+            }
             Type::Pointer(ty) => ty.subst_ty_params(subst),
             Type::Function(ty) => {
                 let subst = subst.clone().strip_refinement();
@@ -1841,15 +1931,15 @@ impl<FV> RefinedType<FV> {
             | (Type::Bool, Type::Bool)
             | (Type::String, Type::String)
             | (Type::Never, Type::Never) => Default::default(),
-            (Type::Param(pty), ty) if !ty.free_ty_params().contains(&pty.index()) => {
+            (Type::Param(pty), ty) if !ty.free_ty_params().contains(&pty.type_param_index()) => {
                 TypeParamSubst::singleton(
-                    pty.index(),
+                    pty.type_param_index(),
                     RefinedType::new(ty.clone(), other.refinement.clone()),
                 )
             }
-            (ty, Type::Param(pty)) if !ty.free_ty_params().contains(&pty.index()) => {
+            (ty, Type::Param(pty)) if !ty.free_ty_params().contains(&pty.type_param_index()) => {
                 TypeParamSubst::singleton(
-                    pty.index(),
+                    pty.type_param_index(),
                     RefinedType::new(ty.clone(), self.refinement.clone()),
                 )
             }
@@ -1861,6 +1951,24 @@ impl<FV> RefinedType<FV> {
             (Type::Tuple(ty1), Type::Tuple(ty2)) => ty1.unify_ty_params(ty2),
             (Type::Array(ty1), Type::Array(ty2)) => ty1.unify_ty_params(ty2),
             (Type::Enum(ty1), Type::Enum(ty2)) => ty1.unify_ty_params(ty2),
+            (Type::Alias(a1), Type::Alias(a2))
+                if a1.forall_sort_index() == a2.forall_sort_index() =>
+            {
+                assert_eq!(a1.args().len(), a2.args().len());
+                let args1: Vec<RefinedType<FV>> = a1
+                    .args()
+                    .iter()
+                    .cloned()
+                    .map(|ty| RefinedType::unrefined(ty).vacuous())
+                    .collect();
+                let args2: Vec<RefinedType<FV>> = a2
+                    .args()
+                    .iter()
+                    .cloned()
+                    .map(|ty| RefinedType::unrefined(ty).vacuous())
+                    .collect();
+                unify_tys_params(args1, args2)
+            }
             (t1, t2) => panic!("unify_ty_params: mismatched types t1={:?}, t2={:?}", t1, t2),
         }
     }
@@ -1875,7 +1983,11 @@ impl RefinedType<Closed> {
 /// Substitutes type parameters in a sort.
 fn subst_ty_params_in_sort<T>(sort: &mut chc::Sort, subst: &TypeParamSubst<T>) {
     match sort {
-        chc::Sort::Null | chc::Sort::Int | chc::Sort::Bool | chc::Sort::String => {}
+        chc::Sort::Null
+        | chc::Sort::Int
+        | chc::Sort::Bool
+        | chc::Sort::String
+        | chc::Sort::Forall(_) => {}
         chc::Sort::Param(idx) => {
             let type_param_idx = TypeParamIdx::from_usize(*idx);
             if let Some(rty) = subst.get(type_param_idx) {
diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs
index 03477f02..71196fde 100644
--- a/src/rty/subtyping.rs
+++ b/src/rty/subtyping.rs
@@ -123,6 +123,10 @@ where
                 let cs2 = self.relate_sub_refined_type(&got.elem, &expected.elem);
                 clauses.extend(cs2);
             }
+            (Type::Param(got), Type::Param(expected))
+                if got.forall_sort_idx == expected.forall_sort_idx => {}
+            (Type::Alias(got), Type::Alias(expected))
+                if got.forall_sort_index() == expected.forall_sort_index() => {}
             _ => panic!(
                 "inconsistent types: got={}, expected={}",
                 got.display(),
diff --git a/tests/ui/annot-error/array_index_literal_int.rs b/tests/ui/annot-error/array_index_literal_int.rs
new file mode 100644
index 00000000..bb64b171
--- /dev/null
+++ b/tests/ui/annot-error/array_index_literal_int.rs
@@ -0,0 +1,24 @@
+// Reproduces: an integer literal used as an `Array<Int, T>` index in a spec
+// expression fails to type-check (E0308 "expected `Int`, found integer").
+//
+// `thrust_models::model::Array<I, T>` has an `Index<I>` impl whose index
+// type is the `I` parameter; for `Array<Int, T>` that is the `model::Int`
+// ZST, which is not the same as Rust's `{integer}` literal type. The spec
+// attribute path lowers `it[0]` as a Rust expression, so the `0` must be
+// a `model::Int`-typed term. No such literal is constructible in Rust
+// source today.
+//
+// See `array_index_literal_int_workaround.rs` for the bound-variable
+// form that sidesteps the literal.
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    thrust_models::exists(|it: thrust_models::model::Array<thrust_models::model::Int, i64>|
+        it[0] == 0
+    )
+)]
+fn head(arr: Vec<i64>) -> i64 {
+    arr[0]
+}
+
+fn main() {}
diff --git a/tests/ui/annot-error/array_index_literal_int_workaround.rs b/tests/ui/annot-error/array_index_literal_int_workaround.rs
new file mode 100644
index 00000000..74d74953
--- /dev/null
+++ b/tests/ui/annot-error/array_index_literal_int_workaround.rs
@@ -0,0 +1,27 @@
+// Annotation-side workaround for `array_index_literal_int.rs`.
+//
+// Rather than writing the literal `0` as the index (which fails because
+// the `Index<I>` impl on `Array<I, T>` requires `I`-typed indices, and
+// `model::Int` has no Rust literal form), bind the index with an
+// existential and let typeck infer its sort:
+//
+//   exists(|idx| it[idx] == 0)
+//
+// `idx` gets the `model::Int` sort from the `Index<I>` site's expected
+// `I = model::Int`. The expression type-checks; the trade-off is that
+// the spec no longer pins a specific index like "0" or "1" — it just
+// asserts "there exists some index such that the value at that index is 0".
+
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    thrust_models::exists(|it: thrust_models::model::Array<thrust_models::model::Int, i64>|
+        thrust_models::exists(|idx|
+            it[idx] == 0
+        )
+    )
+)]
+fn head(arr: Vec<i64>) -> i64 {
+    arr[0]
+}
+
+fn main() {}
diff --git a/tests/ui/annot-error/formula_fn_capture_local.rs b/tests/ui/annot-error/formula_fn_capture_local.rs
new file mode 100644
index 00000000..ba7ec28c
--- /dev/null
+++ b/tests/ui/annot-error/formula_fn_capture_local.rs
@@ -0,0 +1,47 @@
+// Reproduces: a `formula_fn` produced by `requires`/`ensures`/`invariant!`
+// cannot capture the surrounding function's local bindings (E0434 "can't
+// capture dynamic environment in a fn item").
+//
+// The macro lowers the spec into a free `fn _thrust_ensures_X(...)` whose
+// only inputs are the host parameters (lowered to their `Model::Ty`) and
+// the closure's bound variables. Any reference to a `let`-bound name in
+// the host function is rejected.
+//
+// Same shape, applied to `_invariant_with_context!`: the host signature
+// re-declared in the macro head (e.g. `fn run<B, F>(self, f: B, g: F)`)
+// is *not* threaded into the `formula_fn` parameters either; the macro
+// currently only lowers the closure params plus the synthetic
+// `__ThrustSelf` (for `Self` rewrite).
+//
+// No annotation-side workaround: this is a macro bug in
+// `thrust-macros/src/invariant.rs::expand_invariant` (the host-signature
+// re-declaration is parsed but its parameters are dropped on the floor).
+// Either fix the macro to lower the re-declared signature's params via
+// `type_lowering.lower_params(...)` and add them to the formula_fn, or
+// restructure the invariant to not mention the host parameters (which
+// often defeats the point of the invariant).
+
+#[thrust_macros::context]
+trait Foo {
+    fn run<B, F>(self, f: B, g: F) -> B
+    where
+        Self: Sized,
+        F: FnOnce(B) -> B,
+    {
+        let mut x: i64 = 0;
+        while x < 1 {
+            thrust_macros::_invariant_with_context!(
+                #[thrust::_outer_context(trait Foo {})]
+                fn run<B, F>(self: Self, f: B, g: F) -> B
+                where
+                    Self: Sized,
+                    F: FnOnce(B) -> B;
+                |x: i64| x == f && g == f
+            );
+            x += 1;
+        }
+        f
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/annot-error/invariant_context_self_trait_bound.rs b/tests/ui/annot-error/invariant_context_self_trait_bound.rs
new file mode 100644
index 00000000..25f9ca12
--- /dev/null
+++ b/tests/ui/annot-error/invariant_context_self_trait_bound.rs
@@ -0,0 +1,50 @@
+// Reproduces: when an `_invariant_with_context!` rewrites `Self` to a
+// synthetic `__ThrustSelf` generic in the injected `formula_fn`, it does
+// NOT automatically propagate the host trait bound (here `Self: Foo`).
+// Calling trait items (the user-defined predicates `completed` / `step`
+// and the associated `Item` type) on the synthetic `Self` therefore
+// fails with E0599 / E0220 "no function / associated type named X found
+// for `__ThrustSelf`".
+//
+// See `invariant_context_self_trait_bound_workaround.rs` for a partial
+// workaround (`Self: Sized + Foo` in the re-declared where clause) that
+// silences E0599 (the trait method calls) but leaves E0220 (the
+// associated type) untouched — fully fixing the latter requires the
+// `expand_invariant` macro to also rewrite `Self` to `__ThrustSelf` in
+// the propagated where-clause predicates.
+
+#[thrust_macros::context]
+trait Foo {
+    type Item;
+
+    #[thrust_macros::predicate]
+    fn completed(self) -> bool;
+    #[thrust_macros::predicate]
+    fn step(self, item: Self::Item, dist: Self) -> bool;
+
+    fn run<B, F>(mut self, init: B, mut f: F) -> B
+    where
+        Self: Sized,
+        F: FnMut(B, Self::Item) -> B,
+    {
+        let mut accum = init;
+        while true {
+            thrust_macros::_invariant_with_context!(
+                #[thrust::_outer_context(trait Foo { type Item; })]
+                fn run<B, F>(mut self: Self, init: B, mut f: F) -> B
+                where
+                    Self: Sized,
+                    F: FnMut(B, Self::Item) -> B;
+                |accum: B| thrust_models::exists(
+                    |item: Self::Item|
+                        Self::step(*self, item, *self)
+                        && accum == init
+                )
+            );
+            break;
+        }
+        accum
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/annot-error/invariant_context_self_trait_bound_workaround.rs b/tests/ui/annot-error/invariant_context_self_trait_bound_workaround.rs
new file mode 100644
index 00000000..3fc07657
--- /dev/null
+++ b/tests/ui/annot-error/invariant_context_self_trait_bound_workaround.rs
@@ -0,0 +1,60 @@
+// Annotation-side partial workaround for
+// `invariant_context_self_trait_bound.rs`.
+//
+// Adding the host trait bound to the re-declared signature's where
+// clause (`Self: Sized + Foo` instead of just `Self: Sized`) makes the
+// `expand_invariant` macro copy it into the `formula_fn`'s where
+// clause, so `__ThrustSelf: Foo` is in scope. That silences the trait
+// method-call errors (E0599 for `__ThrustSelf::step` /
+// `__ThrustSelf::completed`).
+//
+// What it does NOT fix: E0220 for `__ThrustSelf::Item`. The macro's
+// `where_predicates()` walk copies the re-declared where-clause
+// predicates verbatim — `Self` is *not* rewritten to `__ThrustSelf` in
+// the copied predicates, so the copy still talks about `Self` (host
+// type) rather than `__ThrustSelf` (synthetic). The associated type
+// `Item` lookup goes through `Self` instead of `__ThrustSelf`, and Rust
+// complains. Fully fixing this needs the macro to rewrite `Self` to
+// `__ThrustSelf` in the propagated where-clause predicates, then add
+// `<__ThrustSelf as Foo>::Item` (or an analogous `Item` projection) to
+// the `__ThrustSelf` parameter scope.
+
+#[thrust_macros::context]
+trait Foo {
+    type Item;
+
+    #[thrust_macros::predicate]
+    fn completed(self) -> bool;
+    #[thrust_macros::predicate]
+    fn step(self, item: Self::Item, dist: Self) -> bool;
+
+    fn run<B, F>(mut self, init: B, mut f: F) -> B
+    where
+        Self: Sized,
+        F: FnMut(B, Self::Item) -> B,
+    {
+        let mut accum = init;
+        while true {
+            thrust_macros::_invariant_with_context!(
+                #[thrust::_outer_context(trait Foo { type Item; })]
+                fn run<B, F>(mut self: Self, init: B, mut f: F) -> B
+                where
+                    // ← the partial-fix: add the host trait bound to
+                    //   the re-declared where clause. The macro copies
+                    //   it to the formula_fn where, so __ThrustSelf: Foo
+                    //   resolves the trait method calls.
+                    Self: Sized + Foo,
+                    F: FnMut(B, Self::Item) -> B;
+                |accum: B| thrust_models::exists(
+                    |item: Self::Item|
+                        Self::step(*self, item, *self)
+                        && accum == init
+                )
+            );
+            break;
+        }
+        accum
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/annot-error/invariant_context_trait_method.rs b/tests/ui/annot-error/invariant_context_trait_method.rs
new file mode 100644
index 00000000..d4bea507
--- /dev/null
+++ b/tests/ui/annot-error/invariant_context_trait_method.rs
@@ -0,0 +1,27 @@
+// Reproduces: `#[thrust_macros::invariant_context]` attached to a *trait*
+// method fails with E0401 ("can't use `Self` from outer item").
+//
+// `invariant_context` is `ItemFn`-only (`thrust-macros/src/invariant_context.rs`).
+// On a trait method it parses, but it never threads the trait-level `Self`
+// through to the generated `formula_fn`, so the injected
+// `_invariant_with_context!` macro ends up rewriting the closure body against
+// the outer trait's `Self` (which is out of scope) and Rust rejects the use.
+
+#[thrust_macros::context]
+trait Foo {
+    type Item;
+
+    #[thrust_macros::invariant_context]
+    fn run(&mut self)
+    where
+        Self: Sized,
+    {
+        let mut x: i64 = 0;
+        while x < 1 {
+            thrust_macros::invariant!(|x: i64| x >= 0);
+            x += 1;
+        }
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/annot-error/invariant_context_trait_method_workaround.rs b/tests/ui/annot-error/invariant_context_trait_method_workaround.rs
new file mode 100644
index 00000000..5630319d
--- /dev/null
+++ b/tests/ui/annot-error/invariant_context_trait_method_workaround.rs
@@ -0,0 +1,49 @@
+// Annotation-side workaround for `invariant_context_trait_method.rs`.
+//
+// The `#[thrust_macros::invariant_context]` attribute is `ItemFn`-only
+// (its `expand` parses as `syn::ItemFn`), so attaching it to a trait
+// method triggers E0401 because the trait's `Self` is out of scope for
+// the generated `formula_fn`. The other annotation-side attempt —
+// hand-rolling `thrust_macros::_invariant_with_context!` inside the
+// loop body — runs into the same problem (the macro's `SelfRewriter`
+// only kicks in when the closure body actually mentions `Self`;
+// otherwise `Self: Model` constraints are produced against the outer
+// `Self` and Rust rejects them).
+//
+// Workaround: drop the invariant on the trait method, and instead
+// provide it on the concrete impl method, where `invariant_context`
+// works (`ItemFn` parse target). The impl is the only place the
+// invariant is meaningful anyway: the trait method's spec is
+// independent of any concrete iterator type.
+
+#[thrust_macros::context]
+trait Foo {
+    type Item;
+
+    fn run(&mut self);
+}
+
+struct Bar;
+
+impl thrust_models::Model for Bar {
+    type Ty = Bar;
+}
+
+#[thrust_macros::context]
+impl Foo for Bar {
+    type Item = i64;
+
+    // `invariant_context` on an impl method is fine: the host is an
+    // `ItemFn` (`impl` method) and `Self` is the impl's self-type,
+    // not the trait's.
+    #[thrust_macros::invariant_context]
+    fn run(&mut self) {
+        let mut x: i64 = 0;
+        while x < 1 {
+            thrust_macros::invariant!(|x: i64| x >= 0);
+            x += 1;
+        }
+    }
+}
+
+fn main() {}
diff --git a/tests/ui/pass/traits/fold.rs b/tests/ui/pass/traits/fold.rs
new file mode 100644
index 00000000..7935394e
--- /dev/null
+++ b/tests/ui/pass/traits/fold.rs
@@ -0,0 +1,139 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60
+
+use thrust_models::{Model, exists, forall, model::Mut};
+
+#[thrust_macros::context]
+trait Iterator {
+    type Item;
+
+    #[thrust_macros::ensures(
+        Self::completed(*self)
+        || exists(|i| (result == Some(i)) && Self::step(*self, i, !self))
+    )]
+    #[thrust_macros::ensures(!Self::completed(*self) || (result == None && *self == !self))]
+    fn next(&mut self) -> Option<Self::Item>;
+
+    #[thrust_macros::predicate]
+    fn completed(self) -> bool;
+    #[thrust_macros::predicate]
+    fn step(self, item: Self::Item, dist: Self) -> bool;
+
+    #[thrust_macros::invariant_context]
+    #[thrust_macros::requires(true)]
+    #[thrust_macros::ensures(
+        exists(|it: thrust_models::model::Array<thrust_models::model::Int, <Self as Model>::Ty>|
+        exists(|fn_: thrust_models::model::Array<thrust_models::model::Int, thrust_models::model::Closure<F>>|
+        exists(|acc: thrust_models::model::Array<thrust_models::model::Int, <B as Model>::Ty>|
+        exists(|l: thrust_models::model::Int|
+            it[0] == self &&
+            fn_[0] == f &&
+            acc[0] == init &&
+            Self::completed(it[l - 1]) &&
+            result == acc[l - 1] &&
+            forall(|i: thrust_models::model::Int|
+                0 <= i && i < l - 1 ==>
+                exists(|item|
+                    !Self::completed(it[i]) &&
+                    Self::step(it[i], item, it[i + 1]) &&
+                    thrust_macros::pre!(Mut::new(fn_[i], fn_[i+1])(acc[i], item)) &&
+                    thrust_macros::post!(
+                        Mut::new(fn_[i], fn_[i+1])(acc[i], item),
+                        acc[i + 1]
+                    )
+                )
+            )
+        ))))
+    )]
+    fn fold<B, F>(mut self, init: B, mut f: F) -> B
+    where
+        Self: Sized,
+        F: FnMut(B, Self::Item) -> B,
+    {
+        let mut accum = init;
+        while let Some(x) = self.next() {
+            thrust_macros::invariant!(
+                |accum: B, init: thrust_models::FnParam<B>, f: F, self: Self|
+                exists(|it: thrust_models::model::Array<thrust_models::model::Int, <Self as Model>::Ty>|
+                exists(|fn_: thrust_models::model::Array<thrust_models::model::Int, thrust_models::model::Closure<F>>|
+                exists(|acc: thrust_models::model::Array<thrust_models::model::Int, <B as Model>::Ty>|
+                exists(|l: thrust_models::model::Int|
+                    it[0] == self &&
+                    fn_[0] == f &&
+                    acc[0] == init.at_entry() &&
+                    accum == acc[l - 1] &&
+                    forall(|i: thrust_models::model::Int|
+                        0 <= i && i < l - 1 ==>
+                        exists(|item: <Self::Item as Model>::Ty|
+                            !Self::completed(it[i]) &&
+                            Self::step(it[i], item, it[i + 1]) &&
+                            thrust_macros::pre!(Mut::new(fn_[i], fn_[i+1])(acc[i], item)) &&
+                            thrust_macros::post!(
+                                Mut::new(fn_[i], fn_[i+1])(acc[i], item),
+                                acc[i + 1]
+                            )
+                        )
+                    )
+                ))))
+            );
+            accum = f(accum, x);
+        }
+        accum
+    }
+}
+
+#[derive(PartialEq)]
+struct Range {
+    start: i64,
+    end: i64,
+}
+
+impl thrust_models::Model for Range {
+    type Ty = Range;
+}
+
+#[thrust_macros::context]
+impl Iterator for Range {
+    type Item = i64;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        if self.start < self.end {
+            let item = self.start;
+            self.start += 1;
+            Some(item)
+        } else {
+            None
+        }
+    }
+
+    #[thrust_macros::predicate]
+    fn completed(self) -> bool {
+        // (tuple_proj<Int-Int>.0 self) is equivalent to self.start
+        // !(self.start < self.end) is written as following:
+        "(not (<
+            (tuple_proj<Int-Int>.0 self_)
+            (tuple_proj<Int-Int>.1 self_)
+        ))";
+        true
+    }
+
+    #[thrust_macros::predicate]
+    fn step(self, item: Self::Item, dist: Self) -> bool {
+        // self.end == dist.end && self.start == item && self.start + 1 == dist.start
+        // is written as following:
+        "(and
+            (= (tuple_proj<Int-Int>.1 self_) (tuple_proj<Int-Int>.1 dist))
+            (= (tuple_proj<Int-Int>.0 self_) item)
+            (= (+ (tuple_proj<Int-Int>.0 self_) 1) (tuple_proj<Int-Int>.0 dist))
+        )";
+        true
+    }
+}
+
+fn main() {
+    let mut range = Range { start: 0, end: 5 };
+    let sum = range.fold(0, |x, y| x + y);
+
+    assert!(sum == 10);
+}
\ No newline at end of file
diff --git a/tests/ui/pass/traits/simple_loop.rs b/tests/ui/pass/traits/simple_loop.rs
new file mode 100644
index 00000000..857ecdb3
--- /dev/null
+++ b/tests/ui/pass/traits/simple_loop.rs
@@ -0,0 +1,28 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60
+
+#[thrust_macros::context]
+trait A {
+    #[thrust_macros::requires(Self::p(x))]
+    #[thrust_macros::ensures(Self::p(result))]
+    fn f(&self, x: i64) -> i64;
+
+    #[thrust_macros::predicate]
+    fn p(x: i64) -> bool;
+}
+
+#[thrust_macros::requires(T::p(x))]
+#[thrust_macros::ensures(T::p(result))]
+fn target<T: A>(a: &T, x: i64) -> i64 {
+    let mut v = x;
+    let mut i = 0;
+    while i < 3 {
+        v = a.f(v);
+        i += 1;
+    }
+
+    v
+}
+
+fn main() {}
diff --git a/tests/ui/pass/traits/simple_loop_2int.rs b/tests/ui/pass/traits/simple_loop_2int.rs
new file mode 100644
index 00000000..6edb3530
--- /dev/null
+++ b/tests/ui/pass/traits/simple_loop_2int.rs
@@ -0,0 +1,28 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60
+
+#[thrust_macros::context]
+trait A {
+    #[thrust_macros::requires(Self::p(x, x))]
+    #[thrust_macros::ensures(Self::p(result, result))]
+    fn f(&self, x: i64) -> i64;
+
+    #[thrust_macros::predicate]
+    fn p(x: i64, y: i64) -> bool;
+}
+
+#[thrust_macros::requires(T::p(x, x))]
+#[thrust_macros::ensures(T::p(result, result))]
+fn target<T: A>(a: &T, x: i64) -> i64 {
+    let mut v = x;
+    let mut i = 0;
+    while i < 3 {
+        v = a.f(v);
+        i += 1;
+    }
+
+    v
+}
+
+fn main() {}
diff --git a/tests/ui/pass/traits/simple_loop_call.rs b/tests/ui/pass/traits/simple_loop_call.rs
new file mode 100644
index 00000000..39115fd8
--- /dev/null
+++ b/tests/ui/pass/traits/simple_loop_call.rs
@@ -0,0 +1,49 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60
+
+#[thrust_macros::context]
+trait A {
+    #[thrust_macros::requires(Self::p(x))]
+    #[thrust_macros::ensures(Self::p(result))]
+    fn f(&self, x: i64) -> i64;
+
+    #[thrust_macros::predicate]
+    fn p(x: i64) -> bool;
+}
+
+#[thrust_macros::requires(T::p(x))]
+#[thrust_macros::ensures(T::p(result))]
+fn target<T: A>(a: &T, x: i64) -> i64 {
+    let mut v = x;
+    let mut i = 0;
+    while i < 3 {
+        v = a.f(v);
+        i += 1;
+    }
+
+    v
+}
+
+#[derive(PartialEq)]
+struct B(i64);
+
+impl thrust_models::Model for B {
+    type Ty = B;
+}
+
+#[thrust_macros::context]
+impl A for B {
+    fn f(&self, x: i64) -> i64{
+        x
+    }
+
+    #[thrust_macros::predicate]
+    fn p(x: i64) -> bool {
+        "(> x 0)"; true
+    }
+}
+
+fn main() {
+    
+}
diff --git a/tests/ui/pass/traits/simple_loop_self.rs b/tests/ui/pass/traits/simple_loop_self.rs
new file mode 100644
index 00000000..0c026e06
--- /dev/null
+++ b/tests/ui/pass/traits/simple_loop_self.rs
@@ -0,0 +1,28 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60
+
+#[thrust_macros::context]
+trait A {
+    #[thrust_macros::requires(Self::p(*self, x))]
+    #[thrust_macros::ensures(Self::p(*self, result))]
+    fn f(&self, x: i64) -> i64;
+
+    #[thrust_macros::predicate]
+    fn p(self, x: i64) -> bool;
+}
+
+#[thrust_macros::requires(T::p(*a, x))]
+#[thrust_macros::ensures(T::p(*a, result))]
+fn target<T: A>(a: &T, x: i64) -> i64 {
+    let mut v = x;
+    let mut i = 0;
+    while i < 3 {
+        v = a.f(v);
+        i += 1;
+    }
+
+    v
+}
+
+fn main() {}
diff --git a/tests/ui/pass/traits/simple_loop_self_mut.rs b/tests/ui/pass/traits/simple_loop_self_mut.rs
new file mode 100644
index 00000000..53a69e22
--- /dev/null
+++ b/tests/ui/pass/traits/simple_loop_self_mut.rs
@@ -0,0 +1,32 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60
+
+#[thrust_macros::context]
+trait A {
+    #[thrust_macros::requires(Self::p(*self, !self, x))]
+    #[thrust_macros::ensures(Self::p(*self, !self, result))]
+    fn f(&mut self, x: i64) -> i64;
+
+    #[thrust_macros::predicate]
+    fn p(self, after: Self, x: i64) -> bool;
+}
+
+// impl thrust_models::Model for A {
+//     type Ty = A;
+// }
+
+#[thrust_macros::requires(T::p(*a, !a, x))]
+#[thrust_macros::ensures(T::p(*a, !a, result))]
+fn target<T: A>(a: &mut T, x: i64) -> i64 {
+    let mut v = x;
+    let mut i = 0;
+    while i < 3 {
+        v = a.f(v);
+        i += 1;
+    }
+
+    v
+}
+
+fn main() {}
diff --git a/tests/ui/pass/traits/two_loops.rs b/tests/ui/pass/traits/two_loops.rs
new file mode 100644
index 00000000..198354b1
--- /dev/null
+++ b/tests/ui/pass/traits/two_loops.rs
@@ -0,0 +1,40 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60
+
+#[thrust_macros::context]
+trait A {
+    #[thrust_macros::requires(true)]
+    #[thrust_macros::ensures(Self::p(*result))]
+    fn f(&self) -> &Self;
+    #[thrust_macros::requires(Self::q(*self))]
+    #[thrust_macros::ensures(Self::q(*result))]
+    fn g(&self) -> &Self;
+
+    #[thrust_macros::predicate]
+    fn p(self) -> bool;
+    #[thrust_macros::predicate]
+    fn q(self) -> bool;
+}
+
+#[thrust_macros::requires(T::q(*y))]
+#[thrust_macros::ensures(T::p(*result.0) && T::q(*result.1))]
+fn target<'a, T: A>(x: &'a T, y: &'a T) -> (&'a T, &'a T) {
+    let mut v = x;
+    let mut w = y;
+    let mut i = 0;
+    while i < 3 { // The loop depends on P
+        v = v.f();
+        i += 1;
+    }
+
+    let mut j = 0;
+    while j < 3 { // The loop depends on Q
+        w = w.g();
+        j += 1;
+    }
+
+    (v, w)
+}
+
+fn main() {}