Rust Project Goals

Update: opened https://github.com/rust-lang/a-mir-formality/pull/210 with today's work. We are discussing how to move the checker to support polonius-alpha. To that end, we introduced feature gates (so that a-mir-formality can model nightly features) and did some refactoring of the type checker aiming at allowing outlives to become flow-sensitive.

Update: opened https://github.com/rust-lang/a-mir-formality/pull/207 which contains support for &mut, wrote some new tests (including one FIXME), and added a test for NLL Problem Case #3 (which behaved as expected).

One interesting thing (cc Ralf Jung) is that we have diverged from MiniRust in a few minor ways:

• We do not support embedding value expressions in place expressions.
• Where MiniRust has a AddrOf operator that uses the PtrType to decide what kind of operation it is, we have added a Ref MIR operation. This is in part because we need information that is not present in MiniRust, specifically a lifetime.
• We have also opted to extend goto with the ability to take multiple successors, so that goto b1, b2 can be seen as "goto either b1 or b2 non-deterministically" (the actual opsem would probably be to always go to b1, making this a way to add "fake edges", but the analysis should not assume that).

The PR also includes two big improvements to the a-mir-formality framework:

• support for (for_all) rules that can handle "iteration"
• tracking proof trees, making it much easier to tell why something is accepted that should not be

PR https://github.com/rust-lang/a-mir-formality/pull/206 contains a "first draft" for the NLL rules. It checks for loan violations (e.g., mutating borrowed data) as well as some notion of outlives requirements. It does not check for move errors and there aren't a lot of tests yet.

Current status:

• The RFC for auto impl supertraits has been updated to address SemVer compatibility issues.
• There is a parsing PR kicking off an experimental implementation. The tracking issue for this experimental implementation is here.

There hasn't been too much progress over the last few weeks and I've been mostly taking a Christmas break. Nicholas Nethercote has been looking into the performance of the new trait solver, cleaning up canonicalization and slightly improving its performance: https://github.com/rust-lang/rust/pull/150748 https://github.com/rust-lang/rust/pull/150859.

Shoyu Vanilla looked into https://github.com/rust-lang/trait-system-refactor-initiative/issues/251 and uncovered the underlying bug there. While this issue also affects the old solver and the proper fix for it requires where-bounds on binders, we can work around this bug in the trait solver for now and intend to do so.

We've started another crater run with all our recent changes and adwin has started to triage it, uncovering one new issue up until now. Intend to continue going through that over the next few weeks.

There's also a lot in-progress work going on. I am collaborating with Niko Matsakis to specify and later RFC the cycle semantics of Rust. León Orell Valerian Liehr is working on a replacement for the rustdoc's auto trait impl synthesis: https://github.com/rust-lang/rust/pull/149019. @tiff is working on a fix a MIR borrowck unsoundness: https://github.com/rust-lang/trait-system-refactor-initiative/issues/159. Shoyu Vanilla and I are improving the way we propagate inference constraints from the expected return type to function arguments, fixing https://github.com/rust-lang/trait-system-refactor-initiative/issues/259.

We've continued to fix a bunch of smaller issues over the last month. Tim (Theemathas Chirananthavat) helped uncover a new potential issue due to non-fatal overflow which we'll have to consider before stabilizing the new solver: https://github.com/rust-lang/trait-system-refactor-initiative/issues/258.

I fixed two issues myself in https://github.com/rust-lang/rust/pull/148823 and https://github.com/rust-lang/rust/pull/148865.

tiif with help by Boxy fixed query cycles when evaluating constants in where-clauses: https://github.com/rust-lang/rust/pull/148698.

adwin fixed a subtle issues involving coroutine witnesses in https://github.com/rust-lang/rust/pull/149167 after having diagnosed the underlying issue there last month. They've also fixed a smaller diagnostics issue in https://github.com/rust-lang/rust/pull/149299. Finally, they've also fixed an edge case of impl well-formedness checking in https://github.com/rust-lang/rust/pull/149345.

Shoyu Vanilla fixed a broken interaction of aliases and fudging in https://github.com/rust-lang/rust/pull/149320. Looking into fudging and HIR typeck Expectation handling also uncovered a bunch of broken edge-cases and I've openedhttps://github.com/rust-lang/rust/issues/149379 to track these separately.

I have recently spent some time thinking about the remaining necessary work and posted a write-up on my personal blog: https://lcnr.de/blog/2025/12/01/next-solver-update.html. I am currently trying to get a clearer perspective on our cycle handling while slowly working towards an RFC for the changes there. This is challenging as we don't have a good theoretical foundation here yet.

This month's update:

• tiif is making progress on https://github.com/rust-lang/trait-system-refactor-initiative/issues/159
• we discussed how to investigate and fix the remaining correctness issues in Tage's work, to be able to evaluate it more accurately: in particular around variance and bidirectional edges, and without the reliance on NLL (having computed region values / errors)
• we've tried to see if it'd be possible to remove the cfg region elements
• Amanda is still working on her two papers, one about the current borrow checker and one about the work on Polonius. Her major PR for the restructuring of placeholder handling during region inference is stalled due to a conflict with further trait solver developments and may have to be abandoned. Work with the larger types team is ongoing and smaller patches/refactorings/improvements are being landed in the meantime.
• https://github.com/rust-lang/rust/pull/149639 has now landed, and https://github.com/rust-lang/rust/pull/150551 is still in review
• I've also fixed more small inefficiencies (computing boring/relevant locals on-demand in diagnostics, removed conversions between locations and points, etc) building on top of the previous PRs (so they need to be reviewed first)
• I've looked at crates.io again with the alpha, to find functions that are slower than with NLLs. AFAICT the worst case there is 60% for a 5KLOC function with 42K loans, 255K statements, and 125K outlives constraints. I'll see what we can do with this. Small composable functions is still good advice.
• there seem to be optimization opportunities to 1. limit propagation to the smaller number of blocks that could be affected by bidirectional edges, 2. for unifying invariant lifetimes of live locals that are assigned at most once (à la use-def chains), 3. for invalidations that are just the activation of a reservation
• we discussed possible plans to gather actual statistics, using the infrastructure that was created for the Metrics project
• we're also preparing the new project goal for this year, where we'll want to stabilize the alpha 🤞

• I should be able to open a PR in the next couple days

done in https://github.com/rust-lang/rust/pull/150551

This month's key developments were:

• borrowck support in a-mir-formality has been progressing steadily — it has its own dedicated updates in https://github.com/rust-lang/rust-project-goals/issues/122 for more details
• we were also able to find a suitable project for the master's student project on a-mir-formality (and they accepted and should start around February) and which will help expand our testing coverage for the polonius alpha as well.
• tiif has kept making progress on fixing opaque type soundness issue https://github.com/rust-lang/trait-system-refactor-initiative/issues/159. It is the one remaining blocker for passing all tests. By itself it will not immediately fix the two remaining (soundness) issues with opaque type region liveness, but we'll able to use the same supporting code to ensure the regions are indeed live where they need to be.
• I quickly cleaned up some inefficiencies in constraint conversion, it hasn't landed yet but it maybe won't need to because of the next item
• but most of the time this month was spent on this final item: we have the first interesting results from the rewriting effort. After a handful of wrong starts, I have a branch almost ready to switch the constraint graph to be lazy and computed during traversal. It removes the need to index the numerous list of constraints, or to convert liveness data to a different shape. It thus greatly reduces the current alpha overhead (some rare cases look faster than NLLs but I don't yet know why, maybe due to being able to better use the sparseness, low connectivity of the constraint graph, and a small number of loans). The overhead wasn't entirely removed of course: the worst offending benchmark has a +5% wall-time regression, but icounts are worse looking (+13%). This was also only benchmarking the algorithm itself, without the improvements to the rest of borrowck mentioned in previous updates. I should be able to open a PR in the next couple days, once I figure out how to best convert the polonius mermaid graph dump to the new lazy localized constraint generation.
• and finally, happy holidays everyone!

Key developments:

• I prototyped building blocks to fix the liveness soundness issue, but this was deemed too brittle.
• so we prepared a meeting for the types team to discuss the problem, and possible solutions.
• it turns out the issue is related to another soundness issue for opaque types in the new trait solver, https://github.com/rust-lang/trait-system-refactor-initiative/issues/159, and that tiif is already working on. The same solution is needed for both issues: with the full implied bounds available for opaque types in liveness, we'll able to require all the regions outliving the opaque lower bound to be live, while ignoring the unrelated regions (that the hidden type cannot use anyway). There will be no relevant dead region through which loans flow, and code relying on unused lifetimes being dead (like a lot of ed2024 code with the default capture changes) will still compile
• we prepared another types-team meeting to discuss polonius in general, and the alpha algorithm in particular, to share knowledge among the team. This will also be helpful to then on apply member constraints in a location-sensitive manner, since right now they're applied at the SCC level and we need to make sure these constraints with the choice regions are present in the localized subset graph.
• niko and tiif have made a lot of progress on adding support for borrow checking in a-mir-formality, so I've also joined these meetings, since we'll also want to model the alpha.
• I've looked into Prusti's Place Capability Graphs, and plan to see how to integrate the alpha there, and if possible with the fuzzing capabilities mentioned in the paper, with the usual goal to expand testing as we've mentioned many times
• we also had some discussion for a possible masters' student project, and thought about different practical and theoretical topics

Nothing this month, been busy with other stuff :)

This month I've written some documentation for how Const Generics is implemented in the compiler. This mostly covers the implementation of the stable functionality as the unstable features are quite in flux right now. These docs can be found here: https://rustc-dev-guide.rust-lang.org/const-generics.html

I've made a tracking issue on the dev guide repo for this project goal: rust-lang/rustc-dev-guide#2663. I've also written documentation for coercions: rust-lang/rustc-dev-guide#2662. There have been a few extra additions to the list in the previous update.