Support ?Sized bounds in lifetime*.rs

(fixes #1104 )

source/rust_verify/src/lifetime_ast.rs

@@ -28,13 +28,18 @@ impl Id {
     pub(crate) fn to_string(&self) -> String {
         crate::lifetime_emit::encode_id(self.kind, self.rename_count, &self.raw_id)
     }
+    pub(crate) fn is_typ_param(&self) -> bool {
+        self.kind == IdKind::TypParam
+    }
 }
 
 pub(crate) type Typ = Box<TypX>;
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub(crate) enum TypX {
     Primitive(String),
     TypParam(Id),
+    // inside trait declarations, Self is special:
+    TraitSelf,
     Never,
     Ref(Typ, Option<Id>, Mutability),
     Phantom(Typ),
@@ -136,6 +141,7 @@ pub(crate) enum ClosureKind {
 pub(crate) enum Bound {
     Copy,
     Clone,
+    Sized,
     Id(Id),
     // use TypX::Datatype to represent Trait bound
     Trait(Typ),

source/rust_verify/src/lifetime_emit.rs

@@ -58,6 +58,7 @@ impl ToString for TypX {
         match self {
             TypX::Primitive(s) => s.clone(),
             TypX::TypParam(id) => id.to_string(),
+            TypX::TraitSelf => "Self".to_string(),
             TypX::Never => "!".to_string(),
             TypX::Ref(t, lifetime, Mutability::Not) => {
                 "&".to_string() + &lifetime_string(lifetime) + &t.to_string()
@@ -702,7 +703,7 @@ fn emit_generic_params(state: &mut EmitState, generics: &Vec<GenericParam>) {
     }
 }
 
-fn emit_generic_bound(bound: &GenericBound, bare: bool) -> String {
+fn emit_generic_bound(bound: &GenericBound, bare: bool, emit_sized: bool) -> String {
     let mut buf = String::new();
     if !bare {
         buf += &bound.typ.to_string();
@@ -723,6 +724,11 @@ fn emit_generic_bound(bound: &GenericBound, bare: bool) -> String {
         Bound::Clone => {
             buf += "Clone";
         }
+        Bound::Sized => {
+            if emit_sized {
+                buf += "Sized";
+            }
+        }
         Bound::Id(x) => {
             buf += &x.to_string();
         }
@@ -743,12 +749,75 @@ fn emit_generic_bound(bound: &GenericBound, bare: bool) -> String {
     buf
 }
 
-fn emit_generic_bounds(state: &mut EmitState, bounds: &Vec<GenericBound>) {
-    if bounds.len() > 0 {
-        state.write(" where ");
-        for bound in bounds.iter() {
-            state.write(emit_generic_bound(bound, false));
-            state.write(", ");
+// Return (bare bounds ": U", where bounds "where ...")
+fn simplify_assoc_typ_bounds(
+    trait_name: &Id,
+    assoc_name: &Id,
+    bounds: Vec<GenericBound>,
+) -> (Vec<GenericBound>, Vec<GenericBound>) {
+    // When rustc sees "trait T { type X: U; }",
+    // it converts it into "trait T { type X where <Self as T>::X: U; }".
+    // However, if we emit "where <Self as T>::X: U" directly,
+    // rustc seems to lose track of the bound, as described in this issue:
+    // https://github.com/rust-lang/rust/issues/113195
+    // Therefore, we need to convert the bound back to the simpler bare "X: U" syntax.
+    // (Also note that "type X: for<'a> U<'a>" becomes "type X where for<'a> <Self as T>::X: U<'a>")
+    let mut bares: Vec<GenericBound> = Vec::new();
+    let mut wheres: Vec<GenericBound> = Vec::new();
+    for bound in bounds {
+        let is_bare = match &*bound.typ {
+            TypX::Projection { self_typ, trait_as_datatype, name } if name == assoc_name => {
+                match (&**self_typ, &**trait_as_datatype) {
+                    (TypX::TraitSelf, TypX::Datatype(id, _, _)) if id == trait_name => true,
+                    _ => false,
+                }
+            }
+            _ => false,
+        };
+        if is_bare {
+            bares.push(bound);
+        } else {
+            wheres.push(bound);
+        }
+    }
+    (bares, wheres)
+}
+
+fn emit_generic_bounds(
+    state: &mut EmitState,
+    params: &Vec<GenericParam>,
+    bounds: &Vec<GenericBound>,
+    emit_sized: bool,
+) {
+    use std::collections::HashSet;
+    let mut printed_where = false;
+    let print_where = |state: &mut EmitState, printed_where: &mut bool| {
+        if !*printed_where {
+            *printed_where = true;
+            state.write(" where ");
+        }
+    };
+    let mut sized: HashSet<Id> = HashSet::new();
+    for bound in bounds.iter() {
+        print_where(state, &mut printed_where);
+        state.write(emit_generic_bound(bound, false, emit_sized));
+        state.write(", ");
+        if !emit_sized && bound.bound == Bound::Sized {
+            if let TypX::TypParam(x) = &*bound.typ {
+                sized.insert(x.clone());
+            }
+        }
+    }
+    if !emit_sized {
+        for param in params {
+            print_where(state, &mut printed_where);
+            if param.const_typ.is_none()
+                && param.name.is_typ_param()
+                && !sized.contains(&param.name)
+            {
+                state.write(param.name.to_string());
+                state.write(" : ?Sized, ");
+            }
         }
     }
 }
@@ -787,7 +856,7 @@ pub(crate) fn emit_fun_decl(state: &mut EmitState, f: &FunDecl) {
         }
     }
     state.end_span(f.sig_span);
-    emit_generic_bounds(state, &f.generic_bounds);
+    emit_generic_bounds(state, &f.generic_params, &f.generic_bounds, false);
     match &*f.body {
         (_, ExpX::Block(..)) => {
             emit_exp(state, &f.body);
@@ -857,7 +926,7 @@ fn emit_copy_clone(
     state.write(format!(" {bound_name} for "));
     state.write(d.name.to_string());
     emit_generic_params(state, &generic_args);
-    emit_generic_bounds(state, &generic_bounds);
+    emit_generic_bounds(state, &vec![], &generic_bounds, false);
     state.write(" ");
     state.write(body);
 }
@@ -868,18 +937,25 @@ pub(crate) fn emit_trait_decl(state: &mut EmitState, t: &TraitDecl) {
     state.write("trait ");
     state.write(&t.name.to_string());
     emit_generic_params(state, &t.generic_params);
-    emit_generic_bounds(state, &t.generic_bounds);
+    emit_generic_bounds(state, &t.generic_params, &t.generic_bounds, true);
     state.write(" {");
     state.push_indent();
     for (a, bounds) in &t.assoc_typs {
+        let (bares, wheres) = simplify_assoc_typ_bounds(&t.name, a, bounds.clone());
         state.newline();
         state.write("type ");
         state.write(a.to_string());
-        if bounds.len() > 0 {
+        let sized = bares.iter().any(|b| b.bound == Bound::Sized);
+        let unsize = if sized { vec![] } else { vec!["?Sized".to_string()] };
+        if bounds.len() + unsize.len() > 0 {
             state.write(" : ");
-            let bounds_strs: Vec<_> =
-                bounds.iter().map(|bound| emit_generic_bound(bound, true)).collect();
+            let bounds_strs: Vec<_> = bares
+                .iter()
+                .map(|bound| emit_generic_bound(bound, true, false))
+                .chain(unsize.into_iter())
+                .collect();
             state.write(bounds_strs.join("+"));
+            emit_generic_bounds(state, &vec![], &wheres, false);
         }
         state.write(";");
     }
@@ -901,7 +977,7 @@ pub(crate) fn emit_datatype_decl(state: &mut EmitState, d: &DatatypeDecl) {
     let suffix_where = match &*d.datatype {
         Datatype::Struct(Fields::Pos(..)) => d.generic_bounds.len() > 0,
         _ => {
-            emit_generic_bounds(state, &d.generic_bounds);
+            emit_generic_bounds(state, &d.generic_params, &d.generic_bounds, false);
             false
         }
     };
@@ -910,7 +986,7 @@ pub(crate) fn emit_datatype_decl(state: &mut EmitState, d: &DatatypeDecl) {
             let suffix = if suffix_where { "" } else { ";" };
             emit_fields(state, fields, suffix);
             if suffix_where {
-                emit_generic_bounds(state, &d.generic_bounds);
+                emit_generic_bounds(state, &d.generic_params, &d.generic_bounds, false);
                 state.write(";");
             }
         }
@@ -948,7 +1024,7 @@ pub(crate) fn emit_assoc_type_impl(
     state.write(&trait_as_datatype.to_string());
     state.write(" for ");
     state.write(&self_typ.to_string());
-    emit_generic_bounds(state, &generic_bounds);
+    emit_generic_bounds(state, &generic_params, &generic_bounds, false);
     state.write(" {");
     state.push_indent();
     for fn_ in fns {

source/rust_verify/src/lifetime_generate.rs

@@ -96,6 +96,7 @@ pub(crate) struct State {
     remaining_typs_needed_for_each_impl: HashMap<DefId, (Id, Vec<DefId>)>,
     enclosing_fun_id: Option<DefId>,
     enclosing_trait_ids: Vec<DefId>,
+    inside_trait_assoc_type: u32,
 }
 
 impl State {
@@ -122,6 +123,7 @@ impl State {
             remaining_typs_needed_for_each_impl: HashMap::new(),
             enclosing_fun_id: None,
             enclosing_trait_ids: Vec::new(),
+            inside_trait_assoc_type: 0,
         }
     }
 
@@ -401,7 +403,11 @@ fn erase_ty<'tcx>(ctxt: &Context<'tcx>, state: &mut State, ty: &Ty<'tcx>) -> Typ
             Box::new(TypX::Primitive(ty.to_string()))
         }
         TyKind::Param(p) if p.name == kw::SelfUpper => {
-            Box::new(TypX::TypParam(state.typ_param("Self", None)))
+            if state.inside_trait_assoc_type > 0 {
+                Box::new(TypX::TraitSelf)
+            } else {
+                Box::new(TypX::TypParam(state.typ_param("Self", None)))
+            }
         }
         TyKind::Param(p) => {
             let name = p.name.as_str();
@@ -1757,6 +1763,8 @@ fn erase_mir_predicates<'a, 'tcx>(
                 let trait_path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, id);
                 let bound = if Some(id) == ctxt.tcx.lang_items().copy_trait() {
                     Some(Bound::Copy)
+                } else if Some(id) == ctxt.tcx.lang_items().sized_trait() {
+                    Some(Bound::Sized)
                 } else if state.trait_decl_set.contains(&trait_path) {
                     let substs = pred.trait_ref.args;
                     let (trait_typ_args, _) = erase_generic_args(ctxt, state, substs, true);
@@ -2099,6 +2107,7 @@ fn erase_trait<'tcx>(ctxt: &Context<'tcx>, state: &mut State, trait_id: DefId) {
 
     let mut assoc_typs: Vec<(Id, Vec<GenericBound>)> = Vec::new();
     let assoc_items = ctxt.tcx.associated_items(trait_id);
+    state.inside_trait_assoc_type += 1;
     for assoc_item in assoc_items.in_definition_order() {
         match assoc_item.kind {
             rustc_middle::ty::AssocKind::Const => {}
@@ -2161,6 +2170,7 @@ fn erase_trait<'tcx>(ctxt: &Context<'tcx>, state: &mut State, trait_id: DefId) {
             erase_impl_assocs(ctxt, state, impl_id);
         }
     }
+    state.inside_trait_assoc_type -= 1;
 
     assert!(state.enclosing_trait_ids.pop().is_some());
 }

source/rust_verify_test/tests/assoc_type_impls.rs

@@ -377,6 +377,21 @@ test_verify_one_file! {
     } => Err(err) => assert_vir_error_msg(err, "found a cyclic self-reference in a definition, which may result in nontermination")
 }
 
+test_verify_one_file! {
+    #[test] view_ref_unsized verus_code! {
+        // https://github.com/verus-lang/verus/issues/1104
+        use vstd::prelude::*;
+        fn id<T: View>(t: T) -> T {
+            t
+        }
+        fn test() {
+            let bytes: [u8; 4] = [0, 0, 0, 0];
+            let byte_slice: &[u8] = bytes.as_slice();
+            id(byte_slice);
+        }
+    } => Ok(())
+}
+
 test_verify_one_file! {
     #[test] mention_external_trait_with_assoc_type verus_code! {
         use vstd::prelude::*;

source/vstd/view.rs

@@ -19,7 +19,7 @@ pub trait DeepView {
     spec fn deep_view(&self) -> Self::V;
 }
 
-impl<A: View> View for &A {
+impl<A: View + ?Sized> View for &A {
     type V = A::V;
 
     #[verifier::inline]
@@ -28,7 +28,7 @@ impl<A: View> View for &A {
     }
 }
 
-impl<A: DeepView> DeepView for &A {
+impl<A: DeepView + ?Sized> DeepView for &A {
     type V = A::V;
 
     #[verifier::inline]
@@ -38,7 +38,7 @@ impl<A: DeepView> DeepView for &A {
 }
 
 #[cfg(feature = "alloc")]
-impl<A: View> View for alloc::boxed::Box<A> {
+impl<A: View + ?Sized> View for alloc::boxed::Box<A> {
     type V = A::V;
 
     #[verifier::inline]
@@ -48,7 +48,7 @@ impl<A: View> View for alloc::boxed::Box<A> {
 }
 
 #[cfg(feature = "alloc")]
-impl<A: DeepView> DeepView for alloc::boxed::Box<A> {
+impl<A: DeepView + ?Sized> DeepView for alloc::boxed::Box<A> {
     type V = A::V;
 
     #[verifier::inline]