`forbidden dyn type: dyn core::error::Error` when using `thiserror` (`#[error(transparent)]`)

[Dspil]

Description

When using the thiserror crate to derive Error for an enum, using the #[error(transparent)] (or #[source]) attribute causes a forbidden dyn type compilation failure in Creusot.

Error Output

warning: support for trait objects (dyn) is limited and experimental
  --> src/lib.rs:13:13
   |
13 |     #[error(transparent)]
   |             ^^^^^^^^^^^
   |
   = note: `#[warn(creusot::experimental)]` on by default

warning: calling external function `as_dyn_error` with no contract will yield an impossible pecondition
  --> src/lib.rs:13:13
   |
13 |     #[error(transparent)]
   |             ^^^^^^^^^^^ function called here
   |
   = note: `#[warn(creusot::contractless_external_function)]` on by default

warning: calling external function `source` with no contract will yield an impossible precondtion
  --> src/lib.rs:13:13
   |
13 |     #[error(transparent)]
   |             ^^^^^^^^^^^ function called here

error: forbidden dyn type: dyn std::error::Error (dyn support is currently minimal, please opn an issue to improve this feature)

warning: `minimal_creusot_dyn_error` (lib) generated 4 warnings
error: could not compile `minimal_creusot_dyn_error` (lib) due to 1 previous error; 4 warning emitted

Minimal Reproducible Example

Cargo.toml

[package]
name = "minimal_creusot_dyn_error"
version = "0.1.0"
edition = "2021"

[dependencies]
thiserror = "1.0.64"
creusot-std = "0.11.0-dev"

src/lib.rs

use thiserror::Error;

use creusot_std::prelude::*;

#[derive(Debug, Error)]
pub enum InnerError {
    #[error("inner")]
    Inner,
}

#[derive(Debug, Error)]
pub enum MyError {
    #[error(transparent)]
    Inner(#[from] InnerError),
}

[Lysxia]

Thanks for the report. We should add Error to the whitelist (and possibly other std traits commonly used with dyn).

[jhjourdan]

@Dspil : dyn is Rust's way to support truly higher-order functions, which are difficult to support in Creusot just like higher-order in any verification system. We have some ideas for that, but we will not support dyn in the near future.

In order to support code generated by already existing macros in pieces of code Creusot sees beut does not prove anything about, we have a whitelist of traits for which we allow dyn because they should be safe as far as verification is concerned.

@Lysxia What about adding in the white list all the external traits for which we do not have any extern specs. The dyn feature should be safe for them, because one cannot call any of its methods from verified code anyway. This would include thiserror::Error.

[Dspil]

Sounds good, thanks for this! Making it compile is all we need too.

[jhjourdan]

If you do not use these types in verified code (including in the prototype of functions called by verified code), another easy possibility is to move these in modules marked with #[trusted], which should prevent Creusot from looking at it. If this does not work, then this is a bug.