[feliperodri]

kani autoharness aborts on any crate that declares a #[rustc_comptime] function. core has 27 of them, so the standard library run dies during candidate collection — which is what currently blocks the four autoharness jobs on model-checking/verify-rust-std#687, the same four that #4820 unblocked from the E0080 side:

do not use `optimized_mir` for constants: Const { allow_const_fn_promotion: false }

My fault, from #4820: the const-block precondition search guards its MIR fetch with is_mir_available and then calls optimized_mir. That guard is not enough — a #[rustc_comptime] function's body is a const context, which rustc's optimized_mir provider refuses to serve even while the MIR is available. instance_mir is rustc's own dispatcher between optimized_mir and mir_for_ctfe, so the fix is to stop making that choice here and use it.

The part I actually had to check: whether switching providers loses the detection #4820 exists for. It does not, and the test pins it. A #[rustc_comptime] function whose body carries const { assert!(N >= 4) } is still reported as skipped for that reason, read out of the CTFE body — and so is the plain const fn shape core::escape uses, which goes through optimized_mir as before. If someone later "simplifies" this back, that assertion is what fails.

Verified rather than read:

• The issue's reproducer fails on main with the ICE and completes on this branch, reporting size_of::<i32> as skipped for having no body — the output the issue predicted with the panic suppressed.
• All three shapes core has are covered and all three ICE on main: the body-less #[rustc_intrinsic] #[rustc_comptime] declaration (intrinsics::size_of), one with a body (TypeId::trait_info_of), and one with a const-block precondition. The middle one is now harnessed rather than skipped, so the CTFE body is genuinely being read.
• script-based-pre 76/76 with the new test, kani 610/610, expected 478/478, fmt and clippy clean.

One thing for a reviewer to weigh: current_fn.rs:408 has the same is_mir_available + optimized_mir pattern, for a closure's parent. I could not construct a case that reaches it with a const-context parent, so I left it alone rather than change code I cannot test — but it is the same shape, and worth a look by someone who knows that path better.

Resolves #4839

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.