Remix.run Logo
▲ kelseyfrog a day ago

I feel like I'd have something to learn from seeing the code.

Won'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.

▲tyromaniac a day ago | parent [-]

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.

If 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.

▲Someone 10 hours ago | parent | next [-]

> If 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;
  }
You’ll need to add code to detect cycles other than 1, 4, 2, 1, 4, 2,… to that. That can be done in constant space (https://en.wikipedia.org/wiki/Cycle_detection#Floyd’s_tortoi...)

Ideally, you also need a way to detect runs towards infinity. That is harder.

Otherwise, an optimising compiler can use the forward progress guarantee and optimize that to:

  cpp bool collatz(unsigned long long n)
  {
    return true;
  }
and then completely remove the precondition.
▲tyromaniac 8 hours ago | parent [-]

I think I saw years ago that clang replaced a collatz impl with true. Why is it that the "forward progress garuntee" would let it do that?

▲kccqzy 21 hours ago | parent | prev [-]

You may have to internally use bignums since collatz orbits can become very large before shrinking.

▲tyromaniac 21 hours ago | parent [-]

That's a good point. I wonder how difficult comptime bignum would be in comptime. Seems like there's no proven bounds I could find either