Dyn traits are not implemented

[the-ssd]

Hello, I was trying to use creusot to verify that redox kernel didn't have any panics, and ran into a bit of a problem.

The kernel uses "dyn traits", which are not implemented.

This is where creusot crashes

Is it possible to implement them?

Here is a maybe working implementation

ImplSource::Builtin(_, _) => match *substs.type_at(0).kind() {
    rustc_middle::ty::Closure(closure_def_id, closure_substs) => {
        TraitResolved::Instance(closure_def_id, closure_substs)
    }
    rustc_middle::ty::Dynamic(_, _, _) => {
        TraitResolved::UnknownNotFound
    }
    _ => {
        todo!()
    }
},

If it is resolved, then I still have a problem with error: const generic parameters are not yet supported, (compiles on stable and nightly). It seems like they are also not supported by creusot

Here is the snippet.

pub struct AlignedBox<T: ?Sized, const ALIGN: usize> {
    inner: Unique<T>,
}

impl<T: ?Sized, const ALIGN: usize> AlignedBox<T, ALIGN> {
    fn layout(&self) -> Layout {
        layout_upgrade_align(Layout::for_value::<T>(&*self), ALIGN) // error: const generic parameters are not yet supported
    }
}
const fn layout_upgrade_align(layout: Layout, align: usize) -> Layout {
    const fn max(a: usize, b: usize) -> usize {
        if a > b {
            a
        } else {
            b
        }
    }
    let Ok(x) = Layout::from_size_align(layout.size(), max(align, layout.align())) else {
        panic!("failed to calculate layout");
    };
    x
}

[jhjourdan]

Thanks for the report!

You are right that there are still quite a few Rust features which are missing in Creusot. Dyn types and const generic parameters are among those.

We do not expect fundamental problems with const generics. We have rather clear ideas about what should be done. This "just has to be done", but we lack resources/developper time for this. You are welcome, though!

As for dyn types, things are more subtle. We could provide a naive implementation, which would essentially declare as abstract any logical method of a dyn type, but that would not be very useful, since we would not be able to do any proof about such an object. On the other hand, having a useful support for trait objects raises many difficult design questions, which we don't have good answers yet.