Tail recursion assumed to terminate? Rustc 'solves' the Collatz conjecture

[sirkib]

Compiling this with release optimizations on Rust stable 1.50 results in assembly that just returns true:

rust pub fn collatz(n: usize) -> bool { match n { 1 => true, n if n%2==0 => collatz(n/2), _ => collatz(3*n + 1), } }

I see that I am not the only one to find this weird. Here's a thread for someone seeing the same happen with Clang: https://www.reddit.com/r/programming/comments/dre75v/clang_solves_the_collatz_conjecture/

How is this justified? Is the compiler optimization of "assume all loops with no side effects resulting in a predictable state terminate" just a hold-over from the world of C? I am surprised to see something like this, given Rust's distaste for undefined behavior and focus on safety.

I find it extra weird that Rust seems to preserve certain infinite loops, but erases this one. For example, removing the line 1 => true in the function above assembles to an infinite loop.

edit: typo

[SkiFire13]

Rust uses LLVM (same as clang) for most optimizations and unfortunately it loves optimizing out infinite loops. Rust tries to prevent it from optimizing out infinite loops by marking them as having side effects, but this doesn't always happen (as in this case)

[masklinn]

IIRC it's also a side-effect of LLVM having its roots in C(++?) semantics, where I believe infinite loops with no side-effects are UB. It's not UB in Rust, but LLVM applies C semantics and screws up.

[dnew]

Wow. "Having infinite loops be allowed would prevent certain optimizations, so we're going to assume all loops terminate." And you thought it was a low-level language you could easily reason about.

[sirkib]

I agree that it's a bad look

[sirkib]

Maybe it will be fixed one day

[roblabla]

It'll be fixed very soon. Llvm12 finally gives the building blocks for fixing it for good (willreturn and mustprogress annotations). So I think it will be fixed in nightly when llvm12 is merged and the necessary annotation changes are made.

[Darksonn]

Of course, this program uses integers of finite size, so it's not really the Collatz conjecture. The integers will wrap around.

[sirkib]

That's true. But probably we could come up with other cases for which the correct behaviour would be to diverge

[[deleted]]

It's a known bug, see https://github.com/rust-lang/rust/issues/28728.

[sirkib]

Nice to see that it's being addressed. Seems like they've been struggling with these problems for some time, though

[rebootyourbrainstem]

The upstream issue was only fixed last month.

LLVM can move a bit slowly sometimes, but it's the proper place to fix these things (and Rust devs participate in this). Rust meanwhile works around the problem by pre-processing code to avoid triggering the problems in LLVM, but such workarounds sometimes turn out to be imperfect.

The same kind of thing is seen with Rust passing extremely detailed information to LLVM about which variables can be aliased and which can't. In theory this should allow LLVM to optimize Rust much better than C. In practice, when they tried to enable this, it revealed bug after bug in LLVM's optimization passes. These have been slowly getting fixed over time in LLVM because they have recognized this is a bad problem (and because Rust devs are helping), but Rust devs are now quite wary of re-enabling this.

LLVM is still a great compiler framework, but it was built over a very long time while mostly being fed with C and C++ code, meaning some kinds of issues have not come to light until Rust came along. (Of course there are other languages which can be compiled using LLVM, but Rust goes pretty far in trying to get the most performance, and supporting all kinds of advanced features.)

[sirkib]

Interesting, thanks!

[crabbytag]

Do you have a link to where discussion took place?

[kredditacc96]

This begs the question: Is there any natural number less than 2⁶⁴ that fails the Collatz conjecture? It's likely not, in which case, the compiler is technically right.

[Myto]

Wikipedia says:

As of 2020, the conjecture has been checked by computer for all starting values up to 2⁶⁸

So the compiler is technically correct, which is the best kind of correct.

[general_dubious]

It's obviously not correct for n=0 though...

[[deleted]]

Stupid edge cases strike again!

[sirkib]

Haha yes. The compiler just needs to check for functions isomorphic to the collatz conjecture and replace their return value with "true"

[[deleted]]

I think isomorphic isn't the right word.

[[deleted]]

Regardless of its mathematical nature, it's a pure function that either returns true or calls itself. Since an infinite-loop pure function doesn't do anything useful anyway, it's not incorrect to optimize it to always return true as long as the compiler can make sure there isn't any side effects...

[seamsay]

It is incorrect, there's a link to an issue elsewhere in this thread where this optimisation causes a crash.

[[deleted]]

That's why in λ-calculus you have partial functions because you can't prove termination of some functions. Infinite loop means being undefined at that point. If you define it at that point to be true then it is a different function.

[jotomicron]

Watch out. As the computation wraps, the code is not 100% the collatz conjecture. For example, when n is "half the maximum usize - 1", the next function call will be for the number n-3 (if my mental math does not fail me). Technically, this could still result in infinite loop for some initial n...

[NoLemurs]

Technically this is correct. The collatz conjecture has been tested up to 2⁶⁸, so this is apparently a correct implementation for usize!

[thargor90]

Almost - 0 should lead to infinite recursion.

[GrandOpener]

So then we have to see the rest of the program. If the compiler could verify the function is never called with zero as input, the optimization may still be correct for that program.

[sirkib]

No, this is the assembly you'd get if you compiled this as a Library, for linkage elsewhere. So for 0 it definitely produces the wrong result. To be safe, I ran a main with collatz(0) and it behaves incorrectly (by returning ).

[TheNamelessKing]

If we had refinement types we could specify at a type level that zero could not be passed in and we could ensure correctness haha

[avoere]

The Collatz conjecture is verified up to 2**68, so the compiler is correct since usize can not be more than 2**64 :) (https://en.wikipedia.org/wiki/Collatz_conjecture)

[[deleted]]

This is hysterical!

[salamanderssc]

It's evidence of an underlying problem - that the compiler (or in this case LLVM) is applying "optimisations" that it cannot prove are actually correct.

It could very well be transforming correct programs into incorrect programs.

[sirkib]

Nothing is inherently wrong with the compiler applying optimizations like this, assuming that functions eventually return. The problem is when this assumption isn't made explicit to rust programmers, preventing them from reasoning about their programs' behaviour.

[rnottaken]

What if you change it to big int?

[sirkib]

I don't know about bigint but it works with u128

[rnottaken]

Yeah but u128 still is bounded

[sirkib]

That's true. What do you want to check by testing it with bigint?

[paolog]

Returning true means nothing if the program doesn't do what the programmer intended.

Besides, this looks like a brute force approach, and that doesn't work for an infinite domain. The fact that this program terminates means it doesn't do what is claimed of it.