How to specify a crate without verify it?

[Halbaroth]

Let's imagine you have a crate, says C1, and you want to specify it. However, you do not want to verify the crate.
I proceed as follows:

1. Add creusot-contracts as a dependency of C1.
2. Create a specs module that contains the specification (some implementations of View and DeepModels and extern_spec macro calls).

Now, suppose you want to use these specifications in another crate, says C2, and verify C2. So you add C1 with Creusot's specifications as a dependency of C2.

However, running cargo creusot prove in C2 will attempt to verify C1 too. In particular, it will try to emit Coma files for all C1, which is impossible because C1 contains features unsupported by Creusot. This is why I want to axiomatize C1 instead.

A straightforward workaround is to create a new crate, C1-creusot, that depends on both C1 and creusot-contracts. But I need to implement Creusot's traits on types of C1, which cannot be done in C1-creusot.

The only solution I found so far is to put my specifications in Creusot itself.

Any suggestions?

[jhjourdan]

I already anticipated this issue, but I don't have a good solution.

Ideally, I would prefer the C1-creusot approach, that let us avoid modifying crate C1. But the main problem here is that the orphans rule won't let us implement e.g., DeepModel ... I wish there were an "unsafe" way of disabling orphans check, but there isn't apparently.

So we are left with a few somewhat non-satisfying solutions (suggestions welcome):

• In C1-Creusot, create wrappers around every types and functions defined in C1. I can't see a case where this does not work, but this is rather tedious (but anyway, you need to write the specs, so this is probably not an issue to spend time copying all the functions prototypes). Another issue is interoperability: if C2 exposes some values of a type defined in C1-creusot, users would expect the unwrapped type, but C2 would use the wrapped type.
• Annotate items in C1 using #[trusted]. This tells Creusot not to try verifying these, and therefore this should prevent Creusot crashing when reading C1. You can do this module-wise (so you don't need major edits to the crate). If this does not try, please tell me what is the feature which is still not accepted by Creusot, and I will manage to add some sort of dummy support.

[xldenis]

Crates sometimes have a mechanism for "remote derives" maybe we could copy that?

[Halbaroth]

But the main problem here is that the orphans rule won't let us implement e.g., DeepModel ... I wish there were an "unsafe" way of disabling orphans check, but there isn't apparently.

Indeed, I also searched for a way to disable this rule but I guess it is impossible by design and unlikely to change in the future.

Annotate items in C1 using #[trusted]. This tells Creusot not to try verifying these, and therefore this should prevent Creusot crashing when reading C1. You can do this module-wise (so you don't need major edits to the crate). If this does not try, please tell me what is the feature which is still not accepted by Creusot, and I will manage to add some sort of dummy support.

Awesome! I was looking for this feature! I used #[trusted] on functions but it was really tedious to apply it everywhere.

[jhjourdan]

I'll leave the issue open, because it corresponds to a real problem, but as we don't really have a solution, we probably won't do anything soon.

[Halbaroth]

Sure, your workaround with #[trusted] works fine for my crate. Thanks.

[Halbaroth]

The workaround with #[trusted] does not work :/
I put this macro on each module declaration in the lib.rs file of hashbrown, but still I got the error:

not implemented 

After turning on the trace messages, Creusot outputs:

[2025-03-11T16:37:23Z TRACE creusot::translation::traits] TraitResolved::resolve DefId(1:8921 ~ core[1b69]::iter::traits::collect::IntoIterator::into_iter) [raw::bitmask::BitMask]
[2025-03-11T16:37:23Z TRACE creusot::translation::traits] TraitResolved::resolve ImplSourceUserDefinedData(impl_def_id=DefId(0:2589 ~ hashbrown[47bd]::raw::bitmask::{impl#1}), args=[], nested=[])
[2025-03-11T16:37:23Z TRACE creusot::translation::specification] no_panic: false
[2025-03-11T16:37:23Z TRACE creusot::translation::specification] terminates: false
[2025-03-11T16:37:23Z TRACE creusot::translation::specification] no_panic: false
[2025-03-11T16:37:23Z TRACE creusot::translation::specification] terminates: false
[2025-03-11T16:37:23Z TRACE creusot::translation::traits] TraitResolved::resolve DefId(1:9053 ~ core[1b69]::iter::traits::iterator::Iterator::next) [raw::bitmask::BitMaskIter]
[2025-03-11T16:37:23Z TRACE creusot::translation::traits] TraitResolved::resolve ImplSourceUserDefinedData(impl_def_id=DefId(0:2593 ~ hashbrown[47bd]::raw::bitmask::{impl#2}), args=[], nested=[])
[2025-03-11T16:37:23Z TRACE creusot::translation::specification] no_panic: false
[2025-03-11T16:37:23Z TRACE creusot::translation::specification] terminates: false
[2025-03-11T16:37:23Z TRACE creusot::translation::specification] no_panic: false
[2025-03-11T16:37:23Z TRACE creusot::translation::specification] terminates: false
[2025-03-11T16:37:23Z TRACE creusot::translation::traits] TraitResolved::resolve DefId(1:3784 ~ core[1b69]::ops::function::FnMut::call_mut) [dyn [Binder { value: Trait(core::ops::FnMut<(usize,)>), bound_vars: [] }, Binder { value: Projection(Output = bool), bound_vars: [] }] + '{erased}, (usize,)]

From my understanding, the macro #[trusted] does not prevent Creusot from implementing its own traits for types in the modules. For instance, Creusot's stdlib implements FnMutExt for all FnMut types:

impl<Args: Tuple, F: FnMut<Args>> FnMutExt<Args> for F {
    #[predicate(prophetic)]
    #[open]
    #[allow(unused_variables)]
    #[rustc_diagnostic_item = "fn_mut_impl_postcond"]
    fn postcondition_mut(self, args: Args, result_state: Self, result: Self::Output) -> bool {
        true /* Dummy */
    }
...

Therefore, Creusot implements this trait for FnMut types in raw for example?

[jhjourdan]

Indeed, there is a generic instance of FnMutExt for any mutable closure. But I don't see why this would cause issues here.

I think I understand what is causing this error: it seems like Creusot is searching for the call_mut instance of a dyn FnMut type. I can try to emit some dummy code in this case, but I don't see why this could happen if using #[trusted]. Perhaps you could give me a backtrace?

[jhjourdan]

(Using RUST_BACKTRACE=1)

[Halbaroth]

Sure,

thread 'rustc' panicked at creusot/src/translation/traits.rs:298:22:
not implemented
stack backtrace:
   0: rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::panicking::panic
   3: creusot::translation::traits::TraitResolved::resolve_item
   4: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
   5: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
   6: rustc_middle::thir::visit::walk_expr
   7: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
   8: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
   9: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  10: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  11: rustc_middle::thir::visit::walk_expr
  12: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  13: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  14: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  15: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  16: rustc_middle::thir::visit::walk_expr
  17: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  18: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  19: rustc_middle::thir::visit::walk_expr
  20: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  21: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  22: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  23: rustc_middle::thir::visit::walk_expr
  24: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  25: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  26: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  27: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  28: rustc_middle::thir::visit::walk_expr
  29: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  30: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  31: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  32: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  33: <creusot::validate::purity::PurityVisitor as rustc_middle::thir::visit::Visitor>::visit_expr
  34: creusot::validate::purity::validate_purity
  35: creusot::translation::before_analysis
  36: <creusot::callbacks::ToWhy as rustc_driver_impl::Callbacks>::after_expansion
  37: rustc_interface::passes::create_and_enter_global_ctxt::<core::option::Option<rustc_interface::queries::Linker>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2}>::{closure#2}::{closure#0}
  38: rustc_interface::interface::run_compiler::<(), rustc_driver_impl::run_compiler::{closure#0}>::{closure#1}

[Halbaroth]

I think I understand what is causing this error: it seems like Creusot is searching for the call_mut instance of a dyn FnMut type. I can try to emit some dummy code in this case, but I don't see why this could happen if using #[trusted]. Perhaps you could give me a backtrace?

I don't understand too, as all the occurrences of FnMut are in modules that should be ignored by Creusot with #[trusted].
The presence of raw::bitmask::BitMaskIter in the trace is also suspicious since raw module should be ignored.

Besides, I have a question. Is there a way to exclude the code generated by macros from the verification?

[jhjourdan]

I'm preparing a fix.

Besides, I have a question. Is there a way to exclude the code generated by macros from the verification?

Not really. IT's not clear what that would mean, because the expansion of the macro is part of the AST which is verified, so we need to make it transparent.

[jhjourdan]

Could you please check once #1428 is merged?