Update toolchain to 2025-12-10

[Lysxia]

No description provided.

[Lysxia]

Building creusot-contracts currently crashes:

thread 'rustc' panicked at /home/sam/.rustup/toolchains/nightly-2025-12-10-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_next_trait_solver/src/coherence.rs:442:17:
internal error: entered unreachable code: unnameable type in coherence: FnDef(DefId(2:3524 ~ core[f9b0]::default::Default::default), [?0t])
stack backtrace:
   0:     0x704beea7350b - <std[4e041eb9831d95d2]::backtrace::Backtrace>::create
   1:     0x704beea73455 - <std[4e041eb9831d95d2]::backtrace::Backtrace>::force_capture
   2:     0x704bedae1553 - std[4e041eb9831d95d2]::panicking::update_hook::<alloc[10595c53490534ae]::boxed::Box<rustc_driver_impl[d6ef0231697d3f85]::install_ice_hook::{closure#1}>>::{closure#0}
   3:     0x704beea862e2 - std[4e041eb9831d95d2]::panicking::panic_with_hook
   4:     0x704beea689b8 - std[4e041eb9831d95d2]::panicking::panic_handler::{closure#0}
   5:     0x704beea5f9e9 - std[4e041eb9831d95d2]::sys::backtrace::__rust_end_short_backtrace::<std[4e041eb9831d95d2]::panicking::panic_handler::{closure#0}, !>
   6:     0x704beea6a56d - __rustc[47f3c1cf3382b6b6]::rust_begin_unwind
   7:     0x704bec1270ec - core[f9b0cf5fccb69ea1]::panicking::panic_fmt
   8:     0x5788f25a2514 - <rustc_next_trait_solver[8796a32d6ba0f85a]::coherence::OrphanChecker<rustc_infer[6dde30dc5d8796a7]::infer::InferCtxt, rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt, <creusot[f07d8a7e3e012a46]::translation::traits::GraphTraversal>::remote_crates_allow_impls::{closure#0}> as rustc_type_ir[11d804b8e3da8d8a]::visit::TypeVisitor<rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt>>::visit_ty
                               at /home/sam/.rustup/toolchains/nightly-2025-12-10-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_next_trait_solver/src/coherence.rs:442:17
   9:     0x5788f2565a5a - <rustc_middle[858d3a7a7a03c869]::ty::Ty as rustc_type_ir[11d804b8e3da8d8a]::visit::TypeVisitable<rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt>>::visit_with::<rustc_next_trait_solver[8796a32d6ba0f85a]::coherence::OrphanChecker<rustc_infer[6dde30dc5d8796a7]::infer::InferCtxt, rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt, <creusot[f07d8a7e3e012a46]::translation::traits::GraphTraversal>::remote_crates_allow_impls::{closure#0}>>
                               at /home/sam/.rustup/toolchains/nightly-2025-12-10-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_middle/src/ty/structural_impls.rs:379:17
  10:     0x5788f2565a5a - <rustc_middle[858d3a7a7a03c869]::ty::generic_args::GenericArg as rustc_type_ir[11d804b8e3da8d8a]::visit::TypeVisitable<rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt>>::visit_with::<rustc_next_trait_solver[8796a32d6ba0f85a]::coherence::OrphanChecker<rustc_infer[6dde30dc5d8796a7]::infer::InferCtxt, rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt, <creusot[f07d8a7e3e012a46]::translation::traits::GraphTraversal>::remote_crates_allow_impls::{closure#0}>>
                               at /home/sam/.rustup/toolchains/nightly-2025-12-10-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_middle/src/ty/generic_args.rs:354:44
  11:     0x5788f209ce8d - <&rustc_middle[858d3a7a7a03c869]::ty::list::RawList<(), rustc_middle[858d3a7a7a03c869]::ty::generic_args::GenericArg> as rustc_type_ir[11d804b8e3da8d8a]::visit::TypeVisitable<rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt>>::visit_with::<rustc_next_trait_solver[8796a32d6ba0f85a]::coherence::OrphanChecker<rustc_infer[6dde30dc5d8796a7]::infer::InferCtxt, rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt, <creusot[f07d8a7e3e012a46]::translation::traits::GraphTraversal>::remote_crates_allow_impls::{closure#0}>>
                               at /home/sam/.rustup/toolchains/nightly-2025-12-10-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_middle/src/ty/generic_args.rs:707:9
  12:     0x5788f25849b0 - <rustc_type_ir[11d804b8e3da8d8a]::predicate::TraitRef<rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt> as rustc_type_ir[11d804b8e3da8d8a]::visit::TypeVisitable<rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt>>::visit_with::<rustc_next_trait_solver[8796a32d6ba0f85a]::coherence::OrphanChecker<rustc_infer[6dde30dc5d8796a7]::infer::InferCtxt, rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt, <creusot[f07d8a7e3e012a46]::translation::traits::GraphTraversal>::remote_crates_allow_impls::{closure#0}>>
                               at /home/sam/.rustup/toolchains/nightly-2025-12-10-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_type_ir/src/predicate.rs:55:10
  13:     0x5788f25a1efb - rustc_next_trait_solver[8796a32d6ba0f85a]::coherence::orphan_check_trait_ref::<rustc_infer[6dde30dc5d8796a7]::infer::InferCtxt, rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt, !, <creusot[f07d8a7e3e012a46]::translation::traits::GraphTraversal>::remote_crates_allow_impls::{closure#0}>::{closure#0}
                               at /home/sam/.rustup/toolchains/nightly-2025-12-10-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_next_trait_solver/src/coherence.rs:237:24
  14:     0x5788f25a149a - rustc_next_trait_solver[8796a32d6ba0f85a]::coherence::orphan_check_trait_ref::<rustc_infer[6dde30dc5d8796a7]::infer::InferCtxt, rustc_middle[858d3a7a7a03c869]::ty::context::TyCtxt, !, <creusot[f07d8a7e3e012a46]::translation::traits::GraphTraversal>::remote_crates_allow_impls::{closure#0}>
                               at /home/sam/.rustup/toolchains/nightly-2025-12-10-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_next_trait_solver/src/coherence.rs:220:1
  15:     0x5788f22c4d10 - <creusot[f07d8a7e3e012a46]::translation::traits::GraphTraversal>::remote_crates_allow_impls
                               at /home/sam/rust/creusot/creusot/src/translation/traits.rs:515:9
  16:     0x5788f22c5e48 - <creusot[f07d8a7e3e012a46]::translation::traits::TraitResolved>::resolve_item
                               at /home/sam/rust/creusot/creusot/src/translation/traits.rs:253:19
  17:     0x5788f244129d - creusot[f07d8a7e3e012a46]::backend::resolve::resolve_user_resolve
                               at /home/sam/rust/creusot/creusot/src/backend/resolve.rs:275:5
  18:     0x5788f2440ba0 - creusot[f07d8a7e3e012a46]::backend::resolve::is_resolve_trivial
                               at /home/sam/rust/creusot/creusot/src/backend/resolve.rs:36:15
  19:     0x5788f22499d8 - creusot[f07d8a7e3e012a46]::backend::resolve::elaborate_resolve_def::<creusot[f07d8a7e3e012a46]::backend::clone_map::elaborator::ExpansionProxy>
                               at /home/sam/rust/creusot/creusot/src/backend/resolve.rs:198:8
  20:     0x5788f22bf6de - creusot[f07d8a7e3e012a46]::backend::clone_map::elaborator::term::<creusot[f07d8a7e3e012a46]::backend::clone_map::elaborator::ExpansionProxy>
                               at /home/sam/rust/creusot/creusot/src/backend/clone_map/elaborator.rs:1248:17
  21:     0x5788f224e299 - <creusot[f07d8a7e3e012a46]::backend::clone_map::elaborator::Expander>::expand_logic
                               at /home/sam/rust/creusot/creusot/src/backend/clone_map/elaborator.rs:250:56
  22:     0x5788f2257541 - <creusot[f07d8a7e3e012a46]::backend::clone_map::elaborator::Expander>::expand
                               at /home/sam/rust/creusot/creusot/src/backend/clone_map/elaborator.rs:604:48
  23:     0x5788f2256966 - <creusot[f07d8a7e3e012a46]::backend::clone_map::elaborator::Expander>::update_graph
                               at /home/sam/rust/creusot/creusot/src/backend/clone_map/elaborator.rs:588:18
  24:     0x5788f20a651f - <creusot[f07d8a7e3e012a46]::backend::clone_map::Dependencies>::provide_deps
                               at /home/sam/rust/creusot/creusot/src/backend/clone_map.rs:438:41
  25:     0x5788f241cdf2 - creusot[f07d8a7e3e012a46]::backend::program::translate_function
                               at /home/sam/rust/creusot/creusot/src/backend/program.rs:80:38
  26:     0x5788f20b7241 - <creusot[f07d8a7e3e012a46]::backend::Why3Generator>::translate
                               at /home/sam/rust/creusot/creusot/src/backend.rs:84:28
  27:     0x5788f25d8dd0 - creusot[f07d8a7e3e012a46]::translation::after_analysis
                               at /home/sam/rust/creusot/creusot/src/translation.rs:80:14
  28:     0x5788f2422aa4 - <creusot[f07d8a7e3e012a46]::callbacks::ToWhy as rustc_driver_impl[d6ef0231697d3f85]::Callbacks>::after_expansion
                               at /home/sam/rust/creusot/creusot/src/callbacks.rs:124:17
  29:     0x704bf0519511 - <rustc_interface[4a8bddddb5d81cd1]::passes::create_and_enter_global_ctxt<core[f9b0cf5fccb69ea1]::option::Option<rustc_interface[4a8bddddb5d81cd1]::queries::Linker>, rustc_driver_impl[d6ef0231697d3f85]::run_compiler::{closure#0}::{closure#2}>::{closure#2} as core[f9b0cf5fccb69ea1]::ops::function::FnOnce<(&rustc_session[a5a2d75711ca37ea]::session::Session, rustc_middle[858d3a7a7a03c869]::ty::context::CurrentGcx, alloc[10595c53490534ae]::sync::Arc<rustc_data_structures[2f76b7e71d86dee2]::jobserver::Proxy>, &std[4e041eb9831d95d2]::sync::once_lock::OnceLock<rustc_middle[858d3a7a7a03c869]::ty::context::GlobalCtxt>, &rustc_data_structures[2f76b7e71d86dee2]::sync::worker_local::WorkerLocal<rustc_middle[858d3a7a7a03c869]::arena::Arena>, &rustc_data_structures[2f76b7e71d86dee2]::sync::worker_local::WorkerLocal<rustc_hir[f601393c59240e29]::Arena>, rustc_driver_impl[d6ef0231697d3f85]::run_compiler::{closure#0}::{closure#2})>>::call_once::{shim:vtable#0}
  30:     0x704bf03bf945 - rustc_interface[4a8bddddb5d81cd1]::interface::run_compiler::<(), rustc_driver_impl[d6ef0231697d3f85]::run_compiler::{closure#0}>::{closure#1}
  31:     0x704bf03291ca - std[4e041eb9831d95d2]::sys::backtrace::__rust_begin_short_backtrace::<rustc_interface[4a8bddddb5d81cd1]::util::run_in_thread_with_globals<rustc_interface[4a8bddddb5d81cd1]::util::run_in_thread_pool_with_globals<rustc_interface[4a8bddddb5d81cd1]::interface::run_compiler<(), rustc_driver_impl[d6ef0231697d3f85]::run_compiler::{closure#0}>::{closure#1}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>
  32:     0x704bf0328f9d - <std[4e041eb9831d95d2]::thread::lifecycle::spawn_unchecked<rustc_interface[4a8bddddb5d81cd1]::util::run_in_thread_with_globals<rustc_interface[4a8bddddb5d81cd1]::util::run_in_thread_pool_with_globals<rustc_interface[4a8bddddb5d81cd1]::interface::run_compiler<(), rustc_driver_impl[d6ef0231697d3f85]::run_compiler::{closure#0}>::{closure#1}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>::{closure#1} as core[f9b0cf5fccb69ea1]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  33:     0x704bf0327378 - <std[4e041eb9831d95d2]::sys::thread::unix::Thread>::new::thread_start
  34:     0x704be9c9caa4 - <unknown>
  35:     0x704be9d29c6c - <unknown>
  36:                0x0 - <unknown>

I found the rust commit that breaks it (feb13036efe). To investigate.

[jhjourdan]

I found the rust commit that breaks it (feb13036efe). To investigate.

Are you sure? That's weird, because it seems completely unrelated to the error message...

[jhjourdan]

Also, this panic does not exists on rustc master.

[jhjourdan]

huh... its not master, but main...

[Lysxia]

That commit introduced the error message... although it's true there could be other changes that caused us to end up in that branch.

[jhjourdan]

See rust-lang/compiler-team#940. After this commit, the coherence mechanism assumes that "unnamable types" cannot appear in coherence queries.

We are using the coherence mechanism to make sure some Resolve and Invariant trait instances do not exist. Thus, we are using coherence for pretty much any type. This is causing the crash.

[jhjourdan]

Here is a proposed plan:

1- Refactor the trait query mechanism so that we do no longer distinguish TraitResolved::UnknownNotFound and TraitResolved::NoInstance. The only places where this makes a difference is for Invariant and Resolve.

2- For these traits, we still need to call coherence. We can either:
a- Try to replace unnamable types (i.e., closures and fndefs) with other types with similar properties, and call rustc's orphan check. Since the orphan check is purely syntactic, we could replace closures and fndefs with with types with the same locality (i.e., inference variables for local types, bool for non-local types).
b- Vendor the orphan checker, without the new error. It actually seems standalone, so we can vendor it without vendoring the whole trait solver.

BTW, FnDef types are always considered non-local by rustc (old version). I think this has no impact in our case, but this was probably a small bug.

[Lysxia]

I note that the test suite is unchanged if we just remove the orphan check.

[jhjourdan]

Good!

So the problem with the orphan check should be the only one we need to fix.