Because I kind of expected the algorithm would say "hey this loop is bounded up to 4K, this nested one is up to 3K, therefore I can't prove the total is below 1M, therefore I reject", but from your description it sounds like it actually does some kind of bounded model checking up to 1M instructions instead of taking shortcuts like this? Or did you mean it actually does take shortcuts like this?

The idea here is that without any kind of loop, it's quite tricky to do some basic packet processing. For instance, if you want to clamp the MSS of a TCP connection, you have to grovel through TCP options, which do not occur at fixed offsets or in a particular order; you want to write a "for" loop over the (inherently limited) range of bytes at the computed offset of the TCP options. You can trivially bound that loop by the MTU of the link your program is loaded on (and also the limited possible size of TCP options), the loop won't iterate that many times, and it won't do much inside the loop.

But it's very much not the case that bounded loops give you general-purpose programming, like to implement your own data structures. BPF programs rely on kernel helpers and userland programs that maintain maps and read perf to do that stuff.

  int nested_loops(volatile struct pt_regs* ctx)
  {
    int i, j, sum = 0, m;

    for (j = 0; j < 300; j++)
      for (i = 0; i < j; i++) {
        if (j & 1)
          m = ctx->rax;
        else
          m = j;
        sum += i * m;
      }

    return sum;
  }

  int while_true(volatile struct pt_regs* ctx)
  {
    int i = 0;

    while (true) {
      if (ctx->rax & 1)
        i += 3;
      else
        i += 7;
      if (i > 40)
        break;
    }

    return i;
  }

1. If the answer is no, then what is the precise reason? Is there a legitimate reason for it? After all, a bounded loop that loops for too long is just as bad as one that never terminates, so clearly they need a way to upper-bound the instruction count for any loop—at which point, why is the bound even relevant? The only reason I can think of is that they do simplistic analysis (e.g. multiplying the bounds on nested loops to naively approximate an overall bound), but your examples suggest they have more sophisticated (SMT/BMC?) solvers, and it's not obvious to me why a modern solver would fail on all unbounded loops.

2. If the answer is yes, then it would seem they actually do allow unbounded loops after all?

The other possibility is they're using the word "bounded" differently (e.g. maybe as a synonym for "terminating"), in which case it would be true that they would need bounded loops by definition.