Verifying 3rd party dependency crate results in compiler panic

[nshyrei]

I have a 3rd party dependency crate vulkano that I use (https://crates.io/crates/vulkano). Building the project with cargo-prusti crashes with the following compiler panic:

Checking vulkano v0.34.1
error: internal compiler error: compiler\rustc_hir_typeck\src\lib.rs:180:9: can't type-check body of DefId(0:17398 ~ vulkano[676d]::display::{impl#28}::IntoIter)
   --> vulkano-7de5a6fabca05a00\9fac29e\vulkano\src\macros.rs:938:13
    |
938 |               type IntoIter = std::iter::Flatten<
    |               ^^^^^^^^^^^^^
    |
   ::: vulkano-7de5a6fabca05a00\9fac29e\vulkano\src\display.rs:723:1
    |
723 | / vulkan_bitflags_enum! {
724 | |     #[non_exhaustive]
725 | |
726 | |     /// A set of [`DisplayPlaneAlpha`] values.
...   |
745 | |     PER_PIXEL_PREMULTIPLIED, PerPixelPremultiplied = PER_PIXEL_PREMULTIPLIED,
746 | | }
    | |_- in this macro invocation
    |
    = note: this error: internal compiler error originates in the macro `vulkan_bitflags_enum` (in Nightly builds, run with -Z macro-backtrace for more info)

thread 'rustc' panicked at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c\compiler\rustc_errors\src\lib.rs:995:33:
Box<dyn Any>
stack backtrace:
   0:     0x7fff216a64da - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h7d96bb47b8259b19
   1:     0x7fff216db27b - core::fmt::write::h391d4f99a7c9ba61
   2:     0x7fff2169bda1 - <std::io::IoSliceMut as core::fmt::Debug>::fmt::h825b775f4681ab30
   3:     0x7fff216a625a - std::sys_common::backtrace::lock::h7c90b1b69e137e00
   4:     0x7fff216a9b13 - std::panicking::panic_hook_with_disk_dump::h0b73811722203766
   5:     0x7fff216a96ab - std::panicking::panic_hook_with_disk_dump::h0b73811722203766
   6:     0x7fff09b5dac0 - rustc_driver_impl[f4795a6955707fde]::ice_path
   7:     0x7fff216aa4eb - std::panicking::rust_panic_with_hook::hddc10c471e545221
   8:     0x7fff09e1c538 - <rustc_hir_typeck[dc82029c3f72c98b]::generator_interior::drop_ranges::NodeInfo as core[a2a52c79d6995320]::fmt::Debug>::fmt
   9:     0x7fff09e1a159 - <rustc_hir_typeck[dc82029c3f72c98b]::generator_interior::drop_ranges::NodeInfo as core[a2a52c79d6995320]::fmt::Debug>::fmt
  10:     0x7fff09df48f9 - <rustc_hir_typeck[dc82029c3f72c98b]::expectation::Expectation as core[a2a52c79d6995320]::fmt::Debug>::fmt
  11:     0x7fff09df2ee6 - <rustc_hir_typeck[dc82029c3f72c98b]::expectation::Expectation as core[a2a52c79d6995320]::fmt::Debug>::fmt
  12:     0x7fff09df2c5d - <rustc_hir_typeck[dc82029c3f72c98b]::expectation::Expectation as core[a2a52c79d6995320]::fmt::Debug>::fmt
  13:     0x7fff09e1c6cf - <rustc_hir_typeck[dc82029c3f72c98b]::generator_interior::drop_ranges::NodeInfo as core[a2a52c79d6995320]::fmt::Debug>::fmt
  14:     0x7fff09e1c70d - <rustc_hir_typeck[dc82029c3f72c98b]::generator_interior::drop_ranges::NodeInfo as core[a2a52c79d6995320]::fmt::Debug>::fmt
  15:     0x7fff09e1a43f - <rustc_hir_typeck[dc82029c3f72c98b]::generator_interior::drop_ranges::NodeInfo as core[a2a52c79d6995320]::fmt::Debug>::fmt
  16:     0x7fff09e19c06 - <rustc_hir_typeck[dc82029c3f72c98b]::generator_interior::drop_ranges::NodeInfo as core[a2a52c79d6995320]::fmt::Debug>::fmt
  17:     0x7fff08cb45cd - <rustc_hir_typeck[dc82029c3f72c98b]::method::probe::Pick>::maybe_emit_unstable_name_collision_hint
  18:     0x7fff094c899f - rustc_query_impl[aabbd44c70ac20af]::query_callbacks
  19:     0x7fff094fe68f - rustc_query_impl[aabbd44c70ac20af]::query_callbacks
  20:     0x7fff09599bf4 - rustc_query_impl[aabbd44c70ac20af]::query_callbacks
  21:     0x7fff0953b4d2 - rustc_query_impl[aabbd44c70ac20af]::query_callbacks
  22:     0x7ff64ccba73d - <unknown>
  23:     0x7ff64cc7d2ec - <unknown>
  24:     0x7ff64cc72660 - <unknown>
  25:     0x7ff64cc77afb - <unknown>
  26:     0x7ff64cc725dd - <unknown>
  27:     0x7ff64cc77afb - <unknown>
  28:     0x7ff64cc8182c - <unknown>
  29:     0x7ff64cc80e50 - <unknown>
  30:     0x7ff64ccf30ac - <unknown>
  31:     0x7ff64ccf51e0 - <unknown>
  32:     0x7ff64c1b8df3 - <unknown>
  33:     0x7fff05d25fb4 - rustc_driver_impl[f4795a6955707fde]::args::arg_expand_all
  34:     0x7fff05d3d2e4 - <rustc_middle[d8286ac0ea2cb69]::ty::SymbolName as core[a2a52c79d6995320]::fmt::Display>::fmt
  35:     0x7fff05d3ee06 - <rustc_middle[d8286ac0ea2cb69]::ty::SymbolName as core[a2a52c79d6995320]::fmt::Display>::fmt
  36:     0x7fff216bdb9c - std::sys::windows::thread::Thread::new::h5e1d00b22c07e079
  37:     0x7fffe9987344 - BaseThreadInitThunk
  38:     0x7fffe9c626b1 - RtlUserThreadStart

note: we would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: rustc 1.74.0-nightly (ca2b74f1a 2023-09-14) running on x86_64-pc-windows-msvc

note: compiler flags: --crate-type lib -C embed-bitcode=no -C debuginfo=2

note: some of the compiler flags provided by cargo are hidden

query stack during panic:
#0 [typeck] type-checking `display::<impl at vulkano\src\macros.rs:936:9: 936:43>::IntoIter`
end of query stack
note: Prusti version: 0.2.2, commit e632f70 2024-02-01 12:14:41 UTC, built on 2024-02-01 12:36:55 UTC

Now I am happy to not verify this crate altogether, but none of the flags like [NO_VERIFY_DEPS] (https://viperproject.github.io/prusti-dev/dev-guide/config/flags.html#no_verify_deps) or [NO_VERIFY] (https://viperproject.github.io/prusti-dev/dev-guide/config/flags.html#no_verify) seem to work in any form including env vars or Prusti.toml file.

[fpoli]

Thank you for the report. From a quick look, my stacktrace suggests that the panic happens while Prusti is running <ModelUsageVisitor as NonSpecExprVisitor>::visit_expr (code below). Using the Prusti release v-2023-01-26-1935 I do not get this error, so I suspect that this is a bug of rustc. We should update Prusti to use the latest version of rustc to see if the bug has been fixed in the meantime.

prusti-dev/prusti-interface/src/specs/checker/type_model_checks.rs

Lines 80 to 93 in e632f70

	fn visit_expr(&mut self, expr: &'tcx hir::Expr<'tcx>) {
	if let hir::ExprKind::MethodCall(_, _, _, call_span) = expr.kind {
	let maybe_method_decl_hir_id: Option<hir::HirId> = self.get_called_method(expr);
	if let Some(method_decl_hir_id) = maybe_method_decl_hir_id {
	let attrs = self.env_query.get_local_attributes(method_decl_hir_id);
	if has_to_model_fn_attr(attrs) {
	self.model_usages_in_non_spec_code.push(call_span);
	}
	}
	}
	}
	}

My stacktrace:

thread 'rustc' panicked at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/compiler/rustc_errors/src/lib.rs:995:33:
Box<dyn Any>
stack backtrace:
   0:     0x7f0f67562efc - std::backtrace_rs::backtrace::libunwind::trace::h652247f520429b18
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7f0f67562efc - std::backtrace_rs::backtrace::trace_unsynchronized::h20ba733a518048ae
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f0f67562efc - std::sys_common::backtrace::_print_fmt::ha9cb2d71bba5eb16
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7f0f67562efc - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h527f3c0db321cf86
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7f0f675c915c - core::fmt::rt::Argument::fmt::hc5a8cd063e05c609
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/core/src/fmt/rt.rs:138:9
   5:     0x7f0f675c915c - core::fmt::write::h818c732e4e373aa5
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/core/src/fmt/mod.rs:1094:21
   6:     0x7f0f6755593e - std::io::Write::write_fmt::h07440f3e98279257
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/io/mod.rs:1714:15
   7:     0x7f0f67562ce4 - std::sys_common::backtrace::_print::h4b50c3b478ae2a37
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7f0f67562ce4 - std::sys_common::backtrace::print::hf2c7643f5414af94
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7f0f67565dda - std::panicking::panic_hook_with_disk_dump::{{closure}}::h62ff4ef3ec32306d
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/panicking.rs:280:22
  10:     0x7f0f67565ad5 - std::panicking::panic_hook_with_disk_dump::hcd58ca7cb67f8702
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/panicking.rs:314:9
  11:     0x7f0f6a7690b9 - <rustc_driver_impl[8b2874cda94e7cd4]::install_ice_hook::{closure#0} as core[b0493a3e457862f3]::ops::function::FnOnce<(&core[b0493a3e457862f3]::panic::panic_info::PanicInfo,)>>::call_once::{shim:vtable#0}
  12:     0x7f0f67566693 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h2b79b1e8b8bd4402
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/alloc/src/boxed.rs:2021:9
  13:     0x7f0f67566693 - std::panicking::rust_panic_with_hook::ha2c93276d1208654
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/panicking.rs:757:13
  14:     0x7f0f6a9eab54 - std[843b1ee06368cddb]::panicking::begin_panic::<rustc_errors[e553a123e183cff8]::ExplicitBug>::{closure#0}
  15:     0x7f0f6a9e82b6 - std[843b1ee06368cddb]::sys_common::backtrace::__rust_end_short_backtrace::<std[843b1ee06368cddb]::panicking::begin_panic<rustc_errors[e553a123e183cff8]::ExplicitBug>::{closure#0}, !>
  16:     0x7f0f6aa0ec16 - std[843b1ee06368cddb]::panicking::begin_panic::<rustc_errors[e553a123e183cff8]::ExplicitBug>
  17:     0x7f0f6aa0e2ee - <rustc_errors[e553a123e183cff8]::HandlerInner>::span_bug::<rustc_span[82af0e0afe7e8690]::span_encoding::Span, alloc[606cb6f3851bb62a]::string::String>
  18:     0x7f0f6aa0e10b - <rustc_errors[e553a123e183cff8]::Handler>::span_bug::<rustc_span[82af0e0afe7e8690]::span_encoding::Span, alloc[606cb6f3851bb62a]::string::String>
  19:     0x7f0f6a9ceb4d - rustc_middle[ad90ed66b4303932]::util::bug::opt_span_bug_fmt::<rustc_span[82af0e0afe7e8690]::span_encoding::Span>::{closure#0}
  20:     0x7f0f6a9ceb7a - rustc_middle[ad90ed66b4303932]::ty::context::tls::with_opt::<rustc_middle[ad90ed66b4303932]::util::bug::opt_span_bug_fmt<rustc_span[82af0e0afe7e8690]::span_encoding::Span>::{closure#0}, !>::{closure#0}
  21:     0x7f0f6a9ce138 - rustc_middle[ad90ed66b4303932]::ty::context::tls::with_context_opt::<rustc_middle[ad90ed66b4303932]::ty::context::tls::with_opt<rustc_middle[ad90ed66b4303932]::util::bug::opt_span_bug_fmt<rustc_span[82af0e0afe7e8690]::span_encoding::Span>::{closure#0}, !>::{closure#0}, !>
  22:     0x7f0f699cad94 - rustc_middle[ad90ed66b4303932]::util::bug::span_bug_fmt::<rustc_span[82af0e0afe7e8690]::span_encoding::Span>
  23:     0x7f0f697f3db0 - rustc_hir_typeck[1d417f91be3ec530]::typeck
  24:     0x7f0f6884954e - rustc_query_impl[e537a3258c4e1a56]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[e537a3258c4e1a56]::query_impl::typeck::dynamic_query::{closure#2}::{closure#0}, rustc_middle[ad90ed66b4303932]::query::erase::Erased<[u8; 8usize]>>
  25:     0x7f0f6884951e - <rustc_query_impl[e537a3258c4e1a56]::query_impl::typeck::dynamic_query::{closure#2} as core[b0493a3e457862f3]::ops::function::FnOnce<(rustc_middle[ad90ed66b4303932]::ty::context::TyCtxt, rustc_span[82af0e0afe7e8690]::def_id::LocalDefId)>>::call_once
  26:     0x7f0f68920e58 - rustc_query_system[404b1af824500f21]::query::plumbing::try_execute_query::<rustc_query_impl[e537a3258c4e1a56]::DynamicConfig<rustc_query_system[404b1af824500f21]::query::caches::VecCache<rustc_span[82af0e0afe7e8690]::def_id::LocalDefId, rustc_middle[ad90ed66b4303932]::query::erase::Erased<[u8; 8usize]>>, false, false, false>, rustc_query_impl[e537a3258c4e1a56]::plumbing::QueryCtxt, false>
  27:     0x7f0f6a0e46f1 - rustc_query_impl[e537a3258c4e1a56]::query_impl::typeck::get_query_non_incr::__rust_end_short_backtrace
  28:     0x55fd10f90533 - <prusti_interface::specs::checker::type_model_checks::ModelUsageVisitor as prusti_interface::specs::checker::common::NonSpecExprVisitor>::visit_expr::h037892247f929c0f
  29:     0x55fd10f5c7a9 - rustc_hir::intravisit::walk_expr::he69b9c275b775907
  30:     0x55fd10f50a52 - rustc_hir::intravisit::walk_generic_args::h19816db272b4a4cf
  31:     0x55fd10f5638c - rustc_hir::intravisit::walk_ty::h8e5a9f5fce680e64
  32:     0x55fd10f509cc - rustc_hir::intravisit::walk_generic_args::h19816db272b4a4cf
  33:     0x55fd10f5638c - rustc_hir::intravisit::walk_ty::h8e5a9f5fce680e64
  34:     0x55fd10f6185c - rustc_hir::intravisit::walk_item::hf728d6eec02be310
  35:     0x55fd10f60e06 - rustc_hir::intravisit::walk_item::hf728d6eec02be310
  36:     0x55fd10fbfed4 - <prusti_interface::specs::checker::type_model_checks::IllegalModelUsagesChecker as prusti_interface::specs::checker::common::SpecCheckerStrategy>::check::heaf4b4f8771d37e0
  37:     0x55fd10fc1946 - prusti_interface::specs::checker::SpecChecker::check::h9125bbb6de956f50
  38:     0x55fd1065e15d - <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis::h7d8f5df69404394f
  39:     0x7f0f69c789d6 - <rustc_interface[1527d435bc9889c9]::interface::Compiler>::enter::<rustc_driver_impl[8b2874cda94e7cd4]::run_compiler::{closure#1}::{closure#2}, core[b0493a3e457862f3]::result::Result<core[b0493a3e457862f3]::option::Option<rustc_interface[1527d435bc9889c9]::queries::Linker>, rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>
  40:     0x7f0f69c71c04 - std[843b1ee06368cddb]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[1527d435bc9889c9]::util::run_in_thread_with_globals<rustc_interface[1527d435bc9889c9]::interface::run_compiler<core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>, rustc_driver_impl[8b2874cda94e7cd4]::run_compiler::{closure#1}>::{closure#0}, core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>
  41:     0x7f0f69c7135e - <<std[843b1ee06368cddb]::thread::Builder>::spawn_unchecked_<rustc_interface[1527d435bc9889c9]::util::run_in_thread_with_globals<rustc_interface[1527d435bc9889c9]::interface::run_compiler<core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>, rustc_driver_impl[8b2874cda94e7cd4]::run_compiler::{closure#1}>::{closure#0}, core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>::{closure#1} as core[b0493a3e457862f3]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  42:     0x7f0f67571075 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h7bff668e3fcc7cec
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/alloc/src/boxed.rs:2007:9
  43:     0x7f0f67571075 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h6cf1c11e2e0c58d1
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/alloc/src/boxed.rs:2007:9
  44:     0x7f0f67571075 - std::sys::unix::thread::Thread::new::thread_start::hfa7d5fcc9039f5da
                               at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys/unix/thread.rs:108:17
  45:     0x7f0f65c94ac3 - start_thread
                               at ./nptl/pthread_create.c:442:8
  46:     0x7f0f65d26850 - __GI___clone3
                               at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81
  47:                0x0 - <unknown>

[fpoli]

For the record, Prusti v-2023-01-26-1935 fails with this other error complaining about Prusti using a version of rustc that is too old:

error: package `half v2.3.1` cannot be built because it requires rustc 1.70 or newer, while the currently active rustc version is 1.68.0-nightly
Either upgrade to rustc 1.70 or newer, or use
cargo update -p half@2.3.1 --precise ver
where `ver` is the latest version of `half` supporting rustc 1.68.0-nightly

[nshyrei]

@fpoli Seems like this #1470 is a relevant PR that will potentially fix the issue but it is stuck.

[fpoli]

Indeed :) We had to balance our efforts between updating the current master and finishing a large refactoring. The latter is going to bring many advantages -- e.g., making rustc updates easier -- and is almost ready, so I think it's best to keep prioritizing that.

[nshyrei]

@fpoli Do you know why the flags [NO_VERIFY_DEPS] or [NO_VERIFY] might not work for me? As I said it's not important for me to check this 3rd party crate as I am only interested in my portion of the project. I use Prusti.toml to specify a flag and I know for sure that it is being used, because if I duplicate the keys in the file Prusti will fail before starting the check.

[fpoli]

That's because we want Prusti to collect the contracts that are declared in the dependencies, even when those contracts are not verified with respect to their implementation.

To do what you are proposing we would need one new flag to skip collecting the specifications from the dependencies, e.g., something called ignore_deps_contracts. When that's enabled, the important thing is to make Prusti enter this branch, so that rustc runs (almost) as in a normal compilation. If anywant (@pixelshot91?) wants to give a try before us, I think that this should be a relatively easy contribution. The configuration flags are defined here and documented here.

[nshyrei]

@fpoli Correct me If I am wrong, but I believe that entering this branch will skip verification all together for the whole project, because I have tried https://github.com/viperproject/prusti-dev/blob/c1a5b128d938333a821af0a554be4562905bb82a/docs/dev-guide/src/config/flags.md#be_rustc before and I only saw regular rustc output.

[fpoli]

Sorry, it's because I didn't state the complete condition. We already have a way of detecting whether Prusti is currently compiling the main crate or a dependency, it's is_primary_package. So, the full condition for entering the "act as rustc" branch should become something like the following

if config::be_rustc() || build_script_build || (!is_primary_package && config::ignore_deps_contracts()) {

[nshyrei]

@fpoli What I am asking is will

prusti-dev/prusti/src/driver.rs

Line 93 in c1a5b12

driver::main();

verify or it will simply compile the project with rustc ?

[fpoli]

driver::main() compiles a single crate as rustc would do, but that does not affect how other crates (e.g., the dependencies) are compiled. More in detail, cargo-prusti launches cargo, which ends up launching multiple times prusti-driver: one for each crate to be compiled (i.e., the root one, and the dependencies). The driver::main() call is in prusti-driver, and in your case you want to execute it when running on the dependencies (ignoring all the contracts in them) but not when running on the main crate, because it should be verified.

[nshyrei]

@fpoli Created a PR #1496

[nshyrei]

@fpoli Unfortunately I don't see my issue fixed. I have picked latest nightly https://github.com/viperproject/prusti-dev/releases/tag/v-2024-02-26-1521 and I for sure know that the flag is used, because if I corrupt the flag name a bit in Prusti.toml the verifier will panic with:

thread 'main' panicked at prusti-utils\src\config.rs:241:9:
Found an unknown configuration flag `ignore_deps_contsdracts` in the file `.\Prusti.toml`
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

[fpoli]

This was missing: #1498

Whitout that fix, with version v-2024-02-26-1521, you can declare a PRUSTI_IGNORE_DEPS_CONTRACTS=true environment variable — e.g., in the prusti-assistant.extraPrustiEnv setting of Prusti-Assistant — and it works.

[nshyrei]

@fpoli Ok, with PRUSTI_IGNORE_DEPS_CONTRACTS I am getting a bunch of prusti-related compile messages now, but no rustc crashes so I assume it indeed works. I am closing this as resolved, thank you very much.