From 6cf229dfececebd3ec3d8a494a87b35f49cb5a6a Mon Sep 17 00:00:00 2001 From: coord_e Date: Sat, 28 Mar 2026 23:22:59 +0900 Subject: [PATCH 1/3] Use Model trait to map logical model with Rust types --- src/analyze.rs | 12 +- src/analyze/annot.rs | 40 ++++ src/analyze/basic_block.rs | 2 +- src/analyze/did_cache.rs | 68 ++++++- src/analyze/local_def.rs | 2 +- src/refine/template.rs | 126 ++++++++---- std.rs | 185 +++++++++++++----- tests/ui/fail/adt_mut.rs | 4 + tests/ui/fail/annot_preds_trait.rs | 4 + tests/ui/fail/annot_preds_trait_multi.rs | 8 + tests/ui/fail/iterators/annot_range_loop.rs | 4 + tests/ui/fail/iterators/annot_range_next.rs | 4 + .../fail/iterators/fixed_filter_loop_none.rs | 8 + .../fail/iterators/fixed_filter_next_some.rs | 8 + tests/ui/fail/iterators/range.rs | 4 + tests/ui/fail/list_length_const.rs | 4 + tests/ui/fail/list_sum_const.rs | 4 + tests/ui/pass/adt_mut.rs | 4 + tests/ui/pass/annot_preds_trait.rs | 4 + tests/ui/pass/annot_preds_trait_multi.rs | 8 + tests/ui/pass/iterators/annot_range_loop.rs | 4 + tests/ui/pass/iterators/annot_range_next.rs | 4 + .../pass/iterators/fixed_filter_loop_none.rs | 8 + .../pass/iterators/fixed_filter_next_some.rs | 8 + tests/ui/pass/iterators/range.rs | 4 + tests/ui/pass/list_length_const.rs | 4 + tests/ui/pass/list_sum_const.rs | 4 + 27 files changed, 452 insertions(+), 87 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index 46b3f3d..b9203f2 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -29,6 +29,9 @@ mod crate_; mod did_cache; mod local_def; +// TODO: organize structure and remove cross dependency between refine +pub use did_cache::DefIdCache; + pub fn local_of_function_param(idx: rty::FunctionParamIdx) -> Local { Local::from(idx.index() + 1) } @@ -209,6 +212,11 @@ impl<'tcx> Analyzer<'tcx> { } } + pub fn def_ids(&self) -> did_cache::DefIdCache<'tcx> { + // DefIdCache is backed by Rc + self.def_ids.clone() + } + pub fn add_clause(&mut self, clause: chc::Clause) { self.system.borrow_mut().push_clause(clause); } @@ -234,7 +242,7 @@ impl<'tcx> Analyzer<'tcx> { .iter() .map(|field| { let field_ty = self.tcx.type_of(field.did).instantiate_identity(); - TypeBuilder::new(self.tcx, def_id).build(field_ty) + TypeBuilder::new(self.tcx, self.def_ids(), def_id).build(field_ty) }) .collect(); rty::EnumVariantDef { @@ -355,7 +363,7 @@ impl<'tcx> Analyzer<'tcx> { def_id: DefId, generic_args: mir_ty::GenericArgsRef<'tcx>, ) -> Option { - let type_builder = TypeBuilder::new(self.tcx, def_id); + let type_builder = TypeBuilder::new(self.tcx, self.def_ids(), def_id); let deferred_ty = match self.defs.get(&def_id)? { DefTy::Concrete(rty) => { diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 649b549..745191e 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -49,6 +49,46 @@ pub fn ignored_path() -> [Symbol; 2] { [Symbol::intern("thrust"), Symbol::intern("ignored")] } +pub fn model_ty_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("model_ty"), + ] +} + +pub fn int_model_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("int_model"), + ] +} + +pub fn mut_model_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("mut_model"), + ] +} + +pub fn box_model_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("box_model"), + ] +} + +pub fn array_model_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("array_model"), + ] +} + /// A [`annot::Resolver`] implementation for resolving function parameters. /// /// The parameter names and their sorts needs to be configured via diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index f31e320..29b086d 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -1116,7 +1116,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, local_def_id.to_def_id()); + let type_builder = TypeBuilder::new(tcx, ctx.def_ids(), local_def_id.to_def_id()); Self { ctx, tcx, diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index efeea6b..cdae6b8 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -1,15 +1,23 @@ //! Retrieves and caches well-known [`DefId`]s. use std::cell::OnceCell; +use std::rc::Rc; use rustc_middle::ty::TyCtxt; use rustc_span::def_id::DefId; +use rustc_span::symbol::Symbol; use rustc_target::abi::FieldIdx; #[derive(Debug, Clone, Default)] struct DefIds { unique: OnceCell>, nonnull: OnceCell>, + + model_ty: OnceCell>, + int_model: OnceCell>, + mut_model: OnceCell>, + box_model: OnceCell>, + array_model: OnceCell>, } /// Retrieves and caches well-known [`DefId`]s. @@ -19,14 +27,14 @@ struct DefIds { #[derive(Clone)] pub struct DefIdCache<'tcx> { tcx: TyCtxt<'tcx>, - def_ids: DefIds, + def_ids: Rc, } impl<'tcx> DefIdCache<'tcx> { pub fn new(tcx: TyCtxt<'tcx>) -> Self { Self { tcx, - def_ids: DefIds::default(), + def_ids: Rc::new(DefIds::default()), } } @@ -63,4 +71,60 @@ impl<'tcx> DefIdCache<'tcx> { Some(nonnull_def.did()) }) } + + fn annotated_def(&self, path: &[Symbol]) -> Option { + let map = self.tcx.hir(); + for item_id in map.items() { + let def_id = item_id.owner_id.to_def_id(); + if self.tcx.get_attrs_by_path(def_id, path).next().is_some() { + return Some(def_id); + } + + let item = map.item(item_id); + if let rustc_hir::ItemKind::Trait(_, _, _, _, trait_item_refs) = item.kind { + for trait_item_ref in trait_item_refs { + let def_id = trait_item_ref.id.owner_id.to_def_id(); + if self.tcx.get_attrs_by_path(def_id, path).next().is_some() { + return Some(def_id); + } + } + } + } + None + } + + pub fn model_ty(&self) -> Option { + *self + .def_ids + .model_ty + .get_or_init(|| self.annotated_def(&crate::analyze::annot::model_ty_path())) + } + + pub fn int_model(&self) -> Option { + *self + .def_ids + .int_model + .get_or_init(|| self.annotated_def(&crate::analyze::annot::int_model_path())) + } + + pub fn mut_model(&self) -> Option { + *self + .def_ids + .mut_model + .get_or_init(|| self.annotated_def(&crate::analyze::annot::mut_model_path())) + } + + pub fn box_model(&self) -> Option { + *self + .def_ids + .box_model + .get_or_init(|| self.annotated_def(&crate::analyze::annot::box_model_path())) + } + + pub fn array_model(&self) -> Option { + *self + .def_ids + .array_model + .get_or_init(|| self.annotated_def(&crate::analyze::annot::array_model_path())) + } } diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 59151bf..a76823d 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -842,7 +842,7 @@ 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, local_def_id.to_def_id()); + let type_builder = TypeBuilder::new(tcx, ctx.def_ids(), local_def_id.to_def_id()); Self { ctx, tcx, diff --git a/src/refine/template.rs b/src/refine/template.rs index 6d3b5dd..7bcd22b 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -6,6 +6,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::chc; use crate::refine; use crate::rty; @@ -69,6 +70,8 @@ where #[derive(Clone)] pub struct TypeBuilder<'tcx> { tcx: mir_ty::TyCtxt<'tcx>, + def_ids: DefIdCache<'tcx>, + param_env: mir_ty::ParamEnv<'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`]. @@ -77,7 +80,7 @@ pub struct TypeBuilder<'tcx> { } impl<'tcx> TypeBuilder<'tcx> { - pub fn new(tcx: mir_ty::TyCtxt<'tcx>, def_id: DefId) -> Self { + pub fn new(tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, def_id: DefId) -> Self { let generics = tcx.generics_of(def_id); let mut param_idx_mapping: HashMap = Default::default(); for i in 0..generics.count() { @@ -90,8 +93,11 @@ impl<'tcx> TypeBuilder<'tcx> { mir_ty::GenericParamDefKind::Const { .. } => {} } } + let param_env = tcx.param_env_reveal_all_normalized(def_id); Self { tcx, + def_ids, + param_env, param_idx_mapping, } } @@ -104,18 +110,59 @@ impl<'tcx> TypeBuilder<'tcx> { rty::ParamType::new(index).into() } + fn resolve_model_ty(&self, ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> { + let Some(model_ty_def_id) = self.def_ids.model_ty() else { + return ty; + }; + let args = self.tcx.mk_args(&[ty.into()]); + 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.param_env, projection_ty) + { + return normalized_ty; + } + ty + } + + // TODO: consolidate two impls + fn model_adt( + &self, + adt: &mir_ty::AdtDef<'tcx>, + args: &'tcx mir_ty::List>, + ) -> Option> { + if Some(adt.did()) == self.def_ids.int_model() { + return Some(rty::Type::int()); + } + + if Some(adt.did()) == self.def_ids.mut_model() { + let elem_ty = self.build(args.type_at(0)); + return Some(rty::PointerType::mut_to(elem_ty).into()); + } + + if Some(adt.did()) == self.def_ids.box_model() { + let elem_ty = self.build(args.type_at(0)); + return Some(rty::PointerType::own(elem_ty).into()); + } + + if Some(adt.did()) == self.def_ids.array_model() { + let idx_ty = self.build(args.type_at(0)); + let elem_ty = self.build(args.type_at(1)); + return Some(rty::ArrayType::new(idx_ty, elem_ty).into()); + } + + None + } + // TODO: consolidate two impls pub fn build(&self, ty: mir_ty::Ty<'tcx>) -> rty::Type { + let ty = self.resolve_model_ty(ty); match ty.kind() { mir_ty::TyKind::Bool => rty::Type::bool(), - mir_ty::TyKind::Uint(_) | mir_ty::TyKind::Int(_) => rty::Type::int(), mir_ty::TyKind::Str => rty::Type::string(), - mir_ty::TyKind::Ref(_, elem_ty, mutbl) => { + mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Not) => { let elem_ty = self.build(*elem_ty); - match mutbl { - mir_ty::Mutability::Mut => rty::PointerType::mut_to(elem_ty).into(), - mir_ty::Mutability::Not => rty::PointerType::immut_to(elem_ty).into(), - } + rty::PointerType::immut_to(elem_ty).into() } mir_ty::TyKind::Tuple(ts) => { // elaboration: all fields are boxed @@ -138,17 +185,10 @@ impl<'tcx> TypeBuilder<'tcx> { let ret = rty::RefinedType::unrefined(self.build(sig.output())); rty::FunctionType::new(params, ret.vacuous()).into() } - mir_ty::TyKind::Adt(def, params) if def.is_box() => { - rty::PointerType::own(self.build(params.type_at(0))).into() - } - // TODO: Declare this in std.rs - mir_ty::TyKind::Adt(def, params) - if self.tcx.is_diagnostic_item(rustc_span::sym::Vec, def.did()) => - { - let content = rty::ArrayType::new(rty::Type::Int, self.build(params.type_at(0))); - rty::TupleType::new(vec![content.into(), rty::Type::Int]).into() - } mir_ty::TyKind::Adt(def, params) => { + if let Some(model_ty) = self.model_adt(def, params) { + return model_ty; + } if def.is_enum() { let sym = refine::datatype_symbol(self.tcx, def.did()); let args: IndexVec<_, _> = params @@ -245,17 +285,42 @@ where R: TemplateRegistry, S: TemplateScope, { + fn model_adt( + &mut self, + adt: &mir_ty::AdtDef<'tcx>, + args: &'tcx mir_ty::List>, + ) -> Option> { + if Some(adt.did()) == self.inner.def_ids.int_model() { + return Some(rty::Type::int()); + } + + if Some(adt.did()) == self.inner.def_ids.mut_model() { + let elem_ty = self.build(args.type_at(0)); + return Some(rty::PointerType::mut_to(elem_ty).into()); + } + + if Some(adt.did()) == self.inner.def_ids.box_model() { + let elem_ty = self.build(args.type_at(0)); + return Some(rty::PointerType::own(elem_ty).into()); + } + + if Some(adt.did()) == self.inner.def_ids.array_model() { + let idx_ty = self.build(args.type_at(0)); + let elem_ty = self.build(args.type_at(1)); + return Some(rty::ArrayType::new(idx_ty, elem_ty).into()); + } + + None + } + pub fn build(&mut self, ty: mir_ty::Ty<'tcx>) -> rty::Type { + let ty = self.inner.resolve_model_ty(ty); match ty.kind() { mir_ty::TyKind::Bool => rty::Type::bool(), - mir_ty::TyKind::Uint(_) | mir_ty::TyKind::Int(_) => rty::Type::int(), mir_ty::TyKind::Str => rty::Type::string(), - mir_ty::TyKind::Ref(_, elem_ty, mutbl) => { + mir_ty::TyKind::Ref(_, elem_ty, mir_ty::Mutability::Not) => { let elem_ty = self.build(*elem_ty); - match mutbl { - mir_ty::Mutability::Mut => rty::PointerType::mut_to(elem_ty).into(), - mir_ty::Mutability::Not => rty::PointerType::immut_to(elem_ty).into(), - } + rty::PointerType::immut_to(elem_ty).into() } mir_ty::TyKind::Tuple(ts) => { // elaboration: all fields are boxed @@ -273,19 +338,10 @@ where let ty = self.inner.for_function_template(self.registry, sig).build(); rty::Type::function(ty) } - mir_ty::TyKind::Adt(def, params) if def.is_box() => { - rty::PointerType::own(self.build(params.type_at(0))).into() - } - mir_ty::TyKind::Adt(def, params) - if self - .inner - .tcx - .is_diagnostic_item(rustc_span::sym::Vec, def.did()) => - { - let content = rty::ArrayType::new(rty::Type::Int, self.build(params.type_at(0))); - rty::TupleType::new(vec![content.into(), rty::Type::Int]).into() - } mir_ty::TyKind::Adt(def, params) => { + if let Some(model_ty) = self.model_adt(def, params) { + return model_ty; + } if def.is_enum() { let sym = refine::datatype_symbol(self.inner.tcx, def.did()); let args: IndexVec<_, _> = diff --git a/std.rs b/std.rs index d823a4a..71b7a73 100644 --- a/std.rs +++ b/std.rs @@ -1,30 +1,123 @@ // This file is injected to source code by Thrust +mod thrust_models { + pub trait Model { + #[thrust::def::model_ty] + type Ty; + } + + pub mod model { + use std::marker::PhantomData; + + #[thrust::def::int_model] + pub struct Int; + + #[thrust::def::mut_model] + pub struct Mut(PhantomData); + + #[thrust::def::box_model] + pub struct Box(PhantomData); + + #[thrust::def::array_model] + pub struct Array(PhantomData, PhantomData); + + pub struct Vec(pub Array, pub usize); + } + + impl Model for isize { + type Ty = model::Int; + } + + impl Model for i32 { + type Ty = model::Int; + } + + impl Model for i64 { + type Ty = model::Int; + } + + impl Model for usize { + type Ty = model::Int; + } + + impl Model for u32 { + type Ty = model::Int; + } + + impl Model for u64 { + type Ty = model::Int; + } + + impl Model for bool { + type Ty = bool; + } + + impl Model for () { + type Ty = (); + } + + impl Model for (T0,) where T0: Model { + type Ty = (::Ty,); + } + + impl Model for (T0, T1) where T0: Model, T1: Model { + type Ty = (::Ty, ::Ty); + } + + impl Model for (T0, T1, T2) where T0: Model, T1: Model, T2: Model { + type Ty = (::Ty, ::Ty, ::Ty); + } + + impl<'a, T> Model for &'a mut T where T: Model { + type Ty = model::Mut<::Ty>; + } + + impl<'a, T> Model for &'a T where T: Model { + type Ty = &'a ::Ty; + } + + impl Model for Box where T: Model { + type Ty = model::Box<::Ty>; + } + + impl Model for Vec where T: Model { + type Ty = model::Vec<::Ty>; + } + + impl Model for Option where T: Model { + type Ty = Option<::Ty>; + } + + impl Model for Result where T: Model, E: Model { + type Ty = Result<::Ty, ::Ty>; + } +} + #[thrust::extern_spec_fn] #[thrust::requires(true)] #[thrust::ensures(result == )] -fn _extern_spec_box_new(x: T) -> Box { +fn _extern_spec_box_new(x: T) -> Box where T: thrust_models::Model { Box::new(x) } #[thrust::extern_spec_fn] #[thrust::requires(true)] #[thrust::ensures(*x == ^y && *y == ^x)] -fn _extern_spec_std_mem_swap(x: &mut T, y: &mut T) { +fn _extern_spec_std_mem_swap(x: &mut T, y: &mut T) where T: thrust_models::Model { std::mem::swap(x, y); } #[thrust::extern_spec_fn] #[thrust::requires(true)] #[thrust::ensures(^dest == src && result == *dest)] -fn _extern_spec_std_mem_replace(dest: &mut T, src: T) -> T { +fn _extern_spec_std_mem_replace(dest: &mut T, src: T) -> T where T: thrust_models::Model { std::mem::replace(dest, src) } #[thrust::extern_spec_fn] #[thrust::requires(opt != std::option::Option::::None())] #[thrust::ensures(std::option::Option::::Some(result) == opt)] -fn _extern_spec_option_unwrap(opt: Option) -> T { +fn _extern_spec_option_unwrap(opt: Option) -> T where T: thrust_models::Model { Option::unwrap(opt) } @@ -34,7 +127,7 @@ fn _extern_spec_option_unwrap(opt: Option) -> T { (*opt == std::option::Option::::None() && result == true) || (*opt != std::option::Option::::None() && result == false) )] -fn _extern_spec_option_is_none(opt: &Option) -> bool { +fn _extern_spec_option_is_none(opt: &Option) -> bool where T: thrust_models::Model { Option::is_none(opt) } @@ -44,7 +137,7 @@ fn _extern_spec_option_is_none(opt: &Option) -> bool { (*opt == std::option::Option::::None() && result == false) || (*opt != std::option::Option::::None() && result == true) )] -fn _extern_spec_option_is_some(opt: &Option) -> bool { +fn _extern_spec_option_is_some(opt: &Option) -> bool where T: thrust_models::Model { Option::is_some(opt) } @@ -54,7 +147,7 @@ fn _extern_spec_option_is_some(opt: &Option) -> bool { (opt != std::option::Option::::None() && std::option::Option::::Some(result) == opt) || (opt == std::option::Option::::None() && result == default) )] -fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T { +fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T where T: thrust_models::Model { Option::unwrap_or(opt, default) } @@ -64,21 +157,21 @@ fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T { (exists x:T0. opt == std::option::Option::::Some(x) && result == std::result::Result::::Ok(x)) || (opt == std::option::Option::::None() && result == std::result::Result::::Err(err)) )] -fn _extern_spec_option_ok_or(opt: Option, err: E) -> Result { +fn _extern_spec_option_ok_or(opt: Option, err: E) -> Result where T: thrust_models::Model, E: thrust_models::Model { Option::ok_or(opt, err) } #[thrust::extern_spec_fn] #[thrust::requires(true)] #[thrust::ensures(^opt == std::option::Option::::None() && result == *opt)] -fn _extern_spec_option_take(opt: &mut Option) -> Option { +fn _extern_spec_option_take(opt: &mut Option) -> Option where T: thrust_models::Model { Option::take(opt) } #[thrust::extern_spec_fn] #[thrust::requires(true)] #[thrust::ensures(^opt == std::option::Option::::Some(src) && result == *opt)] -fn _extern_spec_option_replace(opt: &mut Option, src: T) -> Option { +fn _extern_spec_option_replace(opt: &mut Option, src: T) -> Option where T: thrust_models::Model { Option::replace(opt, src) } @@ -88,7 +181,7 @@ fn _extern_spec_option_replace(opt: &mut Option, src: T) -> Option { (exists x:T0. opt == ::Some(x)> && result == std::option::Option::<&T0>::Some()) || (opt == ::None()> && result == std::option::Option::<&T0>::None()) )] -fn _extern_spec_option_as_ref(opt: &Option) -> Option<&T> { +fn _extern_spec_option_as_ref(opt: &Option) -> Option<&T> where T: thrust_models::Model { Option::as_ref(opt) } @@ -106,21 +199,21 @@ fn _extern_spec_option_as_ref(opt: &Option) -> Option<&T> { result == std::option::Option::<&mut T0>::None() ) )] -fn _extern_spec_option_as_mut(opt: &mut Option) -> Option<&mut T> { +fn _extern_spec_option_as_mut(opt: &mut Option) -> Option<&mut T> where T: thrust_models::Model { Option::as_mut(opt) } #[thrust::extern_spec_fn] #[thrust::requires(exists x:T0. res == std::result::Result::::Ok(x))] #[thrust::ensures(std::result::Result::::Ok(result) == res)] -fn _extern_spec_result_unwrap(res: Result) -> T { +fn _extern_spec_result_unwrap(res: Result) -> T where T: thrust_models::Model { Result::unwrap(res) } #[thrust::extern_spec_fn] #[thrust::requires(exists x:T1. res == std::result::Result::::Err(x))] #[thrust::ensures(std::result::Result::::Err(result) == res)] -fn _extern_spec_result_unwrap_err(res: Result) -> E { +fn _extern_spec_result_unwrap_err(res: Result) -> E where T: thrust_models::Model, E: thrust_models::Model { Result::unwrap_err(res) } @@ -130,7 +223,7 @@ fn _extern_spec_result_unwrap_err(res: Result) -> E (exists x:T0. res == std::result::Result::::Ok(x) && result == std::option::Option::::Some(x)) || (exists x:T1. res == std::result::Result::::Err(x) && result == std::option::Option::::None()) )] -fn _extern_spec_result_ok(res: Result) -> Option { +fn _extern_spec_result_ok(res: Result) -> Option where T: thrust_models::Model, E: thrust_models::Model { Result::ok(res) } @@ -140,7 +233,7 @@ fn _extern_spec_result_ok(res: Result) -> Option { (exists x:T0. res == std::result::Result::::Ok(x) && result == std::option::Option::::None()) || (exists x:T1. res == std::result::Result::::Err(x) && result == std::option::Option::::Some(x)) )] -fn _extern_spec_result_err(res: Result) -> Option { +fn _extern_spec_result_err(res: Result) -> Option where T: thrust_models::Model, E: thrust_models::Model { Result::err(res) } @@ -150,7 +243,7 @@ fn _extern_spec_result_err(res: Result) -> Option { (exists x:T0. *res == std::result::Result::::Ok(x) && result == true) || (exists x:T1. *res == std::result::Result::::Err(x) && result == false) )] -fn _extern_spec_result_is_ok(res: &Result) -> bool { +fn _extern_spec_result_is_ok(res: &Result) -> bool where T: thrust_models::Model, E: thrust_models::Model { Result::is_ok(res) } @@ -160,7 +253,7 @@ fn _extern_spec_result_is_ok(res: &Result) -> bool { (exists x:T0. *res == std::result::Result::::Ok(x) && result == false) || (exists x:T1. *res == std::result::Result::::Err(x) && result == true) )] -fn _extern_spec_result_is_err(res: &Result) -> bool { +fn _extern_spec_result_is_err(res: &Result) -> bool where T: thrust_models::Model, E: thrust_models::Model { Result::is_err(res) } @@ -204,47 +297,47 @@ fn _extern_spec_i32_is_negative(x: i32) -> bool { #[thrust::extern_spec_fn] #[thrust::requires(true)] -#[thrust::ensures(result.1 == 0)] -fn _extern_spec_vec_new() -> Vec { +#[thrust::ensures(*result.1 == 0)] +fn _extern_spec_vec_new() -> Vec where T: thrust_models::Model { Vec::::new() } #[thrust::extern_spec_fn] #[thrust::requires(true)] -#[thrust::ensures(^vec == ((*vec).0.store((*vec).1, elem), (*vec).1 + 1))] -fn _extern_spec_vec_push(vec: &mut Vec, elem: T) { +#[thrust::ensures(^vec == ((*(*vec).0).store(*(*vec).1, elem), *(*vec).1 + 1))] +fn _extern_spec_vec_push(vec: &mut Vec, elem: T) where T: thrust_models::Model { Vec::push(vec, elem) } #[thrust::extern_spec_fn] #[thrust::requires(true)] -#[thrust::ensures(result == (*vec).1)] -fn _extern_spec_vec_len(vec: &Vec) -> usize { +#[thrust::ensures(result == *(*vec).1)] +fn _extern_spec_vec_len(vec: &Vec) -> usize where T: thrust_models::Model { Vec::len(vec) } #[thrust::extern_spec_fn] -#[thrust::requires(index < (*vec).1)] -#[thrust::ensures(*result == (*vec).0.select(index))] -fn _extern_spec_vec_index(vec: &Vec, index: usize) -> &T { +#[thrust::requires(index < *(*vec).1)] +#[thrust::ensures(*result == (*(*vec).0).select(index))] +fn _extern_spec_vec_index(vec: &Vec, index: usize) -> &T where T: thrust_models::Model { as std::ops::Index>::index(vec, index) } #[thrust::extern_spec_fn] -#[thrust::requires(index < (*vec).1)] +#[thrust::requires(index < *(*vec).1)] #[thrust::ensures( - *result == (*vec).0.select(index) && - ^result == (^vec).0.select(index) && - ^vec == ((*vec).0.store(index, ^result), (*vec).1) + *result == (*(*vec).0).select(index) && + ^result == (*(^vec).0).select(index) && + ^vec == (<(*(*vec).0).store(index, ^result)>, (*vec).1) )] -fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T { +fn _extern_spec_vec_index_mut(vec: &mut Vec, index: usize) -> &mut T where T: thrust_models::Model { as std::ops::IndexMut>::index_mut(vec, index) } #[thrust::extern_spec_fn] #[thrust::requires(true)] -#[thrust::ensures((^vec).1 == 0)] -fn _extern_spec_vec_clear(vec: &mut Vec) { +#[thrust::ensures(*(^vec).1 == 0)] +fn _extern_spec_vec_clear(vec: &mut Vec) where T: thrust_models::Model { Vec::clear(vec) } @@ -253,24 +346,24 @@ fn _extern_spec_vec_clear(vec: &mut Vec) { #[thrust::ensures( (^vec).0 == (*vec).0 && ( ( - (*vec).1 > 0 && - (^vec).1 == (*vec).1 - 1 && - result == std::option::Option::::Some((*vec).0.select((*vec).1 - 1)) + *(*vec).1 > 0 && + *(^vec).1 == *(*vec).1 - 1 && + result == std::option::Option::::Some((*(*vec).0).select(*(*vec).1 - 1)) ) || ( - (*vec).1 == 0 && - (^vec).1 == 0 && + *(*vec).1 == 0 && + *(^vec).1 == 0 && result == std::option::Option::::None() ) ) )] -fn _extern_spec_vec_pop(vec: &mut Vec) -> Option { +fn _extern_spec_vec_pop(vec: &mut Vec) -> Option where T: thrust_models::Model { Vec::pop(vec) } #[thrust::extern_spec_fn] #[thrust::requires(true)] -#[thrust::ensures(result == ((*vec).1 == 0))] -fn _extern_spec_vec_is_empty(vec: &Vec) -> bool { +#[thrust::ensures(result == (*(*vec).1 == 0))] +fn _extern_spec_vec_is_empty(vec: &Vec) -> bool where T: thrust_models::Model { Vec::is_empty(vec) } @@ -278,13 +371,13 @@ fn _extern_spec_vec_is_empty(vec: &Vec) -> bool { #[thrust::requires(true)] #[thrust::ensures( ( - (*vec).1 > len && - ^vec == ((*vec).0, len) + *(*vec).1 > len && + ^vec == (<(*vec).0>, ) ) || ( - (*vec).1 <= len && + *(*vec).1 <= len && ^vec == *vec ) )] -fn _extern_spec_vec_truncate(vec: &mut Vec, len: usize) { +fn _extern_spec_vec_truncate(vec: &mut Vec, len: usize) where T: thrust_models::Model { Vec::truncate(vec, len) } diff --git a/tests/ui/fail/adt_mut.rs b/tests/ui/fail/adt_mut.rs index d3347dd..8b8b8c5 100644 --- a/tests/ui/fail/adt_mut.rs +++ b/tests/ui/fail/adt_mut.rs @@ -6,6 +6,10 @@ pub enum X { B(bool), } +impl thrust_models::Model for X { + type Ty = Self; +} + #[thrust::trusted] #[thrust::requires(true)] #[thrust::ensures(true)] diff --git a/tests/ui/fail/annot_preds_trait.rs b/tests/ui/fail/annot_preds_trait.rs index bd0bdbc..f3b0a2c 100644 --- a/tests/ui/fail/annot_preds_trait.rs +++ b/tests/ui/fail/annot_preds_trait.rs @@ -6,6 +6,10 @@ struct A { x: i64, } +impl thrust_models::Model for A { + type Ty = Self; +} + trait Double { // Support annotations in trait definitions #[thrust::predicate] diff --git a/tests/ui/fail/annot_preds_trait_multi.rs b/tests/ui/fail/annot_preds_trait_multi.rs index a277358..713f3e2 100644 --- a/tests/ui/fail/annot_preds_trait_multi.rs +++ b/tests/ui/fail/annot_preds_trait_multi.rs @@ -17,6 +17,10 @@ struct A { x: i64, } +impl thrust_models::Model for A { + type Ty = Self; +} + impl Double for A { #[thrust::predicate] fn is_double(self, doubled: Self) -> bool { @@ -38,6 +42,10 @@ struct B { y: i64, } +impl thrust_models::Model for B { + type Ty = Self; +} + impl Double for B { #[thrust::predicate] fn is_double(self, doubled: Self) -> bool { diff --git a/tests/ui/fail/iterators/annot_range_loop.rs b/tests/ui/fail/iterators/annot_range_loop.rs index 6edf6d7..b65be43 100644 --- a/tests/ui/fail/iterators/annot_range_loop.rs +++ b/tests/ui/fail/iterators/annot_range_loop.rs @@ -23,6 +23,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; diff --git a/tests/ui/fail/iterators/annot_range_next.rs b/tests/ui/fail/iterators/annot_range_next.rs index e2aa0d6..1143c1b 100644 --- a/tests/ui/fail/iterators/annot_range_next.rs +++ b/tests/ui/fail/iterators/annot_range_next.rs @@ -23,6 +23,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; diff --git a/tests/ui/fail/iterators/fixed_filter_loop_none.rs b/tests/ui/fail/iterators/fixed_filter_loop_none.rs index a0438eb..2c213c5 100644 --- a/tests/ui/fail/iterators/fixed_filter_loop_none.rs +++ b/tests/ui/fail/iterators/fixed_filter_loop_none.rs @@ -6,6 +6,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; @@ -24,6 +28,10 @@ struct FixedFilter { iter: Range, } +impl thrust_models::Model for FixedFilter { + type Ty = FixedFilter; +} + impl Iterator for FixedFilter { type Item = ::Item; diff --git a/tests/ui/fail/iterators/fixed_filter_next_some.rs b/tests/ui/fail/iterators/fixed_filter_next_some.rs index 6579fb0..7f3f16c 100644 --- a/tests/ui/fail/iterators/fixed_filter_next_some.rs +++ b/tests/ui/fail/iterators/fixed_filter_next_some.rs @@ -6,6 +6,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; @@ -24,6 +28,10 @@ struct FixedFilter { iter: Range, } +impl thrust_models::Model for FixedFilter { + type Ty = FixedFilter; +} + impl Iterator for FixedFilter { type Item = ::Item; diff --git a/tests/ui/fail/iterators/range.rs b/tests/ui/fail/iterators/range.rs index 55fae4e..0199ef0 100644 --- a/tests/ui/fail/iterators/range.rs +++ b/tests/ui/fail/iterators/range.rs @@ -6,6 +6,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; diff --git a/tests/ui/fail/list_length_const.rs b/tests/ui/fail/list_length_const.rs index a182df4..dfdbbd4 100644 --- a/tests/ui/fail/list_length_const.rs +++ b/tests/ui/fail/list_length_const.rs @@ -7,6 +7,10 @@ enum List { Nil, } +impl thrust_models::Model for List { + type Ty = Self; +} + fn length(la: &List) -> i32 { match la { List::Cons(_, lb) => length(lb) + 1, diff --git a/tests/ui/fail/list_sum_const.rs b/tests/ui/fail/list_sum_const.rs index 2035c0c..751a5fb 100644 --- a/tests/ui/fail/list_sum_const.rs +++ b/tests/ui/fail/list_sum_const.rs @@ -7,6 +7,10 @@ enum List { Nil, } +impl thrust_models::Model for List { + type Ty = Self; +} + fn sum(la: &List) -> i32 { match la { List::Cons(x, lb) => sum(lb) + *x, diff --git a/tests/ui/pass/adt_mut.rs b/tests/ui/pass/adt_mut.rs index bd74b6c..f20a151 100644 --- a/tests/ui/pass/adt_mut.rs +++ b/tests/ui/pass/adt_mut.rs @@ -6,6 +6,10 @@ pub enum X { B(bool), } +impl thrust_models::Model for X { + type Ty = Self; +} + #[thrust::trusted] #[thrust::requires(true)] #[thrust::ensures(true)] diff --git a/tests/ui/pass/annot_preds_trait.rs b/tests/ui/pass/annot_preds_trait.rs index bb2e37c..b16b5e8 100644 --- a/tests/ui/pass/annot_preds_trait.rs +++ b/tests/ui/pass/annot_preds_trait.rs @@ -6,6 +6,10 @@ struct A { x: i64, } +impl thrust_models::Model for A { + type Ty = Self; +} + trait Double { // Support annotations in trait definitions #[thrust::predicate] diff --git a/tests/ui/pass/annot_preds_trait_multi.rs b/tests/ui/pass/annot_preds_trait_multi.rs index a51ff84..9467b16 100644 --- a/tests/ui/pass/annot_preds_trait_multi.rs +++ b/tests/ui/pass/annot_preds_trait_multi.rs @@ -17,6 +17,10 @@ struct A { x: i64, } +impl thrust_models::Model for A { + type Ty = Self; +} + impl Double for A { #[thrust::predicate] fn is_double(self, doubled: Self) -> bool { @@ -38,6 +42,10 @@ struct B { y: i64, } +impl thrust_models::Model for B { + type Ty = Self; +} + impl Double for B { #[thrust::predicate] fn is_double(self, doubled: Self) -> bool { diff --git a/tests/ui/pass/iterators/annot_range_loop.rs b/tests/ui/pass/iterators/annot_range_loop.rs index 823553a..dd798ad 100644 --- a/tests/ui/pass/iterators/annot_range_loop.rs +++ b/tests/ui/pass/iterators/annot_range_loop.rs @@ -23,6 +23,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; diff --git a/tests/ui/pass/iterators/annot_range_next.rs b/tests/ui/pass/iterators/annot_range_next.rs index ec474f5..6cafdd3 100644 --- a/tests/ui/pass/iterators/annot_range_next.rs +++ b/tests/ui/pass/iterators/annot_range_next.rs @@ -23,6 +23,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; diff --git a/tests/ui/pass/iterators/fixed_filter_loop_none.rs b/tests/ui/pass/iterators/fixed_filter_loop_none.rs index 7db846d..393a1a3 100644 --- a/tests/ui/pass/iterators/fixed_filter_loop_none.rs +++ b/tests/ui/pass/iterators/fixed_filter_loop_none.rs @@ -6,6 +6,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; @@ -24,6 +28,10 @@ struct FixedFilter { iter: Range, } +impl thrust_models::Model for FixedFilter { + type Ty = FixedFilter; +} + impl Iterator for FixedFilter { type Item = ::Item; diff --git a/tests/ui/pass/iterators/fixed_filter_next_some.rs b/tests/ui/pass/iterators/fixed_filter_next_some.rs index dac7c8b..b7cd3f8 100644 --- a/tests/ui/pass/iterators/fixed_filter_next_some.rs +++ b/tests/ui/pass/iterators/fixed_filter_next_some.rs @@ -6,6 +6,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; @@ -24,6 +28,10 @@ struct FixedFilter { iter: Range, } +impl thrust_models::Model for FixedFilter { + type Ty = FixedFilter; +} + impl Iterator for FixedFilter { type Item = ::Item; diff --git a/tests/ui/pass/iterators/range.rs b/tests/ui/pass/iterators/range.rs index d8ec012..97f3de6 100644 --- a/tests/ui/pass/iterators/range.rs +++ b/tests/ui/pass/iterators/range.rs @@ -6,6 +6,10 @@ struct Range { end: i64, } +impl thrust_models::Model for Range { + type Ty = Range; +} + impl Iterator for Range { type Item = i64; diff --git a/tests/ui/pass/list_length_const.rs b/tests/ui/pass/list_length_const.rs index 2354d21..2e26b8a 100644 --- a/tests/ui/pass/list_length_const.rs +++ b/tests/ui/pass/list_length_const.rs @@ -7,6 +7,10 @@ enum List { Nil, } +impl thrust_models::Model for List { + type Ty = Self; +} + fn length(la: &List) -> i32 { match la { List::Cons(_, lb) => length(lb) + 1, diff --git a/tests/ui/pass/list_sum_const.rs b/tests/ui/pass/list_sum_const.rs index cefdbe0..2d1d460 100644 --- a/tests/ui/pass/list_sum_const.rs +++ b/tests/ui/pass/list_sum_const.rs @@ -7,6 +7,10 @@ enum List { Nil, } +impl thrust_models::Model for List { + type Ty = Self; +} + fn sum(la: &List) -> i32 { match la { List::Cons(x, lb) => sum(lb) + *x, From c77f54c7d4753d5faec7c093dd68403b776cc0e3 Mon Sep 17 00:00:00 2001 From: coord_e Date: Sun, 29 Mar 2026 12:07:28 +0900 Subject: [PATCH 2/3] Workaround Closure model via manually replacing type --- src/analyze/annot.rs | 8 ++++++ src/analyze/did_cache.rs | 8 ++++++ src/refine/template.rs | 57 +++++++++++++++++++++++++++++++++++++--- std.rs | 7 +++++ 4 files changed, 77 insertions(+), 3 deletions(-) diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs index 745191e..c9d80e3 100644 --- a/src/analyze/annot.rs +++ b/src/analyze/annot.rs @@ -89,6 +89,14 @@ pub fn array_model_path() -> [Symbol; 3] { ] } +pub fn closure_model_path() -> [Symbol; 3] { + [ + Symbol::intern("thrust"), + Symbol::intern("def"), + Symbol::intern("closure_model"), + ] +} + /// A [`annot::Resolver`] implementation for resolving function parameters. /// /// The parameter names and their sorts needs to be configured via diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs index cdae6b8..9646be8 100644 --- a/src/analyze/did_cache.rs +++ b/src/analyze/did_cache.rs @@ -18,6 +18,7 @@ struct DefIds { mut_model: OnceCell>, box_model: OnceCell>, array_model: OnceCell>, + closure_model: OnceCell>, } /// Retrieves and caches well-known [`DefId`]s. @@ -127,4 +128,11 @@ impl<'tcx> DefIdCache<'tcx> { .array_model .get_or_init(|| self.annotated_def(&crate::analyze::annot::array_model_path())) } + + pub fn closure_model(&self) -> Option { + *self + .def_ids + .closure_model + .get_or_init(|| self.annotated_def(&crate::analyze::annot::closure_model_path())) + } } diff --git a/src/refine/template.rs b/src/refine/template.rs index 7bcd22b..fceb757 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -110,7 +110,50 @@ impl<'tcx> TypeBuilder<'tcx> { rty::ParamType::new(index).into() } - fn resolve_model_ty(&self, ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> { + /// Replaces {closure} types with thrust_models::Closure<{closure}>. + /// + /// Ideally, we want to have `impl Model for F where F: Fn` instead of this and let + /// normalization do the work. However, it doesn't work: + /// 1. it simply conflicts with other blanket impls + /// 2. attempts to fake the impl via override_queries have failed so far + fn replace_closure_model(&self, ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> { + let Some(closure_model_id) = self.def_ids.closure_model() else { + return ty; + }; + + struct ReplaceClosureModel<'tcx> { + tcx: mir_ty::TyCtxt<'tcx>, + closure_model_id: DefId, + } + + use mir_ty::fold::TypeFoldable; + impl<'tcx> mir_ty::fold::TypeFolder> for ReplaceClosureModel<'tcx> { + fn interner(&self) -> mir_ty::TyCtxt<'tcx> { + self.tcx + } + + fn fold_ty(&mut self, ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> { + use mir_ty::fold::TypeSuperFoldable; + if let mir_ty::TyKind::Closure(_, args) = ty.kind() { + let args = self + .tcx + .mk_args(&[args.as_closure().tupled_upvars_ty().into()]); + let adt_def = self.tcx.adt_def(self.closure_model_id); + return mir_ty::Ty::new_adt(self.tcx, adt_def, args); + } + ty.super_fold_with(self) + } + } + + ty.fold_with(&mut ReplaceClosureModel { + tcx: self.tcx, + closure_model_id, + }) + } + + fn resolve_model_ty(&self, orig_ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> { + let ty = self.replace_closure_model(orig_ty); + let Some(model_ty_def_id) = self.def_ids.model_ty() else { return ty; }; @@ -151,6 +194,11 @@ impl<'tcx> TypeBuilder<'tcx> { return Some(rty::ArrayType::new(idx_ty, elem_ty).into()); } + if Some(adt.did()) == self.def_ids.closure_model() { + let tupled_upvars_ty = args.type_at(0); + return Some(self.build(tupled_upvars_ty)); + } + None } @@ -210,7 +258,6 @@ impl<'tcx> TypeBuilder<'tcx> { unimplemented!("unsupported ADT: {:?}", ty); } } - mir_ty::TyKind::Closure(_, args) => self.build(args.as_closure().tupled_upvars_ty()), kind => unimplemented!("unrefined_ty: {:?}", kind), } } @@ -310,6 +357,11 @@ where return Some(rty::ArrayType::new(idx_ty, elem_ty).into()); } + if Some(adt.did()) == self.inner.def_ids.closure_model() { + let tupled_upvars_ty = args.type_at(0); + return Some(self.build(tupled_upvars_ty)); + } + None } @@ -361,7 +413,6 @@ where unimplemented!("unsupported ADT: {:?}", ty); } } - mir_ty::TyKind::Closure(_, args) => self.build(args.as_closure().tupled_upvars_ty()), kind => unimplemented!("ty: {:?}", kind), } } diff --git a/std.rs b/std.rs index 71b7a73..e3a2b80 100644 --- a/std.rs +++ b/std.rs @@ -21,6 +21,9 @@ mod thrust_models { #[thrust::def::array_model] pub struct Array(PhantomData, PhantomData); + #[thrust::def::closure_model] + pub struct Closure(PhantomData); + pub struct Vec(pub Array, pub usize); } @@ -56,6 +59,10 @@ mod thrust_models { type Ty = (); } + impl Model for model::Closure { + type Ty = model::Closure; + } + impl Model for (T0,) where T0: Model { type Ty = (::Ty,); } From d628b8391d742cb924749f774586b0374568c1c2 Mon Sep 17 00:00:00 2001 From: coord_e Date: Tue, 31 Mar 2026 00:26:13 +0900 Subject: [PATCH 3/3] Impl Model for tuples with 0..10 elems --- std.rs | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/std.rs b/std.rs index e3a2b80..6d60601 100644 --- a/std.rs +++ b/std.rs @@ -55,25 +55,29 @@ mod thrust_models { type Ty = bool; } - impl Model for () { - type Ty = (); - } - impl Model for model::Closure { type Ty = model::Closure; } - impl Model for (T0,) where T0: Model { - type Ty = (::Ty,); + macro_rules! impl_tuple_model { + ($($T:ident),*) => { + impl<$($T),*> Model for ($($T,)*) where $($T: Model),* { + type Ty = ($(<$T as Model>::Ty,)*); + } + }; } - impl Model for (T0, T1) where T0: Model, T1: Model { - type Ty = (::Ty, ::Ty); - } - - impl Model for (T0, T1, T2) where T0: Model, T1: Model, T2: Model { - type Ty = (::Ty, ::Ty, ::Ty); - } + impl_tuple_model!(); + impl_tuple_model!(T0); + impl_tuple_model!(T0, T1); + impl_tuple_model!(T0, T1, T2); + impl_tuple_model!(T0, T1, T2, T3); + impl_tuple_model!(T0, T1, T2, T3, T4); + impl_tuple_model!(T0, T1, T2, T3, T4, T5); + impl_tuple_model!(T0, T1, T2, T3, T4, T5, T6); + impl_tuple_model!(T0, T1, T2, T3, T4, T5, T6, T7); + impl_tuple_model!(T0, T1, T2, T3, T4, T5, T6, T7, T8); + impl_tuple_model!(T0, T1, T2, T3, T4, T5, T6, T7, T8, T9); impl<'a, T> Model for &'a mut T where T: Model { type Ty = model::Mut<::Ty>;