circular reasoning is a potential source of unsoundness [LWN.net]

circular reasoning is a potential source of unsoundness

Posted Mar 30, 2026 15:29 UTC (Mon) by daroc (editor, #160859)
In reply to: circular reasoning is a potential source of unsoundness by garyguo
Parent article: Rust's next-generation trait solver

I didn't go as deep into the weeds as I could have with the details of when circular reasoning is or isn't sound; the Rust compiler documentation that I linked goes into more detail. There are two different kinds of cycles that one can have in a type system: inductive and coinductive. Inductive cycles are always unsound (and the plan remains to have the Rust type system reject them). Coinductive cycles can be sound, with the right logical foundations.

Via the Curry-Howard correspondence, an inductive cycle is an infinite loop, or a recursive function without a base case. A coinductive cycle, on the other hand, corresponds to something like a generator: a process that continues indefinitely, but does some additional work at each step such that, when consumed by a process that doesn't try to reach the "end" of the sequence, it all works out.

The main thing is that, when attempting to find a coinductive proof, it's necessary to ensure that the cycle has a length greater than one (or, to use type theory jargon, that the loop is productive). Note that that doesn't prevent the actual generated code from being an infinite loop (because Rust doesn't consider that to be unsound, and a programmer could already write a trait implementation that way), but it does prevent a "impl<T> Trait for T where T: Trait" situation, which is probably undesirable.

Right now, the next-generation solver will only do coinductive reasoning for a limited number of autotraits (Send, etc.). If/when it can be shown safe to extend this to user-defined traits, then it will be. But since this whole area is complex and subtle, the types team is moving slowly and making sure they don't introduce unsoundness.

to post comments

circular reasoning is a potential source of unsoundness

Posted Mar 30, 2026 17:10 UTC (Mon) by NYKevin (subscriber, #129325) [Link] (4 responses)

The "obvious" concern I would have with this is user-defined unsafe traits.

In the case of Send and Sync, the traits impose a negative obligation. Types in Rust are thread-safe by default, and they can only become thread-unsafe through the use of interior mutability or raw pointers. So it's entirely reasonable to coinductively infer Send and Sync. If you never encounter something manifestly !Send or !Sync in your chain of reasoning, then there can't be any source of thread-unsafety, so inferring Send or Sync is fine.

On the other hand, the unsafe trait TrustedLen imposes a positive obligation. Specifically, if a type implements TrustedLen, then unsafe code may soundly assume that its len() method returns the right value, and execute UB if that assumption turns out to be wrong. In pragmatic terms, that means the Source of Truth for len() must be hidden behind some visibility annotation so that foreign safe code cannot mess with it. If len() is computed by calling into something else, then that callee is under the same obligation, transitively all the way down to the ground truth.

In the case of TrustedLen, I don't think there exists a counterexample where coinduction actually produces an unsound implementation. Coinduction implies, to my mind, that you end up with TrustedLen-or-some-equivalent all the way down, and there's no actual soundness hole. But it is the sort of thing that would keep me awake at night if I were responsible for trait-solving in Rust. Users can define arbitrary unsafe traits with arbitrary soundness requirements, and those requirements typically exist only in documentation or comments, not in actual code the compiler can read and understand. Who is to say whether any one of those unsafe traits might be incompatible with coinduction?

circular reasoning is a potential source of unsoundness

Posted Mar 30, 2026 17:34 UTC (Mon) by daroc (editor, #160859) [Link] (2 responses)

I suspect the answer is the same as any other unsafe thing that breaks the language: "don't do that". You can't have a coinductive loop without at least one trait implementation block, so for an unsafe trait, that unsafe trait implementation is the specific use of unsafe that could break things.

But yes, one of the remaining open items to work on before the next-generation trait solver can be stabilized is documentation, which will presumably include documenting how any proposed changes to the type system interact with unsafe code.

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 1:22 UTC (Tue) by NYKevin (subscriber, #129325) [Link] (1 responses)

Sure, but what happens if someone has already constructed an incomplete loop, which is only sound in the current version of Rust because coinduction is impossible (and therefore the loop cannot be closed)? You could imagine a situation where the "missing link" of the loop is implementable in safe code, and that would retroactively render the existing (unsafe) implementations unsound.

I don't think you can fix it with an edition, either. Trait solving is semantic, not syntactic.

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 11:49 UTC (Tue) by daroc (editor, #160859) [Link]

Oh, I see your point! That's an interesting thought.

You're right; I'm not sure how that ought to be handled. I don't think the list of considerations for unsafe code to be aware of have changed very much over time.

Perhaps it would still be possible to make it an edition change by tagging each trait implementation with which edition it comes from, and disallowing coinductive cycles that dip into previous editions, but that's pure speculation on my part.

circular reasoning is a potential source of unsoundness

Posted Mar 31, 2026 3:36 UTC (Tue) by theemathas (guest, #183008) [Link]

This exact issue has been raised in https://github.com/rust-lang/rust/issues/149743

There's currently no good answer to this yet.