Off-topic, but collatz(x) == 1 for all positive 64-bit integers (actually, this has been verified up to 2^71: https://link.springer.com/article/10.1007/s11227-025-07337-0). I recently made this tool if anyone wants to try it with 1,000-digit integers or ranges: https://www.proofatlas.ai/explore/collatz/.
replySPARK (Ada) has compile time pre and post conditions, and it works well. If you declare the post-condition Collatz (n) = 1, the compiler can't help you, and compilation will fail. If you've got a difficult condition, you're going to have to help the theorem prover, often by introducing "ghost" functions, or by simply softening the condition. In the latter case, you can't prove total correctness, but you can often still prove things like absence of run-time errors.
replyJust curious, but what's the definition of collatz(long) look like?
replyreply
I meant the C++ definition of collatz that would verify the precondition.
replyI haven't tried it and am afk rn but I'd imagine you just define a constexpr function that implements collatz and use that in your contract.
reply(Edit: if the input is constexpr itself) Its also quire easy to think about specializing a few templates and doing it that way. If you look up an example of the fib sequence in c++ templates you'll get the general idea.
I feel like I'd have something to learn from seeing the code.
replyWon't you just run into a constexpr evaluation depth error with a suggestion to set -fconstexpr-depth? I don't see how this is the gotcha it's made out to be.
I'd exepct something like that to happen. Worth reiterating that the whole scenario is for a hypothetical different implementation of contract that would execute comptime, as noted in the parent thread.
replyIf you wanted a c++26 preconditon for collatz tho, here it is. ```cpp bool collatz(unsigned long long n) { while (n != 1) n = n % 2 ? 3 * n + 1 : n / 2; return true; }
void f(unsigned long long n) pre(collatz(n)); ``` That's basically what you'd write if you were doing it with asserts, as the linked article states, just now you add it to the declaration.